Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 98
Текст из файла (страница 98)
Доказанная нами теорема о порядках -~ — это, так сказать, арифа метическая версия обобщенного принципа индукции для О-щ-фигур, Замечание 2. Вместо принципа индукции для О-щ-фигур нам хватило бы и теоремы о том, что всякая убывающая последовательность О-щ-фигур после конечного числа шагов обрывается (кончается нулем), Сравнительно простое доказательство этой теоремы приводится в Приложении т)!). А теперь, пользуясь принципом индукции для О-щ-фигур, можно, следуя Генцену, убедиться в непротиворечивости системы (Е). Для этого формализм (Х) сначала сводится к некоторому другому ').
Об этом формализме — назовем его (Вз) — мы здесь только скажем, что в нем всякое доказательство состоит из так называемых секвенций, т. е. обобщенных импликаций вида где И„..., Иг и Зт, "., За суть формулы, построенные из элементарных с помощью знаков конъюнкции, дизъюнкции и отрицания, а также кванторов всеобщности и существования, Число г антецедентов, равно как и число д сукцедентов секвенции может быть любым, в том числе оно может равняться и нулю '). ') См. с.
621 и далее. *) То, что для успеха доказательства зто сведение не существенна и что, более того, для формализма (2) или для формализма, получающегося из него путем исключения формульных переменных, соответствующее рассуждение получается даже несколько более простым, было показано Л. Кальмаром осенью 1938 г. в одной до сих пор не опубликованной работе »ОЬег Оеп!гепз Ветге)з №г 6!е »Н!бегзргисьз!ге!Ье!! бег ге»пеп хаЫеп!Ьеог!е», Вскоре после этого В.
Аккерману удалось а использованием индукции до первого е-числа довести рассмотренный в гл. 1! (с. 124 †1) метод, исходящий из первона. чального гильбертовского подхода и не ведущий финитными средствами к искомому результату, до доказательства непротиворечивости арифметического формализма. См. его работу: Ас й егго а пп»Н. Еиг ТН!бегзргисЬ»!ге!Ье!! бег ЕаЫеп1Ьеог!е.— Ма!Ь. Апп., 1940, 117, Б. 162 — 194.
Изложение этих доказательств Кальмара и Аккерманн будет дано в Приложении Н. ») Такие секвенции Генцеи использовал уже в работе; Оеп!геп С. Уп!егзисйипйеп 6Ьег баз !ой!»сье $сЫ!еаеп — Ма№. 2., !934, 39, № 2 — 3 (русский перевод см. в сб. »й!атематическая теория логического вывод໠— МлФизматгна, 1967, с. 9 †?4. †Пр. перев.). Секвенцин вида й!ы " ° яг впервые были введены Паулем Герцем в его исследованиях по системам предложений: Н е г1 г Р. ОЬег Ах!ощепзуз!егпе 1йг Ье)!еЬ»йе за1муыеще.— Ма!Ь.
Апп., !923, 89, № !г2 и 19гз, 101, № 4. Фигуры заключения Геицеиа примыкают к формализму систем предложений Герца. Секвенция яг " »»г ьВ» " й)а где г н е отличны ог нуля, при содер;нательном ее понимании, равнозначна импликацни а,й...йк,— е, Н „. Н иа, -«- 6», ..., ч»а Е» Н " Н Ве П», ..., яг-ь ) !В16 эпг) секвенция равнозначна формуле секвенция равнозначна формуле а <пустая секвеицня» -ь равнозначна ложной формуле. Из противоречивости системы (Е) следовала бы выводимость в формализме (Зг) пустой секвенцин, т.
е. секвенции без антецедента и сукцедеита. Поэтому для доказательства непротиворечивости системь! (Е) достаточно показать, что в (Зз) невыводима пустая секвеиция. Для этого некоторым элементарно-рекурсивным способом каждому выводу в (3,) приписывается определенная О-щ-фигура— порядковое число этого вывода. Затем показывается, как по каждому выводу пустой секвенции, в предположении, что таковой у нас имеется, с помощью некоторого редукционного шага можно получить другой вывод пустой секвенции, с меньшим порядковым числом, Отсюда вытекает, что если с — порядковое число и если для любого в, меньшего г, всякий вывод в (3,) с порядковым числом и (при условии, что таковые вообще бывают) оканчивается непустой секвенцией, то это должно быть верно и для с. Отсюда по принципу индукции для О-ю-фигур получается, что в (3») вообще не существует вывода пустой секвенции.
Замечание. Примененное в этом доказательстве косвенное рассуждение с точки зрения финитной установки не является проблематичным, так как допущение о существовании вывода в (3!) с порядковым числом и, оканчивающегося пустой секвенцией, обладает интуитивно ясной определенностью. — Впрочем, этою косвенного рассуждения здесь можно было бы и избежать. В самом деле, это генцеиогское доказательство можно, например, превратить в позитивное доказательство утверждения о том, что у любой выводимой в (3!) секвенции, у которой в антецеденте и сукценденте фигурируют только равенства между цифрами, имеется по крайней мере одна истинная (в смысле выделенной оценки ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ ПРИЛОЖЕНИЕ ! истинности равенства) формула в сукцеденте или по крайней мере одна ложная (в том же самом смысле) в антецеденте.
Метод этого кратко намеченного здесь доказательства позволяет вместе с тем получить и некоторые более сильные результаты. В частности, в связи с вопросом о внешней непротиворечивости ') мы упомянем результат о том, что рассмотренный формализм остается непротиворечивым, если к нему добавить какие-либо верифицируемые формулы ') в качестве исходных, а также если ввести какие-либо функциональные знаки для вычислимых функций или предикатные символы для разрешимых отношений между числами вместе с характеризующими их аксиомами, которые на основе неформального истолкования этих символов либо сами являются верифицируемыми формулами, либо выводятся из формул этого рода.
Геиценовский метод доказательства рассчитан не только на до сих пор осуществленное с его помощью доказательство непротиворечивости для арифметического формализма, но з значительной мере и на возможные применения к более широким формализмам, в частности к формализму анализа'). В самом деле, основная идея геиценовского доказательства связана не с тем, что в рассматриваемом формализме имеется какая-либо возможность исключать трансфинитные средства, а только с тем, что, с одной стороны, выводы данного формализма в известной мере могут быть вполне упорядочены по степени их сложности и что, с другой стороны, для таких выводов, заключительные формулы которых изображают нечто в элементарном смысле ложное, может быть определена редукция, в результате однократного применения которой к заданному выводу, так сказать, исключается некоторый шяг этого вывода н порядковое число вывода при этом уменьшается.
Разумеется,— и это является одним из последствий теоремы Геделя — чем шире рассматриваемый формализм, тем более высокими должны быть используемые в доказательствах порядковые типы, т. е. тем более сложными должны быть формы применяемого обобщенного принципа индукции, и методические требования к содержательному обоснованию этих принципов задают масштаб тех методических предпосылок, которые должны быть положены в основу нашей содержательной установки для того, чтобы мы могли доказать непротиворечивость рассматриваемого формализма.
1] См. о. 35!, ') См, и. бб. з) Формзлиззция инзлизи, иии и фирмзлнмзцяя иряфметини, можез быть осущестилеиз с помощью итличиющихся друг оз друге зниииилентных форме. лизмое; но здесь имеется знзчительно большее ииогообрззие возможностей.— Различные виды формзлнззции знзлизз обсуждвотся и ПриЛожении !Ч; см. с. 546 и далее. СВЕДЕНИЯ ОБ ИСЧИСЛЕНИИ ПРЕДИКАТОВ И ПРИМЫКАЮЩИХ К НЕМУ ФОРМАЛИЗМАХ й 1. Чистое исчисление предикатов Переменными у нас являются: свободные и связанные индивидные переменные, а также формульные переменные без аргументов и формульные переменные с одним или несколькими местами для аргументов. В качестве индивидиых переменных мы используем строчные, а в качестве формульиых — прописные буквы латинского алфавита. Свободные и связанные индивидные переменные мы рассматриваем как различные сорта переменных.
Для их различения мы используем одни буквы этого алфавита в качестве свободных переменнйх, а другие — в качестве связанных; так, в качестве свободных переменных мы, как правило, берем буквы а, Ь, с, й, 1, т, а, г и з, а в качестве связанных — х, у, г, и, о и ш. Замечание. Мы оставляем за собой право придерживаться этого разграничения по мере надобности; будет вполне достаточно, если мы всякий раз сможем соблюдать его внутри отдельных связных дедуктивных рассмотрений. Этой свободой мы уже поль. возились и отношении буквы 1, которая в гл.
П1 данного тома использовалась как связанная, а в гл, 1Ч как свободная переменная. Формульные переменные считаются различными, если оии либо различаются как буквы, либо имеют разное число аргументов. Символами являются: символы для связок исчисления высказываний (отрицание, конъюнкция, дизъюикция, импликация и эквивалентность) и к в а н т о р ы (всеобщности и существования).
Применяя отрицание, мы получаем из выражения 'Л выражение )Я; из выражений 6 и л) применением конъюнкции, дизьюнкции, имплнкации и эквивалентности МЫ получаем соответственно выражения В б1 6„ Я Ч 5, В Е, а Е. Каждый из кванторов всеобщности и существования имеет при себе по одной связанной переменной. Употребление этих кванторов в роли логических операций состоит в том, что, исходя из какого-либо выражения 6 (с), в котором встречается свободная 459 ПРИЛОЖЕНИЯ чистое исчисление предикдтов переменная с и не встречается связанная переменная т, мы строим выражения зУйЯ (й) и ЭрЯ (р). При этом 6(х) обозначает выражение, которое получается из 6(с) в результате повсеместной замены в этом последнем переменной с переменной х.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
