Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 56
Текст из файла (страница 56)
Это может быть проделано следующим образом. Из формулы 'тх л(у Чг (А (х, у) & А (у, г) -». А (х, г)) мы по правилу (е') в) получим А (а, Ъ) & А (Ь, с)-«А (а, с), а отсюда по правилам исчисления высказываний получим А (Ь, с)-»- (А (а, Ь)-»- А (а, с)). Применив схему (а) и переименовав х в г, мы получим А (6, с) — »- Чг (А (г, Ь)-»- А (г, с)), ') См. с. 163. ') См. с. 175. а отсюда, используя тоя«дественную формулу (В-«С)-»- (В-»- В & С), получи»1 формулу А (6, с) — »- А (Ь, с) &»гг (А (г, Ь) — А (г, с)), которая по правилу (1) ') может быть преобразована в формулу А(6, с) — «)(г(А(!6 с) & (А (г, 6) — »-А(г, с))).
Теперь применение правила (с) в) даст нам формулу »Ух ЗуА(х, у) — «'эх Зу эг(А (х, у) & (21(е, х) — А (г, у))), которая вместе с формулой )гх ЗуА (х, у), имеющейся в наше»1 распоряжении в качестве исходной формулы, по схеме ааключения дает искомую формулу )(х Зуав(А(х, у) & (А(г, х) — «А (г. у))). 2. Привлечение аксиом равенства; дедекиндово определение бесконечности; введение штрих-символа. Доказательство непротивоРечивости системы фоРмУл ()те), а таккю системы (Е„), соответствующей формуле Ж, целесообразно провести так, чтобы в рассмотрение вошло и равенство с аксиомами ()1) и ()в) и чтобы указанная непротиворечивость была таким обрааом доказана не только для того случая, когда мы за основу берем исчисление предикатов, но и для расширенного исчисления, получающегося в результате присоединения аксиом равенства.
Благодаря атому мы наряду с характеристикой бесконечности индивидной области через выполнение одной из формул»т, М и 47 получим возможность рассматривать то определение бесконечности, которое в свое время было сформулировано Дедекиндом в). По Дедекинду, система каких-либо объектов — а мы говорим: индивидная область — называется бесконечной, если она допускает вааимно однозначное отображение на какую-либо собственную (т. е.
содержащую не все элементы атой системы) подспстему. Это условие в свою очередь равнозначно требованик» выполнимости определенной системы формул. Действительно, всякому отображению соответствует некоторый предикат с двумя аргументами: «Ь является образом а»; с другой стороны, для того чтобы предикат Р (а, Ь) соответствовал в атом смысле взаимно однозначному отображению индивндной области на своло собственную подобласть, ') См. е. 179. ') См. е..!76. в) 1) е 6 е 11 1 и д Г».
»Уев в)п6 ппй квв ведеп 6!е 2»11)еп? — ))гвппве!»ме)6, 1887. В ПЕРЕХОД ОТ ВОПРОСА О НЕВЫВОДИМОСТИ 266 НАЧАЛА АРИФМЕТИКИ игл, 7« необходимо и достаточно, чтобы оп удовлетворял условиям, опи- сываемым следующими четырьмя формулами: чхЗуР(х, у), Эх1Уу 1Р(у, х), Чх'зу чг(Р(х, у) АР(х, г) — «у=г), )(х зу зг (Р (х, г) А.
Р (у, г) «х = у). ('3) третья из формул (»6*), т. е формула Чх Чу7и Ю(Р(х, и) Ь Р (у, и) А. Р(е, х) — «Р(Р, у)), Первая из этих формул (3) утверждает, что для всякого элемента индивидной области имеется обраа, вторая — что по крайней мере один элемент не является образом, третья утверждает, что отображение однозначно, а четвертая — что однозначно обратное отображение. Таким образом, существование взаимно одноаначного отображения индивидной области на собственную подобласть равноаначно существованию некоторого предпката Р, удовлетворяющего четырем формулам (З).
Связывая эти четыре формулы знаком коныонкции, мы получим некоторую формулу 3. Выполнимость этой формулы и есть то, в чем, по Дедекинду, состоит бесконечность какой-либо индивидной области. Эта выполнимость может быть констатирована в финитном арифметическом смысле, если мы вместо Р (а, Ь) подставим отношение непосредственного следования (Ь непосредственно следует аа а).
Однако с точки зрения теории доназательств алесь, как и в случае формул Я и Ж, еще требуется показать, что отрицание ч2 формулы '3 не выводимо. Здесь открывается возможность некоторого упрощения, основывающаяся на том, что, докааав невыводимость формулы ~'3, мы заодно получим и невыводимость чй(. Это может быть установлено путем рассуждений, аналогичных тем, которые мы ранее лровели для формул 5 и р (только теперь всюду, где речь идет о выводимости, следует принимать во внимание и наличие аксиом равенства), если мы сможем утверждать, что из формул (3) беа того, чтобы затрагивать входящую в них формульную переменную, выводятся те формулы (6*), которые получаются иа формул («)) з реаультате аамены формульной переменной О' с двумя аргументами переменной Р с теми же самыми аргументами.
А это действительно так. При этом формулы (Ж*) оказываются выводимыми уже только из трех формул, входящих в состав (3). Именно, первые две формулы систем (Ж) и (И*) совпадают, а из четвертой формулы, входящей в (ю), т. е. из зх ту Мг(Р (х, г) А Р (у, г) — «х = у), может быть получена следующим образом. Сначала из чх~Уу Мг(Р(х, г) бс Р(у, г) — «х= у) по правилу (е') получаел«формулу Р (а, с) б: Р (Ь, е) — «а = Ь; затем из второй аксиомы равенства подстановкой получаем а = Ь-«(Р (д, а)-+. Р (О, Ь)). Полученные формулы по правилу силлогизма дают Р (а, с) д: Р (Ь, с)-«(Р (д, а)-«- Р (е), Ь)). Отсюда путем элементарных преобразований (применение правила соединения посылок и опускание ли|пних скобок) получается формула Р (а, е) б: Р (Ь, е) е«Р (д, а)«Р (е), Ь), а из нее применением правила (з) получается искомая формула Чх'Тузиков(Р(х, и)АР(у, и) АР(о, х) — «Р(Р, у)).
Тем самым, подобно формуле р, мы можем исключить из нашего рассмотрения формулу И, и тогда наша задача сведется к установлению невыводимости формул чЯ и 13, причем эту певыводимость нужно будет устанавливать по отношению к расшиРенному исчислению предикатов, т. е. по отношению к исчислению предпкатов с присоединением аксиом равенства. Это расширение теперь становится неизбежным, так как в формуле 3 фигурирует знак равенства. Точно так же, как для установления невыводнмости формулы 15 достаточно было показать непротиворечивость формул Я»), теперь для установления невызодимостн формулы 1 3 достаточно будет убедиться в непротиворечивости системы формул, которая получится нз формул (3), если формульную переменную Р (а; Ь) заменить каким-либо предикатным символом.
Однако здесь целесообразно проиавести еще одну модификацию, которая подсказывается содержательной арифметической моделью формул (З). Действительно, при этой интерпретации на место формульной переменной Р (а, Ь) будет стоять отношение «Ь непосредственно следует за а». Вместо того чтобы формализовать это отношение посредством какого-либо предикатного символа с двумя аргументами, мы можем при помощи функционального знака с одним аргументом формализовать ту математическую функцшо, которая любому числу а сопоставляет число, непосредственно следующее за ним.
С атой целью мы возьмем символ, который будем называть штрихом. В отличие от прочих функциональных знаков, которые обычно пишутся слева, штрих будет писаться справа вверху от 1гл, Р» НЛЧЛЛЛ АРИФМЕТИКИ '«х Зу (х' =- у), Лх Чд (у' ~= х), »«х 7у 'Уг (х' = у А х' = г — э. у = г), 'Ух «у '«г (х' = г А у' = г — э- х = у) .
а=-а Ь' = Ь' -» (а = Ъ -+. а = Ь), ') См. с. 146. ») См. с. 174. ') См. с. 214. аргумента. Используя знак равенства, мы теперь можем отношение «Ь непосредственно следует эа а» формализовать посредством равенства а' = Ь. Подставив это равенство вместо формульиой переменной Р (а, Ь) в формулы (Ж), мы получим следующие четыре формулы: Снова оказывается, что, установив непротиворечивость этих формул (в рамках расширенного исчисления предикатов), мы докажем н невыводимость (в расширенном исчислении предикатов) формулы )'Л. Упрощение, получающееся в результате прнменения этого приема, проявляется в том, что первая и третья формулы этой системы оказываются выводимыхш из аксиом равенства. Действительно, из формулы подстановкой получаем а =-= а; из нее, применив основную формулу (Ь) и схему заключения, получаем 3х (а' =- х), а отсюда, переименовав хв у и применив правило (у') '), получаем формулу эхЛу(х = у), т.
е. первую из формул (Ж«). Далее, из второй аксиомы равенства подстановкой получаем формулу а =- Ь вЂ” » (а' =- с-+. Ь = с); из нее по правилу соединения посылок получаем а' =- Ь А а' = с — » Ь = с, а отсюда по правилу (е) г) получаем третью иа формулы («)»' Чх7у)гг(х'= — у А х'=-г-»у=-г). пегеход от вопгосл о невыводимости 269 таким образом, нам нужно рассмотреть только вторую и четвер- тую иэ формул (ю«), так что в целом мы должны будем в рамках расширенного исчисления предикатов доказать непротиворечи- вость системы, состоящей только нз следующих пяти формул: 'ух 1(с<х), 'Ух 7у )(г (х у А- у < г -+.