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

интуиционистской арифметики - специальная операция, переводящая формулы интуиционистской арифметики в формулы вида [img: http://localhost:8080/file/010408-190.jpg] где [img: http://localhost:8080/file/010408-191.jpg] - наборы переменных по вычислимым функциям специального вида. При этом выводимые формулы переводятся в истинные формулы в смысле нек-рои четко описанной семантики. Эта интерпретация, к-рая была использована К. Гёделем [img: http://localhost:8080/file/010408-192.jpg] для нового доказательства непротиворечивости арифметики формальной, представляет также значительный интерес как нек-рая семантика для языка формальной арифметики. Рассматривается бескванторная аксиоматич. теория Тс бесконечным числом типов переменных. Класс переменных данного типа определяется индуктивно, а именно: 1) [img: http://localhost:8080/file/010408-193.jpg] - переменные типа 0, переменные для натуральных чисел; 2) пусть теория содержит переменные типов [img: http://localhost:8080/file/010408-194.jpg] тогда теория содержит и переменные типа t, где tесть [img: http://localhost:8080/file/010408-195.jpg]. Переменные типа tобозначаются через [img: http://localhost:8080/file/010408-196.jpg] и рассматриваются как переменные для вычислимых в нек-ром смысле функций, перерабатывающих каждый набор функций типов [img: http://localhost:8080/file/010408-197.jpg] соответственно в функцию типа [img: http://localhost:8080/file/010408-198.jpg]. Язык Тсодержит термы различных типов: переменная [img: http://localhost:8080/file/010408-199.jpg] типа [img: http://localhost:8080/file/010408-200.jpg] является термом типа [img: http://localhost:8080/file/010408-201.jpg], 0 есть терм типа О, символ s, к-рый служит для обозначения функции прибавления единицы к натуральному числу, есть терм типа (0,0). Остальные термы образуются с помощью правил порождения: Черча [img: http://localhost:8080/file/010408-202.jpg] -абстракции и примитивной рекурсии для функций произвольного типа. Атомарные формулы теории Тсуть равенства [img: http://localhost:8080/file/010408-203.jpg], где [img: http://localhost:8080/file/010408-204.jpg] - термы типа 0. Формулы теории Тполучаются из атомарных с помощью логических связок исчисления высказываний [img: http://localhost:8080/file/010408-205.jpg]. Постулатами Тявляются аксиомы и правила вывода интуиционистского исчисления высказываний, аксиомы для равенства, аксиомы Пеано для 0 и S, уравнения примитивных рекурсий, аксиома применения функции, определенной l-абстракцией, и, наконец, принцип математич. индукции, сформулированный в виде правила вывода без употребления кванторов. Через [img: http://localhost:8080/file/010408-206.jpg] обозначим теорию Т, пополненную кванторами по переменным произвольного типа и соответствующими логическими аксиомами и правилами вывода для кванторов. Г. и. переводит всякую формулу [img: http://localhost:8080/file/010408-207.jpg] (а следовательно, и всякую формулу интуиционистской арифметики) в формулу вида [img: http://localhost:8080/file/010408-208.jpg] где [img: http://localhost:8080/file/010408-209.jpg] - формула без кванторов, а [img: http://localhost:8080/file/010408-210.jpg] - наборы переменных различных типов, [img: http://localhost:8080/file/010408-211.jpg] - совокупность всех свободных переменных формулы [img: http://localhost:8080/file/010408-212.jpg]. Пусть F - формула интуиционистской арифметики и [img: http://localhost:8080/file/010408-213.jpg] - ее гёделевская интерпретация. Если Fвыводима в формальной интуиционистской арифметике, то может быть построен терм [img: http://localhost:8080/file/010408-214.jpg] теории Ттакой, что формула [img: http://localhost:8080/file/010408-215.jpg] выводима в Т. Таким образом, непротиворечивость арифметики сводится к установлению непротиворечивости бескванторной теории Т. Интуиционистская семантика на основе Г. и. определяется следующим образом: формула Fсчитается истинной, если найдется вычислимый терм [img: http://localhost:8080/file/010408-216.jpg] такой, что бескванторная формула [img: http://localhost:8080/file/010408-217.jpg] истинна при всяком вычислимом z.