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

уточнение интуиционистской семантики арифметич. суждений на основе понятия частично рекурсивной функции, предложенное С. Клини (см. [1], [2]). Для всякой замкнутой арифметич. формулы Fопределяется отношение "натуральное число ереализует формулу F", обозначаемое erF. Отношение erF определяется индуктивно в соответствии с построением формулы F. 1) Если F - элементарная формула без свободных переменных, т. е. формула вида s=t, где s и t - постоянные термы, то erF тогда и только тогда, когда е=0 и значения термов s и tсовпадают. Пусть Аи В - формулы без свободных переменных. 2) [img: http://localhost:8080/file/041875-116.jpg] тогда и только тогда, когда [img: http://localhost:8080/file/041875-117.jpg], где аrА, brВ. 3) [img: http://localhost:8080/file/041875-118.jpg] тогда и только тогда, когда [img: http://localhost:8080/file/041875-119.jpg] и аrА или е=21.3b и brВ. 4) еr (АЙВ)тогда и только тогда, когда е - гёделев номер такой одноместной частично рекурсивной функции j, что для любого натурального числа а, если аrА, то j применима к aи j(а)rВ. 5) [img: http://localhost:8080/file/041875-120.jpg] тогда и только тогда, когда er(AЙ1=0). Пусть А(х)- формула без свободных переменных, отличных от х;если п - натуральное число, то [img: http://localhost:8080/file/041875-121.jpg] - терм, изображающий в формальной арифметике число n. 6) [img: http://localhost:8080/file/041875-122.jpg] тогда и только тогда, когда е = 2n.3a и [img: http://localhost:8080/file/041875-123.jpg]. 7) [img: http://localhost:8080/file/041875-124.jpg] тогда и только тогда, когда е- гёделев номер такой общерекурсивной функции f, что для любого натурального пчисло f(n)реализует [img: http://localhost:8080/file/041875-125.jpg] Замкнутая формула Fназывается р е а л и з у е м о й, если существует число е, реализующее F. Формула А(y1,...,ym), содержащая свободные переменные y1,..., у m, может рассматриваться как предикат от y1,..., y т("формула A (у 1,..., у т)реализуема"). Если формула Fвыводима из реализуемых формул в интуиционистском арифметическом исчислении, то Fреализуема (см. [3]). В частности, всякая формула, доказуемая в интуиционистской арифметике, реализуема. Можно указать такую формулу А(х), что формула [img: http://localhost:8080/file/041875-126.jpg] не реализуема. Соответственно, в этом случае формула [img: http://localhost:8080/file/041875-127.jpg] реализуема, хотя является классически ложной. Всякая предикатная формула [img: http://localhost:8080/file/041875-128.jpg], доказуемая в интуиционистском исчислении предикатов, обладает тем свойством, что каждая арифметич. формула, получающаяся из [img: http://localhost:8080/file/041875-129.jpg] подстановкой, реализуема. Предикатные формулы, обладающие этим свойством, наз. р е а л из у е м ы м и. Было показано [4], что пропозициональная формула [img: http://localhost:8080/file/041875-130.jpg] где Dобозначает формулу [img: http://localhost:8080/file/041875-131.jpg], реализуема, но не выводима в интуиционистском исчислении высказываний.