§ 2. Решение проблемы разрешимости; теоремы о полноте

1. Распознавание выводимости таких предваренных формул исчисления предикатов, у которых все кванторы всеобщности предшествуют всем кванторам существования; разрешимость в конечном.

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

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

где обозначает выражение без кванторов, а представляет собой единственный квантор существования.

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

Прежде всего мы докажем следующую теорему:

Если формула вида

не содержащая, кроме квантора никаких других кванторов и такая, что в ней встречается не более I свободных индивидных переменных, является -тождественной, то она является также и выводимой.

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

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

и если вместо переменных

мы подставим соответственно цифры

[вследствие чего перейдет в некоторое выражение ], то в результате получится

Значит, эта формула (по определению -тождественной формулы) должна получаться подстановкой из тождественной формулы исчисления высказываний. Если мы теперь внесем изменения в подстановку, заменив цифру 1 всюду, где она встречается в качестве аргумента в подставляемой элементарной формуле, переменной а, цифру 2 — переменной цифру переменной , то в результате этой модификации подстановки получится формула

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

можно будет перейти к формуле

Доказанная теорема немедленно может быть обобщена следующим образом: Если формула вида

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

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

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

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

Отсюда, по только что доказанной теореме, получается, что формула

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

Но от формулы

мы по правилу снова придем к формуле

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

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

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

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

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

Для примера рассмотрим случай, когда формула имеет вид

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

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

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

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

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

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