Формулы, общезначимость.
Формулы F и G назовем равносильными, если при любой интерпретации их истинностные значения совпадают.(I)F(I)=G(I).
Отметим, что все равносильные пары формул, приведенные в логике высказываний, сохраняются и здесь.
1. (Qx)F[x] -дизъ- G -экв- (Qx)(F[x] -дизъ- G)
2. (Qx)F[x]<*>G -экв- (Qx)(F[x]<*>G)
3. -экв- (x)
4. -экв- (x)
5. (х)F[x]<*>(x)H[x] -экв- (x)(F[x]<*>h[x])
6. (x)F[x] -дизъ- (x)H[x] -экв- (x)(F[x] -дизъ- H[x])
7. (Q1x) F[x] -дизъ- (Q2x) H[x] -экв- (Q1x) (Q2z) (F[x] -дизъ- H[z])
8. (Q3x) F[x]<*>(Q4x) H[x] -экв- (Q3x) (Q4z) (F[x]<*>H[z]),
Q1, Q2, Q3, Q4, - или
Замечание: если Q1 = Q2 = , а Q3 = Q4 = , то переменные можно не переименовывать.
Формула G является логическим следствием формул F1, F2,…, Fn тогда и только тогда, когда для каждой интерпретации I, если
F1ÙF2Ù…ÙFn истина в I, то G так же истинно на I.
Замечание 1. логика предикатов является расширением логики высказываний. Если формула в логике предикатов не содержит
переменных и кванторов, то ее можно рассматривать просто как формулу в логике высказываний.
Замечание 2. справедливы теоремы:
1. G логическое следствие F1, F2,…, Fn, тогда и только тогда, когда F1ÙF2Ù…ÙFn->G -экв- И – общезначимость.
2. G логическое следствие F1, F2,…, Fn, тогда и только тогда, когда F1ÙF2Ù…ÙFn<*>- противоречивость.
Доказать общезначимость формулы по интерпретации невозможно, так как количество интерпретаций бесконечно.
Можно предложить два направления решения этой проблемы:
• Выбор определенной интерпретации;
• Приведение к определенному виду.
Формула F в логике первого порядка находится в предваренной нормальной форме, если она имеет вид (Q1x1)(Q2x2)…(Qnxn)M, где
Qixi : х или х, а М – формула не содержащая кванторов.
(Q1x1)(Q2x2)…(Qnxn) называется префиксом, М – матрицей формулы F.
Любую формулу преобразованиями можно привести к предваренной форме.
Алгоритм преобразования формулы в предваренную нормальную форму:
шаг 1: избавиться от -> и <->
шаг 2: -экв- F -экв- и -экв-
, знак отрицания проносится внутрь формул.
Шаг 3: переименовываем связанные переменные, если это необходимо.
Шаг 4: используя равносильности, выносим кванторы в самое начало формул.
Получаем формулу, равносильную исходной и находящуюся в проверенной нормальной форме.
Можно построить аксиометрическое исчисление предикатов: определив формально алфавит и формулы, добавив к аксиомам и правилам
вывода исчисления высказываний две аксиомы:
• (x)F(x)->F(t)
• F(t)->(x)F(x), где t – не содержит переменной х.
Правила вывода переменной х:
1. F->G(x) правило введения квантора общности.
F->(x)G(x)
2. G(x)->F правило введения квантора существования.
(x)G(x)->F
Замечание. F не зависит от х.