Рекурсивная Реализуемость

уточнение интуиционистской семантики арифметич. Суждений на основе понятия частично рекурсивной функции, предложенное С. Клини (см. [1], [2]). Для всякой замкнутой арифметич. Формулы Fопределяется отношение "натуральное число ереализует формулу F", обозначаемое erF. Отношение erF определяется индуктивно в соответствии с построением формулы F. 1) Если F - элементарная формула без свободных переменных, т. Е. Формула вида s=t, где s и t - постоянные термы, то erF тогда и только тогда, когда е=0 и значения термов s и tсовпадают. Пусть Аи В - формулы без свободных переменных. 2) тогда и только тогда, когда , где аrА, brВ. 3) тогда и только тогда, когда и аrА или е=21.3b и brВ. 4) еr (АЙВ)тогда и только тогда, когда е - гёделев номер такой одноместной частично рекурсивной функции j, что для любого натурального числа а, если аrА, то j применима к aи j(а)rВ.

5) тогда и только тогда, когда er(AЙ1=0). Пусть А(х)- формула без свободных переменных, отличных от х;если п - натуральное число, то - терм, изображающий в формальной арифметике число n. 6) тогда и только тогда, когда е = 2n.3a и . 7) тогда и только тогда, когда е- гёделев номер такой общерекурсивной функции f, что для любого натурального пчисло f(n)реализует Замкнутая формула Fназывается р е а л и з у е м о й, если существует число е, реализующее F. Формула А(y1,. .,ym), содержащая свободные переменные y1,. ., у m, может рассматриваться как предикат от y1, ..., y т("формула A (у 1,. .., у т )реализуема"). Если формула Fвыводима из реализуемых формул в интуиционистском арифметическом исчислении, то Fреализуема (см.

[3]). В частности, всякая формула, доказуемая в интуиционистской арифметике, реализуема. Можно указать такую формулу А(х), что формула не реализуема. Соответственно, в этом случае формула реализуема, хотя является классически ложной. Всякая предикатная формула , доказуемая в интуиционистском исчислении предикатов, обладает тем свойством, что каждая арифметич. Формула, получающаяся из подстановкой, реализуема. Предикатные формулы, обладающие этим свойством, наз. Р е а л из у е м ы м и. Было показано [4], что пропозициональная формула где Dобозначает формулу , реализуема, но не выводима в интуиционистском исчислении высказываний. Лит.:[1] К 1 е е n e S. С., "J. Symbolic Logic", 1945, v. 10, p. 109-24. [2] К л и н и С.

К., Введение в метаматематику, пер. С англ., М., 1957. [3] N e l s o n D., "Trans. Amer. Math. Soc.", 1947, v. 61, p. 307-68. [4] R о s e G. F., там же, 1953, v. 75, p. 1 -19. [5] H о в и к о в П. С., Конструктивная математическая логика с точки зрения классической, М., 1977. В. Е. Плиско.