Система аксиом для исчисления предикатов

Аксиомы теории К разбиваются на два класса: логические аксиомы и собственные (или нелогические) аксиомы.

Логические аксиомы: каковы бы ни были формулы А. В и теории К, следующие формулы являются логическими аксиомами теории К:

(1) А → (В→А)

(2) (А → (В→β)) → ((А → В)→(А→β));

(3) (˥ В→˥А) →((˥ В→А) →В);

(4) ∀ х_iА (х_i) →А(t), где А (х_i) есть формула теории К и t есть терм теории К, свободный для х_i, и тогда мы получаем аксиому ∀ х_iА (х_i) →А(х_i).

(5) ∀ х_i(А→В) →(А→ ∀ х_i В), если формула А не содержит свободных вхождений х_i.