Лекция 7

примером неразрешимой формальной системы. В доказанной А. Чёрчем теореме говорится об

отсутствии эффективной процедуры при решении вопроса относительно произвольной формулы исчисления предикатов первого порядка, является ли эта формула теоремой. Однако при доказательстве заключительного утверждения (цели) из начальной системы аксиом, посылок мы придерживаемся правила, что если все аксиомы и посылки принимают истинностное значение И, то и заключительное утверждение также принимает значение И. Из-за этого ограничения иногда исчисление предикатов первого порядка и называют полуразрешимым.

Гостиная находится рядом с кухней. Выстрел раздался на кухне и

мог быть услышан во всех близлежащих комната. Дворецкий, обладающий хорошим слухом, сказал, что он не слышал выстрела. Детектив должен доказать, что если горничная сказала правду, то дворецкий солгал.
P  Q: если горничная сказала правду, то дворецкий был в гостиной.
Q  R: если дворецкий был в гостиной, то он находился рядом с кухней.
R  L: если дворецкий был рядом с кухней, то он слышал выстрел.
M  L: если дворецкий сказал правду, то он не слышал выстрела.
Требуется доказать, что если горничная сказала правду, то дворецкий солгал, т.е. P  M.
Представим посылки в КНФ: (P  Q) & (Q  R) & (R  L) & (M  L).
Аналогично заключение: P  M.
Задавая интерпретации, в которых истинны посылки, нетрудно обнаружить, что будет истинно и заключение. Желающие могут выписать истинностную таблицу, чтобы в этом убедиться.

Fn и G, то говорят, что формула G является логическим

следствием F1, F2, …, Fn (или G логически следует из F1, F2, …, Fn) тогда и только тогда, когда для любой интерпретации I, в которой F1 & F2 & … & Fn истинна, G также истинна.
Для обозначения логического следования формулы G из посылок F1, F2, …, Fn будем писать F1, F2, …, Fn ╞ G. Символ ╞ есть некоторое отношение между формулами, причем, если посылки соединены знаком &, то имеет место двуместное отношение: F1 & F2 & … & Fn ╞ G.

теоремы, связывающие понятия логического следования с понятиями общезначимости и противоречивости.
Теорема1.

Даны формулы F1, F2, …, Fn и G. Формула G является логическим следствием формул F1, F2, …, Fn тогда и только тогда, когда формула F1 & F2 & … & Fn  G общезначима, т.е. ╞ F1 & F2 & … & Fn  G. Формула F1 & F2 & … & Fn  G называется теоремой, а G называется заключением теоремы.
Теорема 2. Даны формулы F1, F2, …, Fn и G. Формула G является логическим следствием формул F1, F2, …, Fn тогда и только тогда, когда формула F1 & F2 & … & Fn & G противоречива.
Таким образом, факт, что данная формула является логическим следствием конечной последовательности формул, сводится к доказательству общезначимости или противоречивости некоторой формулы. Следовательно, имеется полная аналогия при выводе заключения теоремы из множества аксиом или посылок в формальной системе, и многие проблемы в математике могут быть сформулированы как проблемы доказательства теорем.
Обозначим общезначимую формулу через , а противоречивую – через .

дворецкий), и покажем, что формула (P  Q) & (Q

 R) & (R  L) & (M  L)  (P  M) общезначима.
Действительно, [(P  Q) & (Q  R) & (R  L) & (M  L)]  P  M = = P & Q  Q & R  R & L  M & L  P  M = = Q  R  L  M  P  M = .
Аналогично можно показать противоречивость формулы (P  Q) & (Q  R) & (R  L) & (M  L) &  (P  M) = .
Для доказательства общезначимости, или противоречивости формул исчисления высказываний используем процедуры приведения к нормальным формам – ДНФ и КНФ.

в виде так называемой нормальной формы.
Атом или его отрицание будем

называть литерой.
Говорят, что формула логики высказываний В представлена в конъюнктивной нормальной форме (КНФ) тогда и только тогда, когда она имеет форму B = B1 & B2 & … & Bm, где каждая из Bi (i =1,m ) есть дизъюнкция литер. Например, В = (Х1  Х2) & (Х1  Х2  Х3) & Х3 представлена в КНФ.
Аналогично говорят, что формула логики высказываний В представлена в дизъюнктивной нормальной форме (ДНФ) тогда и только тогда, когда она имеет форму A = A1  A2  …  An, где каждая из Ai (i = 1,n ) есть конъюнкция литер. Например, A = (Х1 & Х2 & Х3)  (Х1 & Х2)  Х3 представлена в ДНФ.

