Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 25
Текст из файла (страница 25)
т. 1, с. 482). Первая из этих двух формул дедуктивно равна формуле А (а) -» А (1»»А (х)), а из второй с помощью формул а' Ф а и ) (а' ( а) получается формула А (а) - р»А (х) ~ а'. взятой совместно с е-формулой, содержательно соответствует принцип, гласящий, что «для любого числового предиката г41, выполняющегося по крайней мере для одного числа, существует такое число, что для него предикат $ выполняется, а для его предшественника, если таковой существует (т. е. если это число отлично от нуля), предикат $ не выполняется». Очевидно, что данный принцип является следствием принципа наименьшего числа.
По сравнению с этим в содержательном отношении более выразительным принципом он обладает тем преимуществом, что структурно он более прост, так как может быть сформулирован без использования понятия «меньше»'). !20 исслндовлиин дннфмнтики пи! помон!и з.символд 1гл и Благодаря указанной новой формализации принципа полной индукции наш подход к исключению связанных переменных при условии включения полной индукции становится совершенно аналогичным предыдущему. Теперь снова после исключения кванторов и возвратного переноса подстановок в исходные формулы можно провести исключение свободнгях переменных, и у нас опять получится некоторое «нормированное доказательствоа, в котором дедуктивная взаимосвязь формул будет основываться лишь на схемах заключения, на повторениях формул и переименованиях связанных переменных.
Отличие от нормированных доказательств, рассматривавшихся до сих пор'), теперь будет заключаться в том, что в качестве исходных формул, содержащих е-символ, помимо критических формул а(() г((в,Л(6)~ и формул е-равенства з) будут допускаться еще и такие формулы, которые получаются путем подстановки из формулы А (а) -г- е, А (х) -ь а' а), так что мы должны будем допустить в качестве критических фо р мул второго рода исходные формулы вида Й(!) — г-е Л(г) чь(', Однако несмотря на это формальное сходство со случаями, рассмотренными ранее, у нас нет никаких перспектив распространения нашей процедуры исключения в-символов на случай, рассматриваемый сейчас.
Действительно, если бы нам удалось произвести соответствующее обобщение, то тем самым мы получили бы способ, который позволял бы исключить из вывода любой формулы, не содержащей связанных переменных, не только связанные переменные, но и применения схемы индукции. В самом деле, как было показано выше'), применение схемы индукции всегда может быть заменено соозветствугощими применениями е-формулы, формулы А (а) -+.
в„А (х) Ф а', аксиомы равенства ()з) и формулы а~О- 6(а)'=а. Если бы мы смогли устранить еще и связанные переменные, а значит, и те исходные формулы, которые содержат е-символ, то тем самым применение схемы индукции было бы вообще сведено к надлежащему использованию формул ()з) и а~О-ьб(а)'=а. Но возможности такого ') См.
с. 40 и 93 з) См. с. 92. з) При этои мы опять разрешаем при подстановке вместо формульной переменной А (а) переименовывать связанную переменную х (см. об этом с. 31). з) См. с, 117 и далее. ! з! в.симнол и вопмллиздция ппинцнпд индткции 121 рода устранения схемы индукции, разумеется, быть не может'). Так как распространение первой е-теоремы на арифметический формализм оказывается невозможным, то перед нами встает задача установления непротиворечивости арифметического формализма без использования этой теоремы.
Прежде всего, посмотрим, в какой мере мы можем воспользоваться здесь нашими прежними идеями. Формализм, с которым мы имеем дело, состоит из исчисления предикатов с добавлением к нему е-символа и е-формулы, а также системы аксиом (У), в которой в качестве индивидного символа фигурирует один только символ О, в качестве предикатного символа — один только знак равенства, а в качестве функциональных знаков — штрих- символ и символы для суммы и произведения. Аксиома индукции, как мы только что установили, может быть заменена формулами а -ь О -ь 6 (а)' = а г) В этом можно убедиться на простых примерах. Возьмем две аксиомы Пеано и' ~ 0 и а'=Ь'- а=Ь. Из них с помощью элементарного исчисления со свободными переменными и схемы индукции можно вывести формулу а' чь и.
Теперь допустим, что из этого вывода можно так устранить применение схемы индукции, что вместо нее всякий раэ будут применяться только формулы (Лз) и ать о-~6(а)'=а, Тогда мы получим вывод формулы и'чьа из указанных двух аксиом Пеано в рамках одного только элементарного исчисления со свободными переменными. Применение аксиомы равенства (Лз) в этом выводе мы могли бы заменить применением специальных аксиом равенства, и так как при атом в качестве преднкатного символа выступал бы одни только знак равенства, а в качестве функциональных знаков †штр-символ и символ 6, то для замены аксиомы (зз) было бы достаточно формул (Л,), (О, п=Ь-ь п' =Ь' и и = Ь -~ 6 (и) = 6 (Ь).
Тем самым из аксном п=а, а Ь-~(п=с-ьь=с), а=Ь а'=Ь', а' Ф и, а Ь вЂ” 6 (п) =6 (Ь), а Ф 0 — ь 6 (п)' =а средствами элементарного исчисления со свободными переменными была бы выведена формула и' чь и. Но тогда, добавив ниднвидный символ в вместе с аксиомой п=в — ьп'=в, из которой с помощью формулы в=в выводится формула в'=в, мы получили бы противоречие, так что была бы выводима и формула 0'=О.
Однако в том, что это не так, можно убедиться с помощью следующего распределения значений для равенств без переменных: равенство а=! будем считать и с т и ни ы и тогда, когда оба терна з и ! содержат символ в, а также тогда, когда з и ! не содержат символа в и совпадают либо непосредственно, либо после вычисления (обычным способом) встречающихся в этих термах анячеиий функции 6; во всех остальных случаях равенство з ! будем считать ложным.
При таком распределении асе перечисленные аксиомы, в том числе и добавленная нами аксиома а= в -ь а' =в, являются верифицируемыми, а поэтому всякая формула без переменных, выводимая из них средствами элементарного исчисления со свободнымн переменными, должна быть истинной, В то же самое время формула 0'=0 является лог!гной.
122 исслндовднин дпиемктики пои помОщи е.симаолд (гл. и и А (и) -ь- е„А (х) Ф и', так что мы и возьмем их вместо нее в качестве исходных формул.. Для нашего доказательства непротиворечивости достаточно, показать, что каждая выводимая формула без переменных при «естественном» распределении истинностных значений, складываю-: щемся из выделенного распределения истиниостных значений для равенства, рекурсивной процедуры вычисления постоянных сумм н произведений и из истолкования связок исчисления высказываний как истинностных функций, является истинной.
Поэтому ' для нашего доказательства доста1очно будет рассматривать только выводы формул без переменных. К каждому такому выводу мы можем применить операции исключения кванторов, возвратного переноса подстановок в исходные формулы и исключения свободных переменных.
Мы можем, далее, заменить применения аксиомы (,!ч) применением специальных аксиом равенства вместе с допущением формул е-равенства в качестве исходных. При этом будут использоваться те специальные аксиомы равенства, которые соответствуют содержащимся в нашем формализме предикатным символам '). В итоге мы получим некоторое «нормированное доказательство», Под этим термином мы теперь будем понимать последовательность формул, обладающую следующими свойствами: ! .
Каждая формула этой последовательности строится из символов =, О, ', +,, б, символов исчисления высказываний и е-символа с соответствующими связанными переменными. 2. Каждая из ее формул является либо исходной формулой, либо повторением некоторой предшествующей ей формулы (возможно, объединенным с переименованием какого-либо числа связанных переменных), либо результирующей формулой какой-либо схемы заключения.
3. Каждая исходная формула или получается в результате подстановки либо из некоторой тождественно истинной формулы . исчисления высказываний, либо из некоторой собственной аксиомы ') Из зтнх формул равенства соответстеуюшне формулы длз символов суммы н произведения выводятся, как мы знаем, нз рекурсивных равенств длк суммы к произведения н формул (3,), (1) н а=Ь- а'=Ь' (см т. 1 с. 461).
Тем не менее отсюда не следует, что этн формулы равенства являются нзлншними в качестве всходных формул, так как после замены схемы вндукцнн, формулами а чь О -е 6 (а)' а н А (а) -ь е»А (х)чь а мы имеем в своем распоряжении схему индукции только в качестве пронзводного правиле н всякий рзз вывод этой схемы требует нспольаованнз аксиомы равенства (3з). 4 з1 -символ и оонмллизлция пнинципд индукции 123 этого формализма, либо из одной из формул А(а) — »А (е А(х)), А (и) -ь В„А (х) ~ и', или же является формулой е-равенства. Формулы вида Я (() -+ Я (е Я (у)) Я(1)-эе Я(ь) ~Г, получающиеся в результате подстановки из двух только что упомянутых формул, мы будем называть кр ити ческ ими формулами первого и соответственно второго рода, связанными с В-термом а Я(й).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
