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

 

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

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

Примем следующие соглашения. Пусть 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) φ ⊢ ψ и ψ ⊢ φ;.