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