Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 26
Текст из файла (страница 26)
Собственные аксиомы формализма (в том числе и специальные аксиомы равенства), а также тождественно истинные формулы исчисления высказываний обладают тем свойством, что любые получающиеся из них в результате подстановки формулы без переменных при естественном распределении истинностных значений являются истинными формулами. Отсюда привычным рассуждением мы получаем, что заключительная формула любого нормированного доказательства, если в ией не встречаются е-символы, при естественном распределении истинностных значений тоже является истинной формулой.
Рассматриваемый нами подход нацелен на получение возможности преобразовывать любое нормированное доказательство формулы без переменных в такое нормированное доказательство той же самой формулы, которое уже не содержит В-символов. Однако для нашей цели вовсе не обязательно производить исключение е-символов так, чтобы получающееся при этом доказательство снова было нормированным; было бы вполне достаточно, если бы все встречающиеся в этом доказательстве е-термы мы смогли так заменить цифрами, чтобы каждая исходная формула стала при этом истинной (при естественном распределении истинностных значений).
Действительно, такие замены сохранили бы все схемы заключения и потому в итоге у нас получилась бы некоторая последовательность формул, каждая формула которой (а значит, и заключительная) являлась бы истинной. Если мы теперь заметим, что все исходные формулы, получающиеся в результате подстановки из какой-либо собственной аксиомы или из тождественно истинной формулы исчисления высказываний, при любой замене е-термов цифрами переходят в истинные формулы, то станет ясно, что задача искомого нами доказательства сводится к тому, чтобы для е-термов, фигурирую- 124 исследование кинематики пни помощи «-символа [гл.
и щих в данном нормированном доказательстве, найти такие замены" их цифрами, при которых все критические формулы первого и второго рода, равно как и формулы е-равенства, перейдут в истинные формулы. Учитывая это, Гильберт в первую очередь взялся за задачу исключения е-символов') задолго до того, как он придумал веду- -' щий к е-теореме общий метод устранения е-символов. Рассмотрев сначала простые случаи нормированных доказательств, он указал метод, позволяющий находить для встречающихся в этих доказа-, тельствах е-термов цифровые замены, обладающие нужными свой- ствами.
Этот метод в общих чертах дает подход к исключению е-тер- мов, и поначалу казалось, что этим методом удастся без принци- . пиальных затруднений доказать непротиворечивость не только арифметического формализма, но даже и формализма анализа. Однако, когда были предприняты попытки решить эту задачу, неожиданно обнаружились значительные трудности, так что ' наиболее продвинутые реализации упомянутого гильбертовского': подхода, восходящие к В. Аккерману и Дж. фон Нейману, по ' их результатам лишь несущественным образом превзошли нп-тео-" рему, которая достаточно просто получается с помощью е-теоремы., Тем не менее имеет смысл рассмотреть этот подход более под-. робно, так как получаемый при этом подходе метод оказывается, важным для целого ряда применений и так как пока еще остается, открытым вопрос о возможности дальнейшего развития этого подхода, 9 4.
Первоначальный гильбертовский подход к проблеме исключения а-символов и его дальнейшее развитие') а) Простейшие частные случаи. Для того чтобы дать представление о гильбертовской процедуре замены, мы поначалу,, рассмотрим нормированные доказательства одного совсем простого ", типа. Именно, будем предполагать, что для любого из рассмат- '. риваемых нами нормированных доказательств может быть указан такой е-терм е 6(р), что все критические формулы первого рода, этого доказательства связаны с этим термом и что других а-тер-.
мов в этом доказательстве нет. х) См. т. 1, с. 419 — 423. Применение приведенной на с. 419 обобщенной:. схемы индукции может быть сведено к двум применениям обычной схемы ин-; дукции. ') Читатель, желающий познакомиться лишь с основыми идеями итого' гильбертов«ного подхода, может прочитать один только п. а) настоящего парах.', рафа, а затем перейти либо к п. д), либо прямо к гл, Ш. ппгвонлчхльный Гильпеитовскип подход 125 Мы будем также предполагать, что в рассматриваемом нами случае отсутствуют критические формулы второго рода и формулы в-равенства.
Речь будет идти о том, чтобы в рассматриваемом доказательстве е-терм е 6(р) заменить какой-нибудь цифрой так, чтобы все критические формулы этого доказательства после замены оказались истинными. Рассматриваемые критические формулы имеют внд 6(«)ч 6(ехЯ(Б)). При этом терм е 6(р) нв может входить в формулу 6(с), потому что в противном случае он был бы вложен в самого себя; но он может входить в 1. Сначала мы попробуем заменить терм в Я(й) цифрой О. В результате этой замены все критические формулы перейдут в формулы без переменных. Истинностное значение любой такой формулы вполне определяется нашим способом вычисления функциональных выражений, строящихся с помощью знаков +,, и б, на основе выделенного распределения истинностных значений для равенства, а также нашей трактовки связок исчисления высказываний как истинностных функций. Если в результате этой замены все критические формулы данного доказательства получат значение «истина», то поставленная цель уже будет достигнута.
В противном случае мы возьмем первую из тех критических формул, которые принимают значение «ложые После замены а-герма а«6(х) цифрой 0 эта формула будет иметь вид 6 ()) -ь Я (0), где ( — некоторый терм без переменных. Пусть теперь 1 — цифра, получающаяся в результате вычислении терма 1. Согласно нашему распределению истинностных значений для формул без переменных, 6(1) имеет то же самое значение, что и 6((); тем самым формула 6 (1) -ь-6 (0) принимает значение «ложьз. Но это означает, что 6(1) — истинная формула, а Я (0) — ложная. Теперь произведем новую замену, а именно, заменим терм ехй)(Р) цифРой 1.
Тогда каждаЯ из РассматРиваемых кРитических формул перейдет в формулу вида Я (1) -ь. Я (1), не содержащую переменных. Но эта формула всегда будет истин- пеРВОНАчАльныв ГилъвеРТОВСкия подхОд 126 исследовхние АРифметики пги помощи е-снмволА 1гл. и 127 ной, так как истинно ее заключение 6('). Итак, замена терма' аг6(Л) цифрой 1 дает желаемый результат. Таким образом, не позже чем через два шага мы получаем-' замену, в результате которой все критические формулы становятся истинными: либо желаемый эффект дает уже замена герма е 6(х) цифрой О (мы будем называть эту замену О-заменой),; либо с помощью О-замены мы найдем некоторый пример такой цифры 1, что формула 21(1) будет истинной и тогда замена терма е 21(г) этой цифрой (мы будем называть эту замену экз ем п ля рной) будет заменой с нужными свойствами.
Не представляет никакого труда модифицировать этот способ так, чтобы он вел нас к цели и в том случае, когда имеются также и критические формулы второго рода. Любая связанная с а-термом е Л (г) критическая формула второго рода имеет вид Л (1) ,Л (Х) чь 1', где терм 1 может содержать в себе и терм е 6(х). Прн О-замеие; такая формула всегда превратится в истинную.
Значит, если; в результате О-замены все критические формулы первого рода';, окажутся истинными, то поставленная нами цель уже будет до-; стигнута. В противном случае, как известно, для терма в 21(х). найдется экземплярная замена, т. е. замена такой цифрой 1, что; формула 6(1) является истинной. Но эта замена может и ие перевести все критические формулы второго рода в истинные. Действительно, при этой замене произвольная формула второго рода перейдет в формулу вида 6 (д) -+1~ в', которая имеет то же самое истинностное значение, что и формула 6 (г) -~ 1 чь г', где г — цифра, получающаяся в результате вычисления герма без'.,* переменных д. Эта формула может на самом деле оказаться ложной: например, в том случае, когда 1 совпадает с г', а фор- мула 6(г) является истинной. Но тогда г является цифрой, мень-: шей 1 и такой, что формула 6(г) является истинной.
Эту возможность мы теперь с самого начала исключим сле- дующим приемом. После того как будет найден соответствующий' пример 1, мы найдем истиииостиые значения формул 6(О), 6(О), Л(О"), ..., 6(1). Относительно первой из них мы уже знаем, что она является'. ложной, относительно последней, — что она является истинной. Пусть 6(ш) — первая формула в этой последовательности, являющаяся истинной. Тогда мы произведем еще одну замену, замещая терм а Л (х) цифрой а. В результате этой замены все критические формулы первого рода станут истинными, так как 6(а) являе; 'я истинной формулой.
Но и критические формулы второго рода тоже окажутся истинными, Действительно, если бы одна из наших критических формул второго рода перешла в ложную формулу, то, согласно замеченному выше, мы нашли бы некоторую цифру г, меньшую ~в, для которой формула 6(1) являлась бы истинной, что противоречило бы выбору ~п. Таким образом, в результате замены терма е,6(х) цифрой ш все критические формулы становятся истинными. Итак, мы приходим к следующей альтернативе: либо желаемый результат нам дает уже сама О-замена, либо мы оказываемся в состоянии построить пример некоторой отличной от нули цифры 1 такой, что формула 6(:,) является истинной (экземплярная замена).
Если мы затем среди тех цифр п из ряда от О до 1, для которых 6 (и) является истинной формулой, возьмем наименьшую и обозначим ее буквой ш, то замена терма е 6 (Л) цифрой ш переведет все критические формулы рассматриваемого доказательства в истинные. Эту замену мы для краткости будем называть минимальной. Тем самым для рассматриваемого частного типа нормированных доказательств найден искомый способ исключения е-термов.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
