§ 5. Включение полной индукции

1. Формализация принципа полной индукции с помощью формулы и с помощью схемы; равносильность обеих формализаций; инвариантность запаса выводимых формул без формульных переменных относительно добавления к системе схемы индукции.

Замечательным следствием полученных результатов является также тот факт, что если рассматривать лишь формулы без

формульных переменных, то присоединение принципа полной индукции не может расширить совокупности выводимых формул.

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

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

От аксиоматической версии этого принципа мы теперь можем перейти к его формализации; она может быть произведена, с одной стороны, посредством некоторой формулы, а с другой стороны, посредством некоторой схемы. Эта формула, аксиома индукции, записывается в виде

Что же касается схемы индукции, то она имеет вид

Эта схема (подобно схемам нашего исчисления предикатов) должна применяться при условии, что переменная а в встречается только там, где она указана в качестве аргумента.

В том, что это ограничение необходимо, можно убедиться на простых примерах. Если мы, например, возьмем в качестве формулу

то соответствующие формулы

т. е.

и

будут выводимыми. Если бы мы допустили применение схемы индукции к этим формулам, то в результате получили бы формулу

а из нее подстановкой — формулу

которая в сочетании с выводимыми формулами

привела бы нас к противоречию.

Оба способа формализации принципа полной индукции равносильны в том смысле, что схема индукции может быть получена из аксиомы индукции в качестве производного правила, а с другой стороны, аксиома индукции тоже может быть выведена с помощью схемы индукции.

Именно, подстановкой формулы вместо именной формы мы из аксиомы индукции получаем формулу

Если переменная а встречается в формуле только там, где она указана в качестве аргумента, т. е. если в переменная а не встречается, то из формулы

мы по правилу получим формулу

эта формула вместе с

по правилам исчисления высказываний дает формулу

а эта последняя в сочетании с формулой

дает формулу

Таким образом, от формул

мы с помощью аксиомы индукции приходим к формуле

И обратно, если мы в качестве правила возьмем схему индукции, то формула

окажется выводимой. Действительно, обозначим для краткости формулу посредством Тогда, на основании схемы индукции, для вывода достаточно будет вывести формулы

т. е.

и

Первая из этих двух формул получается непосредственной подстановкой из тождественной формулы

а вторая с использованием тождественной формулы

может быть получена из формулы

которая в свою очередь получается подстановкой из основной формулы (а) исчисления предикатов.

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

Представим себе, что нам дан вывод формулы произведенный на основе исчисления предикатов с помощью аксиом (А) и с привлечением схемы индукции. Предположим, что формула не содержит формульных переменных. Тогда мы сможем, пользуясь нашей прежней методикой, разложить это доказательство на нити, поступая со схемой индукции аналогично тому, как мы поступали со схемой заключения, т. е. сопоставляя каждой такой схеме фигуру вида

При этом следует заметить, что переменная а в третьей формуле схемы не связана с переменной а во второй формуле; то, что для этих двух формул схемы индукции мы берем одну и ту же переменную а, представляет собой некоторое соглашение, само по себе не необходимое.

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

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

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

какой-нибудь новой, ранее не встречавшейся переменной и продолжая эту замену в обратном направлении.

В остальном мы, как и раньше, перенесем подстановки назад, а затем исключим быть может еще оставшиеся формульные переменные. Все эти преобразования не затрагивают заключительной формулы так как она формульных переменных не содержит.

В получившейся таким образом фигуре разложения мы рассмотрим теперь одно из тех применений схемы индукции (соответственно тех фигур, получающихся из них в результате проведенных модификаций), которым при просмотре нитей

доказательства в направлении от исходных формул (т. е. в направлении развертывания вывода) не предшествует никакое другое применение схемы индукции. Пусть формулы этой схемы в первоначальном выводе имели вид

а в результате выполненных преобразований на их месте оказались формулы

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

Нити доказательства, ведущие от исходных формул к формулам

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

путем подстановок и повторного применения схемы заключения можно будет вывести

Таким образом, для любой цифры формула оказывается выводимой из системы аксиом (А). Кроме того, эта формула не содержит формульных переменных. Следовательно, по одному из наших утверждений о системе аксиом формула

а значит, и формула

тоже могут быть выведены из системы аксиом (А) без использования схемы индукции.

Если мы теперь для какого-нибудь такого вывода формулы осуществим разложение его на нити, возвратный перенос подстановок и исключение формульных переменных, то полученную таким образом не содержащую схем индукции фигуру разложения с заключительной формулой мы сможем подставить вместо всех тех нитей нашей первоначальной фигуры разложения, которые ведут от исходных формул к формуле

Таким образом, в результате получится некоторое новое разложенное на нити доказательство формулы в фигуре разложения которого схема индукции встречается на один раз меньше, чем в первоначальной фигуре разложения.

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

Тем самым мы фактически показали, что в результате присоединения схемы индукции к системе аксиом (А) выводимыми оказываются только те формулы без формульных переменных, которые можно было вывести и без использования этой схемы. В точности то же самое справедливо и в отношении аксиомы индукции, так как она выводима с помощью схемы индукции и, следовательно, не может дать больше, чем сама эта схема.

Из этого результата мы можем, в частности, сделать вывод о непротиворечивости системы, которая получится, если к системе (А) присоединить аксиому или схему индукции.