3. Нормальная форма формулы расширенного одноместного исчисления предикатов на основе дедуктивного равенства.

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

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

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

Доказательство следует методу, предложенному Беманом.

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

Эту операцию перехода от свободных переменных к связанным и обратно мы будем кратко называть «заменой» (Austausch) свободных переменных связанными и соответственно связанных переменных свободными.

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

1. Формульные переменные без аргументов.

2. Формульные переменные с одной свободной переменной в качестве аргумента.

3. Равенства между свободными переменными.

4. Формулы вида

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

5. Формулы вида

где выражения и имеют структуру, указанную в п. 4.

6. Количественные формулы, т. е. формулы вида

Кроме того, полученную нами формулу, построенную из составных частей типов 1—6, мы можем, пользуясь правилами исчисления высказываний, перевести в формулу, являющуюся конъюнктивной нормальной формой относительно этих составных частей.

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

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

Тогда из формулы

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

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

а тем самым и формула

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

Из этого замечания вытекает, что в полученной нами конъюнктивной нормальной форме каждый конъюнктивный член может рассматриваться сам по себе. Каждый такой член имеет вид дизъюнкции, члены которой суть формулы типов 1—6 или же отрицания таких формул. Здесь прежде всего можно перевести отрицания формул типов 4 и 5 в формулы тех же самых типов, но уже не являющиеся отрицаниями других формул. В самом деле, отрицания формул вида

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

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

Переменная В может встречаться только в составных частях типов 2, 4 и 5. В случае, когда содержится в составных частях вида

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

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

мы применим эквивалентности согласно которым всякая формула

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

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

(в которой, конечно, вместо могут стоять и какие-нибудь другие свободные переменные).

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

где выражение, не содержащее формульной переменной

Теперь все такие члены нашей дизъюнкции мы можем перевести в члены вида

Действительно, для формул типа 2 и их отрицаний мы в своем распоряжении имеем эквивалентности

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

могут быть переведены в формулы

После того как эти преобразования будут выполнены, вся наша дизъюнкция (после подходящей перестановки членов) приобретет вид

где выражения уже не содержат формульной переменной

Эту формулу можно сначала перевести по правилу (9) 4) в

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

т.е. в формулу вида

где снова выражения не содержат формульной переменной

Эта формула дедуктивно равна формуле

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

а так как дизъюнктивный член

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

с другой стороны, исходя из этой формулы и применяя тождественную формулу

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

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

возвращаемся к формуле

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

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

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

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

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

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

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

где переменная С в не входит.

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

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

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