Гёделя Интерпретация

интуиционистской арифметики - специальная операция, переводящая формулы интуиционистской арифметики в формулы вида где - наборы переменных по вычислимым функциям специального вида. При этом выводимые формулы переводятся в истинные формулы в смысле нек-рои четко описанной семантики. Эта интерпретация, к-рая была использована К. Гёделем для нового доказательства непротиворечивости арифметики формальной, представляет также значительный интерес как нек-рая семантика для языка формальной арифметики. Рассматривается бескванторная аксиоматич. Теория Тс бесконечным числом типов переменных. Класс переменных данного типа определяется индуктивно, а именно. 1) - переменные типа 0, переменные для натуральных чисел.

2) пусть теория содержит переменные типов тогда теория содержит и переменные типа t, где tесть . Переменные типа tобозначаются через и рассматриваются как переменные для вычислимых в нек-ром смысле функций, перерабатывающих каждый набор функций типов соответственно в функцию типа . Язык Тсодержит термы различных типов. Переменная типа является термом типа , 0 есть терм типа О, символ s, к-рый служит для обозначения функции прибавления единицы к натуральному числу, есть терм типа (0,0). Остальные термы образуются с помощью правил порождения. Черча -абстракции и примитивной рекурсии для функций произвольного типа. Атомарные формулы теории Тсуть равенства , где - термы типа 0. Формулы теории Тполучаются из атомарных с помощью логических связок исчисления высказываний .

Постулатами Тявляются аксиомы и правила вывода интуиционистского исчисления высказываний, аксиомы для равенства, аксиомы Пеано для 0 и S, уравнения примитивных рекурсий, аксиома применения функции, определенной l-абстракцией, и, наконец, принцип математич. Индукции, сформулированный в виде правила вывода без употребления кванторов. Через обозначим теорию Т, пополненную кванторами по переменным произвольного типа и соответствующими логическими аксиомами и правилами вывода для кванторов. Г. И. Переводит всякую формулу (а следовательно, и всякую формулу интуиционистской арифметики) в формулу вида где - формула без кванторов, а - наборы переменных различных типов, - совокупность всех свободных переменных формулы .

Пусть F - формула интуиционистской арифметики и - ее гёделевская интерпретация. Если Fвыводима в формальной интуиционистской арифметике, то может быть построен терм теории Ттакой, что формула выводима в Т. Таким образом, непротиворечивость арифметики сводится к установлению непротиворечивости бескванторной теории Т. Интуиционистская семантика на основе Г. И. Определяется следующим образом. Формула Fсчитается истинной, если найдется вычислимый терм такой, что бескванторная формула истинна при всяком вычислимом z. Лит.:[1]Гёдель К., в сб. Математическая теория логического вывода, М., 1967, с. 299-310. А. Г. Драгалин.