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

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

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

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

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

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

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

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

где и обладают свойствами, указанными в п. 4.

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

Отличие от обыкновенного одноместного исчисления предикатов проявляется в том, что здесь добавляются пп. 3, 5 и 6, связанные с равенством.

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

Выражение, стоящее квантором или кроме связанных переменных и может, вообще говоря, содержать еще и свободные переменные.

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

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

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

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

1) формульные переменные без аргументов [т. е. формулы типа 1];

2) формульные переменные с отличной от х переменной в качестве аргумента;

3) равенства между двумя отличными от х переменными;

4) выражения вида

или

где каждый из членов

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

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

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

применяя формулы

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

стояла в левой части; этого можно достичь, применив формулу 2)):

Наконец, мы можем добиться того, чтобы в составных частях

ни один из членов дизъюнкции не был отрицанием равенства и чтобы в составных частях

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

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

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

а затем, с применением формулы 6а)), в

т. е. в выражение, построенное с помощью связок исчисления высказываний из составных частей типа 2) и 3).

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

в котором один из членов конъюнкции представляет собой равенство типа .

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

(соответственно конъюнкция

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

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

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

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

представляют собой то, что в доказываемой нами теореме мы назвали формулами типа 4. А формулы остальных типов, применяя можно перевести в такие выражения, которые с помощью связок исчисления высказываний могут быть построены из составных частей типов 2) и 3) и из формул типов 5 и 6.

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

теперь состоит из составных частей типов 1, 4, 5, 6, 2) и 3).

В том случае, когда перед формулой больше нет ни одного квантора всеобщности или существования, составные части типов 2) и 3) могут содержать только свободные индивидные переменные; следовательно, они являются формулами типов 2 и 3. В этом случае вся формула в целом оказывается составленной из формул типов 1, 2, 3, 4, 5, 6 с помощью связок нсчисления высказываний, и тем самым мы достигаем поставленной цели. Если же связанные переменные

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

переменные, отличные от

но это обстоятельство не меняет ничего существенного в протекании нашего процесса. Действительно, так как составные части типов 4, 5 и 6 не содержат ни одной из переменных то мы можем обращаться с ними в точности так же, как с формульными переменными без аргумента, т. е. выражение, стоящее после кванторной приставки, сначала можно будет перевести в конъюнктивную, соответственно дизъюнктивную нормальную форму, причем все составные части типов 4, 5 и 6 можно будет рассматривать как нерасчленимое целое (подобно элементарным формулам). Если мы теперь применим — как мы это делали раньше — к последнему из кванторов, входящих в приставку, правила (8) и то составные части типов 4, 5 и 6 выйдут из области действия этого квантора. Получившуюся теперь формулу можно охарактеризовать аналогично формуле, полученной нами на соответствующем месте первого шага нашей процедуры. Единственное различие заключается в том, что при перечислении возможностей 1), 2), 3), 4) мы к составным частям категории 1) должны будем, кроме формульных переменных без аргументов, причислить еще и формулы типов 4, 5 и 6. Дальнейшее течение процедуры, где речь идет только о преобразовании формул типа 4), будет таким же, как и в предыдущем случае.

После этого мы либо достигнем поставленной цели (если все кванторы, стоящие перед формулой будут исчерпаны, т. е. если все связанные переменные будут вовлечены в составные части типов 4, 5 и 6), либо сможем применить нашу процедуру еще раз. При каждом применении этой процедуры количество кванторов, стоящих перед формулой, будет уменьшаться на единицу. Таким образом, если число кванторов у исходной предваренной нормальной формы равно то -кратное применение нашей процедуры приведет нас к формуле, обладающей заданным свойством, т. е. к такой формуле, которая образована из составных частей типов 1, 2, 3, 4, 5 и 6 с помощью связок исчисления высказываний. Тем самым исходная формула окажется разложенной в примарные формулы.

Заметим также, что рассмотренный способ разложения в примарные формулы не приводит к появлению каких-либо новых свободных индивидных переменных. Таким образом, если исходная формула с самого начала не содержала свободных индивидных переменных, то и после произведенного разложения в примарные формулы в результирующей формуле их также не будет. Тем самым не смогут появиться никакие составные части типов 2 и 3, так что все примарные формулы обязательно будут формулами "типов 1, 4, 5 и 6,

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

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