НОВОСТИ    БИБЛИОТЕКА    ЭНЦИКЛОПЕДИЯ    БИОГРАФИИ    КАРТА САЙТА    ССЫЛКИ    О ПРОЕКТЕ  

ГЁДЕЛЯ ИНТЕРПРЕТАЦИЯ

ГЁДЕЛЯ ИНТЕРПРЕТАЦИЯ интуиционистской арифметики - специальная операция, переводящая формулы интуиционистской арифметики в формулы вида ∃x∀y А(х, у, z) где х, у и z - наборы переменных по вычислимым функциям специального вида. При этом выводимые формулы переводятся в истинные формулы в смысле нек-рой четко описанной семантики. Эта интерпретация, к-рая была использована К. Гёделем (К. Gödel) для нового доказательства непротиворечивости арифметики формальной, представляет также значительный интерес как нек-рая семантика для языка формальной арифметики.

Рассматривается бескванторная аксиоматич. теория Т с бесконечным числом типов переменных. Класс переменных данного типа определяется индуктивно, а именно: 1) х0, у0, z0, ... - переменные типа 0, переменные для натуральных чисел; 2) пусть теория содержит переменные типов t0, t1, ..., tk, тогда теория содержит и переменные типа t, где t есть (t0, ..., tk). Переменные типа t обозначаются через xt, yt, zt, ... и рассматриваются как переменные для вычислимых в нек-ром смысле функций, перерабатывающих каждый набор функций типов t1, ..., tk соответственно в функцию типа t0. Язык Т содержит термы различных типов: переменная хt типа t является термом типа t, 0 есть терм типа 0, символ s, к-рый служит для обозначения функции прибавления единицы к натуральному числу, есть терм типа (0, 0). Остальные термы образуются с помощью правил порождения: Чёрча λ-абстракции и примитивной рекурсии для функций произвольного типа. Атомарные формулы теории Т суть равенства (t = r), где t, r - термы типа 0. Формулы теории Т получаются из атомарных с помощью логических связок исчисления высказываний &, ∨, ⊃, ¬. Постулатами Т являются аксиомы и правила вывода интуиционистского исчисления высказываний, аксиомы для равенства, аксиомы Пеано для 0 и S, уравнения примитивных рекурсий, аксиома применения функции, определенной λ-абстракцией, и, наконец, принцип математич. индукции, сформулированный в виде правила вывода без употребления кванторов. Через Т+ обозначим теорию Т, пополненную кванторами по переменным произвольного типа и соответствующими логическими аксиомами и правилами вывода для кванторов.

Г. и. переводит всякую формулу F из Т+ (а следовательно, и всякую формулу интуиционистской арифметики) в формулу вида

∃x∀y А(х, у, z)

где А(х, у, z) - формула без кванторов, а х, у, z - наборы переменных различных типов, z - совокупность всех свободных переменных формулы Р.

Пусть F - формула интуиционистской арифметики и ∃x∀y А(х, у, z) - ее гёделевская интерпретация. Если F выводима в формальной интуиционистской арифметике, то может быть построен терм t(z) теории Т такой, что формула A(t(z), у, z) выводима в Т. Таким образом, непротиворечивость арифметики сводится к установлению непротиворечивости бескванторной теории Т.

Интуиционистская семантика на основе Г. и. определяется следующим образом: формула Р считается истинной, если найдется вычислимый терм t(z) такой, что бескванторная формула A (t(z), у, z) истинна при всяком вычислимом z.

Лит.: [1] Гёдель К., в сб.: Математическая теория логического вывода, М., 1967, с. 299-310.

А. Г. Драгалин.


Источники:

  1. Математическая Энциклопедия. Т. 1 (А - Г). Ред. коллегия: И. М. Виноградов (глав ред) [и др.] - М., «Советская Энциклопедия», 1977, 1152 стб. с илл.











© MATHEMLIB.RU, 2001-2021
При копировании материалов проекта обязательно ставить ссылку на страницу источник:
http://mathemlib.ru/ 'Математическая библиотека'
Рейтинг@Mail.ru