Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 69
Текст из файла (страница 69)
> и.)+ 1,, 6. !1(п,, и<) ! 6), получается равенство (24) 32(аз, ..., аа, (>(7)(а„..., а,)))=за(7)(а<, ..., а,)). Это рассуждение мы вскоре поясним с помощью одного примера. Формулы (23) и (24), взятые друг с другом, дают равенство <р, (Ьа (7! (а„..., а,))) = О, из которого в силу определения функции фо, применяя уже упоминавшиеся ранее выводимые формулы 61(а<, ..., ПР!)=ОЧ<<1(а„..., по<)=! (1=1, ..., >), мы получаем искомую формулу 5*, которая получается из $ в результате замены каждой из элементарных формул ч)1 (а„..., ао,) соответствующим равенством а<(!1„..., АР.! =О. 17 Пункт 6 приведенного формального вывода мы поясним на примере.
Пусть $ — формула '<<хо<у=(г((А(х, у)-~ ) А (у, х>) !«А(х, 2)). Тогда формула 5 запишется в виде (А (аз, аз) -~ '1 А (а„а>)) а> А (а„» (а„п,)+ ! ). В данном случае у иас имеется только одна формульная переменная и поэтому нам не нужно нумеровать формульные переменные и соответствующие им функции <1(а<,..., и! ). Достаточно '! взять одну двуместную функцию <(а„аз), которая для любой пары чисел п„п, изображает номер формулы А(п,, п<). Эта функция определяется равенством !(и 1) !О. 72.за, 112 з' С помощью этой функции номер формулы (А(п„п,) — ~", А(п.„п,)) А А (п„>>(п>, !!.,>д !) — в которой вместо выражения О(г„н,)+! надо <ндс!аеить его яначоиие — изобразится значением выражения 20,7 В,7 (3071(2<,22) И31(ВФВ!)) 111(В! 0(В! Ва)а О В соответствии с этим в качестве <>(3) мы должны взять функцию 20 7'о'7 (ВО 71 <ч~ <<> ч*< >>.
НЗП <ч*и>. >ь <и> ! 11 <10 <7>. 7+ 1> и у нас получится (3071<а,, а > !!31<аа аи) 111<а„п<а„а >+ О Ь(„( „пз)) =20.7 Теперь, используя первое из равенств (20), а также определения функци <р, и <р, и „ й формулы (22), мы получим сначала равенство <рд (йз (а„а„О)) = ! (а„пз), а затем формулы аз Ф аз ->. йз (а„аз, 1) = 20, 7>30 7 ( 10+206<а„аа> !131<аа а> 111<», ч<а, а > ! !> и а> = аз — рз (а„а„1) = 20 7<за> М! 20 6<а,.
«1>1!3 (!0+20 6<а„а~>)) 111<аа Ч<а„ап+!> Аналогично мы получим формулы ад ~ аз -а- 92 (пз, пз. 2) = 20. 7<за.> > 10.! 20 6<аа а > !!3 (!О+ 20 6<аз аа>) 1!1<аа 0<аа а >+1> и а =и -а йз(а„аз, 2)= 20 . 7<за.7 !0 ! 20 6<0, а> !3.(!О+206<а„а>)) 11(10.1.206<а„о<аа ал>->- ) а из них формУлы а< ~ь а — <р, (а, (а„аз, 2)) = 1 (пп 7) (аз аз) + 1) и пд= пз — > <р> (аз(п>~ аз~ 2)) Теперь формулы (21) и (22) с использованием альтернативы а! Ф <72>><аз =-аз дают равенства ,;,(а„а„З) = 20 7<30'7 10+20 6< > !3 (!0+20 6< >) 11(>0+ 20 6< ч< >+ и) и фз (йз (а„а„З)) = О.
Р!3 последнего с помощью формулы (21) получается импликация 3~3->-йз(а„пз, з)=02(аз, а>ь 3) з~в э и АРИФМЕТИЗАЦИЯ ТЕОРЕМЫ ГЕДЕЛЯ О ПОЛНОТЕ 319 МЕТОД АРИФМЕТИЗАЦИИ МЕТАМАТЕМАТИКИ игл. щ а затем, с использованием формулы 3( Ь (з), непосредственно вытекающей из определения функции Ь(з),— равенство 3, (а„а„з (~) (а„а,))) й, (а„а„З), из которого с помощью (23) получается равенство <р,(а,(а,, а„З)) =О. Это равенство в сочетании с выражением для 6,(пд, а„З) и в салу определения ~; сначала дает равенство здп(зяп(Ф,(10+20 6(а,, а,))).сР,(З (10+20.6(а„а,)))+ <Ре (10+ 20 6 (аы т) (ам а,) -1- 1))) = О, а затем с помощью формулы 6 (а, Ь) = 0)/6 (а, Ь) = 1 дает равенство зцп (6 (а„а,)) кап (6 (а„а,)) + 6 (а,, и (а„а,) + 1) — О.
Из последнего равенства мы получим формулу (6(а„а,) ~0~/6(а„а,) ФО) й6(аи п(ам а,,)+1) =О, а из нее преобразованием †форму (6(а,, а,)=0-+-6(а,, а,) ФО) й6(а„т)(а„а,)+1) =О. Но это н есть та формула, которая из формулы 5, т. е. из (А(аи а,)-~) А(а,„а,)) й А(а„т)(а,, ае)+1), получается в результате подстановки равенства 6(а, Ь) =0 вместо формульной переменной А(а, Ь), т. с. это и есть искомая формула ((*.— Тем самым мы получили дедуктивный аналог теоремы Геделя о полноте. Именно, мы показали, что для всякой формулы 5 исчисления предикатов, имеющей вид У7, ... УЗ„.-)9, ...
ВФ,6(ЕЫ -, Е„Р., ..., 9,), где ги ..., 1„г„..., Š— полный список входящих в эту формулу инднвидных переменных, а г н 6 отличны от нуля, можно указать такую рекурсивную функцию а (й), что для каждого числа 1 значение Ч(1) равно нулю нлн отлично от нуля в зависимости от того, выполнима или не выполнима бескванторная формула бь так что для любого Г значение 9(1) отлично от нуля тогда и только тогда, когда отрицание формулы 1)г выводимо средствами исчисления высказываний.
Как мы ранее показали, выводимость средствами исчисления высказываний формулы ) ~5г для какого-либо числа 1 уже является достаточным условием опровержимости формулы 5 в исчислении предикатов. Таким образом, из неопровержимости формулы 5 следует, что функция ч(Ь) равна 0 при любом значении аргумента, так что формула а (й) =О, у которой й является единственной входящей в нее переменной, верифицируема. Мы также показали, что при помощи арифметического формализма, состоящего из формализма системы (2) вместе с )А-символом, формулами ()А,), (и,) н (р,) и дополнительной исходной формулой е (Ь) =О, выводима некоторая формула ~~*, получающаяся из Я в результате подстановок вместо формульных переменных.
Из установленных фактов мы немедленно получаем доказательство сформулированной в конце предыдущей главы теоремы о том, что любая неопровержимая формула исчисления предикатов неопровержима и в любом арифметически непротиворечивом формализме, т. е. в любом таком формализме, который непротиворечив сам, а также остается непротиворечивым после добавления к нему арифметического формализма (если этот последний в него еще не включен) н, быть может, сверх того каких-нибудь верифицируемых формул в качестве исходных.
В самом деле, пусть 6( — какая-либо формула исчисления предикатов, относительно которой установлено, что она неопровержима в исчислении предикатов, т. е. что ее отрицание ) Я невыводимо в исчислении предикатов. Формула П6( дедуктивно равна некоторой сколемовской нормальной форме Я, которая может быть преобразована в отрицание ",5 некоторой формулы 5 рассмотренного нами специального вида. Зта формула, так же как и й, неопровержима в исчислении предикатов, и дланя нее, по доказанному, можно указать такую рекурсивную функцию Ч (Й), что формула а(й) =0 будет верифицируемой и с помощью арифметического формализма с добавлением этой формулы к числу исходных будет выводима некоторая формула 5*, которая получается из 5 в результате подстановок вместо формульных переменных.
Если формула 21 опровергается в некотором формализме г, то она и подавно будет опровергаться в формализме 6, который получается в результате объединения Ь' с арифметическим формализмом и добавления к числу исходных формул верифицируемой формулы а(Ь) =О. Значит, в этом формализме О выводима формула ) Я; и так как этот формализм включает в себя исчисление предикатов и символы арифметического формализма, то в 0 выводима и дедуктивно равная формуле )6( формула )5, а также получающаяся из нее в результате подстановок формула )й*. Но так как формализм 6 содержит арифметический формализм и исходную формулу р(Ь)=0, то в ием выводима формула )1*. Следовательно, формализм 6 противоречив, т. е.
объединение формализма Ь' с арифметическим формализмом при добавлении некоторой верифицируемой исходной формулы ведет к противоречию. Поэтому вывод формулы Гй в арифметически непротиворечивом формализме невозможен. МЕТОД АРИФМЕТИЗАЦИИ МЕТАМАТЕМАТИКИ [ГЛ. 1У Полученному результату можно также придать и другую формулировку, приняв во внимание связь, имеющую место между формулами логики предикатов и системами аксиом.
Непротиворечивость какой-либо системы аксиом, представленной с помощью конечного числа формул без функциональных знаков, равносильна неопровержимости формулы 5 логики предикатов, которая получается из этой системы, если входящие в ее состав формализо-' ванные аксиомы связать знаком конъюнкции, а затем заменить Бее входящие в них символы основных предикатов формульными переменными с соответствующим числом мест для аргументов, а все индивидные символы — индивидными переменными, связываемыми проставленными в начале формул кванторами существования. Переход от формулы Гт с помощью соответствующих арифметических подстановок к формуле 5е по смыслу представляет собой построение ариф»септической модели рассматриваемой системы аксиом, так как формулы, изображающие эти аксиомы, при замене символов для основных предикатов арифметическими выражениями, подставляемыми вместо соответствующих формульных переменных, переходят в доказуемые арифметические формулы (доказуемые, конечно, только при добавлении некоторой верифицируемой исходной формулы Ч(й)=0, которая выражает непротиворечивость этой системы аксиом в математической формализации и которая сама по себе не обязана быть выводимой в формализме арифметики).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
