§ 4. Переход к одной (в области формул, не содержащих формульных переменных) дедуктивно завершенной системе аксиом

1. Выводимость ряда верифицируемых формул в рассматриваемой системе аксиом; доказательство с помощью «цифр второго рода».

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

является также и верифицируемой.

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

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

выводимыми не являются. Такова, например, формула

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

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

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

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

истинно, а неравенство

ложно. Для каждой отличной от цифры первого рода и для каждой цифры второго рода неравенство

истинно, а неравенство

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

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

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

или неравенств

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

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

и соответственно

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

Ввиду сказанного, мы приходим к следующим изменениям в процедуре редукции.

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

с числом штрихов меньшим чем мы теперь преобразуем в выражение

вместо использованного ранее выражения

а неравенство

при преобразуем в выражение

вместо использованного ранее выражения

В случае замены

вместо выражения

будет фигурировать выражение

а в случае замены

вместо

будет фигурировать выражение

кроме того, вместо каждого из конъюнктивных членов

будет стоять выражение

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

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

Отсюда следует, что формула

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

которая является ложной.