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

Тогда формулу 6а можно будет получить из 6м а эту последнюю — из 6 в результате ряда подстановок. Таким образом, по выводу формулы чг. в формализме г" мы получим некоторый вывод формулы 6з. Новая заключительная формула 6з уже не будет содержать свободных переменных. Поэтому, если первая е-теорема будет верна для случая, когда в заключительной формуле вывода нет свободных переменных, то по данному выводу формулы Жв мы получим такой ее вывод, который будет осуществляться средстЬами одного только элементарного исчисления со свободными переменными.

Тогда, не нарушая структуры этого вывода, мы можем заменить в нем вновь введенные инднвндные и преднкатные символы, для которых никаких специальных аксиом не формулировалось, подходящими свободными индивидными и формульными переменнымн; в результате этого мы получим вывод средствами элементарного исчисления со свободными переменными некоторой формулы К„из которой в результате некоторых подстановок может быть получена формула 6». Но от 6, мы можем перейти к (В средствами исчисления высказываний. Тем самым связанные переменные можно будет исключить и нз вывода формулы 6.

Поэтому для доказательства первой е-теоремы достаточно рассмотреть случай, когда заключительная формула вывода аг. не содержит свободных переменных. Это предположение относительно (О и будет лежать в основе наших дальнейших рассуждений. Второй шаг нашей подготовки будет состоять в исключении кванторов всеобщности и существования. Как было показано а) если Ь (6) — рзссмзтривземзя в данном случае формула, в Ь(зь' (а))— формула, получающаяся из иее в результате указанной подстановки, то, с едкой стороны, 1(йй(а)) получается в результате иодствиовки из в(8); в с другой стороны, мы можем из Ь(ВВ(»)) сиичвлв получить подстановкой формулу Ь ( ) йй (а)), и затем с помощью формулы (6 И (а)) 1/($ 1 л1 (а)), которая получается подстановкой из тождественной формулы (л — и) Ч(4 ) 8) получить формулу 3 (ж) п едыдущем параграфе, с помощью е-формулы и явных опред " ( ) ( ) м жно устранить применения основных формул 1 а и (Ь) и схем (и) и (()) исчисления предикатов ).

Итак, пусть нам дан вывод формулы ~~, не использующий фо ( ) и (Ь) а также схем (а) и ()»). В этом выводе каждое выражение»1(эй((э) мы заменим выражением (е,1 ( )), Ь( 3( о а каждое выражение Зой(э) выражением а(е»Ь((о)). Эти подстановки переведут (е ) и (и ) в формулы, получаемые подстановкой из формулы А А. В результате кванторы исключатся полность так что в альнеишем д " связанныв переменные будут встречаться дт исклгочительно в связи с яэи с е-символом, а в доказательстве бу ут ия употребляться толь ко повторения, подстановки, переименован я связанных переменных и схема заклк»пенять К преобразованному таким образом выводу мы теперь примеопе анни разложения доказательства на нити и возвратного ним оп р переноса подстановок в исходные форму еще оставшиеся свободные переменные, заменив все индивидные переменные одним и т м те. же (произвольно взятым) индивидным символом, все и ори ф , ульные переменные с одинаковым числом аргументов одним и тем же преднкатным символом с тем же ез самым числом аргу: ментов, а все формульные переменные бе аргумент ов одной и той же формулой без переменных.

В реобразования, производимые над рассма р т иваемым се эти и ы Е, так как выводом, не затрагивают заключительной формуль она по условию не содержит ни кванторов„ни свободных переменных и остается неизменной при разложении вывода и переносе подстановок. ыво .„омлы 6 Таким образом мы получаем некоторый вывод орму (термин <вывод» упот„е отребляется здесь в несколько обобщенном смысле слова' з)) со следующими свойствами: асс встречающиеся в этом выводе гор. у фо м лы построены из индивидных символов, предикатных символов, функциональных символов, е-символа (с соответствующими связанными переменными ми, и символов исчисления высказываний. Каждая исходная формул р д а п е ставляет соб б фо м л, получающуюся в результате подстановки из ой ли о ч ормулу, п лы исчисления выскакакой-либо тождественно истинной 'формулы исчи зываний, либо одну из аксиом '11„ ..., ч)1, либо формулу, получающуюся из одной из этих аксиом в результа ьтате подстановки, либо формулу, получающуюся а результате подстановки из е-формулы.

Взаимосвязь формул доказательства при этом основывается лишь на повторениях формул, переименованиях связанных переменных и схемах заключения. .акого род д, ') См. с. 33. а) См. г. 1, гл. Е!, с. 275 — 280 или !1риложеиие !> с, 475 и далее, ») См. т. 1, с. 283. 40 исключение связдыных переменных (гл. ! дающий указанными свойствами, мы будем называть н о р м и р о ° ванным доказательством. Если в полученном нами нормированном доказагельстве формулы ьк не будет исходных формул, получающихся (в результате подстановки) из е-формулы, то мы сможем обойтись в нем совершенно без использования е-символов.

Действительно, структура нашего нормированного доказательства полностью сохранится, если мы заменим в нем каждый в-терм переменной а, причем, очевидным образом, подстановки достаточно будет производить вместо тех е-термов, которые не являются составными частями каких-либо других е-термов. В результате такой замены мы ПОЛУЧИМ НЕКОтарЫй ВЫВОД фОрМуЛЫ Ь. ИЗ аКСИОМ ))ы ..., $1, который осуществляется средствами одного только элементарного исчисления со свободными переменными; при этом мы получим вывод и в первоначальном смысле этого слова, так как для каждой исходной формулы, получающейся в результате подстановки из тождественной формулы исчисления высказываний или из одной из аксиом '7,, ..., '$1, мы можем дополнительно дописать ее вывод из соотвехствующей формулы. Итак, утверждение первой е-теоремы в отмеченном выше случае доказано, и, следовательно, нам достаточно показать, что из любого нормированного доказательства произвольной формулы чв могут быть устранены те исходные формулы, которые получаются в результате подстановки в е-формулу.

Мы будем называть такие исходные формулы к р и т и ч е с к и м и формулами, причем формулу " (() "(ее Я (в)) мы будем называть критической формулой, связан ной с атермом в„Я(»). (При этом е-терм, с которым связана данная критическая формула, мы будем указывать лишь с точностью до обозначения входящих в него связанных переменных.) б) Гнльбертовский подход. Теперь доказательство первой е-теоремы свелось к тому, чтобы показать, что из любого нормированного доказательства могут быть устранены все критические формулы.

Метод, которым мы проведем это устранение, восходит к Гильберту. Для изложения этого метода мы сначала рассмотрим частный случай, когда все критические формулы доказательства связаны с одним и тем же е-термом. Пусть эти формулы имеют вид ') 6 ((,) — Я (Е,Л (е)), Ф) Я ((„) -+. 6 (е 6 (е)), х) Здесь явно используется тот факт, что ие может быть двух таких рзздичяых формул Й (с) и Я (с), для которых е я (г) и е Я(х) были бы одипвиа'г' - х ДОКХЗХтрЛЬГТВО ПРРЕОИ етРОР М е ы 41 ч! (е означают не которые термы, которые также могут -си.. Н е ра исключения будет основы- соде(ю!сати е-си. -символы, аша процеду а е 91 ) всюду, где он встречается я на том, что если терм е .

р те подстановки из какой-ли о замены п ° у' ол чалась в результате п д " ф числения высказываний или из з о м л 7„..., $П будет получаться из той же формулы но истинной ормулы исчи осле указанной замены ьтате некоторой подстановки и п я ь чо м л вывода также сохранится. При этом взаимосвязь ормул в . 3 есь следует еще раз под Замечание.,д черкнуть что термы, обо начениями связанных отличающиеся дру г от д уга лишь з .

В частности, это должно е еменных, х, мы считаем одинаковыми. ч п и выполнении указанных заме . н. этого вместо критических формул (К) появятся формулы вида 6х-э 6((х), й)„ - Я ((х). лы Л((,) пРи помощи тождественно Все они выводятся из орм истинной формулы А-ь В- о м л 6((х) к числу исходных форПоэтому, если мы добавим формулу екото ый вывод формулы, в кот б ф риро ать в нем ф Т т ст анены, т. е. удут игу не качсстве исходи ых, а в качестве выведенн о., нас получается некоторый вывод рм Ь (( ! ствами элементарного исчисления со свободными переменными.

т никаких свободных переить вывод м лы этому выводу можно построить выв д 6 ((д) -ь (Е, 6 1 более не используется в качестве исходной форс е ств элементарного исчисления мулы, и, следовательно, кроме средств э была исключена нашим соглашением выми е-термами. Теиви возможность ылв и связанными иеремеииыми.

ше"ии иоддязви и~~ау В м. т. 1, с. !9З вЂ” 199. Приведенное твм доквз сдедуюшее виже Рассматриваемого нами формализма, В р замечание, К ю гение сеязАННЫХ перрменнь и'л. г со свободными переменными, в ием использ т ием иаюльзуются ~~л~ко аксиомы б . *, что применение де " е ается осо енно элемента ным, так ается р ., ак как в рассматриваемом разу не встречаются ни схемы (сс) и (р), новки; таким образом, он опи ветс исчисление высказываний.

р тся исключительно на Совершенно аналогично том мулы му, как мы пришли к выводу фор- 6(1,)-«Ж, мы получим также выводы формул 6(1е) -«6, 6(1„)-«~; для этих выводов тоже потреб е уются лишь аксиомы ЧТ ... 7 влементарное исчисление со свобо н е со сво одными переменными. Формулы Л (1,) -»- ~, ®1 (1п) взятые совместно, с помощью ночи формулу щью исчисления высказываний дают нам 6(1) Ч...чй((1„) а С другой стороны мы можем сле ю формулы ЛЕДУЮЩИМ Обраэом ПОЛУЧИть вьшод ) 11 (1,) й...

а -) 6(1„) Б удем снова исходить из но мн ован ормнрованного доказательства формульг фр ул сг у фрмулы выводима из формулы их ормул с помо ью щью исчисления высказываний ~ 6 (1г) "'г ' г ) )1 (1п) так как формула 6 (1 ) -« Л (е,6 (Л)) для г=1, ..., и — выводима из ) Л(1 ) с исполь венно истинн " ф ой формулы ( г) льзованием тождест- ) А-«(А-«В). Следовательно, если в нормированном до Сле, р ванном доказательстве формулы 6 из ""рмул (Й) мы вставим ее вывод из фо д из формулы ) 6 (1,) а ...