Среди множества тождественно истинных формул существует подмножество, являющееся аксиомами исчисления предикатов, облегчающие процесс эквивалентных преобразований в процессе логического вывода. Ниже приведён набор наиболее распространённых аксиом (правил) для исчисления предикатов: 1) правило обобщения (или введения квантора общности): “если F1(t) F2(x) – выводимая формула и F1(t) не содержит свободной переменной x, то F1(t) x(F2(x)) также выводима”__(F1(t) F2(x))__(F1(t) x(F2(x))) 2) правило удаления квантора общности: “если каждая предметная переменная входит в предикат F(x), то можно ввести терм t, свободный от предметной переменной x, но удовлетворяющий требованиям предиката F(t)”x(F(x))F(t) 3) правило конкретизации: “если F1(x) F2(t) выводимая формула и F2(t) не содержит свободных вхождений x, то x(F1(x) F2(t)) также выводима”__F1(x) F2(t)__x(F1(x) F2(t)) 4) правила введения квантора существования: “если терм t входит в предикат f(t), то существует по крайней мере одна предметная переменная x, удовлетворяющая требованиям этого предиката F(x)”__F(t)__x(F(x)) 5) правила смены кванторов_x(F(x))_ _x(F(x))_x(F(x)) ; x(F(x)) 6) правила переноса кванторов влево (формирование префикса) (их там очень много…)Приведённый набор правил облегчает эквивалентные преобразования формул в процессе логического вывода. В исчислении предикатов, как и в исчислении высказываний приняты 3 схемы формального вывода: заключения, теорема и противоречие. Вывод заключения из множества посылок записывается также, как и в исчислении высказываний (см. вопрос 6).