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).

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

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

где в правилах 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. φ⊢ψ и ψ⊢φ.