Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 69
Текст из файла (страница 69)
Иэ этого результата мы можем, в частности, сделать вывод о непротиворечивости системы, которая получится, если к системе (А) присоединить аксиому или схему индукции. 2, Упрощение рассматриваемой системы аксиом в результате добавления аксиомы индукции; система (В). При рассмотрении атой системы мы замечаем, что формулы ~ (а<0) и а чь 0 -з- Зх (х' = а) являются в ней излишними. Действительно, в результате контрапоэиции и подстановки иэ формулы а < Ь -~- "1(Ь < а') мы получим формулу О < а' -в.
~ (а < 0). Таким образом, для того чтобы получить формулу 1 (а < 0), нам достаточно вывести формулу 0 < а'. Однако это легко может быть сделано с помощью схемы индукции, если воспользоваться формулами а < а' и а < Ь 8 Ь < с -+. а < с. В процессе этого вывода формула а чь 0 -~ Вх (х' = а) не использовалась. Поэтому для вывода этой формулы мы можем теперь воспользоваться формулой 1 (а <0), а значит, и 1 (О < 0). Иэ этой формулы в сочетании с аФЬ-+ а<Ь~ Ь<а мы прежде всего получим 0=0, а отсюда, с помощью исчисления высказываний, 0 Ф 0 -в Эх (х' = 0). Таким образом, если формулу а чь 0-в Лх (х' = а), доказательство которой мы хотим получить, обозначить для крат- кости посредством Я (а), то формула Я (0) оказывается уже полученной.
Поэтому, в соответствии со схемой индукции, для вывода Я (а) нам достаточно будет вывести формулу Й (а) -+ Я (а'), а для этого достаточно вывести формулу а' чь 0-~ Зх (х' = а'). Но эта формула получается средствами исчисления предикатов из формулы а=а, которая выводится иэ формул а<а', а < Ь -в- '1 (Ь < а'), а чь Ь -в- а < Ь ~/ Ь < а. Таким образом, в результате присоединения аксиомы индукции обе формулы 1(а < 0) и а ~ 0-» Лх(х' = а) оказываются ненужными. включкник полнои индукции 333 1г .сг НАчАлА АгиФмвтикн 332 Имеют место еще и следующие соотношения.
Как мы эв м, иэ формул а Ф Ь -ь а -' Ь 1/ Ь < а и а< Ь-ь 1(Ь<а') может быть выведена формула а<Ь вЂ” э-а'=Ь 1/а'<Ь. и о Обратно, иэ этой последней в сочетании с аксиомой равен " ра енства ( ) и формулами (<,), (< ) можно снова получить формулу а < Ь -+ 3 (Ь < а'). Но к роме того, теперь имеется воаможность воспользоваться аксиомой (или схемой) индукции и вывести формулу а ~ Ь -ь а < Ь ~/ Ь < а иэ формул (вв), (<,), (<в) и формул 0 = 0 и а < Ь -~- а' = Ь г/ а' < Ь. Действительно, сначала рассматриваемая формула элементарным образом может быть преобразована в формулу а = Ь ~/ а < Ь ~/ Ь < а.
Затем , чтобы с помощью схемы индукции вывести эту ф м кото мы б н рую о означим посредством Я (а), достаточно будет у формулу, вывести Я (0) и (д (а) -ь Я (а'). Формулу Я (0), т. е. О=Ь)/0<Ь~/ Ь<0, можно получить из формулы О=а ~/0<а, которая в свою очередь с помощью схемы индукции получается иэ формул 0=0, (с использованием уже упоминавшегося вывода формулы 0 < а'). Формула же Я (а) -~ Я (а') получается из формул ак Ь-~а'=Ь 1/а <Ъ, а = Ь -ь Ь < а, Ь < а -э- Ь < а', первая ив которых была взята нами в качестве исходной, а две другие могут быть получены иа формул а< а', а = Ь-ь(А (а)-эА (Ь)), а < Ь й Ь < с -г- а < с. Между прочим, все зти выводы производятся без использования связанных переменных. Основываясь на установленных соотношениях, мы сначала можем убрать из системы (А), расширенной путем присоединения аксиомы индукции, обе окааавшиеся ненужными формулы, а затем формулы ачс Ь-+ а<Ь ~/ Ь<а, а< Ь-ь-1 (Ь< а') можно будет заменить формулами 0=0, -1 (а<а), а < Ь -ь а' = Ь ~/ а' < Ь, которых, правда, по количеству больше, но они выражают все таки более слабые допущения, постольку поскольку переход от предыдущих двух формул к этим трем может быть непосредственно произведен с помощью формулы ( < в) путем подстановок и использования средств исчисления высказываний, в то время как при обратном переходе для вывода формулы а ф Ь -+.
а < Ь ~/ Ь < а кроме формул (Хв), (<,) и (<,) требуется по существу испольэовать аксиому или схему индукции. Теперь возникает вопрос о том, нельзя ли будет сэкономить еще на чем-нибудь, если снова вместо формулы 0 = 0'взять аксиому (гг). Тогда в качестве аксиом у нас окажутся формулы (<,), (< ), (<в), аксиомы равенства (гг) и (вв), формула а < Ь -ь а' = Ь г/ а' < Ь и аксиома индукции. Как это впервые установил Хазенъегер '), формулу, приведенную здесь в качестве предпоследней аксиомы, можно г) Н в в е а 1 в е 3 в г О.
Е1а Вснгвх ваг ОгбаааявгЬвсг1в.— АгсЬ. шагЬ. Ьо31Ь Спгаб!алеа1огвсЬаах, 1950, 1, ЬЬ 1, 3. 30 — 31. В первом пэданпп нашей книги вопрос о выводпмсств формулы а < Ь-~а' = Ь ~/ в' < Ь пв остальных сформулпрсвиннмх алесь аксиом был только поставлен, но нс бмл решен. игл чз % 61 нАчАлА Агиамнтики ВКЛЮЧЕНИЕ ПОЛНОИ ИНДУКЦИИ будет вывести из остальных аксиом.
Этот вывод может быть произведен следующим образом. Обозначим посредством Й (Ь) формулу )/х (х ( Ь -э х' = Ь ~/ х' ( Ь). Она дедуктивно равна той формуле, которую мы хотим получить. Й (0) получается иа формулы ~ (а( 0), которая с помощью схемы индукции выводится из формул ((т), ((з) и ((а). Поэтому для того, чтобы с помощью схемы индукции получить Й (Ь), достаточно будет вывести формулу Й (Ь) -~ Й (Ь') (а тем самым и Й (а) -А- Й (а )).
С этой целью мы сначала выведем, используя схему индукции, формулу - "Ь ~/ а < Ь), для краткости посредством Й (Ь) -ь- (а < Ь' — ~ а правую часть которой обозначим 6 (а, Ь). Формулу Й(Ь)-~6(0, Ь) мы получим из формулы О=Ь ~/0(Ь, выводимой с помощью схемы индукции иа формул 0 = 0 и 0 (а' (О (а' получается индукцией с помощью (< ) и ((а)). Что же касается формулы (Й(Ь) .6(а, Ь))-~-(Й(Ь)-+ 6(а', Ъ)), то она получается следующим образом.
С помощью (<з) и ((а) мы получаем а' <Ь'-ьа (Ь', с помощью (Х ) и ( -,)— а' (Ь'-1. а-ь Ь. Полученные две формулы друг с другом дают а' < Ь' Й (а < Ь' -+ а = Ь ~/ а < Ь) -~- а ( Ь, т. е, а' (Ь' А 6(а, Ь) -+ а ( Ь. Далее, с помощью исчисления предикатов непосредственно полу- чается Й (Ъ) -+ (а ( Ь -э. а' = Ь ~/ а' ( Ь). Полученные две формулы друг с другом дают Й (Ь) й 6 (а, Ь) й а' (Ь' -~ а' Ь ~/ а' (Ь, (в) а = Ь -~ (А (а) -~ А (Ь)), 1(а<а), а < Ь й Ь(с -~а(с, а<а', ~ А (0) й Ч х (А (х) -+. А (х')) — ~ А (а).
откуда с помощью исчисления высказываний получаем (Й (Ь)-~ 6 (а, Ь)) й Й (Ь)-~- (а' <Ь'-~- а' = Ь ~/ а' <Ь), а тем самым и (Й (Ь) -э- 6 (а, Ь)) — ~ (Й (Ъ) -ъ. 6 (а', Ь)). Итак, мы получили в наше распоряжение формулу Й (Ь) -+ 6 (а, Ь), т. е. Ш Й (Ь) -1- (а ( Ь' -1- а = Ь ~/ а ( Ь). С другой стороны, из уже использованной формулы Й (Ь) -+ (а <Ь-~- а'= Ь ~/ а'<Ь) с помощью (Х,), ((а) и ((,) мы получаем формулу [2) . Й(Ь) -+.
(а (Ь-+. а' <Ь'). Формулы (11 и (21 совместно с получающейся иа (ХА) и (ХА) формулой а = Ь -~ (а' = Ь ) с помощью исчисления высказываний дают формулу Й (Ь) -в (а ( Ъ' -з- а' = Ь' ~/ а' ( Ь') и далев (так как переменная а не входит в Й (Ь)) формулу й (Ь) -~ Чх (х ( Ь' -1- х' = Ь' ~/ х' ( Ь'), т. е. й (Ь) — ~ Й (Ь'). Далее, по схеме индукции получается формула Й (Ь), а вместе с тем и формула а < Ь -~- а' = Ь ~/ а' (Ь, выводимость которой требовалось доказать. Итак, система аксиом, получающаяся из системы (А) добавлением аксиомы индукции, равносильна следующей системе аксиома (гл, т< НАЧАЛА АРИ<РМКТИКИ ДОНАЗАТКЛЬСТВА ННЗАВИСИМОСТИ 6 6] 337 На эту систему аксиом без труда переносятся ранее доказанные нами общие теоремы ').
Таким образом, опять будет иметь место утверждение о том, что любая построенная на имеющихся в нашем распоряжении символов формула, не содеря<ащая формульных переменных, выводима из аксиом системы (В) тогда и только тогда, когда она верифицируема, и что вследствие этого для любой формулы, не содержащей никаких свободных переменных, имеет место выводимость либо самой атой формулы, либо ее отрицания. 5 6. Доказательства независимости 1.
Невыводимость аксиомы индукцик из формул системы (А). В приведенных выше утверждениях всегда речь идет о формулах. не содержащих формульных переменных. С точки зрения выводимости таких формул системы (А) и (В), как мы покааали, являются равносильными. Но эта равносильность немедленно перестает иметь место, как только мы допустим к рассмотрению формулы, в которых содержатся формульные переменные. В самом деле, уже аксиома индукции не выводима средствами системы (А). Для того чтобы доказать это, мы расширим систему (А), присоединив к ней прединатный символ Е (а), а также аксиомы г (О) е (а) -ь 2' (а ). Расширенную таким образом систему мы обозначим символом (А*). Если предположить, что в системе (А) выводима аксиома индукции, то в системе (А*) должна оказаться выводимой формула 2 (а), так как она получается из формул К (О) и г (а) — Я (а') по схеме индукции, а тем самым и с помощью аксиомы индукции, И тем не менее мы покажем, что формула Я (а) не может быть выведена средствами системы (А*).
Это может быть проделано с помощью уже применявшегося однажды метода видоизменении понятия верифицируемости посредствои обобщения понятий н у м е р и ч н о с т и, истинности, л о ж н о с т и и модификации процедуры редукции. Для расширения запаса цифр мы прежде всего введем символ <о и все фигуры, которые получаются иэ ю путем присоединения правого нижнего индекса в виде одной или нескольких звездочек, ь) См, с.
323. например, <йе, <й „. Для любого числа р символом <в мы будем обозначать фигуру, получающуюся из ю э результате присоединения р звездочек; <йе будет обозначать <в. В качестве ц и ф р в т о р о г о р о д а мы возьмем теперь фигуры юр, а также те фигуры <о„, которые получаются иэ них в результате однократного или многократного навешивания символа штриха. Н у м ер и ч е с к и м и мы назовем такие формулы, которые либо являются равенствами или неравенствами, составленными из цифр, либо являются формулами вида Я (а) с какой-либо цифрой а, либо оказываются построенными иэ формул этого рода с помощью связок исчисления высказываний.