Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 93
Текст из файла (страница 93)
Если удастся осуществить эту редукцию так, что ограниченный формализм в отношении непротиворечивости будет равносильным формализму (У), то тем самым непротиворечивость (2) будет до- ') Впервые исчисление высказываний, ограниченное в духе этого требоввния, было построено А. Гейтннгом в его уже упоминавшейся работе: Н е у- 1! пя А. Вне 1огвв1еп цеяе1п дег !о1о!1!оп!»1!зсьен 1.айж.— Вцяйзьег.
ргеизз. АКад. %!зз., рьуз.-вврв К1., 1930, П. Относительно одного еве более сильного ограничения см. рабату И. Йогзвсонв: Зоьвпззап 1. Пег М!пннв!- !гзгий, еш геди»!ег1ег !п1нгйап!»изсьег Гогвэ!!»во»,-Соврав!1!а Мв1Ь., 1936, 4, № 1. казана с точки зрении любых предположений, достаточных для какого-ли о истолкования типа верификации этого ограниченного Мы покажем, что такая редукция, обладающая желательным для нас свойством, действительно оказывается осуществимой. Сначала мы можем исключить дизъюнкцию, квантор сущест- вования и формульные переменные.
Действительно, дизъюнкцию можно выразить через конъюнкцию и отрицание. При этом вся- кая тождественно истинная формула исчисления высказь в ! аний снова перейдет в тождественно истинную формулу. Далее, каж- дое выражение вида ЗХЯ(е) может быть заменено Выражением ) Уй ) 6(е), При этом основная формула (Ь) будет выводимой, (й) — п оизводной. Исключение формульных переменных можно — как это уже неоднократно делалось — произвести с по- мощью метода возвратного переноса подстановок в исходные фор- мулы'). Только при этом нам нужно будет модифицировать по- нятие доказательства, взяв вместо исходных формул, содержащих формул р ф . льные переменные — таковыми являются тождественно истин- ные фор у формулы исчисления высказываний, основная фор у ( ) исчисления предикатов, аксиома равенства ()е) и аксиом дуаин к- ции, — соответствующие схемы формул.
Впрочем, аксиому индук- ции, как известно, ст о с самого начала можно заменить схемой индукции. После того как мы таким образом сузим наш формализм, мы ограничим еще и исчисление высказываний, разрешив применять конъюнкции и импликации только в способах умозаключений по- змтивной логики ).
'). Для формализации этих способов достаточно ыво а' взять следующие схемы формул и схемы вывода ): Я, Я-~- 3 Я-м «), Я-~- (6-м 6) З Я-~- 6 63!ю-+ 6 Я 3! 3 -ь Я, 31 3! З -м З, Я -Ф(3-м6) из которых в качестве производных схем получаются, в частности, следующие: Я Я-м(!б-»-6) Я-»6 Я, 6 Я-+.!В, 6-»-6 5- Я' Яаэ- б ' (Е- 6)- (Я- 6)' 63 Е' Я- 33.6 Ввиду исключения дизъюнкции из рассмотрения, из числа связок исчисления высказываний — помимо импликации, конъюик- ') С .. 1, с. 99 — 101, э также Приложение П!, с.
5!2 и далее. ') См. с. 473. ') Подробнее об этом см. в Приложении П!, в особенности нв с. 52— . 5 1 — 529. 431 непротиворечивость Арифметики выход зд рамки тнории докдздтвльств илт ции и эквивалентности 6 6, которую мы рассматриваем как сокращение для выражения (6-+ Е) й(З-рИ),-у иас остается только отрицание. Мы возьмем его не в качестве основного знака, а в качестве знака, вводимого посредством явного определения ~6 (И вЂ” «О'=0). Опираясь на это определение, мы из схем 6-1.5, И-р(3-~-5) Ий3-р5 и Э 6->-И 6-р(И-з-$) взяв в них вместо 6 формулу 0' = О, получим схемы 6-+-5, 6-р ) 3 )(Яйй) 16 6 — )З Равным образом из производных схем И- (8 -т.
И) 6 -+6 6-р(З-+.5) Ий 3 -р И (3-~-И)-+ (6-~-И) 3 -+ (И -р $) мы получим для отрицания схемы 6-+. 16 6-р6 6-~- ) Е и ~(Ий3) ~3-+ )6 3-р ~6 Разумеется, все этн схемы мы получили бы тем же самым способом и в том случае, если бы, взяв произвольную формулу й, мы определили отрицание посредством эквивалентности ~ 6-(6-«-5). Получаемые таким способом схемы для отрицания — это в точности схемы, действующие в так называемом м и н и м а л ь н о м исчислении Йогансона'). В исчислении высказываний Рейтинга ко всему этому добавляется схема формул )И- (6 — Е), которая у нас может быть выведена на основе данного нами определения отрицания. Действительно, согласно нашему определению, эта схема может быть получена из формулы (6 -+ 0' = 0) -~- (6 -~- 5), а эта формула с помощью имеющихся у нас схем выводима из т) См, подстрочное примечание на с.4 схемы 0' = 0-+.З.
Но эта схема выводима, и е е вывод получается — с использованием схемы индукции и схе мы для равенства †следующ образом: Сначала индукцие унцией по п с использованием выводимой формулы а=Ь-ра'=Ь' получаем фоРмУлУ 0' = 0-+ а' = и С помощью этой формулы индукций по а получаем формулу О' 0- а=О, из которой с использованием выводимой формулы а=ОйЬ=О-+а=Ь получается формула 0'=0-+ а=Ь а из этой формулы подстановкой можно получить формулу 0' = 0-р а = Ь, где с и Ь вЂ” произвольные терм~. Далее получаются следующие Угвержд ния ение отрицаюбой фо м лы И, опираясь на определение И -~- 'З -р 6) можно получить схему ния и на выводимость схемы 0'=0-»- ~И.
о, Из двух формул вида 0 0~3, и 0'=О- Ие с помощью наших схем выводятся формулы 0'=О-ра,йбе и 0'=О-р(З,-+ Юе). 3. Из формулы О' = 0-~-И (а), содержащей свободную переменную а а и не содержащей связанной переменной х, с помощью схемы (се) получается формула 0' = О -+- УуИ (х). А теперь опираясь на эти утверждени и р е ия и п ослеживая процесо построения Е из элементарных формул ( д л (в анном сл чае из 43З 432 выход зд Рамки теории доказательств 1гл. ч НЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ % з1 равенств), можно показать, что формула о=о е выводима при любой формуле 6. Но мы должны еще формализовать предположение о том, что для равенства натуральных чисел имеется его контрадикторная противоположность.
Это может быть сделано следующим образом. Мы вводим в качестве основного знака символ различия ~ вместе со следующими относящимися к нему аксиомами различия'): а ФЬ-»(а =Ь-»О' =0), (а = Ь -» 0 = 0') -» а ~ Ь, (а =~ Ь -» 0' = 0) -» а = Ь. Третья из них представляет собой усиление формулы 0'=0 — »а=Ь, выводимость которой установлена. Из второй аксиомы мы получаем формулу 0' = 0 -» а ~ Ь, аФЬ-» 1(а=Ь), а=Ь- 1(аФЬ), 1(а = Ь) - а Ф Ь, 1(а чь Ь) - (а = Ь), а тем самым и формулы а -6 Ь вЂ” ) (а = Ь), ) ~(а=Ь)- а= Ь а=Ь 1(ЕФЕЬ), 1 ) (аФЬ)- аФЬ. Так, в итоге, мы приходим к следующей модификации формализма (2): в качестве элементарных формул у нас будут фигурировать лишь выражения вида п=6 и а~5, где а и термы, а в качестве формул — такие выражения, которые либо являются элементарными формулами, либо строятся из них применением операций конъюнкции, импликации, эквивалентности, отрицания, а также замены какой-либо свободной переменной связанной переменной (ранее в этом выражении не встречавшейся) ') Чтобы оправдать этот подход, мы сошлемся на то, что в рассматрнваемом формализме все термы, не содержащие свободных переменных, нумернчески вычнслнмы н, следовательно, имеют значенне (в виде некоторой пнфры).
откуда получается, что для расширенного понятия формулы утверждение о выводимости любой формулы вида 0' = 0-» 6 тоже справедливо. Пользуясь знаком отрицания, мы получим из этих трех аксиом формулы с последующим связыванием всего выражения одноименным с этой переменной квантором всеобщности. К таким формулам применимы упомянутые выше пять схем исчисления высказываний, а также определения для эквивалентности и отрицания. В отношении свободных индивидных переменных у нас действует правило подстановки, а для квантора всеобщности имеется схема формул, соответствующая основной формуле (а), а также схема (ех).
Тем самым логическое исчисление описано. К нему добавляется аксиома а = а и схема а = Ь вЂ” (6 (а) -» 6 (Ь)) для равенства. В качестве арифметических аксиом у нас имеются две аксиомы Пеано ) (а' =0) и а' =Ь'-»а=Ь, три аксиомы для символа юь, а также рекурсивные равенства для сложения и умножения. Ко всему этому добавляется еще одна арифметическая схема — схема индукции. Определенный таким образом арифметический формализм мы будем обозначать посредством (3). Можно показать, что в этом формализме выводима всякая формула, выводимая в системе (Е) и не содержащая формульных переменных, дизъюнкций и кван- торов существования.
Действительно, если мы рассмотрим средства, остающиеся в формализме (Х) после исключения формульных переменных, дизъюнкции и квантора существования и после замены всех исходных формул, которые содержат формульиые переменные, соответствующими схемами формул, а аксиомы индукции схемой индукции, то увидим, что в формализме (3) из этих средств непосредственно отсутствуют только следующие два: схемы формул, соответствующие тождественно истинным формулам исчисления высказываний, и взаимозаменяемость выражений а~ 6 и ) (а=3). Эта последняя, однако, имеет место ввиду выведенной нами эквивалентности а чь Ь 1 (а = Ь).
Что же касается схем формул, соответствующих тождественно истинным формулам исчисления высказываний, то у нас рассматриваются лишь те из них, в которых из числа символов исчисления высказываний фигуриру~от только конъюнкция, импликация, эквивалентность и отрицание. Можно показать (мы будем говорить об этом в Приложе. иии П1) '), что любая из этих схем выводима из пяти схем ') См. Прзложевне 111, 1 3, с. 532 — 542. 434 435 НЕПРОТИВОРЕЧИВОСТЬ АРИФМЕТИКИ ) 1(З й 6) -«З 44 6. (й(-«З)-«() $6-« ~ )3) 2. Схема в сочетании с выводимой схемой 3 -«((3 — «6) -«6) З-«( ~ ~(З-«6)-«) ~6). дает схему ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЭАТЕЛЪСТВ системы (3) для конъюнкции и импликации, схем ~Л-«З, Я-«)З )(6ЬЗ) и 16 Я вЂ” «~З (которые, как уже упоминалось, получаются из них с помощью явного определения для отрицания), правила относительно заменимости И З формулой (~Л -«3) й (3-«Я), а также схемы формул ) )й — «Я.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
