2. Подход к пополнению этой системы аксиом; выводимость ряда эквивалентностей как достаточное условие.

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

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

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

Действительно, разберем следующие случаи:

1. Истинное нумерическое равенство имеет вид

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

2. Отрицание нумерического равенства, если оно истинно, имеет вид

или

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

3. Истинное нумерическое неравенство имеет вид

где отлично от . Оно выводится средствами исчисления высказываний с использованием аксиом

4. Отрицание нумерического неравенства, если оно истинно, имеет вид

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

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

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

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

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

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

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

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

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

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

формула

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

Таким образом, редукции формулы

должны быть ложными, а потому редукции формулы

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

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

а из нее [по правилу ] формулу

т. е. формулу Следовательно, формула также выводима.

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

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

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

свою редукцию так что в итоге формула

будет выводимой с помощью расширенной системы аксиом.

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

[Здесь свободные переменные. Количество штрихов t в формулах ((8)), ((9)) и ((10)) произвольно.]