преобразована в нормальную форму с помощью следующего алгоритма.
Шаг 1. А 

В = (А  В) & (В  А).
А  В = А  В.
Шаг 2. А = А.
законы Де-Моргана.
Шаг 3. А  (В & С) = (А  В) & (А  С) (для КНФ).
А & (В  С) = А & В  А & С (для ДНФ).
 
Пример 1. Получим КНФ для формулы (A  (B  C))  D.
(A  (B  C))  D = (A  B  C)  D = (A  B  C)  D =
(A & B & C)  D = (A  D) & (B  D) & (C  D). 
Пример 2. Получим ДНФ для формулы (A & B) & (A  B).
(A & B) & (A  B) = (A  B) & (A  B) = ((A  B) & A)  ((A  B) & B) = (A & B)  (B & A).

возрастут правительственные расходы (R) или возникнет безработица (В). Если правительственные

расходы не возрастут, то налоги будут снижены (N). Если налоги будут снижены и капиталовложения останутся постоянными, то безработица не возникнет. Капиталовложения останутся постоянными. Следовательно, правительственные расходы возрастут.
Запишем формальное представление утверждения.
F1: KRB
F2: R N
F3: N&K  B
F4: K
--------------------------
G: R

преобразуем ее к виду:
F1&F2&F3&F4 G = (F1&F2&F3&F4)G = F1F2F3F4 G
Докажем

общезначимость выражения
(KRB)(R N)(N&K  B)К R
Приведём формулу к нормальной форме:
( KRB)(R N)((N&K)  B)К R =
= K&R &B   R& N  N&K &B К R =
= R &B   R& N  N&K &B К R =
= R &B  R& N  N& B К R = BR&N  N&BКR =
= BN  N&BКR = BN  BКR = И N КR = И
(к подчеркнутым частям формулы многократно применяем тождество
XX&Y= XY,
В B=И).

F1&F2&F3&F4 &G :
(KRB)&(R N)&(N&K  B)& К & R=
= (

K RB)&(R N)&(N  K B)& К & R=
= ( K & К  R & К B & К)&(R &R  N&R) &(N  K B)=
=(R & К B & К)& N&R &(N  K B)=
=(R & К &R B & К &R)& (N & N  K & N  B & N)=
= B & К &R& (K & N  B & N)=
(B & К &R& K & N  B & К &R& B & N)=Л Л=Л
(сомножители, выделенные цветом, обращают логическое произведение в Ложь)
Легко заметить, что доказательство противоречивости выполняется гораздо легче, чем доказательство общезначимости.

для исчисления предикатов 1 порядка из двух теорем (1 и

2), как правило, применяется вторая теорема, т.е. если формула G является логическим следствием формул F1, F2, …, Fn, то надо доказать противоречивость формулы
F1 & F2 & … & Fn & G.
Так как в этой формуле заключение теоремы G опровергается, то и процедуры поиска доказательства называются процедурами поиска опровержения.
Пример.
Рассмотрим задачу. Всякое положительное целое число есть натуральное число. 5- положительное целое. Следовательно, 5- натуральное число. Формализация рассуждения:
x (Р(x)  N(x) )
P(5)___________
N(5)
где Р(х) обозначает «х –положительное целое число», N(x) – «х –натуральное число».

x (Р(x)  N(x) )&P(5)& N(5)
Построим равносильную

