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 ψ – бескванторная формула, пользуясь эквивалентностями

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2.4. Исчисление предикатов

2.4.1. Система аксиом и правил вывода

Зафиксируем некоторую произвольную сигнатуру Σ и определим исчисление предикатов сигнатуры Σ (ИП^Σ).

Формулами ИП^Σ будут формулы сигнатуры Σ.

Примем следующие соглашения. Пусть x₁,…,x_n ‑ переменные, t₁,…,t_n ‑ термы сигнатуры Σ и φ ‑ формула сигнатуры Σ.Запись будет обозначать результат подстановки термов t₁,…,t_n вместо всех свободных вхождений в φ переменных x₁,…,x_n соответственно, причем, если в тексте встречается запись , то предполагается, что для всех i{1,...,n} ни одно свободное вхождение в φ переменной x_i не входит в подформулу φ вида y или y, где у – переменная, входящая в t_i.

Аксиомами ИП^Σ являются следующие формулы для любых формул φ, ψ, χ ИП^Σ, любых переменных x,y,z и любого терма t:

1. φ→(ψ→φ);

2. (φ→ψ)→((φ→(ψ→χ))→(φ→χ));

3. (φ∧ψ)→φ;

4. (φ∧ψ)→ψ;

5. (φ→ψ)→((φ→χ)→(φ→(ψ∧χ)));

6. φ→(φ∨ψ);

7. φ→(ψ∨φ);

8. (φ→χ)→((ψ→x)→((φ∨ψ)→χ));

9. (φ→ψ)→((φ→¬ψ)→¬φ);

10. ¬¬φ→φ;

11. xφ→(φ)_t^x;

12. (φ)_t^x→xφ;

13. x=x;

14. x=y→((φ)_x^z→(φ)_y^z).

Указанные формулы называются схемами аксиом ИП^Σ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом.

Правила вывода ИП^Σ:

1. 

2. 

3. 

где в правилах 2 и 3 переменная x не входит свободно в χ.

Говорят, что формула φ выводима в ИП^Σ из формул φ₁,…,φ_m (обозначается φ₁,…,φ_m⊢φ), если существует последовательность формул ψ₁,…,ψ_k,φ, в которой любая формула либо является аксиомой, либо принадлежит множеству формул {φ₁,…,φ_m}, называемых гипотезами, либо получается из некоторых φ₁,…, φ_i-1 по одному из правил вывода 1-3? Причем при применении правил 2 и 3 переменная x не должна входить ни в одну гипотезу свободно. Выводимость формулы φ из (⊢φ) равносильна тому, что φ ‑ теорема ИП^Σ или доказуемая формула ИП^Σ.

Так же, как в исчислении высказываний, определяется понятие квазивывода.

Формула ψ ИП^Σ называется тавтологией в ИП^Σ, если она получается из формулы φ исчисления высказываний, доказуемой в исчислении высказываний, путем замены всех ее пропозициональных переменных x₁,…,x_n на формулы ψ₁,…,ψ_n ИП^Σ соответственно. Формулу φ при этом называют основой тавтологии.

Утверждение 1. Любая тавтология φ в ИП^Σ доказуема в ИП^Σ.

Формулы φ и ψ ИП^Σ называются пропозиционально эквивалентными, если φ→ψ и ψ→φ – тавтологии. Формулы φ и ψ ИП^Σ называются эквивалентными (обозначаем φ≡ψ), если ⊢φ→ψ и ⊢ψ→φ.

Следствие 1. Если φ и ψ ‑ пропозиционально эквивалентные формулы ИП^Σ, то φ и ψ ‑ эквивалентные формулы ИП^Σ.

Теорема 1 (о дедукции). Пусть φ₁,…,φ_m,φ,ψ – формулы ИП^Σ. Тогда φ₁,…,φ_m,φ⊢ψ φ₁,…,φ_m,⊢φ→ψ.

Следствие 2. Пусть φ и ψ ‑ формулы ИП^Σ. Следующие условия эквивалентны:

1. φ≡ψ;

2. φ⊢ψ и ψ⊢φ.