Предварённая нормальная форма: приведение предикатов

Предварённая нормальная форма (ПНФ, она же пренексная) - это стандартный вид формулы логики предикатов, в котором все кванторы собраны в начале, а дальше идёт бескванторное ядро. К нему приводят перед сколемизацией, перед проверкой выполнимости методом резолюций и просто чтобы увидеть логическую структуру утверждения. Приведение всегда выполнимо и состоит из нескольких механических шагов: убрать импликации, протолкнуть отрицания внутрь, развести одноимённые переменные и вынести кванторы наружу. Ниже разберём каждый шаг и типичные места, где студенты теряют эквивалентность. Если нужно прогнать конкретную формулу, соберите запрос в форме ниже и получите пошаговый вывод.

Что такое предварённая нормальная форма

Формула находится в предварённой нормальной форме, если она имеет вид

$$Q_1 x_1\, Q_2 x_2\, \ldots\, Q_n x_n\, M,$$

где каждый $Q_i$ - это квантор всеобщности $\forall$ или существования $\exists$, а $M$ - бескванторная формула, называемая матрицей. Цепочка кванторов $Q_1 x_1 \ldots Q_n x_n$ называется префиксом. Никакого квантора внутри матрицы быть не должно: они все вынесены влево.

Простой пример. Формула $\forall x\, \exists y\, (P(x) \to Q(x, y))$ уже в ПНФ: префикс $\forall x\, \exists y$, матрица $P(x) \to Q(x, y)$. А формула $\forall x\, P(x) \to \exists y\, Q(y)$ не в ПНФ - квантор $\exists y$ стоит внутри, его ещё предстоит вынести наружу.

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

Рассчитать для своей задачи

Зачем приводить к ПНФ

Предварённая форма - не самоцель, а промежуточный этап. Её используют, чтобы:

• подготовить формулу к сколемизации - устранению кванторов существования через функции Сколема; сколемизация определена именно для пренексных формул;
• получить клаузальную форму для метода резолюций в автоматическом доказательстве теорем;
• проверить логическую структуру утверждения: порядок $\forall$ и $\exists$ в префиксе сразу показывает, от чего зависит выбор объекта;
• сравнить две формулы на эквивалентность, приведя обе к каноническому виду.

Особенно важен порядок кванторов. $\forall x\, \exists y\, R(x, y)$ и $\exists y\, \forall x\, R(x, y)$ - это разные утверждения: в первом $y$ выбирается под каждое $x$, во втором один $y$ годится для всех $x$. Поэтому при выносе кванторов их относительный порядок менять нельзя.

Шаг 1: убрать импликации и эквиваленции

Кванторы удобно выносить только из формул, построенных на $\neg$, $\land$, $\lor$. Поэтому сначала избавляемся от $\to$ и $\leftrightarrow$ по тождествам:

$$\begin{aligned} A \to B &\equiv \neg A \lor B,\\ A \leftrightarrow B &\equiv (\neg A \lor B) \land (\neg B \lor A). \end{aligned}$$

Эквиваленцию раскрывают именно так, а не как $(A \land B) \lor (\neg A \land \neg B)$ - обе формы верны, но первая короче ведёт к ПНФ. После этого шага в формуле остаются только отрицания, конъюнкции и дизъюнкции.

Шаг 2: протолкнуть отрицания к атомам

Теперь загоняем $\neg$ внутрь, к атомарным предикатам, по законам де Моргана и правилам отрицания кванторов:

$$\begin{aligned} \neg(A \land B) &\equiv \neg A \lor \neg B,\\ \neg(A \lor B) &\equiv \neg A \land \neg B,\\ \neg \forall x\, A &\equiv \exists x\, \neg A,\\ \neg \exists x\, A &\equiv \forall x\, \neg A. \end{aligned}$$

Двойное отрицание снимаем: $\neg\neg A \equiv A$. Результат этого шага - негативная нормальная форма, где отрицания стоят только перед атомами. Самая частая ошибка здесь - забыть, что отрицание переключает квантор: $\neg\forall$ становится $\exists$, а не остаётся $\forall$.

Рассчитать для своей задачи

Шаг 3: переименовать связанные переменные

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

