Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 86
Текст из файла (страница 86)
Замечание. Предположение атом, что переменная с в терм! не входит, из утверждения 3 может быть исключено. Действи- тельно, если выполнены остальные предположения утверждения 3, а 1 содержит переменную г, то мы возьмем свободную индивид- ную переменную Ь, не входящую ни в 6(г), ни в 1.
Согласно утверждению 1 формула 5 [Ь] выводима. Поэтому, согласно утвер- ждению 3, выводима формула 5[6(д)], а отсюда, снова согласно утверждению 3, вытекает выводимость формулы 5[6(1)]. Утверждения ! — 4 мы получим следующим образом: 1. Формула 5[0] записывается в виде з(д(0=д 8(70 !!' !3""). С помощью аксиомы равенства (Лз) она выводится из формулы 8(70 !! !3 ), а значит, и из формулы 8(70 11' !3'), т.
е. из 8 ([0 = 0]). Но, согласно нашей лемме, эта формула выводима, так как выводима формула 0=0. Если с — свободная нндивндная переменная, то 5[с] представляет собой формулу Уд(с =д 8(70 !1з з !Зз'з~))' которая с помощью аксиомы (Зз) выводится из формулы 8(70 !!зз !Ззз)> т. е. нз формулы 8 ((г = г]), которая, по нашей лемме, выводима вследствие выводимостп формулы с=с. 2, Пусть 1 — терм, и пусть формула 5[1] выводима, Возьмем две различные свободные индивидные переменные г и Ь, не входящие в 1. Формула 5[1] дедуктивно равна формуле 1 = с — ~.
8 ((1 = с)). Из выводимой формулы 1=з- В=с' по второй 8-схеме мы получаем формулу 8 ((1= <!) -Р8 ((1' г'[). Тем самым мы получаем формулу (1) 1 = г -~- 8 ([1' = г')). С другой стороны, из формулы (2) 1=С-Р1 =С получается формула 1=с-Ф(1'=Ь-»д=з'). Так как Ь и с-свободные индивидные переменные, то формула 8 ((д = Г')) имеет вид 8(70 !1з.з, 13з з з'), н поэтому формула ь = с'-э 8([ь = с']) зэб выход зА РАмки теогии покхзхтельств !ГЛ. Р $21 ФОРМАЛИЗАЦИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА Ззт переводима в формулу Ь=с' Е(70 11 2' 13 2').
Эта формула с помощью аксиомы равенства (32) выводима из формулы 6(70 1122 1322)> т. е. из формулы 6 ((ь = ь)), которая выводима в силу нашей леммы и выводимости формулы Ь=Ь. Поэтому выводима формула Ь = с' -«- 6 ([Ь = с')), а вначит, согласно формуле (2), выводима и формула (3) Е=с [1'=Ь- 6([Ь=с')). Кроме того, из выводимой формулы Ь=с' — (1'=с' — 1'=Ь) мы по второй ч)-схеме получаем формулу 6([Ь=с'))-«6([С'=с'-«1'=Ь)), а первая $-схема дает нам формулу Е ([1' = с' — 1' - Ь)) — [Е ((1 = с')) — Е ([1' = Ь))), которая вместе с предыдущей формулой дает формулу (4) 6 ([ь = с')) - [6 ((с' = с')) - 6 ([1' = ь))).
Полученные нами формулы (1), (3) и (4) с помощью средств исчисления высказываний дают формулу 1 = с - [у - ь 6 ((с' - ь))). Затем с помощью средств исчисления предикатов (так как пере- менная с не входит в 1 и отлична от Ь) мы получаем формулу зу(1=у)- [1'=ь- 6((1'=ь))) и, далее, вследствие выводимости формулы =1у(с=у) — формулу с' = ь -« е ((с' = д)). Но так как переменная Ь в терм 1 не входит, из этой формулы мы получаем формулу 5[у]. 3 П .
Пусть 6(с) и 1 — термы, и пусть < — свободная индивидная переменная, не входящая в 6(1). Пусть формулы 5[6(с)] и 5 И выводимы. Возьмем какую-либо свободную индивидную переменную не йходящую ни в 6(с), ни в 1. Из формул 5(6(с)] и 5(1) мы сначала получим формулы (5) б (с) = Ь вЂ” «-6 ((б (с) = Ь)), Е = с -« Е ((Е = с)). Первая из них в сочетании с выводимой формулой 1 = с -«-(б (Е) = Ь вЂ” 6 (с) = Ь) дает формулу (6) Е с — «(6(1) = Ь-«6((6 (с) =Ь))).
Далее, из выводимой формулы Е = с -«- (6 (с) = Ь -«. 6 (Е) = Ь) мы по второй 6-схеме получаем формулу 6((Е=с))-«Е((6(с) Ь-«6(1)=Ь)), из которой затем с помощью формулы 6 ([6 (с) = д -« б (1) д)) .ч- (Е ((6 (с) Ь)) -« 6 ([6 (Е) Ь)), получающейся по первой е-схеме, получаем формулу Е ([Š— с)) — (Е ((6 (с) = Ь)) — Е ([6 (1) = Ь])), которая вместе с (5) дает формулу (7) Е = с -«(6 ((б (с) = Ь)) -«6 ((6 (1) = Ь))).
Формулы (6) и (7), взятые вместе, дают формулу 1 = с — (б (1) = Ь вЂ” Е ((6 (1) = Ь])), Так как переменная с не входит в 6(1) и отлична от Ь, то из последней формулы, используя выводимую формулу Вх(1 =х), средствами исчисления предикатов получаем формулу 6 (1) = д †«. Е ((6 (Е) = ь)), а эта формула дает нам формулу й [6(1)], так как переменная Ь не входит в терм 6(1). 4.
Что касается схем рекурсии для одноместных и для двуместных функций, то рассуждения в этих двух случаях совершенно аналогичны. Поэтому достаточно рассмотреть схему рекурсии для введения двуместных функциональных знаков: ( (а, О) = а (а), ((а, и') =Ь(а, и, 1(и)). $2! ФОРМАЛИЗАЦИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА ззэ ВЫХОЛ ЗА РАМКИ ТЕОРИИ ПОКАЗАТЕЛЬСТВ ~ГЛ Р Здесь мы предполагаем, что термы е(а) и Ь(а, л, с) содержат только указанные переменные и что формулы 5 [а(а)] и 5 [Ь(а, л, с)] выводимы. Формулы ((а, О) = е (а) и ((а, л') = Ь (а, л, [(а, л)) выводимы в (Х„) с помощью явного определения функции [(а, и), Из этого явного определения получается и конкретное изображение этого функционального знака в нашей нумерации. Арифметическое функциональное выражение, сопоставленное терму 1(а, л) относительно переменных а и л, имеет вид 5,р23 .223" где р и 2 — некоторые конкретные простые числа, и потому формула 5[[(а, и)] имеет вид 'ку(1 (а, п) = у-«6 (70.
11'" '" 13"")). Если обозначить эту формулу посредством 5,(п), то, как легко видеть,, формула 5,(0) будет переводима в формулу 5[1(а, О)], а формула 52(л') — в формулу 5[[(а, п')]. поэтому с помощью схемы индукции, которая, как известно, в (Х„) является производной, формулу 5[[(а, п)] можно получить из формул 5[((а, О)] и 5[[(а, л)] — «5[[(а, п')]. Обе эти формулы выводимы на основе наших предположений. Действительно, формула 5 ([ (а, О)] получается следующим образом. Из выводимой формулы [(а, О) а(а) с помощью аксиомы ()2) мы получаем (8) а(а)=с-«[(а, 0)=с и (9) ( (а, О) = с -«а (а) = с, а из формулы 5[а(а)] получаем (1О) А (а) = с-«к) ([а (а) с]).
Формулы (9) и (10), взятые вместе, дают (11) [(а, 0)=с-+ 6((а(а)=с)). С другой стороны, из формулы (8) по второй 6-схеме можно получить формулу 6 ((а (с) = с)) -« 6 ((1(а, О) = с)), а эта формула, взятая вместе с формулой (11), дает нам формулу ! (а, О) = с-«6 ([[ (а, О) = с]), из которой немедленно получается 5[[(а, О)]. Формула 5[((а, л)]-«5[1 (а, л')] получается следующим образом: Средствами исчисления предикатов мы сначала получаем (12) 5[[(а, л)] — «(1(а, л)=с — «6(([(а, л) с])). Из выводимого рекурсивного равенства [(а, л') Ь(а, л, [(а, л)) с помощью аксиомы ()2) получаем (13) [(а, п)=с-«([(а, и')=д — «Ь(а, л, с)=Г!) и (14) ((а, л)= с-«(Ь(а, л, с)=й- 1(а, л')=Й). Затем из формулы 5[Ь(а, п, с)] получаем формулу Ь(а, л, с) =Г(-«6([Ь(а, л, с) =с()), которая вместе с формулои (13) дает (!5) 1(а, и) с-«(1(а, л') д-«6(!Ь(а, л* с) =4)) С другой стороны, формула (14) по второй 6-схеме дает формулу З(([(а, п) =с)) — 6((Ь(а, л, с) =с(-«[(а, л ) =с()), откуда, с помощью получаемой по первой 6-схеме формулы К3((Ь(а, л, с) =Г! — «[(а, л')=4) — « (6([Ь(а, л, с) Г())-«6([[(а, л') =с())), получается (16) 6([! (а, л) =с])-«(6((5(а, п,с)=д])-«6(([(а п )=4)).
Формулы (12), (15) и (16), взятые вместе, с помощью исчисления высказывании дают нам формулу 1(а, л) с-«(5[1(а, и)]- (!(а, л')=й-«6([[(а, л')=а)))), из которой мы средствами исчисления предикатов с использованием выводимой формулы Бх(1 (а, л) =х) получаем 5[[(а, п)]-«5[[(а, п')]. Тем самым мы завершили доказательство того, что формализм (2'„) удовлетворяет третьему условию на выводимость. Заметим, что это доказательство дает также некоторое финитное уточнение выход зд Рамки тпории доклздтвльств [гл. и й 3! Формализация лриомвтичвского Формализма 40$ утверждения о выводимости формулы ( (т) = 0-м 6 ((1 (пт) = О)) (для любого наперед заданного рекурсивного терма ((пт) с единственной переменной гп), поскольку мы получаем метод, позволяющий по заданному терму 1(т) эффективно строить вывод рассматриваемой формулы. В самом деле, все использованные нами вспомогательные утверждения о тех или иных выводимостях, а также доказательства утверждений 1 — 4 были таковы, что в них либо содержался некоторый способ вывода для формул какого-либо конкретного вида, либо показывалось, как по заданному выводу какой-либо конкретной формулы можно получить вывод какой-либо другой конкретной формулы.
Аналогичное замечание может быть сделано и относительно проведенной нами для формализма (Е ) проверки выполнения первых двух условий на выводимость'). Общий итог предпринятых выше рассмотрений состоит в том, что для формализма (Е ) оказываются выполненными все предположения второй теоремы Геделя о неполноте. Таким образом, согласно этой теореме, формула ЧхЗ(х, и)-ь ) Зхб(х, 3 п), изображающая утверждение о непротиворечивости формализма (Е„), не может быть выведена в (Е ), ибо иначе формализм (Е„) был бы противоречив. Аналогичным образом можно убедиться, что предположение б,) и добавляемые к нему условия на выводимость выполняются также и для всех таких формализмов, которые, с одной стороны, очерчены достаточно четко, а с другой стороны, включают в себя способы умозаключений исчисления предикатов и обладают средствами, достаточными для изображения понятий и способов умозаключений арифметики, так что в них, в частности, изобразимы рекурсивные функции и соответствующие рекурсивные равенства являются либо аксиомами, либо выводимыми формулами, а кроме того, содержится (в качестве основного правила или производной схемы) схема индукции.
Поэтому ко всем таким формализмам применима вторая теорема Геделя о неполноте. Как уже упоминалось ранее„условия, фигурирующие в нашей формулировке этой теоремы, могут быть заменены более общими. В частности, теорема эта — на что указали Гедель и Крайзел— может быть распространена на формализмы без связанных переменных — например, на рекурсивную арифметику Для рекурсивной арифметики это вытекает из того, ранее уже отмеченного обстоятельства, что доказательства, устанавливающие выполни- О См. с. 38! — 333. и (Е„) условий иа выводимость 1 — 3, являются эффектнв- НЫМИ ).
Мы еще вкратце наметим путь, на котором для формализма (Е) можно установить, что формализованное высказывание, утверждающее его непротиворечивость, не может быть выведено в нем самом, если он непротиворечие. д) Распространение второй теоремы Геделя о неполноте на формализм (Е). — Формулировка определения истинности дли этого формализма. Формализм (Е) получается из исчисления предикатов путем добавления к нему символов О, ', +, и а также аксиом равенства (),) и (Лз), аксиом Пеано а' чь 0 н а' = Ь'- а = Ь, рекурсивных равенств для сложения и умножении и аксиомы индукции.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
