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

1. Язык исчисления предикатов. В качестве алфавита исчисления предикатов возьмем то же самое множество Ҩ = σ U X U O, которое служило алфавитом при определении формул алгебры предикатов. За элементами множества σ, Х и О сохраним те же самые обозначения и названия, хотя здесь на все буквы алфавита Ҩ мы должны пока смотреть просто как на символы, не имеющие какого-либо смысла. Например, символ операции f здесь не обозначает какую-либо конкретную операцию, определенную на каком-либо конкретном множестве. То же относится и к символам предикатов. Термины же «символ операции» и «символ предиката» объясняются тем, что в приложениях исчисления предикатов к конкретным математическим теориям мы будем трактовать их (интерпретировать) как операции и предикаты на конкретном множестве. Аналогично, предметным переменным будут придаваться значения из этого множества.

Понятия терма и формулы сигнатуры σ в исчислении предикатов определяются буквально так же, как в алгебре предикатов.

Равенство формул, как и в алгебре предикатов, будем обозначать знаком «=». Из множества всех формул ниже особую роль будут играть формулы, не содержащие свободных вхождений предметных переменных. Они называются замкнутыми формулами, или предложениями.

Таким образом, нами полностью определен язык исчисления предикатов 1-й ступени сигнатуры σ. Обозначим его буквой α. Для формул языка α будут использоваться те же правила сокращения скобок, что и в алгебре предикатов.

Заметим, что кроме исчисления предикатов 1-й ступени в математической логике и в теории моделей рассматриваются исчисления предикатов и логические языки 2-й ступени. В их алфавиты кроме перечисленных выше символов вводятся также символы функциональных и предикатных переменных, и кванторы ,  могут навешиваться не только на предметные переменные, но и на функциональные переменные и предикатные переменные.

2. Аксиомы и правила вывода исчисления предикатов. При построении исчисления предикатов с определенным выше языком α аксиомы и правила вывода могут выбираться по-разному. Мы выберем следующую систему аксиом. Аксиомы этой системы по используемым в них логическим операциям делятся на пять подсистем, которые мы занумеруем римскими цифрами. В подсистемах I – IV под буквами А, В, С понимаются произвольные формулы языка α, ограничения на формулы системы V указываются в формулировках соответствующих аксиом (табл.9.2), где A(x) — формула, содержащая свободные вхождения переменной х, A(t) — формула, полученная заменой в A(x) всех свободных вхождений x термом t, удовлетворяющим условию: ни одно свободное вхождение х в A(x) не находится в области действия квантора по какой-либо переменной, содержащейся в t. При этом условии говорят, что терм t свободен для х в формуле A(x). Далее аксиомы будут обозначаться римскими цифрами с индексами. Например, II₃ — аксиома 3 из подсистемы II.

Таблица 9.2

I	1	A  (B  A)
	2	(A  (B  C))  ((A  B)  (A  C))
II	1	A  B  A
	2	A  B  B
	3	(A  B)  ((A  C)  (A  B  C))
III	1	A  A  B
	2	B  A  B
	3	(A  C)  ((B  C)  (A  B  C))
IV	1
	2
	3
V	1	x A(x)  A(t)
	2	A(t)  x A(x)

Сформулируем теперь правила вывода. Каждое такое правило позволяет из некоторого множества исходных формул получать новые формулы. Поэтому правило вывода записывают обычно в виде «дроби», у которой в «числителе» находятся исходные формулы, а в «знаменателе» — вновь получаемая формула.

I. Правило заключения:

,

где А, В — любые формулы языка α.

II. Правило -введения:

,

где А содержит, а В не содержит свободные вхождения переменной х.

III. Правило -удаления:

,

где А, В — формулы, удовлетворяющие тем же условиям, что и в правиле II.

Формула, находящаяся в «знаменателе» правила вывода, называется непосредственным следствием формул «числителя».

Заметим, что, подставляя в аксиому I₁ вместо А, В произвольные формулы, мы получим бесконечное множество формул. Таким образом, запись аксиомы I₁ является, по существу, схемой, по которой можно получать формулы. То же можно сказать об остальных аксиомах и о формулах из правил вывода.

Определив язык α и аксиомы с правилами вывода, мы определили тем самым логическое исчисление, называемое исчислением предикатов 1-й ступени сигнатуры σ. Меняя σ, т. е. меняя множество формул и сохраняя схемы аксиом и правил вывода, мы будем получать другие исчисления предикатов. В дальнейшем язык α будем считать фиксированным, и соответствующее логическое исчисление будем обозначать той же буквой α.