Возьмём $\forall x\, P(x) \lor \exists x\, Q(x)$. Здесь $x$ под $\forall$ и $x$ под $\exists$ - формально разные переменные, но с одним именем. Переименуем второе: $\forall x\, P(x) \lor \exists z\, Q(z)$. Эта операция называется $\alpha$-преобразованием (переименование связанной переменной) и всегда даёт эквивалентную формулу. Правило простое: давайте каждому квантору своё уникальное имя переменной - тогда захвата на следующем шаге не случится.

Шаг 4: вынести кванторы в префикс

Когда имена разведены, кванторы выносятся наружу по законам пронесения. Главное условие: переменная квантора не входит свободно в ту подформулу, через которую мы его протаскиваем (после шага 3 это гарантировано). Базовые тождества:

$$\begin{aligned} (\forall x\, A) \land B &\equiv \forall x\, (A \land B),\\ (\exists x\, A) \lor B &\equiv \exists x\, (A \lor B),\\ (\forall x\, A) \lor B &\equiv \forall x\, (A \lor B),\\ (\exists x\, A) \land B &\equiv \exists x\, (A \land B). \end{aligned}$$

Аналогичные равенства работают, когда квантор стоит во втором аргументе. Кванторы вытягиваем по одному, сохраняя их взаимный порядок. Когда в матрице не остаётся ни одного квантора, формула в ПНФ. Чтобы не запутаться, какая связка к чему относится при раскрытии импликаций, держите в голове приоритет логических операций в выражении.

Полный пример приведения

Приведём $\forall x\, P(x) \to \exists y\, Q(y)$ к ПНФ.

1. Убираем импликацию: $\neg(\forall x\, P(x)) \lor \exists y\, Q(y)$.
2. Проталкиваем отрицание: $\neg\forall x\, P(x) \equiv \exists x\, \neg P(x)$, получаем $\exists x\, \neg P(x) \lor \exists y\, Q(y)$.
3. Переименование не требуется: $x$ и $y$ уже разные.
4. Выносим кванторы: $\exists x\, \exists y\, (\neg P(x) \lor Q(y))$.

Префикс $\exists x\, \exists y$, матрица $\neg P(x) \lor Q(y)$ - формула в предварённой нормальной форме.

Рассчитать для своей задачи

ПНФ и сколемизация

После ПНФ обычно идёт сколемизация - устранение $\exists$. Каждый квантор существования заменяют на функцию Сколема от всех охватывающих его $\forall$-переменных. Для $\forall x\, \exists y\, R(x, y)$ получаем $\forall x\, R(x, f(x))$: $y$ зависит от $x$, поэтому это функция, а не константа. Если $\exists$ не стоит ни под одним $\forall$, его заменяют константой Сколема (нульместной функцией).

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

Частые ошибки

• Забытое переименование переменных. Два квантора с именем $x$ после выноса сливаются в один диапазон связывания - формула меняет смысл. Сначала разводим имена, потом выносим.
• Перестановка $\forall$ и $\exists$. $\forall x\, \exists y$ и $\exists y\, \forall x$ не эквивалентны. При выносе сохраняйте исходный порядок кванторов.
• Отрицание не переключает квантор. $\neg\forall x\, A$ - это $\exists x\, \neg A$, а не $\forall x\, \neg A$. То же для $\neg\exists$.
• Импликация не раскрыта. Пытаться выносить кванторы прямо из $A \to B$ опасно: $\forall x\, P(x) \to B$ даёт $\exists x\, (P(x) \to B)$, потому что левая часть импликации меняет квантор. Проще сначала перейти к $\neg A \lor B$.
• Сколемизацию путают с приведением к ПНФ. Это разные операции: ПНФ сохраняет эквивалентность, сколемизация - только выполнимость.

FAQ

Всегда ли можно привести формулу к ПНФ? Да. Для любой формулы логики предикатов существует логически эквивалентная ей предварённая нормальная форма. Алгоритм из четырёх шагов конечен и всегда завершается.

Единственна ли предварённая нормальная форма? Нет. У одной формулы есть много эквивалентных ПНФ - порядок выноса независимых кванторов и форма матрицы могут различаться. Канонической делает её уже последующий переход к клаузальной форме.

Чем префикс отличается от матрицы? Префикс - это вынесенная вперёд цепочка кванторов $Q_1 x_1 \ldots Q_n x_n$. Матрица - оставшаяся бескванторная часть формулы. Вместе они и образуют ПНФ: префикс плюс матрица.

Коротко

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