Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 67
Текст из файла (страница 67)
Именно, из второй аксиомы равенства (1,) и из формулы ( -,) мы получаем формулы а <Ь-+ а чад, а(6-» Ь~а (это унсе было неоднократно использовано в предшествующих выводах); из них и из формул а ф 6-» а < Ь )/ Ь <а, а < 6-» а' <Ь' О=а')/0(а в сочетании с (Ю,), ((,) н ((,) дает формулу 0 (а', которая вместе с а<6 — » Ь~а позволяет нам получить формулу а'чь0 е 4! 321 НАЧАЛА АРИФМЕТИКИ Затем формула а < Ь» а' < Ь' а <Ь А Ь <Ь'- а' <Ь'.
а ( Ь-» -1(Ъ (а'). и формулы может быть выведена из (() и из формулы а (сйс -Ь-» а' (Ь, которые в результате подстановки дают формулы Ь (Ь' Формулу (е,) мы также можем вывести из формул ((,) и а чь Ь-» а ( Ь )/ Ь (а. Таким образом, из списка наших аксиом мы можем вычеркнуть четыре формулы, так что в нем останутся только следующие формулы: (у,), ((), (() ( =) а ~ Ь-» а (Ь )/ Ъ -а, 0 =а ~/0(а, 0' ( а -» 3 х (х' = а), а (с бс с < Ь-» а' (Ь. Зту систему формул можно подвергнуть дальнейшим упрощениям.
Именно, формула О=а~/0<а с учетом выводимых из (1е), (<,) и ((,) формул а = Ь-» 1 (Ь (а), а (Ь-» 1 (Ь (а) а Ф Ь-» а < Ь )/ Ь <а дедуктивно равна более простой формуле 1 (а (0). Кроме того, рассмотрим формулу а <сйс <Ь- а' <Ь. Из нее подстановками можно получить формулу а <Ь й Ъ (а' — » а' < а', пеРеход к ОднОЙ системе Аксиом а отсюда с испольаованием формулы 1 (а <а) получается формула а (Ь вЂ” » 1 (Ь (а'). И обратно, из последней формулы можно получить формулу а (с Ь с ( Ь-» а' ( Ь. В самом деле, формула а < Ь-» -~ (Ь < а') в сочетании с выводимой иа а ~ Ь»- а -Ь ~/ Ь (а формулой -1 (Ь (а') — » а' = Ь )/ а' (Ь дает а < Ь-+ а' = Ь~/а' < Ь.
Подставив в нее с вместо Ь и используя формулы (1е) и ((,), мы получим формулу а <с х с < Ь-» а' < Ь. Таким образом, зта формула может быть заменена болев простой формулой Далее, формула 0' <а-1- Зх (х' = а) с помощью остальных наших формул переводима в а ~ 0-» Зх (х' = а).
В самом деле, формула 0'(а- Лх (х' = а) переводима в формулу 0'= а )/ 0' (а-» Лх (х' = а). Таким образом, нам достаточно будет установить, что формула 0' = а ~/ 0' < а переводима в формулу а~О, 21 д. Раеьаерт, и. ВРРаеае ~гл. Рз пезеход к однбн системе Акспом НАЧАЛА АРИФМЕТИКИ 333 т. е. что выводимы две импликации: 0' = а ~/ 0' <а-ь а ~ 0 и а ч6 0-+ 0' = а ~/ 0' < а. В самом деле, первая из этих двух формул получается с использованием формул (Х,), 0' чь 0 и -1(а < 0) а вторая — с использованием формул а ~ Ь -ь. а Ы/ Ь < а, 1(а< 0), а < Ь -+ аз = Ь \/ а' < Ь.
Наконец, формула (<,) может быть выведена из формул («) и а <Ь- -1(Ь <а'). Действительно, из последней формулы подстановкой и контрапо- зи ней получается ц а < а'-~- -1 (а < а). Таким образом, мы пришли к следующей системе аксиом, состоящей из семи формул: а = Ь -ь (А (а) -~.
А (Ь)), а<ЬЙЬ<с-+ а<с, ачьЬ вЂ” ъ.а<Ь ~/ Ь .а, а<а', а<Ь- 1(Ь<а'), -1(а < 0), а ~ 0 — ю- Зх (х' = а) . (А) г) Сы. с. 340 — 347. Позже ') мы покажем, что зти аксиомы независимы друг от друга, 4. Полнота системы (А). Проведенное нами рассмотрение показывает, что если за основу взять приведенную адесь систему (А) то всякая формула, не содержащая формульных пере- аксиом ( , то и. Всле ствие менных, будет дедуктивно равна своеи редукции.
сл д этого всякая верифицируемая формула будет выводима. Мы олжны убедиться еще и в том, что для предложенной нами новой системы аксиом остается в силе теорема о верифиц ру ыд фи и емости всякой выводимой формулы, не содержащей формульных пере- манных. Для этого, как уже упоминалось, достаточно показать, что все вновь присоединенные аксиомы являются верифицируе- мыми. Верифицируемость формул а Ф Ь-~- а -Ь ~/ Ь <а, а < Ь-~- -1 (Ь < а'), -~ (а < 0) усматривается немедленно, а для формулы а ~ь 0-+. Зх (х = а) она получается из того, что редукцией этой формулы является формула а чь 0-~ О = а ~/ 0'< а. Таким образом, мы убеждаемся, что если взять за основу рассмотренную нами систему аксиом (А), то совокупность выводимых формул, пе содержащих формульпых перемепыых, будет совпадать с совокупностью верифицируемых формул.
Подведем итоги. Прежде всего, нами получена следующая Т е о р е м а о п о л н о т е: Длякаждой формулы Я, построенной ив имеющихся в нашем распоряжении символов и не содержащей формульяых и свободных ипдивидпых пере,иенпых, имеет место альтернатива, заключающаяся в том, что с помощью исчисления предикатов из наших аксиом (А) выводима либо Я, либо -1 Я, причем мы всегда можем решить вопрос о том, какой именно из зтих двух случаев имеет место.
В самом деле, редукция 3( такой формулы Я является нумерической формулой и поэтому она либо истинна, либо ложна. Тем самым одна из формул Я и ~Я верифицируема. Формулу Я мы находим по заданной формуле Я с помощью имеющейся у нас процедуры редукции. Та из формул 9( и 1 зс, которая является истинной, является также и выводимой. Далее, каждому шагу выполнения процедуры редукции соответствует определенная переводимость с помощью аксиом системы (А), и зто нам дает вывод формулы Я из формулы 9( илн соответственно формулы ~ Я из формулы ~ К.
Приведем еще одно С л е д с т в и е: Если для каждой цифры 3 оказывается выводимой формула Я(3), не содержащая формульпых переменных, то выводимой будет также формула Я(а), а вместе с пей и 1зхЯ (х). В самом деле, пусть 3( (а) — редукция Я (а); тогда для каждой цифры 33( (3) является редукцией Я(3).
Так как формула Я(3) по предположению выводима, то она верифнцируема. Значит, И (3) при каждой замене встречающихся в ней свободных индивидных переменных цифрами переходит в истинную формулу. Так как зто имеет место для любой цифры Ь, то формула зг (а), а потому ггл.
уг НАЧАЛА АРИФМЕТИКИ 324 5 Ы ВКЛ10ЧЕНИЕ ПОЛНОЙ ИНДУКЦИИ 325 Я(5» уг 35 35) т, е. 0=05/а' =0 а =0~/а =а-+ а =0 5/а' = а', г) См. гть П, с. 49. и Я (а), верифицируема; следовательно, формула Я (а) является также и выводимой. Поскольку выводимость формулы совпадает с ее верифицируемостью иэ указанного следствия получается, что формула 7хЯ(х), не содержащая формульных переменных, верифицируема тогд 1 а и только тогда, когда формула Я(5) верифицируема для любой цифры Аналогичный факт, касающийся формул ЗхЯ (х), если ограничиться формулами без свободных переменных, представляет собой частный случай теоремы о частичной редукции.
Он состоит в том, что всякая формула ЗхЯ (х), не содержащая формульыых и свободных индивидных переменных, верифицируема тогда и только тогда, когда для некоторой конкретной цифры 5 верифицируема формула Я (5), причем в случае верифицируемости ЗхЯ(х) такая цифра 5 находится с помощью процесса редукции этой формулы. Если мы теперь объединим оба эти факта, касающиеся формул 'УхЯ(х) и ЗхЯ(х), и примем во внимание совпадение выводимости с верифицируемостью, то получим теорему о том, что для формул, не содержащих свободных переменных и записанных в предваренной нормальной форме, выводимость совпадает с содержательной фипитной интерпретируемостью, так что, например, формула 7хЗу'эгЗКЯ (х, у, г, и), у которой Я (х, у, з, и) не содержит никаких переменных, кроме х, у, з и и, выводима тогда и только тогда, когда для каждой данной цифРы уг мы можем Указать такУю цифРУ У„что длЯ каждой цифры уэ можно указать цифру гю для которой нумерическая формула будет истинной.
В таком положении вещей находит отчетливое выражение то обстоятельство, что в области, определяемой посредством аксиом :(А) имеет место полная согласованность между формализмом )1 ьт содернвательной точкой зрения. э б. Включение полной индукции $. Формализация принципа полной индукции с помощью формулы и с помощью схемы; равносильность обеих формализаций; пывариантность запаса выводимых формул без формульиых переменных относительно добавлеиыя к системе схемы индукции. Замечательным следствием получеыных результатов является также тот факт, что если рассматривать лишь формулы беэ фор- мульных переменных, то присоединение принципа полной индукции не может расширить совокупности выводимых формул.
С принципом полной индукции как вспомогательным средством для проведения рассуждений мы познакомились уже при рассмотреыии финитной арифметики '). Если согласовать его с нашим новым понятием цифры, то он будет выражать тот факт, что любое высказывание финитного характера, выполняющееся для 0 и такое, что если оно вы~олыяется для какой-нибудь цифры к, то будет выполняться и для и', выполняется для любой цифры. Вместо этого разумного принципа, основывающегося ыа наглядном по своему характеру построении цифр, при аксиоматическом изложении арифметики появляется некая аксиома, которая выражается предложением, аналогичным предложению, выражающему этот принцип, ыо с той разницей, что в ыей речь идет ые о цифрах, а об элементах некоторой иыдизидяой области, и ке о фиыитцых высказываниях, а о высказываниях рассматриваемой нами теории..