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

Формула φ сигнатуры Σ называется бескванторной, если она не содержит кванторов. Бескванторная формула φ является дизъюнктивной (конъюнктивной) нормальной формой, если она получается из некоторой формулы ψ АВ, находящейся в ДНФ (КНФ), заменой всех пропозициональных переменных 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 ψ – бескванторная формула, пользуясь эквивалентностями