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

Формула φ сигнатуры Σ называется бескванторной, если она не содержит кванторов. Бескванторная формула φ является дизъюнктивной (конъюнктивной) нормальной формой, если она получается из некоторой формулы ψ АВ, находящейся в ДНФ (КНФ), заменой всех пропозициональных переменных x₁, …, x_n на некоторые атомарные формулы φ ₁, …, φ _n сигнатуры Σ соответственно.

Говорят, что формула φ сигнатуры Σ находится в пренексной нормальной форме (ПНФ), если она имеет вид Q₁x₁…Q_nx_nψ, где Q_i, ‑ кванторы (1≤ i≤ n), n ψ – дизъюнктивная нормальная форма.

Теорема 1. Для любой формулы φ сигнатуры Σ существует ПНФ ψ, эквивалентная формуле φ;.

Опишим алгоритм приведения формулы к ПНФ:

1) выражаем импликацию, участвующую в построении формулы, через дизъюнкцию и отрицание, используя эквивалентность φ → ψ ≡ φ ∨ ψ;

2) используя законы де Моргана (φ ∧ ψ)≡ φ ∨ ψ, (φ ∨ ψ)≡ φ ∧ ψ

3) и эквивалентности xφ ≡ xφ, xφ ≡ xφ,

переносим все отрицания к атомарным подформулам и сокращаем двойные отрицания по правилу φ ≡ φ;

4) приводим формулу к виду Q₁x₁…Q_nx_nψ, где Q_i, ‑ кванторы (1≤ i≤ n), n ψ – бескванторная формула, пользуясь эквивалентностями

x(φ ∧ ψ)≡ xφ ∧ ψ, x(φ ∨ ψ)≡ xφ ∨ ψ,

x(φ ∧ ψ)≡ xφ ∧ ψ, x(φ ∨ ψ)≡ xφ ∨ ψ,

xφ ≡ x(φ) xφ ≡ x(φ)

5) используя закон дистрибутивности

φ ∧ (ψ ∨ χ)≡ (φ ∧ ψ)∨ (φ ∧ χ),

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

Пример 10. Формулу χ x yφ (x, y)→ x yψ (x, y) привести к ПНФ, считая формулы φ и ψ атомарными.

Решение. Избавившись от импликации, получаем

χ ≡ ( x yφ (x, y))∨ x yψ (x, y).

Переносим отрицание к атомарной подформуле φ (x, y):

χ ≡ x yφ (x, y)∨ x yψ (x, y).

Так как в формуле x yψ (x, y) переменные х, у являются связанными, то по пп. 2΄, 3΄ утверждения 2 имеем

χ ≡ x y(φ (x, y)∨ x yψ (x, y)).

Пусть u, v ‑ некоторые новые переменные. Тогда по пп. 4, 4΄ утверждения 2 получаем

χ ≡ x y(φ (x, y)∨ u v ψ (u, v)),

откуда по по пп. 2΄, 3΄ утверждения 2

χ ≡ x y u v(φ (x, y)∨ ψ (u, v)).

Формула φ (x, y)∨ ψ (u, v) является дизъюнктивной нормальной формой, а значит, формула x y u v(φ (x, y)∨ ψ (u, v)) является ПНФ.