Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 89
Текст из файла (страница 89)
Затем, используя символ М (и, й), мы с помощью эквивалентности У1)(п) (г(грай М(п, г)) строим изображение 8)1! (л) высказывания «число л является номером некоторой истинной предваренной формулы без свободных переменных». Затем с помощью эквивалентности 8)[ (а) У12 (рг (и)) мы получаем изображение У1 (а) высказывания «число л является номером некоторой истинной формулы без свободных переменных» и, наконец, получаем общее определение истинности с помощью формулы Я (л) й )Ух (51 (а, х) й 8, (х) -+ У1 (х)), которую мы будем обозначать посредством У(о (и). Рекурсивное определение формулы У1«(а) получается из сле- дующей эквивалентности: У1«(п)-а=70, 11»са, «).13«!.
»)й~о(ч(а, 4)) йф,(ч(п, 5)) й(ч! (ч(п, 4)) =ч1 (ч(п, 5))) ~/ Зх(х~лйп=З хй(О)(х) й 1У1«(х)) ')/ 1м),(а) Й.ИХЭу[х(п*у(пй ((х = 20 7" 1!" Й У1о (х) Й У1« (у)) ~/ (х= 40 7» 11" й(У)о(х) ~/ У)о(у))) ~/ (х = 80 7". 11" й (У1« (х) -)-У1о (у))) ')/(х=160 7" 11" Й(У[о(х) У1«(у))))[1.
Определение предиката М(п, й) мы сначала поясним нефор- мально. Истинная предваренная формула без кванторной при- ставки представляет собой истинную формулу без переменных. Истинная предваренная формула с Г-кванторной приставкой является либо формулой вида )Ууй[(~) и тогда для любой цифры [ формула 'А (!) является истинной предваренной формулой с 1-кван- торной приставной, либо формулой вида Зхб(х) и тогда по край- ней мере для одной цифры 1 формула 4[(!) Является истинной предваренной формулой с 1-кванторной приставкой. Это определение в арифметической формализации изображается следующим образом: М(п, О) — У)1«(п), М(а, й') (а=50 (ох~с„") '"лй) (п))ЗЙ (ж) Ухм(з[(ч(п, л(п)), 1»А(а)„2 3"), й)~ Ц [а=100 Ксс,") """й 2(п))ЗЙ ЗХМ(З1(ч(л, ). (а)), (РА[„), 2 За), й)1 С помощью формулы М (и, й) мы, как было замечено ранее, можем получить следующие явные определения для формул 8)1 (п) и У[а (а): У) (л):-)г (г ~ рг (л) Й М (рг (а), г)), У[а (и) С (и) й 'рх (31 (и, х) й «Оо (х) — ю- У1 (х)).
Итак, мы получили искомое определение истинности для формализма (Х). Рассматривая его с учетом планируемого применения теоремы Тарского, мы должны напомнить, что в формализме (ЕР) все рекурсивные функции допускают явные определения, причем таким образом, что на основе этих определений рекурсивные равенства являются вьводимыми формулами. Значит, в частности, в (ХР) рекурсивное определение функции рг (а) может быть заме- 4 2! ФОРМАЛИЗАЦИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА 47З 4!2 ВЫХОП ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ [ГЛ.
У нено явным. Равным образом, и рекурсивное определение предиката И, (и) тоже может быть заменено прямым построением соответствующей формулы из (ЕР) и даже из (3.). Отметим далее, что для любой конкретной цифры 1 из формул (Ж) выводима эквивалентность М(п, 1) Й(п), где Й(п) — некоторая (зависящая от 1) формула из (20). Поэтому при любой заданной цифре и формула И(п), ввиду эквивалентности Чз(георг(п)З7М(рг(п), г)) М(рг(п), 0) !7 М(рг(п), 0') )( ... ~/ М(рг(п), 1), где ! — значение терма рг(п), переводима в некоторую формулу из (470). Затем, если и является номером некоторой формулы Я из (Е) без свободных переменных, то рассматриваемая формула переводима в формулу Я. Действительно, для любой такой цифры и значение 1 герма рг(п) является, как мы знаем, номером некоторой переводимой в формулу 'Л предваренной формулы Л„ а формула М(рг(п), О) ~/...
~( М(рг(п), !), в которую переводима формула И(п), со своей стороны, может быть переведена в такую предваренную формулу %, у которой кванторная приставка совпадает с приставкой формулы Я„а стоящее после кванторной приставки выражение имеет внд Из(й (ге %7)); здесь 31, ..., ес — Различные входЯщие в фоРМУЛУ Я, связанные переменные, и если Я, (х„..., хс) — выражение, стоящее в Я, после кванторной приставки, то й(а„..., а,) представляет собой арифметическое функциональное выражение, которое сопоставляется формуле Л, (а„..., а,) относительно переменных а„..., а,. А теперь, опираясь на определение формулы И,(п) и исполь.
зуя выводимую формулу 91(2 3') = а, можно вывести эквивалентность Ие(й(аы " а,)) Яе(аы " а„),' а из этой эквивалентности средствами исчисления предикатов можно вывести формулу й) Я„ которая вместе с выводимыми формулами И(п) И и 1Л Яз дает нам искомую эквивалентность И(п)-Я. Замечание. Если формула 1Л не содержит кванторов и, значит, является формулой без переменных, то непосредственно получаются эквивалентности И (и) И, (и) и Из (и) Я.
Описанную здесь лишь вкратце выводимость формулы И(п) Я мы поясним на примере, когда Я представляет собой формулу Чх(х~О-~-Чу(х у=у')), которая очевидным образом является ложной. Если и — номер этой формулы, то имеет место равенство зр (и) = и, а рг (и) является номером формулы 97хпу( ) (х=О)'Т,с'х у=у'). Этот номер представляет собой число 50 7100'и' ' 40 79,70.ИЕ13з И70.113 11'17~~.!33 И Мы обозначим его буквой !. Формула И(п) переводима в дизьюнкцию М (3, О) )7 " ~~ М (1, 1), которая с помощью выводимых формул М(1, О) Из(1), )И,(1), 1,(!)=7, Л(1)=3, 1=30 Р,"„;" "0 л(0) переводима в 'формулу (1) 1!схМ(31(ъ (7, Л(1)), 7, 2 3'), 0) !/ ...
... ~( 107хМ(31 (т(й Л(1)), 7, 2 3"), ! — 1). Легко видеть, что Л ( )) 100 11еь79.70.11'13',1170 110' ' 13 ' а из определения 31(т, й, 1) получается, что 2.3 31(9(1 Л(!) 7 2,3е) 100.1140.79'0 ' '. з*,п70 И " "оз Выражение, стоящее в правой части этого равенства, мы обозна. чнм посредством с (а). Э 3! ФОРМАЛИЗАЦИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА 4!Э сгл.
ч ВыхОд ЗА РАмки теоеии докАЗАтельстВ Из рекурсивных определений функций') 13„, 7.(п) и ч(п, й) могут быть выведены формулы ч (с (а), гс (с (а))) 131(с(а))=11, Л(с(а))=4, с(а)=100.133(с(а)) Из этих формул мы сначала получим формулу ) Ио (с (а)), а затем формулу М(с(а), й') ЭуМ(31(ч(с(а), )с(с(а))), 11, 2 3"), й). Поэтому дизъюнкцию (1), которая переводима в формулу ЧхМ(с(х), 0) ~/ ... 'ч' 'чхМ(с(х), ! — 1), можно перевести в формулу (2) УхЗуМ(з!(ч(с(х), 7 (с(х))), 11, 2 3"), 0) 3/ ... ... з~ Чхзум(31(ч(с(х), Х(с(х))), 11, 2 3"), 1 — 2) По определению функции 3!(и, й, !) мы получаем равенство 31(ч(с(а), )с(с(а))), 11, 2 3') = 40 73 70.113 3 !Зс 1113 113 11 ' ° 1Т ' .!Зг 3 Выражение, стоящее в правой части этого равенства, мы обозначим посредством 9(а, Ь).
С помощью выводимой формулы 3(а, Ь) чь ~50 п мы получим 1М(й(а, Ь), 73'), а отсюда средствами исчисления предикатов получим формулу )згх)уМ(3(х, у), й'). Поэтому формула (2) переводима в формулу 'охЛуссс!о (3 'х, у)). А теперь, чтобы убедиться в переводимости этой формулы в формулу чсх)у( )(Х=О) ~/ х у=у'), достаточно установить выводимость эквивалентности (3) И, (9 (а, Ь)) ! ! (а = 0) 37' а Ь = Ь'.
Эта эквивалентность легко может быть получена следующим образом. Пользуясь определением формулы И,(п), мы сначала с помощью выводимых формул 3(а Ь) — 40.7 (оежы,з) 11 (ос,ы,с) и Яг(Ч(а, Ь)) получим эквивалентность (4) Ио(й(а, Ь)) Ио(ч(9(а, Ь), 3)) Ч' И,(ч(3(а, Ь), 4)). 1) См. с, 272.
Затем, опираясь на выводимые равенства ч(3(а, Ь), 3) =9.70 !1'3' 13', ч(9(а, Ь), 4)=70 1Р'Иг'3 'Тг3 13333 и снова пользуясь определением И,(и), получим формулы 3)!3(ч(й(а, Ь), 3)) )(~о(2 3')йЖ(2)йч!(2 3') =ч1 (2)) Ио(ч(3(а, Ь), 4)) "®о(5,113'3'.173'3 ) йсъо(2 3"') й ч! (5 11.'3' 17'3 ) = ч1 (2 33').
Но формулы, стоящие в правых частях этих эквивалентностей, с помощью определений формулы ч.о и функций ч! Могут быть переведены в формулы ) )(а — 0) и а Ь-Ь', так что из эквивалентности (4) мы получаем формулу 3)!3(9(а, Ь)) ) )(а=О) ~/а Ь Ь', т. е. искомую эквивалентность (3). Показанная на этом примере выводимость формулы И(п) И средствами формализма (Х ), к которому добавлены формулы (А1), имеет место всякий раз, когда 6 является формулой без свобод- ных ' переменных, а и — ее номером. На основание предыдущего рассуждения это позволяет нам сделать вывод о том, что невоз- можно указать такую формулу 6 (и, й), принадлежащую форма- лизму (Е„), — если, конечно, этот формализм иепротиворечив,— чтобы прй замене символа М(п, й) этой формулой эквивалентно- сти (Ж) становились выводимы формулами.
Действительно, в про- тивном случае формула Зг(г( рг(и) й6 (рг(и), г)) была бы формулой Ио (п) из формализма (Е„), удовлетворяющей условию, что для любой формулы 6 без свободных переменных и для ее номера и в (Ха) выводима эквивалентность Ио(п) 111; но, как мы уже убедились в свое время, возможность построения такого рода формулы не совместима с непротиворечивостью (7Ф) ').