09.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). Далее аксиомы будут обозначаться римскими цифрами с индексами. Например, II3 — аксиома 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.

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

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

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

< Предыдущая		Следующая >