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

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

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

где

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

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

был сделан Г. Беманом отправной точкой его исследования, посвященного одноместному исчислению предикатов; об этом исследовании впоследствии мы будем говорить более подробно.

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

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

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

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

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

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

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

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

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

или

В этих формулах переменная у может быть переименована в х.

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

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

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

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

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

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

У нас получится выражение

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

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

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

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

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

Так мы приходим к формуле

Теперь мы можем [по правилу (i)] вынести из-под квантора существования сначала не содержащий у конъюнктивный член

а затем и не содержащий у дизъюнктивный член

так что у нас получится

Теперь у может быть переименован в х.

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