Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 19

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 19)

Все они не содержат никаких переменных, кроме свободных индивидных, и могут быть выведены из аксиом (Ю,) и (Юа) без использования связанных переменных: формулы, относящиеся к предикатным символам, — непосредственной подстановкой из (За), а формулы, относящиеся к функциональным знакам, — с использованием аксиомы ()х). С нашим преобразованным таким образом доказательством ., формулы чт. мы теперь поступим следующим образом.

Над всякой встречающейся в нем исходной формулой а = 9-ь(й(а)-ьЙ(Ь)) мы надстроим вывод, который получается из вывода соответствующих формул а = Ь-ь (Я (а) -ь л (Ь)), подстановкой в его заключительную формулу термов и и Ь вместо переменных а и Ь; при этом вывод формулы и = Ь -ь (Л (а) -ь 6 (Ь)) производится с использованием формул (Зд), (!р) и формул вида а=Ь- еэч!(», а)=еэ6(», Ь), где всякий раз еэ6(», а) представляет собой некоторый основной тип. К этим достроенным выводам мы снова применим операции возвратного переноса подстановок в исходные формулы и исключения свободных переменных.

При этом на местй любой формулы а=Ь-ьеэлз(», а)=а,6(», Ь) с основным типом аь!В(», а), использованной в качестве исходной, окажется формула а = Ь -ь еэчзе (», а) = небе (», Ь), где еэчз' (», и) и набе (», Ь) суть термы с основным типом е„3 (», а), в которых место аргумента этого основного типа, которое в а„с)(», а) занято переменной а, заполнено термами а и о соответственно.

Полученная таким образом фигура может быть рассматриваема как вывод в рамках того формализма Ре, который получится из Р, если мы опустим аксиому (Юа), заменив ее формулами ((~), и включим в число исходных формул формулы вида а Ь- аэа) (», а) = еэ!В (», Ь), у которых термы а и Ь в термах е,к)(», а) и вэ6(», Ь) стоят на месте некоторого аргумента общего основного типа этих термов '). Конечно, получающийся здесь в ы в о д является выводом лишь в обобщенном смысла этого слова, так как в качестве исходных формул в нем фигурируют такие формулы, которые не являются непосредственно формулами формализма Р*, а только получаются из них в результате некоторых подстановок '). Итак, все аксиомы формализма Ре являются собственными аксиомами без связанных переменных и тем самым единственное отличие от ситуации, которая у нас имелась в гл.

1 при доказательстве первой а-теоремы, заключается в наличии исходных ') Заметим, что терм 9, входящий а состав какого-либо а-терна, не обязательно стоит на месте какого-нибудь аргумента основного типа этого а-герма! он может быть сосгаеной частью некоторого объемлющего его терка, находящегося внутри указанного е-терма. ') Аналогичная ситуация имела меч!о а гл.

!, с. 39. 92 исследования лгифмвтики пви помощи е-символа 1гл. и формул а = й -~ е„6 (», а) = е,6 (», 6), которые представляют собой, так сказать, критические формулы нового вида. Формулу этого вида, у которой заданные термы я; и 6 стоят в термах з,ч)(», в) и а„'сэ(», 1) на месте некоторого' аргумента общего основного типа этих термов (как это всегда,, имеет место у исходных формул этого вида), мы будем называть формулой е-равенства, связанной с е термами е6(», е) и в,ч)(», »).

Общий ранг обоих этих е-термов мы будем считать. рангом этой формулы е-равенства, а общий основной тип обоих этих е-термов мы будем называть основным типом этой формулы ' е-равенства (или же с в я з а н н ы м с нею основным типом, а точнее, основным типом, с которым связана данная формула: а-равенства).

Замечание. В нашем определении формулы е-равен- ства мы не требуем, чтобы рассматриваемые нами термы а и е обязательно были различными. Мы вполне могли бы наложить это ограничение, так как любая формула вида и = а -+ е,ч)(», а) = в„с» (», а) с использованием подстановки может быть выведена средствами исчисления высказываний и поэтому в качестве исходной фор- мулы оказывается излишней. Но чтобы избежать необязатель- ного разбора частных случаев, мы допустим и такие формулы в качестве формул е-равенства. Там, где будет важно их свое- образие, мы будем называть такие формулы вырожденными. Теперь допустим, что из какого-либо вывода рассматриваемого вида нам удалось устранить все формулы е-равенства и крити- ческие формулы, так что, как в проведенном в гл.

1 доказатель- стве нашей в-теоремы'), после замены остающихся термов пере- менной а получается вывод, совершенно не использукчиий свя- занные переменные, причем если заключительная формула 6 первоначального вывода является формулой без связанных пере- менных, то у нас снова получается вывод формулы 6, а если 6 имеет вид :-)й, ... --)й,а(г„..., й,), где Й(ьм ..., ус) не содержит других связанных переменных, отличных от х,..., гс, то получается вывод некоторой дизъюнкции а(1п,...,гп)Ч Ч'(1'Ю, .1!") Тогда для тех исходных формул, которые возникли в результате 4) См.

с. 47 и далее, включения аксиомы пя в пвэвтю е-тво»вмэ эз ея иодстанов овок из добавленных аксиом (1р), мы можем достроить их вывод воды из аксиом (),) и ()е) и таким образом прийти к выводу ассмат атриваемой нами заключительной формулы, укладывающемуся в я в рамки формализма г и протекающему без использования связанных переменных. Тем самым наше доказательство сводится к тому, чтобы процедуру устран нения критических формул надлежащим образом перестроить ли ов проц оцедуру совместного исключения критических форму ф рмул е равенства б) Совместное устранение критических формул и формул з.равеиства. Методика, с помощью которой гильбертовскую процедуру устранения е-символов удается распространить и на форе-равенства, была найдена и в основных своих чертах изложена В. Аккерманом в связи с предпринятой им реализ ц а ней гильбертовского подхода, при котором включение общей аксиомы равенства ()е) было запланировано заранее.

