Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 20
Текст из файла (страница 20)
В дальнейшем, когда будет говориться об устранении критических формул или об устранении формул е-равенства, всегда будет иметься в виду устранение такого типа, при котором заключительная формула рассматриваемого нормированного доказательства либо остается без изменений вообще, либо подвергается одному только дизъюнктивному расщеплению. Подобно нашей прежней процедуре устранения критических формул '), подготавливаемая процедура будет использовать следующие две вспомогательные операции: операцию импликативного добавления посылки и операцию замены е-термов. Операция импликативного добавления формулы ч) заключается в том, что сначала к каждой формуле рассматриваемого нормированного доказательства приписывается в качестве посылки формула З, и затем 1) над каждой формулой 6-~$, стоящей на месте первоначальной формулы 4), надстраивается (если сама эта формула не является допустимой исходной формулой) ее вывод ') бм.
с. 53. ') См. с. 37, 47 и далее. ВВ ИССЛЕДОВАНИЕ АрнфмвтИКИ ПРИ ПОМОЩИ е-СИМВОЛА 1ГЛ. и из формулы йй средствами исчисления высказываний и 2) вместо каждой последовательности формул 6 — Я 6-е.(Я-е ~) 6-е-Ж стоящей на месте какой-либо прежней схемы заключения, поме- щается (тоже осуществляемый средствами исчисления высказыва- ний) вывод третьей из этих формул из первых двух. Импликативное добавление какой-либо формулы 6, не содер- жащей ни формульных переменных„ни кванторов, переводит нормированное доказательство формулы Аг. в нормированное дока- зательство формулы 6 — е й'.. Операция замены какого-либо е-терма р термом 1 заключается .
в том, что В-терм г всюду, где он встречается в рассматриваемом нами нормированном доказательстве, заменяется термом 1. Ранеей) мы установили, что в результате замены какого-либо В-терма е новым термам критическая формула, не связанная с г, может подвергнуться изменениям лишь тогда, когда ее ранг или ее степень превосходит ранг или соответственно степень терма с; а критическая формула, не связанная с г, ранг которой не пре- восходит ранга герма г, в результате этой замены всегда пере- ходит в новую критическую формулу, ранг которой ранен рангу первоначальной формулы.
Теперь рассмотрим вопрос о том, какому изменению в резуль- ' тате замены е-терма р подвергается формула В-равенства а = Ь вЂ” В,6 (», а) = е,6 (»„ Ь), не связанная с термом й. Как известно, эта формула обладает тем свойством, что терм а ' в е-терме е,6(», а) и терм Ь в В-терме В„6(», Ь) стоят на месте некоторого аргумента общего основного типа этих е-термов; с дру- ' гой стороны, терм е, если он входит в эту формулу, может стоять только на месте одного или нескольких аргументов соответствую- щего основного типа или же в посылке а =Ь.
Поэтому данная формула е-равенства, если в результате этой замены она вообще ' подвергается каким-либо изменениям, переходит в некоторую формулу вида а'=Ь* — е,6,(», а*)=В„6,(», Ь*), где В„6,(», с) имеет тот же самый основной тип, что и В,6(», с).
Таким об м образом, получается, что при замене какого-либо ; е-терма е любая не связанная с этим В-термом формула В-равену а В-равен-;: й) См. с. 49 — 51, ВКЛЮЧЕНИЕ АКСИОМЫ Ые) В ПЕРВУЮ Е.ТЕОРЕМУ 97 йп ва, если она вообще подвергается каким-либо изменениям, снова переходит в формулу е-равенства, а ее основной тип — а тем самым и ранг — остается без изменений. Теперь, на основе всех этих замечаний относительно влияния замен иа критические формулы и на формулы е-равенства, мы произведем УстРанение этих фоРмУл по этапам, пУтем последовательного понижения наибольшего из рангов этих формул, подобно тому, как это делалось в прежнем доказательстве нашей е-теоремы.
Действительно, нам будет достаточно разработать метод, позволяющий исключать из нормированных доказательств те критические формулы и формулы е-равенства, которые имеют ранг, наибольший из числа встречающихся. Не будет большой беды, если при этом будут возникать новые критические формулы или формулы е-равенства, лишь бы только они имели более низкий ранг. В случае, когда в заданном нормированном доказательстве наибольший ранг пе имеют только критические формулы, а формул е-равенства с этим рангом нет, мы можем применить нашу прежнюю процедуру исключения критических формул.
Она состоит, как мы помним, в том, что шаг за шагом последовательно уменьшается количество е-термов ранга еп, связанных с какими-либо критическими формулами. Чтобы убедиться, что в рассматриваемой сейчас ситуации эта процедура тоже дает нужный результат, мы напомним, как при ее реализации производится текущий шаг устранения. Среди е-термов ранга щ, связанных в рассматриваемом нормированном доказательсте с какими-либо критическими формулами, мы берем какой-либо Один с максимальной степенью. Пусть связанные с этим термом критические формулы имеют вид 6(1й)-~ 6(е„6 (р)) 6(1„)- 6(В„6 (»)).
Мы строим и частичных доказательств, ге из которых (р = 1, ..., и) получается из рассматриваемого нормированного доказательства в результате замены терма В 6(») термом 1, и последующего импликативного добавления посылки 6 (1е). Эти частичные доказательства являются нормированными, потому что в результате замены герма В„6(») критические формулы, не связанные с этим е-термом, снова переходят в критические формулы, так как их ранг не превосходит а, а формулы В-равенства переходят опять в некоторые формулы е-равенства, так как они ие связаны с этим е термом 4 и.
Гнеьберп П. Береейе 98 ИГ ГЛЕДОВАНИЕ АРИФМЕТИКИ ПРИ ПОМОЩ И МСИМЕОЛА [ГЛ включения А9сиомы Рв в пегвею е.теогеме 99 $ я Затем из первоначальн ого нормированного доказательства пут импликативиого добавления формулы -) е (1,) а ... а ) 6 (1„) мы получаем еще одно, (и+ !)-е частичное доказательство. Если заключительной формулой исходного но ми ова доказательства была форм л 6 - (— у а, то г-е (г= 1, ..., и) частнчн доказательство будет оканчиваться фо й формуло ОЦ Е (1,) -ь.62, где Ю„получается из 6 в е 9) (е); а и результате указанной замены те рма тво удет иметь заклю( ); ( +!)-е частичное доказательство будет чительную формулу ) й) (12) й...
а -) Е (1„) Е Из этих и+1 заключительных формул, взятых вместе по п вилам исчисления высказываний " выводится формула месте, по пра-, ~2'Е' " Ч~ Ч~. Таким образом, первоначальна ф дизъюнктивному расщеплению. (П я ормула по ве г д р ается имеющиеся в полученной дизъю овторения членов возмож о и средствами исчисления высказываний.) В нкции, могут быть ст у ранены ных о д казательств на месте критических фо м сказываиий.) В каждом из этих частич- термом е,е2(9), б формул, связанных с е- (9), удут находиться формулы, получающиеся из тож- дественно истинных фо м л ночи ате некоторой подстановки.
Значит, эти критические фо м в больше не будут использоватьс ться в качестве исходных. П ав ие формулы результате произведенных замен мог т обав ранг, меньший щ. Действительно, и формулы е-равенства, но все они б т и удут иметь "ствительио, в результате замены те ма з л е-равенства, не свя- аиных с этим е-термом, повышения анга п а критические форм лы я ранга произойти не может, ормулы ранга ег, ие связанные с термом е 6 (В), если таковые имеются, в ез ь р зультате этих замен вообще не изме- няются, так как оии имеют степень епеиь, ие превосходящую степени Т аким образом, указанный и нем р действительно ведет к исклюязаиных с термом еьб(ь) критических формул, а коли- чество е.термов ранга еп к кото ым о к орым относятся какие-либо критиформулы, уменьшается иа е нни число раз, мы придем к исключению всех критиче- После этого нап!а задача сводится к тому, чтобы научиться устранять из любого нормированного доказательства, у которого наибольший ранг критических формул и формул е-равенства равен ~е, формулы е-равенства ранга е2.
При этом можно даже допустить, чтобы в процессе этого исключения добавлялись новые формулы е-равенства ранга„меньшего е2, и критические формулы ранга, не превосходящего еь Действительно, если будут исключены все формулы е-равенства ранга ег, то только что описанным способом мы сможем исключить и критические формулы ранга е2. Для устранения формул е-равенства ранга ег достаточно уменьшить число различных основных типов ранга е2 таких, что в рассматриваемом нормированном доказательстве имеются связанные с ними формулы е-равенства.
Допустим, что выбран один из этих основных типов, — например тот, с которым связана первая встречающаяся в данном нормированном доказательстве формула е-равенства ранга е2. Проблема заключается в том, чтобы устранить все связанные с этим основным типом — мы обозначим его буквой 1 — исходные формулы е-равенства. Это делается очень просто, если в рассматриваемом нормированном доказательстве среди е-термов с основным типом 1 нет ни одного такого терма, с которым были бы связаны одновременно хотя бы одна формула е-равенства и хотя бы одна критическая формула. В самом деле, если это условие будет выполнено и если мы заменим переменной и каждый из тех е-термов с основным типом 1, с которым в рассматриваемом нормированном доказательстве связаны какие-либо формулы е-равенства„ то каждая формула е-равенства, имеющая ранг ег, перейдет в формулу вида Ог-~-а=а, которая может быть выведена из формулы (),) средствами исчисления высказываний.
Вместо заключительной формулы (если она вообще подвергнется каким-нибудь изменениям) будет стоять формула, получающаяся из нее в результате произведенных замен. Формулы е-равенства, имеющие ранг, меньший ег, перейдут в новые формулы е-равенства без изменения ранга. Формулы е-равенства Ранга е2, не связанные с основным типом 1, опять перейдут в формулы этого рода, с сохранением их основного типа. А критические формулы, которые имеют ранг, не превосходящий е2, тоже останутся критическими формулами и сохранят свой ранг. Тем самым в результате указанных замен будут устранены все связанные с основным типом 1 формулы е-равенства. Этот прием оказывается неприменимым в том случае, когда с одним из тех е-термов основного типа 1, с которыми связаны какие-либо формулы е-равенства, связаны также и какие-нибудь критические формулы, потому что эти формулы прн замене рассматриваемого е-герма переменной а теряют свой характеристи.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
