SHPORA.net :: PDA | |
Main FAQ гуманитарные науки естественные науки математические науки технические науки Формулы, общезначимость. Формулы 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 не зависит от х. |