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

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

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

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

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

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

а эту формулу, применяя правила можно будет перевести в

что и даст нам искомую сколемовскую нормальную формулу.

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

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

и

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

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

Если теперь мы присоединим к ним нашу формулу

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

посылок и применением схемы заключения), так что получится

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

дает формулу

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

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

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

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

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

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

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

далее, по правилу формулу

можно будет преобразовать в

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

и, по правилам в

совершенно аналогичным образом формулу

можно преобразовать в

и формулу

в

так что в целом мы получим формулу

Эта формула имеет искомый вид нормальной дизъюнкции и при этом она дедуктивно равна заданной формуле

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

Дополнение 1. Рассмотрение приведенного нами доказательства непосредственно показывает, что теорема Сколема, а также и более сильная теорема о нормальной дизъюнкции,

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

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

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

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

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

преобразование которой дает нормальную дизъюнкцию

Подобным же образом для формулы

в которой не встречаются формульные переменные (с аргументами), мы получим дедуктивно равную ей формулу

которая может быть переведена в нормальную дизъюнкцию

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

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

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

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

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

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

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

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