Применяя данную методику к какому-либо конкретному доказательству, из которого будут устраняться е-символы, мы будем пользоваться следующими его свойствами: 1. Каждая исходная формула рассматриваемого доказательства либо получается в результате подстановки из какой-либо тождественно истинной формулы исчисления высказываний или из собственной аксиомы, не содержащей кванторов, либо является критической формулой или формулой е-равенства.

2. В ием отсутствуют кванторы, и дедуктивная взаимосвязь составляющих его формул основывается исключительно на применении схемы заключения, на повторении уже имеющихся формул и на переименованиях связанных переменных. Доказательства такого рода мы будем называть нормированнымими доказательствами (на этот раз в обобщенном смысле'), так как в качестве исходных формул мы теперь допускаем и формулы е-равенства).

Далее, мы воспользуемся тем обстоятельством, что формализм Ре, в рамках которого осуществляется рассматриваемое нормированное доказательство, содержит аксиомы (),) и ((г). Как мы уже видели, с помощью этих аксиом, добавляя формулы е-равенства, можно вывести любую принадлежащую формализму Р* формулу вида а = 5 -з. (ч1 (я) -~ '" (»)) не содержащую формульных переменных. При этом соответствующие формулы з-равенства получаются з пезчльтате подстановки из формул вида а = 6 — е 6 (», а) = е„б (», Ь), ') См. с.

40. З4 исследование АРифметики пги помощи -символа ~гл 1 ВКЛЮЧЕНИЕ АКСИОМЫ (ан В ПЕРВУЮ а-теОРЕМУ где еа5 (», а) представляет собой основной тип некоторого е-терм встречающегося в формуле 'л(с); поэтому ранг любой из испол зуемых формул е-равенства равен рангу некоторого встреча щегося в 6(с) е-терма. Помимо указанных свойств исходного нормированного доказа тельства и рассматриваемого нами формализма мы еще должн четко представлять себе, что заключительная формула доказа-' тельства должна обладать определенными свойствами.

Нашу про' цедуру устранения мы будем строить с таким расчетом, чтоб она охватывала оба рассматриваемых случая е-теоремы: и случай, когда заключительная формула 6 не содержит связанных пере-; менных, и случай, когда заключительная формула имеет вид =)Г " =)Г,'Л(й "° 3„) и не содержит никаких связанных переменных, кроме у1, ..., ье, Любая формула такого вида при исключении из нее кванторов с помощью е-символа, как известно, переходит в формулу вида ( 1' ''~ с)з где а, „., а„-некоторые термы, вне которых ие содержится ни одного е-символа этой формулы, Поэтому наша задача, с одной: стороны, заключается в том, чтобы по любому нормированному доказательству с заключительной формулой 6, не содержащей: з-термов, построить какое-либо нормированное доказательство этой формулы, не содержащее ни критических формул, ни фор- мул е-равенства, а с другой стороны, в том, чтобы по любому нормированному доказательству с заключительной формулой 6 е вида 3((а1, ..., аа), где а,, ..., а„— некоторые термы, включающие в себя все е-термы этой формулы, построить какое-либо норми-, рованное доказательство, не содержащее ни критических формул, ии формул е-равенства, для некоторой формулы ~,Ч" Ч~Еа, где каждый из дизъюнктивных членов К( ((=1, ..., 6) имеет вид ,„(,.(),(О) (!) (() с какими-либо термами (, , ..., 1; .

Решение первой задачи содержится в ре1пении второй, поскольку мы допускаем, чтобы 1, т. е. число аргументов формулы е( (а1, ..., а,), равнялось нулю, В этом случае каждый член дизъюнкции должен совпадать с (х, а из дизъюнкциы ~Ч" Ч6 формула (х может быть получена по правилам исчисления высказываний. Поэтому первую задачу можно отдельно и не рассматривать.

Связь дизъюнкции 61~/ ...')/(Еа с формулой 6 заключается в том, что каждый из ее членов либо совпадает с (х, либо получается из ~~ в результате замены одного или нескольких входящих в й е-термов некоторыми другими термами (которые тоже могут— но не обязаны — быть е-термами). Переход от формулы 6 к такой дизъюнкции (х ~ ...

~ 64 мы в свое время назвали д и з ъ ю н к- 1 "' Е 1 тивным расщеплением этой формулы ). Как уже было отмечено ранее'), последовательное выполнение дпзъюнктивных расщеплений снова дает дизъюиктивное расщепление, так что если 61 получается в результате дизъюнктивного расщепления из 6, а 61 из 6„то 61 тоже получается в результате дизъюнктивного расщепления формулы (е. С учетом сказанного, совместное устранение из какого-либо нормированного доказательства и критических формул, и формул е-равенства может быть сведено к ряду отдельных шагов, на каждом из которых устраняется одна из этих формул. Прн этом поскольку каждый из этих шагов либо оставляет заключительную формулу без изменений, либо дизъюиктивно расщепляет ее, последовательное выполнение всех этих шагов тоже приведет самое ббльшее к дизъюнктивному расщеплению заключительной формулы.

Характеристики

Список файлов книги