Исчисление предикатов - это аксиоматическая теория, символами которой являются, по существу, те же символы, что и в логике предикатов:
1) символы предметных переменных: x1, x2,…;
2) символы предикатов P, Q, R, A, …;
3) логические символы Ø, É;
4) символы кванторов; ", $ ;
5) скобки и запятая.
Сформулированное в разделе 4.1 определение формулы остается в силе и для исчисления предикатов ( с той лишь разницей, что мы употребляем только два логических символа: Ø и É; остальные связки можно определить через эти).
Аксиомы исчисления предикатов. Каковы бы ни были формулы A и B, следующие формулы являются аксиомами (при этом не должно нарушаться определение формулы):
A1. AÉ(BÉA);
A2. (AÉ(BÉC))É((AÉB)É(AÉC));
A3. (ØBÉØA)É((ØBÉA)ÉB).
A4. "x A(x) É A(y), где формула A(x) не содержит переменной y.
A5. A(x) É $y A(y), где формула A(x) не содержит переменной y.
Правила вывода исчисления предикатов:
1. Правило modus ponens;
2. Правило связывания квантором общности: если BÉA(x), то BÉ"xA(x), где формула B не содержит переменной x.
3. Правило связывания квантором существования: если A(x)ÉB, то $xA(x)ÉB, где формула B не содержит переменной x.
4. Правило переименования связанной переменной. Связанную переменную формулы A можно заменить (в кванторе и во всех вхождениях в области действия квантора) другой переменной, не являющейся свободной в A.
Всякая формальная теория, которая имеет в качестве своих аксиом приведенные выше пять аксиом исчисления предикатов, называется формальной теорией первого порядка.
Многочисленные обычные теории такого рода являются по существу вариантами исчисления предикатов первого порядка, дополненного одной или несколькими аксиомами и/или правилами вывода.
Термин "теория первого порядка" означает, что в их формулах действие квантора может распространяться только на предметные переменные. К теориям второго порядка относятся такие формальные теории, в которых действия кванторов может распространяться и на сами предикаты. В формальных теориях более высокого порядка действие кванторов может распространяться и на предикаты от предикатов и т. д.
В исчислении предикатов первого порядка любая теорема является общезначимой формулой. Нам понадобятся несколько лемм.
Лемма 5.5 (ослабленная теорема о дедукции). Если G,A|―B и существует вывод в исчислении предикатов, построенный с применением только правила modus ponens, то G|―AÉB.
Доказательство этой леммы опустим [23, стр. 70].
Лемма 5.6. Если BÉA(x), где формула B не содержит переменной x, является общезначимой, то формула B É "xA(x) так же общезначима.
Доказательство. Пусть x1, x2,..., xn -все свободные переменные формулы BÉ"xA(x). Пусть задана произвольная интерпретация с множеством M и пусть <a1, a2,..., an>, aiÎM, 1 £ i £ n, - произвольный набор значений свободных переменных формулы BÉ"xA(x).
Случай 1. Формула B при этих значениях предметных переменных имеет значение И. Поскольку формула BÉA(x) - общезначима, то для любого элемента aÎM формула A(x) на наборе <a, a1, a2,..., an> имеет значение И (переменная x принимает значение a). Тогда "xA(x) - общезначимая формула и, следовательно, BÉ"xA(x) - так же общезначимая формула.
Случай 2. Формула B при значениях предметных переменных <a1,a2,...,an> имеет значение Л. В силу определения импликации тогда формула BÉ"xA(x) имеет значение И.
Лемма 5.7. Если A(x)ÉB, где формула B не содержит переменной x, - общезначима, то формула $xA(x)ÉB - так же общезначима.
Доказательство. Пусть x1,x2,...,xn - все свободные переменные формулы $xA(x)ÉB. Тогда x, x1, x2,..., xn - список всех свободных переменных формулы A(x)ÉB. Пусть задана произвольная интерпретация с множеством M и пусть <a1, a2,..., an>, aiÎM, 1 £ i £ n, - произвольный набор значений свободных переменных формулы $xA(x)ÉB.
Случай 1. Формула B при значениях предметных переменных <a1,a2,...,an> имеет значение И. В силу определения импликации, тогда формула $xA(x)ÉB имеет значение И.
Случай 2. Формула B при значениях предметных переменных <a1,a2,...,an> имеет значение Л. Поскольку формула A(x)ÉB - общезначима, то для любого элемента aÎM формула A(x) на наборе <a, a1, a2,..., an> имеет значение Л (переменная x принимает значение a). Тогда $xA(x) имеет значение Л на наборе <a1,a2,...,an> и, следовательно, $xA(x)ÉB имеет значение И.