4) Законы де Моргана для кванторов

(x)Р(х)=( x)Р(х),

(x)Р(х)=(x)Р(х).

Процедура преобразования прозвольной формулы логики первого порядка в ПНФ осуществляется по следующему алгоритму:

Шаг 1. Используем законы

F G=(F G)(G F),

F G=FG,

чтобы исключить логические связки и .

Шаг 2. Повторно используем закон

(F)=F,

законы де Моргана

(FG)= FG,

 (FG)= FG

и законы

 ((x)F(x))=(x) F(x),

 ((x)F(x))=(x) F(x),

чтобы подвести знаки отрицания к предикатным символам.

Шаг 3. Переименовываем связанные переменные, если это необходимо.

Шаг 4. Используем законы

(Qx)F(x)G=(Qx)(F(x)G),

(Qx)F(x)G=(Qx)(F(x)G),

(где (Qх) есть или или )

(x)F(x) (x)H(x)=( x)(F(x)H(x)),

(x)F(x)  (x)H(x)=(x)(F(x)H(x)),

(x)F(x)  (x)H(x)=( x)( y)(F(x)H(y)),

(x)F(x) (x)H(x)=(x)(y)(F(x)H(y)),

чтобы вынести кванторы в самое начало формулы для получения ПНФ.

Рассмотрим примеры решения типичных упражнений и задач по теме:

1. Привести формулу (x)Р(х) (x)Q(x) к ПНФ.

Решение.

(x)P(x) (x)Q(x) = ((x)P(x))  ( x)Q(x)=

(x) P(x) (x)Q(x)=(x)(P(x)Q(x)).

Следовательно, предваренная нормальная форма формулы (x)P(x)(x)Q(x) - это (x)(P(x)Q(x)).

2. Получить ПНФ для формулы

(x)(y)((z)(P(x,z)P(y,z)) ( u)Q(x,y,u)).

Решение.

(x)( y)((z)(P(x,z)P(y,z)) ( u)Q(x,y,u))=

=(x)( y)( (z)(Px,z) P(y,z)) (u)Q(x,y,u))=

=(x)(y)((z)(P(x,z)  P(y,z))  ( u)Q(x,y,u))=

=(x)( y)( z)( u)( P(x,z)  P(y,z) Q(x,y,u)).

Следовательно, последняя формула есть ПНФ первой.

3. Покажем приложение логики первого порядка к решению задач. Пусть даны две аксиомы

А₁: (x)(ЧЕЛОВЕК(х) СМЕРТЕН(х)).

А₂: ЧЕЛОВЕК(Конфуций).

Из А₁ и А₂ получить, что Конфуций смертен, т.е. показать, что СМЕРТЕН(Конфуций) есть логическое следствие А₁ и А₂.

Доказательство. Мы имеем

А₁А₂: (x)(ЧЕЛОВЕК(х) СМЕРТЕН(х)) ЧЕЛОВЕК(Конфуций).

Если А₁А₂ истинна в интерпретации I, то обе формулы А₁ и А₂ истинны в I. Так как (ЧЕЛОВЕК(х) СМЕРТЕН(х)) истинна для всех х, то, когда х заменяется на “Конфуций”, (ЧЕЛОВЕК(Конфуций) СМЕРТЕН(Конфуций)) истинна в I, т.е. ЧЕЛОВЕК(Конфуций)СМЕРТЕН(Конфуций) истинна в I. Однако ЧЕЛОВЕК(Конфуций) ложна в I. Следовательно, СМЕРТЕН(Конфуций) должна быть истинной в I. Следовательно, мы показали, что СМЕРТЕН(Конфуций) истинна в I, если (А₁А₂) истинна в I. По определению СМЕРТЕН(Конфуций) есть логическое следствие А₁ и А₂.

Контрольные вопросы и задания по теме:

1. Определение ПНФ.

2. Эквивалентность формул в логике первого порядка.

3. Законы логики первого порядка. Доказательство.

4. Тождества для кванторов. Доказательство.

5. Алгоритм преобразования формул логики первого порядка в ПНФ.

6. Преобразовать следующие формулы в ПНФ:

6.1. (x)(P(x) (y)Q(x,y));

6.2. (x)( ((y)P(x,y) ((z)Q(z) R(x)));

6.3. (x)(y)((z)P(x,y,z) ((u)Q(x,u) (v)(y,v))).

7. Даны следующие утверждения:

F₁: Каждый студент честен.

F₂: Джон нечестен.

Из утверждений F₁ и F₂ получить, что Джон не студент.

#Тема: Скулемовские стандартные формы. Доказательство логических следствий в логике первого порядка

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

Мы уже рассмотрели процедуры решения задач в ЛВ и логике первого порядка путем доказательства теорем. Однако чрезвычайно важны вопросы, связанные с поиском этих доказательств. Наиболее широко используются в настоящее время методы поиска доказательства теорем, предложенные Эрбраном в 1930 г. и Робинсоном в 1965 г. (метод резолюций). Общим для этих процедур является то, что они доказывают опровержение формулы, т.е. вместо общезначимости исходной формулы доказывают противоречивость ее отрицания. Эти процедуры применяются к формулам, представленным в так называемой скулемовской стандартной форме (ССФ).

Основные идеи ССФ :

1. Любая формула логики первого порядка может быть сведена к ПНФ, в которой матрица не содержит никаких кванторов, а префикс есть последовательность кванторов.

2. Поскольку матрица не содержит кванторов, она может быть сведена к КНФ.

3. Сохраняя противоречивость формулы, в ней можно элиминировать кванторы существования путем использования скулемовских функций.

Формула F имеет вид: