Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 133

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 133)

Но в точности так же, как мы за конечное число шагов доходим от в«.(т+!) до а' т, мы дойдем от а' т до а«(т — 1) и т. д., так что в целом спуск с а' (т+ 1) за конечное число шагов приведет нас к О. А теперь рассмотрим спуск, идущий от степени а". Первый шаг спуска ведет нас к фигуре вида а '+...+в ' (а,~...=» а,), где а ) а,. Самое большее эта фигура равна а'> с. Таким образом наш спуск разве лишь удлииится, если мы (в случае неравенства> вставим между в' и упомянутой фигурой еще и а' с, Следова тельно, вопрос о том, является ли а«фигурой конечного спуска.

сводится к аналогичному вопросу относительно фигуры а' ! и, ввиду проведенного нами вспомогательного рассуждения, к ана. логичному вопросу относительно вак Для а' повторяется то же самое, т. е. вопрос о том, является ли эта фигура фигурой конечного спуска, в результате первого шага спуска сводится (в разъясненном выше смысле) к аналогичному вопросу для некоторой степени а'», где а, меньше а,. Повторяя эти рассуждения, мы получим убывающую последо. вательность показателей а)а,)а,>...

Но так как а является фигурой не выше Й-го яруса, то последовательность эта должна оборваться в конечное число шагов, 'тогда при показателе, равном О, у нас получится фигура аз конечного спуска. Следовательно, в конечное число шагов оборвется и весь наш спуск в целом. Замечание. Заметим, что здесь не утверждается какая-то теорема о том, что «если а'< является фигурой конечного спуска то в' тоже обладает этим свойством», Сведение утверждения о конечности спуска фигуры в' к утверждению этого же свойства для в' производится не с помощью такого рода теоремы, а наосно'-.

ве особого характера первого шага спуска, начинающегося св«х). !) Мы имеем здесь ч<о-ты вроде цугцззыгз з шахматах. 624 ПРИЛОЖЕНИЕ ДОКАЗАТЕЛЬСТБО АККЕРМАНА 625 4 21 й 2. Доказательство Аккермана Приводимое здесь доказательство непротиворечивости относится к формализму, который получается из арифметического формализма (Е) в результате присоединения к нему е-формулы А (а) ~- А (е,А (х)). Оно связано с первоначальным гильбертовским подходом к исклю.

чению е-символов и с дальнейшим развитием этого подхода, осуществленным Аккерманом, о чем подробно говорилось в 2 4 гл. 11. Правда, в самом общем случае этот метод не привел нас к желаемому результату. Однако когда Генцен показал, что с помощью некоторого обобщения методов теории доказательств — а именно, при использовании обобщенной индукции до первого е-числа — может быть, доказана непротиворечивость арифметического формализма, Аккерман обнаружил, что связанный с гильбертовскнм подходом метод при соответствующем расширении этого метода также может дать полное доказательство непротиворечивости. Для того чтобы изложить данное доказательство, нам не нужно еще раз подробно повторять все подготовительные мероприятия, подвергнутые детальному обсуждению в гл.

П'). Мы перечислим только ряд необходимых нам фактов: 1. Рассматриваемая нами формальная система заметно упрощается в результате замены аксиомы индукции формулой А (а) -а- Б,А (х) Ф а' и элементарной аксиомой ачьО-е-6(и)'=а и добавления одноместной функции 6 к числу исходных (исходными являются штрих-функция, сложение и умножение). 2. Как известно, для доказательства непротиворечивости нашего формализма достаточно показать, что любая выводимая в нем формула без переменных при естественном определении истинностиых и арифметических функций и при обычном понимании равенств между цифрами является истинной. К этому следует заметить, что в рассматриваемом далее арифметическом формализме допустимьк арифметические функции мы ограничиваем лишь п)ребсванием, ипсбы для любой из них имелся в наличии способ для эффективного вычисления ее значений при любых значениях ее аргументов.

Для такого рода функций могут быть сформулированы аксиомы, от которых требуется лишь, чтобы они, во-первых, не содержали ни связанных индивидных, 21 См. с. 116-119 в 121 — 160. ни формульных переменных (точнее говоря, чтобы они были либо равенствами, либо формулами, построенными из равенств при помощи связок исчисления высказываний) и, во-вторых, чтобы при любой замене свободных переменных цифрами они давали истинные формулы, т. е.

