Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 127
Текст из файла (страница 127)
Все собственные аксиомы системы (Е) (т. е, формулы а'ФО, а'=й'-эа=(з и рекурсивные равенства для сложения и умножения) являются верифицируемыми — и в данном доказательстве непротиворечивости мы будем пользоваться только этим их свойством. Это позволит нам с самого начала наряду с указанными собственными аксиомами допускать и другие верифицируемые собственные аксиомы: в частности, рекурсивные равенства для примитивно рекурсивных функций, а также равенства, позволяющие вычислять какие-либо квазирекурсивные функции, Идя еще дальше, мы можем в целях сокращения выводов допустить также использование в качестве исходных формул равенств вида 1=! и 1=1, где 1 — какой-либо нумерический терм, а 1 †циф, являющаяся его значением.
Такие равенства мы будем называть т е р м а л ь н ы м и. В соответствии с нашим определением все они являются истинными, а следовательно, и верифицируемыми формулами. Формализм, который у нас таким образом возникает, получается из исчисления предикатов в результате присоединения к нему знака равенства, индивидного символа О и штрих-символа, а также аксиомы равенства ()з) и аксиомы индукции, а кроме того, введения символов для вычислимых функций н ') з(ы моглн бы, нан зто делает Кальмар, допустить з качестве нсходных н рззрешамые предвнаты, но с математической точна зрения этот случай не был бы более общим ввиду гого, что зснкнй разрешимый предннат может быть нзображен равенством вида ! О, где ! — некоторый терм, построенмый нз вычнслнмых функций.
') См. г. 1, с. 294, 360, 363; т. П, с, 58 — 59. ПРИЛОЖЕИИЙ правила, разрешающего брать верифицируемые формулы в качестве исходных. Если мы сумеем показать, что всякая иумерическая формула, выводимая средствами этого дедуктивного формализма, является истинной, то тем самым будет установлена его непротиворечивость. Мы начнем с ряда подготовительных рассуждений, которые в свое время мы уже проводили. Они будут касаться возможности упрощения данного формализма без изменения запаса выводимых нумерических формул: 1. Аксиома индукции, как мы знаем, может быть заменена схемой индукции '). 2. Квантор всеобщности, а также основная формула (а) и схема (а) могут быть устранены путем замены каждого выражения 75Я(5) соответствующим ему выражением 135 1Я(5) ').
3. При помощи разложения выводов на нити может быть произведен возвратный перенос всех подстановок с последующим исключением формульных переменных'). 4. Правило переименования связанных переменных может быть исключено, если мы откажемся от выделенной роли переменной х в основной формуле (Ь) и в схеме (р)'). Произведя в нашем формализме указанные модификации, мы придем к следующим правилам построения выводов: Формулы строятся, исходя из элементарных, при помощи связок исчисления высказываний и квантора существования. Элементарные формулы представляют собой равенства терман.
Термы суть либо основные термы, т. е. 0 и свободные индивидные переменные, либо термы, построенные из основных при помощи штрих- символа и символов для вычислимых функций. В качестве исходных формул у нас фигурируют: а) Формулы, истинные в логике высказываний, т. е. получающиеся в результате подстановок из тождественно истинных формул исчисления высказываний. б) Формулы, построенные по схеме Я (1) -« =15Я (5), где 1 — какой-либо терм; мы будем называть их аксиомами для квантора существования. в) Формулы, построенные по схеме < = 5 — «(Я (<) -«Я (6)), где с и 6 — какие-либо термы; мы будем называть их фор м у- лами равенства, 9 См. т. 1, с. 325 — 330.
См. т. 1, с. 289 — ЯО. ' См. т. 1, с. 275 — 283 и 286 — 288, а такжс с. 327 — 328, а) См. т, П, Приложеива 1 с. 475 — 476. ДОКАЗАТЕЛЬСТВО КАЛЬМАРА г) Верифицируемые формулы. Схемами вывода являются: а) Взятая из исчисления высказываний схема заключения б) Схема для квантора существования е (<) — Я 35З (5) -«Я со свободной переменной <, не входящей нн в 21, ни в 6(5). в) Схема индукции") Я(0), Я(<)-«21(<') Я (1) со свободной переменной с, не входящей в Я(0), и с произвольным термам 1. Результирующую формулу какой-либо схемы вывода мы будем называть нижней формулой этой схемы, а остальные формулы схемы — верхними ее формулами.
Относительно двух формул, являющихся верхними формулами какой-либо схемы вывода, мы будем говорить, что они расположены рядом друг с другом. Обозначенную буквой < переменную, фигурирующую в какой-либо схеме для квантора существования или же в схеме индукции, мы будем называть собственной переменной этой схемы. Так как в рассматриваемых схемах ни одной из переменных исключительной роли не отводится, то можно заранее позаботиться о том, чтобы свободные индивидные переменные в выводе обозначались одинаково лишь тогда, когда это диктуется структурой вывода. После такого разделения свободных переменных каждую из них, не являющуюся собственной переменной какой-либо схемы вывода ни в одной из формул, где она встречается, можно будет всюду заменить цифрой О.
Действительно, в результате такой замены одинаковость формул не будет нарушаться, а в остальном для любой из этих переменных в выводе используется лишь ее свойство быть термам.) Эту операцию мы будем называть исключением излишних свободных переменных. В выводе любой нумерической формулы после ° ) Схемой видукпии авторы ранее (см., вапрвмер, т. 1, о 325) яааывалв схему, отличающуюся от данной тем, что в реауль<ирующай формуле вмсс<о чарна 1 там стояла свободяая переменная.
Очевидио, что вти две схемы раввосвлькы. — Прим, пери. ПРИЛОЖЕНИЕ разделения свободных переменных и исключения тех из них, . которые являются излишними, каждая свободная переменная .. будет фигурировать лишь в роли собственной переменной некоторой схемы вывода, после чего уже больше встречаться не будет. Рассмотрим теперь произвольный вывод, построенный в соответствии с нашими правилами и разложенный после этого на: нити. Применим к нему операцию разделения переменных, а затем исключим излишние свободные переменные.
Возьмем заключи- . тельную формулу этого вывода, и, двигаясь по нему в обратном направлении, проследим каждую его нить до того места, где она; упирается в какую-либо исходную формулу или же в нижнюю формулу какой-либо схемы для квантора существования или схемы индукции. Ту часть фигуры вывода, которая при этом получается (включая и формулы, до которых мы дошли в нашем движении), мы будем называть концевым фрагментом данного вывода, а остальную часть — его начальным фра гментом.
Ввиду того, что излишние свободные переменные были нами исключены, в концевом фрагменте вывода свободных переменных не будет вообще. Кроме схем заключения, в концевом фрагменте не будет также никаких схем вывода. В том частном случае, когда в исходном выводе нет кванторов существования, можно с помощью рассуждения, аналогичного тому, которое было проведено при рассмотрении рекурсивной арифметики '), показать, что заключительная формула данного вывода является верифицируемой, а поскольку она является нумерической, — то и истинной. Таким образом, в рассматриваемом частном случае доказательство закончено. Рассуждения, использованные в этом частном случае, могут быть применены и при рассмотрении общего случая.
Сначала мы убедимся, что любая примыкающая к концевому фрагменту схема индукции, т. е. схема И (0), И (т) -~- И (с') И (1) нижняя формула которой Я(1) является для концевого фрагмента исходной, может быть устранена. Действительно, как мы знаем, здесь терм 1 должен быть нумерическим. Пусть 1 — цифра, являющаяся его значением. Тогда 1 является либо нулем, либо цифрой, следующей за некоторой цифрой п. В первом случае равенство 0=1 является истинным, и мы можем взять его в качестве исход. ной формулы, Из этого равенства, взятого вместе с формулой Я (0) и формулой равенства О-1 (И (О) И (1)), 1) си.
т. !, с. 360 — 365, ДОКАЗАТЕЛЬСТВО КАЛЬМАРА дважды применив схему заключения, мы получим И(1). При этом верхняя формула И(с)-~-И(с') вообще не будет использоваться, и потому она вместе со своим выводом может быть опущена.. В противном случае, т. е. в случае, когда 1 представляет собой некоторую цифру и', мы по выводу формулы И(<)- Я(т') построим 1 различных выводов, каждый из которых получается из вывода этой формулы в результате повсеместной замены переменной с цифрой ш, которая по очереди пробегает все значения от 0 до п включительно. Заключительными формулами этих выводов будут формулы И(0) — И(0'), И(0')-~-И(0"), ..., И(п)-~И(п').
Взяв эти формулы вместе с формулой И(0) и применив надлежащее число раз схему заключения, мы получим формулу И(п'), т. е. И(1). А эта формула вместе с истинной формулой 1=1 и формулой равенства 1 = 1- (Я (1) — И (1)) двукратным применением схемы заключения даст нам формулу И(1). Эту операцию исключения схемы индукции мы будем называть операцией устранения индукции. То, что она действительно всякий раз приводит к некоторому упрощению, наперед не очевидно и должно быть показано.
На будущее мы условимся, что если к концевому фрагменту примыкает несколько применений схемы индукции, то всякий раз будет исключаться то из них, которое в рассматриваемой нами разложенной на нити фигуре вывода расположено левее остальных. Благодаря этому процедура устранения индукции становится однозначной. Заметим, что в результате применения этой операции концевой фрагмент рассматриваемого вывода расширяется. А для случая, когда к рассматриваемому концевому фрагменту не примыкает ни одно применение схемы индукции, мы определим некоторую другую операцию — операцию устранения квантора существования. Она будет применяться при соблюдении некоторых дополнительных условий, которые еще должны быть сформулированы.
Для этого мы введем ряднеобходимых понятий и терминов. Формулу вида ЗЕИ(х) мы будем называть экзи стен ци альной, и относительно аксиомы И(1)-~-Э~И(Е), равно как и относительно схемы вывода с нижней формулой ЯВИ(Е)-+.6, мы будем говорить, что они относятся к экзистенциальной формуле )хИ (г). Максимальное число различных, напластовывающихся друг на друга кванторов существования в какой-либо формуле мы будем называть степенью этой формулы. Иными словами, мы будем счцтать, что: формула без кванторов существования имеет 604 еоз ПИ1ЛОЖЕИИЕ $п докАзАтельство кАльмАРА степень, равную нулю; отрицание формулы имеет ту же самую степень, что и сама эта формула; конъюнкция, дизъюнкция, импликация и эквивалентность формул Я и ч.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
