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

Как и в случае исчисления высказываний, при построении исчисления предикатов недостаточно указать лишь способ записи формул. Необходимо задать еще правила преобразования формул, выражаемые аксиомами. В число аксиом исчисления предикатов включаются все 11 аксиом исчисления высказываний.

А1: A-> (B ->A);

A2: ((A-> (B ->C)) -> ((A->B) -> (A->C)));

A3: A/\ B ->A;

A4: A/\ B ->B;

A5: A -> (B -> (A /\ B));

A6: A -> (A\/ B);

A7: B -> (A\/ B);

A8: (A->C) -> ((B-> C) -> ((A \/ B) -> C));

A9: -A -> (A->B);

A10: (A ->B) -> ((A-> -B) -> -A);

A11: A \/ -A.

Первые четыре группы аксиом представляют собой не что иное, как аксиомы исчисления высказываний. К ним добавляются еще две новые аксиомы, составляющие группу V. Этим и исчерпывается система аксиом исчисления предикатов.

1. Для любого xA -> A[t/x],

2. A[t/x] -> существует xA,

где A[t/x] — формула, полученная в результате подстановки терма t вместо каждой свободной переменной x, встречающейся в формуле A.

Правил вывода 2:

Modus ponens: A, A->B делить на / B

Правило обобщения A делить на / для любого x A

Нетрудно видеть, что каждая выводимая формула исчисления предикатов является в то же время и тождественно истинной в наивном теоретико-множественном смысле. Во-первых, очевидно, что аксиомы исчисления предикатов тождественно истинны. Во-вторых, применение правил вывода исчисления предикатов к тождественно истинным формулам приводит к тождественно истинным формулам. Это очевидно для правила заключения. Для правил переименования свободных и связанных переменных это также очевидно.