Зафиксируем некоторую произвольную сигнатуру Σ и определим исчисление предикатов сигнатуры Σ (ИПΣ).
Формулами ИПΣ будут формулы сигнатуры Σ.
Примем следующие соглашения. Пусть x1,…,xn ‑ переменные, t1,…,tn ‑ термы сигнатуры Σ и φ ‑ формула сигнатуры Σ. Запись будет обозначать результат подстановки термов t1,…,tn вместо всех свободных вхождений в φ переменных x1,…,xn соответственно, причем, если в тексте встречается запись , то предполагается, что для всех i{1,...,n} ни одно свободное вхождение в φ переменной xi не входит в подформулу φ вида y или y , где у – переменная, входящая в ti.
Аксиомами ИПΣ являются следующие формулы для любых формул φ, ψ, χ ИПΣ, любых переменных x,y,z и любого терма t:
1) φ→(ψ→φ);
2) (φ→ψ)→((φ→(ψ→χ))→(φ→χ));
3) (φ∧ψ)→φ;
4) (φ∧ψ)→ψ;
5) (φ→ψ)→((φ→χ)→(φ→(ψ∧χ)));
6) φ→(φ∨ψ);
7) φ→(ψ∨φ);
8) (φ→χ)→((ψ→x)→((φ∨ψ)→χ));
9) (φ→ψ)→((φ→¬ψ)→¬φ);
10) ¬¬φ→φ;
11) xφ→(φ)tx;
12) (φ)tx→xφ;
13) x=x;
14) x=y→((φ)xz→(φ)yz).
Указанные формулы называются схемами аксиом ИПΣ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом.
Правила вывода ИПΣ:
1.
2.
3.
где в правилах 2 и 3 переменная x не входит свободно в χ.
Говорят, что формула φ выводима в ИПΣ из формул φ1,…,φm (обозначается φ1,…,φm⊢φ), если существует последовательность формул ψ1,…,ψk,φ, в которой любая формула либо является аксиомой, либо принадлежит множеству формул {φ1,…,φm}, называемых гипотезами, либо получается из некоторых φ1,…, φi-1 по одному из правил вывода 1-3? Причем при применении правил 2 и 3 переменная x не должна входить ни в одну гипотезу свободно. Выводимость формулы φ из (⊢φ) равносильна тому, что φ ‑ теорема ИПΣ или доказуемая формула ИПΣ.
Так же, как в исчислении высказываний, определяется понятие квазивывода.
Формула ψ ИПΣ называется тавтологией в ИПΣ, если она получается из формулы φ исчисления высказываний, доказуемой в исчислении высказываний, путем замены всех ее пропозициональных переменных x1,…,xn на формулы ψ1,…,ψn ИПΣ соответственно. Формулу φ при этом называют основой тавтологии.
Утверждение 1. Любая тавтология φ в ИПΣ доказуема в ИПΣ.
Формулы φ и ψ ИПΣ называются пропозиционально эквивалентными, если φ→ψ и ψ→φ – тавтологии. Формулы φ и ψ ИПΣ называются эквивалентными (обозначаем φ≡ψ), если ⊢φ→ψ и ⊢ψ→φ.
Следствие 1. Если φ и ψ ‑ пропозиционально эквивалентные формулы ИПΣ, то φ и ψ ‑ эквивалентные формулы ИПΣ.
Теорема 1(о дедукции). Пусть φ1,…,φm,φ,ψ – формулы ИПΣ. Тогда φ1,…,φm,φ⊢ψ φ1,…,φm,⊢φ→ψ.
Следствие 2. Пусть φ и ψ ‑ формулы ИПΣ. Следующие условия эквивалентны:
1) φ≡ψ;
2) φ⊢ψ и ψ⊢φ.