Аксиоматическая теория и правила вывода составляют исчисления предикатов.

Символами исчисления предикатов или алфавитом исчисления пре­дикатов являются символы предметных переменных, символы предика­тов, логические символы (отрицание и импликация), символы кванторов, а также скобки и запятая.

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

Аксиомы исчисления предиката.

Пусть А, В и С - любые формулы.

Аксиома 1. А→ (В →А).

Аксиома 2. (А → (В → С)) → ((А → В) → (А → С)).

Аксиома 3. ( → ) →(( → А) → В).

Аксиома 4. ( х_i)А(х_i) → А(х_i), где формула А(х_i) не содержит перемен­ной x_i.

Аксиома 5. A(x_i) → ( x_j)A(x_j), где формула А(x_i) не содержит перемен­ной x_j.

Правила вывода исчисления предикатов.

(1) Пусть (А(х) → В) и В не содержит переменной х, тогда

(((( x)А(х)) → В) .

Это правило связывания квантором существования.

(2) Пусть В → А(х) и В не содержит переменной х, тогда

(В → (( х)A(x))).

Это правило связывания квантором общности.

(3) Связанную переменную формулы В можно заменить другой пе­ременной, не являющейся свободной в В. Это правило переименования связанной переменной.