2.3.7 Теоремы о логическом следствии

Определение 18.Выводом формулыGиз формулU₁, U₂,…, U_nназывается последовательность формулF₁, F₂,…, F_nтакая, чтоF_m есть G, а любаяF_iлибо аксиома, либо одна из формулU_i, либо формула, непосредственно выводимая из предшествующих ей формул.

Вследствие законов ассоциативности скобки в выражениях, связанных отношениями дизъюнкции и конъюнкции могут быть опущены, при этом выражение F₁ Ú F₂ Ú…Ú F_n называется дизъюнкцией формулF₁, F₂,…, F_n, а выражениеF₁ Ù F₂ Ù…Ù F_n называется конъюнкцией формулF₁, F₂,…, F_n.

Теорема 1.Пусть даны формулыF₁, F₂,…, F_n и формула G. G есть логическое следствие F₁, F₂,…, F_n тогда и только тогда, когда формула ((F₁ Ù F₂ Ù…Ù F_n)®G) общезначима.

Теорема 2.Пусть даны формулыF₁, F₂,…, F_n и формула G. G есть логическое следствие F₁, F₂,…, F_n тогда и только тогда, когда формула (F₁ Ù F₂ Ù…Ù F_n ÙØG) противоречива.

Замечание.

Для того чтобы доказать, что данная формула является тавтологией, достаточно доказать, что ее отрицание является противоречием:

Ø((F₁ Ù F₂ Ù…Ù F_n)®G)=

Ø(Ø(F₁ Ù F₂ Ù…Ù F_n) Ú G)=

(F₁ Ù F₂ Ù…Ù F_n) Ù ØG).

Теоремы 1 и 2 очень важны. Из них следует, что доказательство логического следствия одной формулы из конечного множества формул эквивалентно доказательству того факта, что некоторая связанная с конечным множеством формула общезначима или противоречива.

2.3.8 Предваренные (пренексные) нормальные формы исчисления предикатов.

Определение 19.Литерал (литера)есть атом или отрицание атома.

Определение 20. ФормулаFнаходитсяв конъюнктивной нормальной форметогда и только тогда, когдаFимеет вид:F₁ Ù F₂ Ù…Ù F_n,n >=1, где каждая изF₁, F₂,…, F_nестьдизъюнкция литералов.

Определение 21. ФормулаFнаходитсяв дизъюнктивной нормальной форметогда и только тогда, когдаFимеет вид:F₁ Ú F₂ Ú…Ú F_n,n >=1, где каждая изF₁, F₂,…, F_nестьконъюнкция литералов.

В логике высказываний были введены две нормальные формы – КНФ и ДНФ. В логике предикатов также существуют нормальная форма - ПНФ, которая используется для упрощения процедуры доказательства общезначимости или противоречивости формул.

Определение 22:Формула F логики предикатов находится в предваренной нормальной форме, тогда и только тогда, когда формула F имеет вид:

(K₁x₁)…(K_nx_n) (M), где каждое (K_ix_i), i = 1,…,n, есть или ("x_i) или ($x_i), и M есть формула, не содержащая кванторов. (K₁x₁)…(K_nx_n) называется префиксом, а M – матрицей формулы F.

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

Шаг 1.Используем законы законы 1 и 2 исчисления высказываний для того, чтобы исключить логические связки импликации и эквивалентности.

Шаг 2.Многократно используем закон двойного отрицания, законы де Моргана и законы 5 и 6 исчисления предикатов, чтобы внести знак отрицания внутрь формулы.

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

Шаг 4.Используем законы 1, 2, 3, 4, 7,8, 9 и 10 до тех пор, пока все кванторы не будут вынесены в самое начало формулы, чтобы получить ПНФ.

Пример 6. Приведем формулу ("x) P(x) ® ($x) Q(x) к ПНФ:

("x) P(x) ® ($x) Q(x)=Ø(("x) P(x))Ú ($x) Q(x)(по закону 1 логики высказываний)

=($ x)( Ø P(x)) Ú ($ x) ) Q(x)( по закону 5 логики предикатов)

=($ x)( Ø P(x) Ú Q(x))( по закону 8 логики предикатов), что и есть ПНФ исходной формулы.

Пример 7. Привести формулу (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)(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))(по закону 6 законам де Моргана)

= (x)(y)(z)(u) ( P(x, z)   P(y, z))  Q(x, y, u))(закон 3)