формулу: x (Р(x)  N(x) )&P(5)& N(5)
Данная формула верна для всех х, следовательно, она будет верна и для х=5. Получим: (Р(5)  N(5) )&P(5)& N(5) =
= Р(5) &P(5)& N(5)  N(5) &P(5)& N(5) = Л  Л = Л. Логическое следствие заключения из посылок доказано.
Попробуем доказать логическое следствие по теореме 1. Построим формулу x (Р(x)  N(x)) &P(5)  N(5) Выполним равносильные преобразования: ((x (Р(x)  N(x) ) &P(5) )  N(5) =
= (x (Р(x)  N(x))  Р(5)  N(5) =
= x  (Р(x)  N(x))  Р(5)  N(5)
А вот дальнейшее преобразование невозможно: из того факта, что существует х, удовлетворяющий формуле, вовсе не следует, что этот х обязательно равен 5. Далее используем только доказательства путём опровержения.

форма, называемая пренексной нормальной формой (ПНФ). Необходимость введения ПНФ будет

обусловлена в дальнейшем упрощением процедуры доказательства теорем.
Сначала рассмотрим некоторые равносильные формулы в исчислении предикатов. Напомним, что две формулы F и Ф равносильные, т.е. F = Ф, тогда и только тогда, когда истинностные значения этих формул совпадают при любой интерпретации F и Ф. Для подчеркивания факта, что переменная х входит в формулу F, будем писать F[x], хотя F может содержать и другие переменные.

x (F[x]  Ф);
x F[x] & Ф = x (F[x]

& Ф);
x F[x]  Ф = x (F[x]  Ф);
x F[x] & Ф = x (F[x] & Ф) при условии, что переменная х не входит свободно в формулу Ф. Равносильность этих формул очевидна, так как формула Ф не содержит свободно х потому не входит в область действия кванторов.
Далее имеем:
x F[x] & x Ф[x] = x (F[x] & Ф[x]),
x F[x]  x Ф[x] =  x (F[x]  Ф[x]).
Доказательство этих двух равносильностей выполните самостоятельно.
Однако x F[x]  x Ф[x]  x (F[x]  Ф[x]),
x F[x] & x Ф[x]   x (F[x] & Ф[x]).

интерпретации F[1] = И и F[2] = Л, а Ф[1] = Л и Ф[2] = И, получим в

левой части первого неравенства
x F[x]  x Ф[x]  x (F[x]  Ф[x])
значение Л, а в правой – И. Аналогично доказывается и второе неравенство x F[x] & x Ф[x]   x (F[x] & Ф[x]).

В последних двух случаях производим переименование связанных переменных, т.е.
x F[x]  x Ф[x] = x F[x]  у Ф[у] = x у (F[x]  Ф[у]), x F[x] & x Ф[x] = x F[x] & y Ф[y] = x y (F[x] &  Ф[y])
при условии, что переменная у не появляется в F[x].

предикатов находится в ПНФ тогда и только тогда, когда ее

можно представить в форме Кв1х1 Кв2х2 …Квrxr M, где Квixi, i =1,r , есть либо xi, либо xi и М – бескванторная формула. (Кв – сокращение от «квантор»)
Иногда называют Кв1х1 Кв2х2 …  Квrxr префиксом, а М – матрицей формулы F.
Например, формула
F1 = x y (Q(x, y)  P(f(x))  R(x, g(y)))
находится в ПНФ, а формула
F2 = x (P(x)  y Q(x, y)) – не в ПНФ.

. Многократно (пока это возможно) делаем замены: F  Ф = (F  Ф) & (F  Ф),

F  Ф = F  Ф. Результатом этого шага будет формула, равносильная исходной и не содержащая связок  и .
Шаг 2. Продвижение знака отрицания  до атома. Многократно (пока это возможно) делаем замены:
 F = F,
(F  Ф) = F &  Ф,
(F & Ф) = F   Ф,
x F[x] = x (F[x]),
x F[x] = x (F[x]).
Очевидно, что в результате выполнения этого шага получается формула, у которой знаки отрицания  могут стоять лишь перед атомами.
Шаг 3. Переименование связанных переменных. Многократно (пока это возможно) применяется следующее правило: найти самое левое вхождение переменной такое, что это вхождение связано (некоторым квантором), но существует еще одно вхождение этой же переменной; затем сделать замену связанного вхождения на вхождение новой переменной.

используем следующие равносильности:
Кв x F[x]  Ф = Кв x

(F[x]  Ф),
Кв x F[x] & Ф = Кв x (F[x] & Ф),
x F[x] & x Ф[x] = x (F[x] & Ф[x]),
x F[x]  x Ф[x] = x (F[x  Ф[x]),
Кв1x F[x] Кв2x Ф [x] =Кв1x Кв2y (F[x]  Ф[y]),
Кв1x F[x] & Кв2x Ф [x] = Кв1x Кв2y (F[x]& Ф[y]), где , Кв1 и Кв2 – кванторы либо , либо .
После выполнения четвертого шага формула приобретает пренексный вид:
Кв1х1 Кв2х2 … Квrxr M, где Квi, {i = 1,r }  {,}.
Таким образом, мы ограничимся формулами, имеющими пренексный вид.

называемых ‑формул, или формул, содержащих только кванторы всеобщности.
Формула F называется

‑формулой, если она представлена в ПНФ, причем кванторная часть состоит только из кванторов общности, т.е. F = x1x2…xr M,
где М – бескванторная формула.
Отсюда возникает задача устранения кванторов существования в формулах, представленных в ПНФ. Это можно сделать путем введения сколемовских функций.

Квj  {, }, , j =1, r.
Пусть Квi (1  i  r) – квантор

существования в префиксе Кв1х1  Кв2х2 … Квrxr. Если i = 1, т.е. ни один квантор общности не стоит впереди квантора существования, то выбираем константу с из области определения М, отличную от констант, встречающихся в М, и заменяем х1 на с в М. Из префикса квантор существования х1 вычеркиваем. Если перед квантором существования i стоит j1, j2, …, jm кванторов общности, то выбираем m-местный функциональный символ f, отличный от функциональных символов в М, и заменяем xi на функцию
f(xj1, xj2, …, xjm), называемую сколемовской функцией, в М. Квантор существования iхi вычеркиваем из префикса. Аналогично удаляются и другие кванторы существования в ПНФ. В итоге получаем ‑формулу, или формулу, содержащую только кванторы всеобщности.

наименьший индекс i такой, что Кв1, Кв2, …, Квi-1 все

являются кванторами , но Квi = .
Если такого i нет, то СТОП: формула F является -формулой.
Иначе Перейти к шагу 3.
Шаг 3. Если i = 1, т.е. квантор  стоит на первом месте, то вместо x1 в формулу М подставить константу с, отличную от констант, встречающихся в М, и квантор  удалить из префикса.
Если i>1 (квантору  предшествуют несколько кванторов ) то
взять новый (i –1)-местный функциональный символ fi, не встречающийся в F. Заменить F на формулу x1 x2 … xi‑1 Квi+1xi+1 …  Квrxr M[x1, x2, …, xi‑1, fi(x1, x2, …, xi‑1), xi+1, …, xr].
Шаг 4. Перейти к шагу 2.

u, v) & Q(u, w)). Применяя алгоритм Сколема, получаем следующую

последовательность формул:
yzuvw (P(с, y)  R(z, u, v) & Q(u, w));
yzvw (P(с, y)  R(z, f(y, z), v) & Q(f(y, z), w));
yzv (P(с, y)  R(z, f(y, z), v) & Q(f(y, z), g(y, z, v))).
Переход от формулы в пренексной форме к -формуле не затрагивает свойство формулы быть невыполнимой (противоречивой). Это доказывается следующей теоремой.
Теорема. Пусть формула F задана в ПНФ и преобразована в -формулу. Тогда F в пренексной форме логически невыполнима тогда и только тогда, когда невыполнима -формула F.
Таким образом, алгоритм Сколема, сохраняя свойство невыполнимости (противоречивости), приводит произвольную формулу, имеющую пренексный вид, к -формуле.

молодые люди являются студентами. Следовательно, существуют студенты – спортсмены.
Формальная запись

рассуждения:
x (М(x)  S(x))
x (М(х) & C(x))
--------------------
x (C(х) & S(x))
Здесь С(х) - «х – студент», М(х) - «х – молод», S(x) - «х- занимается спортом».
Для доказательства по теореме 2 логического следствия выполним действия по приведению посылок и отрицания заключения сначала к ПНФ, а затем и к ССФ.

S(x)) формула представлена в ПНФ.
Поскольку кванторы существования отсутствуют, ПНФ совпадает

с ССФ: x (M(x)  S(x)) - ССФ
2) F2: x (М(х) & C(x)) формула представлена в ПНФ.
Наличие квантора  требует применения алгоритма Сколема: заменяем х на константу с, квантор  вычеркиваем.
М(с) & C(с) – ССФ.
3)  G: (x (C(х) & S(x)) ) = x (С(x) & S(x)) = x (С(x)   S(x)) – ПНФ.
Поскольку кванторы существования отсутствуют, ПНФ совпадает с ССФ: x (С(x)   S(x)) – ССФ.
Построим произведение F1&F2& G и докажем его противоречивость:
(x (M(x)  S(x))) & М(с) & C(с) &(x (С(x)   S(x)) )
Поскольку формула верна для всех х, формула верна и для х=с. Получим
(M(с)  S(с)) & М(с) & C(с) &(С(с)   S(с)) =
=(M(с) & М(с)  S(с) & М(с)) & (С(с) & C(с)   S(с) & C(с)) =
=(Л  S(с) & М(с)) & (Л  S(с) & C(с)) = S(с) & М(с)&  S(с) & C(с) =Л