Формулы логики первого порядка
Целью параграфа является введение понятия, вынесенного в заголовок параграфа. В принципе это делается так же, как и в логике высказываний, т.е. сначала вводится понятие атомарной формулы, а затем формулы. Только с определением атомарной формулы в случае логики первого порядка ситуация несколько сложнее.
Будем исходить из следующих трех множеств: F,R,V. Элементы множества F – символы (или имена) функций, элементы R – символы (или имена) предикатов, элементы множества V – переменные. Будем считать, что каждому символу функции и предиката поставлено в соответствие натуральное число или ноль – местность (т.е. число аргументов) этого символа. Допускаются нульместные символы функций, которые называются константами, и нульместные символы предикатов (последние будут играть роль атомарных формул логики высказываний). Объединение F и R будем называть сигнатурой. Сигнатуру заранеее фиксировать не будем, она будет определяться содержанием решаемой задачи. Множество V предполагается бесконечным, для обозначения его элементов будут использоваться, как правило, буквы x,y,z,u,y,w с индексами и без них.
В примерах, приведенных выше, мы видели, что для записи предикатов использовались арифметические выражения: 2x, x+y, – x2. Аналогом арифметического выражения в логике служит понятие терма.
Определение. Термом называется
1) переменная и константа;
2) выражение вида f(t1,…,tn), где t1,…,tn – термы, а f – n-местный функциональный символ.
Можно сказать, что терм – выражение, полученное из переменных и констант с помощью символов функций.
Определение. Атомарной формулой называется выражение вида r(t1,…,tn), где t1,…,tn – термы, r – символ n-местного предиката.
Примерами атомарных формул являются выражения x£y2+1, |x-y|<z, x делит нацело y-3.
Определение. Формулой логики первого порядка называется
1) атомарная формула,
2) выражения вида (F)&(G), (F1)Ú(G), Ø(F), (F)®(G),(F)«(G), ("v)(F), ($v)(F), где F и G – формулы логики предикатов, v – переменная.
Формула F в двух последних выражениях называется областью действия квантора по переменной n.
К соглашениям о приоритете операций, принятом в логике высказываний, добавим следующее: кванторы имеют одинаковый приоритет, который больше приоритета всех связок.
Определение. Вхождение переменной в формулу называется связанным, если переменная стоит непосредственно за квантором или входит в область действия квантора по этой переменной. В противном случае вхождение называется свободным.
Например, в формуле
F=t(x)&("y)[s(x,y)®($x)(r(x,y)Út(y))]
Первое и второе вхождение переменной x свободны, третье и четвертое связаны. Все вхождения переменной y связаны.
Определение. Переменная называется свободной в формуле, если существует хотя бы одно свободное вхождение переменной в формулу.
Формула F из предыдущего примера имеет одну свободную переменную x.
Если x1,…,xn – все свободные переменные формулы F, то эту формулу будем обозначать через F(x1,…,xn). Это обозначение будем применять и в том случае, когда не все переменные из x1,…,xn являются свободными в F.
Как и в логике высказываний. В логике первого порядка вводится понятие подформулы. Соответствующее определение получится из определения подформулы из §2 темы 1 добавлением фразы: «Подформулами формул ("v)(F) и ($v)(F) являются они сами и все подформулы формулы F».