2. Привлечение аксиом равенства; дедекиндово определение бесконечности; введение штрих-символа.

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

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

Это условие в свою очередь равнозначно требованию выполнимости определенной системы формул. Действительно, всякому отображению соответствует некоторый предикат с двумя аргументами: «b является образом а»; с другой стороны, для того чтобы предикат соответствовал в этом смысле взаимно однозначному отображению индивидной области на свою собственную подобласть,

необходимо и достаточно, чтобы он удовлетворял условиям, описываемым следующими четырьмя формулами:

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

Связывая эти четыре формулы знаком конъюнкции, мы получим некоторую формулу Выполнимость этой формулы и есть то, в чем, по Дедекинду, состоит бесконечность какой-либо индивидной области.

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

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

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

третья из формул формула

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

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

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

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

Отсюда путем элементарных преобразований (применение правила соединения посылок и опускание лишних скобок) получается формула

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

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

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

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

аргумента. Используя знак равенства, мы теперь можем отношение непосредственно следует за а» формализовать посредством равенства

Подставив это равенство вместо формульной переменной в формулы мы получим следующие четыре формулы:

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

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

подстановкой получаем

из нее, применив основную формулу (b) и схему заключения, получаем

а отсюда, переименовав х в у и применив правило (у) получаем формулу

т. е. первую из формул

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

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

а отсюда по правилу получаем третью из формулы

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

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