2. Упрощение рассматриваемой системы аксиом в результате добавления аксиомы индукции; система (В).

При рассмотрении этой системы мы замечаем, что формулы

и

являются в ней излишними. Действительно, в результате контрапозиции и подстановки из формулы

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

Таким образом, для того чтобы получить формулу

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

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

и

В процессе этого вывода формула

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

а значит, и

Из этой формулы в сочетании с

мы прежде всего получим

а отсюда, с помощью исчисления высказываний,

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

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

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

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

которая выводится из формул

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

оказываются ненужными.

Имеют место еще и следующие соотношения. Как мы зваем, из формул

и

может быть выведена формула

Обратно, из этой последней в сочетании с аксиомой равенства и формулами можно снова получить формулу

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

из формул и формул

Действительно, сначала рассматриваемая формула элементарным образом может быть преобразована в формулу

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

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

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

(с использованием уже упоминавшегося вывода формулы ). Формула же получается из формул

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

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

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

можно будет заменить формулами

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

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

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

и аксиома индукции.

Как это впервые установил Хазенъегер, формулу, приведенную здесь в качестве предпоследней аксиомы, можно

будет вывести из остальных аксиом. Этот вывод может быть произведен следующим образом.

Обозначим посредством формулу

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

С этой целью мы сначала выведем, используя схему индукции, формулу

правую часть которой обозначим для краткости посредством . Формулу

мы получим из формулы

выводимой с помощью схемы индукции из формул получается индукцией с помощью Что же касается формулы

то она получается следующим образом. С помощью мы получаем

с помощью

Полученные две формулы друг с другом дают

т. е.

Далее, с помощью исчисления предикатов непосредственно получается

Полученные две формулы друг с другом дают

откуда с помощью исчисления высказываний получаем

а тем самым и

Итак, мы получили в наше распоряжение формулу

т. е.

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

с помощью мы получаем формулу

Формулы [1] и [2] совместно с получающейся из формулой

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

и далее (так как переменная а не входит в формулу

т. е.

Далее, по схеме индукции получается формула а вместе с тем и формула

выводимость которой требовалось доказать.

Итак, система аксиом, получающаяся из системы (А) добавлением аксиомы индукции, равносильна следующей системе аксиом;

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