чтобы они были верифицируемыми формулами '). Верифицируемой формулой является и аксиома а ~ 0-~ 6 (а) ' = а (здесь функция 6 вычисляется на основе рекурсивных равенств 6(0)=0, 6(п') =и). Наряду с равенствами мы могли бы допустить и другие арифметические элементарные формулы, однако такого рода обобщение было бы несущественным, так как элементарные арифметические отношения такие, например, как «а меньше Ь», «а является делителем Ь» и т, п., как известно, могут быть выражены соответствующими равенствами при помощи вычислимых, и даже примитивно рекурсивных, функций.

3. К выводу любой формулы без переменных может быть прн. менена операция исключения кванторов при помощи е-формулы'), а вслед за тем — операция возвратного переноса подстановок в исходные формулы и операция исключения свободных переменных. После выполнения этих операций из правил вывода останутся только схемы заключения и переименования связанных переменных, а для каждой из исходных формул будет иметь место следующая альтернатива: либо эта формула получается в резуль.

тате подстановки из какой-либо тождественно истинной формулы исчисления высказываний или из верифицнруемой формулы, либо она получается по схеме равенства а = Ь вЂ” (Я (а) — Я (6)) или по одной из схем Я(1) — »Я(БЕЯ(3)) и Я(1)-е е Я(р)~1', где а, 6 и 1 — термы, не содержащие переменных. Исходные формулы двух последних типов мы называем к р и т и ч е с к и м и формулами первого и соответственно второго рода и говорим, что они связаны с е-термом е Я(г) Фигуру доказательства с перечисленными свойствами мы называем нормированнымным доказательством. 4. Пусть нам дано нормированное доказательство какой-либо формулы без переменных.

Если всем входящим в эту формулу е-термам мы сможем сопоставить в качестве их значений некото- а) См. с. 58. а) См, с. 33 — 34. 21 Д. Гнньбере, П. Бернайс ПРИЛОЖЕНИЕ рые цифрь1 таким образом, что одинаковые е-термы получат одинаковые значения, и при этом с учетом обычной процедуры вычисления арифметических функций и обычного понимания нумерических равенств и истинностных функций каждая из исходных формул получит значение «истина», то н заключительная формула получит значение «истина», так как применение схемы заключения от истинных формул ведет к истинным.

Вследствие этого для искомого доказательства непротиворечивости достаточно показать, что для всякого нормированного доказательства можно подобрать такие значения фигурирующих в нем е-термов, прн которых будут выполнены указанные условия для исходных формул. Те из исходных формул, которые получаются в результате подстановок из тождественно истинных или из верифицируемых формул, получают значение «истина» при любых значениях входящих в них е-термов. Поэтому мы должны специально позаботиться об исходных формулах, построенных по схеме равенства, и о критических формулах первого н второго рода. 5. При выборе значений е-термов мы должны учитывать те типы комбинирования е-термов, с которыми связываются понятия в л о ж е н и я и п о дч и н е н и я е-термов или соответственно е-выражений, а также понятия степени е-герма и р а н г а е выражения ').

Мы используем также понятие оси о в ного т и п а: прн этом мы говорим об о с н о в н ы х т и п а х т а к и х-т о е-т е рмов или же просто об основных типах. Среди прочих е-термов основные типы характеризуются тем, что каждый фигурирующий в них в качестве собственной части терм является свободной индивидной переменной и что ни одна нз этих переменных не повторяется дважды. С каждым е-термом однозначно (отвлекаясь от обозначений упомянутых свободных переменных) связывается некоторый основной тип, из которого он получается в результате подстановки термов вместо свободных переменных (быть может, он просто совпадает с ним).

Там, где это не будет вызывать недоразумений, мы будем называть этот основной тип просто основным типом данного е-герма. Для всякогоосновноготипа в нашем распоряжении остается выбор обозначений его свободных переменных (аргументных переменных). Об основном типе з-герма, с которым связана данная критическая формула, мы тоже будем говорить, что эта критическая формула связана с рассматриваемым основным типом. Замечание. Что касается связанных переменных, входящих в е-термы, то они особой роли играть не будут, и при выборе значений для е-термов, отличающихся друг от друга лишь обозначениями этих переменных, мы будем рассматривать такие термы как одинаковые, не оговаривая этого каждый раз особо').

Характеристики

Список файлов книги