5. Непротиворечивость и полнота исчисления высказываний

В этом разделе приведем теоремы, касающиеся свойств исчисления высказываний в целом. Приведем необходимые определения.

Формальная аксиоматическая теория называется полной, если в ней доказуема любая тавтология. Формальная аксиоматическая теория называется непротиворечивой, если в ней не существует вывода формулы A такой, что одновременно доказуемы формулы A и ¬A. Система аксиом формально непротиворечивой теории Т называется независимой, если никакая из аксиом не выводима из остальных по правилам вывода теории Т. Формальную аксиоматическую теорию называют полной в узком смысле, если добавление любой невыводимой формулы в качестве схемы аксиом приводит к противоречивой системе.

Формальная теория Т разрешима, если существует алгоритм, который для любой формулы теории определяет, является ли эта формула теоремой теории Т. Теория Т называется полуразрешимой, если существует алгоритм, который для любой формулы F выдает ответ «Да», если F – теорема, и может быть не выдает никакого ответа, если F не является теоремой.

Теорема.├ _L А А – тавталогия

Доказательство.Докажем только необходимость утверждения. Нетрудно проверить, что аксиомыA₁,A₂,A₃, являются тавталогиями, а правило выводаmodusponensсохраняет тождественную истинность формул, т.е. из ТИ формул по правилу вывода получаются только ТИ формулы.

Следствие. Теория L – формально непротиворечива.

Доказательство.Поскольку все теоремы теорииL– тавталогии, то отрицание тавтологии не есть тавтология. Следовательно, в теорииLне существует одновременно теоремы и ее отрицания.

Теорема.Система аксиом теории L независима.

Теорема.Теория L является разрешимой теорией.

Доказательство. Чтобы узнать выводима ли некоторая формула в исчислении высказываний, достаточно проверить тождественную истинность этой формулы, что можно сделать за конечное число шагов.

6. Методы проверки выводимости формул ив

В этом разделе приводятся некоторые методы проверки тождественной истинности формул ИВ или, как было показано, выводимости формул в ИВ.

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

Алгебраический методболее совершенный. Он базируется на применении законов булевой алгебры. Поскольку разные формулы могут принимать одинаковые значения, то для проверки тождественной истинности можно использовать наиболее простую формулу, например ДНФ (или КНФ), для которых известны методы построения и вычисления значений формулы.

Метод Куайнапредставляет собой модификацию тривиального метода. Пусть <X1,X2, ...,Xk> – множество высказывательных переменных в формулеF. Возьмем первую переменнуюX₁и придадим ей, например, значение И (или Л). Подставим это значение в формулуFи выполним вычисления, которые могут возникнуть при такой подстановке. После выполнения вычислений получим формулуF’с меньшим количеством переменных и применяем к ней описанную процедуру. Если на каком-то шаге получена формула, которая является тавталогией или противоречием независимо от значений высказывательных переменных, входящих в эту формулу, то алгоритм на этом шаге можно остановить. Таким образом, алгоритм Куайна приводит к рассмотрению меньшего количества интерпретаций, чем тривиальный алгоритм. Рассмотрим пример работы метода Куайна.

Пример 1. Проверить выводимость формулы(X&Y&Z)(XY)&(XZ) методом Куайна.

Положим I(X)=Л. ТогдаI((0& Y&Z)(0Y)&(0Z))=И при любой интерпретацииY и Z. Пусть теперь I(X)=И.

Тогда I((1& Y&Z)(1Y)&(1Z))=I(Y&ZY&Z). Для полученной формулы повторим процедуру метода Куайна. ПоложимI(Y)=Л. ТогдаI(0&Z0&Z)=И при любой интерпретацииZ. ПоложимI(Y)=И. ТогдаI(1&Z1&Z)= I(ZZ)=И при любой интерпретацииZ. Таким образом, данная формула является тавталогией, а значит выводима в ИВ.

Пример 2. Проверить выводимость(X&Y&Z) ├ (XY)&(XZ) методом Куайна.

Сначала применим теорему дедукции к данной выводимости. По теореме дедукции можно проверять выводимость (X&Y&Z)(XY)&(XZ). Далее поступаем как в примере 1.

Пример 3. Проверить выводимость(XY) ├ (XY)&(X¬Z) методом Куайна

Сначала применим теорему дедукции к данной выводимости. По теореме дедукции можно проверять выводимость (XY)→ (XY)&(X¬Z).

Положим I(X)=Л. ТогдаI((0Y)→(0Y)&(0¬Z))=И при любой интерпретацииY и Z. Пусть теперь I(X)=И.

Тогда I((1Y)→ (1Y)&(1¬Z))= I(Y→ Y& ¬Z )= I ((¬Y Y)& (¬Y ¬Z ))=

I (¬Y ¬Z ). ПриI(Y)=И, I(Z)=И получаем, что формула ложна. Таким образом, формула не является тавталогией, а значит не выводима.

Рассмотрим теперь метод редукциираспознавания тождественно истинных формул в ИВ. Он особенно удобен, когда в записи формул встречается много импликаций. Суть метода заключается в следующем. Пусть формулаFимеет вид импликации, например,F=AB. Допустим, что в некоторой интерпретации формулаFпринимает значение Л. Тогда в соответствии с таблицей истинности для импликации имеемI(A)=1, I(B)=0.Таким образом, проверка формулыFсводится к проверке формулАиВ. После этого данный процесс применяется к формуламАиВ и т.д.

Пример 4. Проверить выводимость формулы(X(YZ))((XY)(XZ)) методом редукции.

Пусть в некоторой интерпретации формула имеет значение Л. Тогда I(X(YZ))=И, I((XY)(XZ))=Л. Применим теперь метод редукции к формуле(XY)(XZ). Если она в некоторой интерпретации имеет значение Л, тоI(XY)=И, I(XZ)=Л.Для формулыXZ метод редукции даетI(X)=И, I(Z)=Л. ИзI(XY)=И получаем, чтоI(Y)=И. Однако это приводит к противоречию сI(X(YZ))=И. Таким образом, исходная формула не может быть ложной ни при какой интерпретации, т.е. формула является тавталогией, а следовательно выводима в ИВ.

Пример 5. Проверить выводимость формулы(X(YZ)) ├ ((XY)(XZ)) методом редукции.

По теореме дедукции будем доказывать выводимость (X(YZ))((XY)(XZ)). Далее поступаем как в примере 4.

Пример 6. Проверить выводимость(XY) ├ (XY)&(X¬Z) методом редукции.

Сначала применим теорему дедукции к данной выводимости. По теореме дедукции можно проверять выводимость (XY)→ (XY)&(X¬Z). Пусть в некоторой интерпретации формула имеет значение Л. ТогдаI(XY)=И, I((XY)&(X¬Z))=Л. ОтсюдаI(X¬Z)=Л и I(X)=И, I(Z)=И. Таким образом, существует интерпретация переменных (I(X)=И, I(Y)=И, I(Z)=И), при которой формула является ложной. Значит, формула не выводима в ИВ.

Наиболее известный классический алгоритм проверки выводимости формул в ИВ называется методом резолюций. В основе метода резолюций положена следующая теорема (доказательство от противного).

Теорема. ЕслиГ, A├ _L B, где В – любое противоречие, то Г├ _L А.

Доказательство.Г, A├ _L B  Г&A├ _L B  ├ _L Г&A B  Г&A B –тавталогия. Преобразуем эту формулу.

Г&A B≡( Г&A)В≡( Г&A) ≡ГА≡ГА. Следовательно,ГА – тавталогия, тогда и только тогда, когдаГ├ _L А.

В качестве формулы Впри доказательстве от противного по методу резолюций принято использовать пустую формулу, которую будем обозначать. Пустая формула не имеет никакого значения и не является истинной ни при какой интерпретации и, по определению является противоречием.

Метод резолюций работает с особой стандартной формой формул, которые называются предложениями. Предложение – это дизъюнкция переменных или их отрицаний (литералов). Любая формула исчисления высказываний может быть преобразована во множество предложений следующим образом. Сначала формула приводится к КНФ, а затем конъюнкция дизъюнкций литералов разбивается на множество предложений.

Пример.Найдем множество предложений, соответствующих формуле

А(ВА)

Приведем формулу к КНФ.

А(ВА) ≡А(ВА) ≡А(ВА) ≡А(В&A) ≡(AB)&A

Таким образом, множество предложений состоит из двух формулAB,A.

Рассмотрим теперь правило резолюции, т.е. правило вывода, которое используется в методе резолюций. ПустьАиВ– два предложения в ИВ и пустьА=Р А₁, аВ=Р В₁, гдеР– переменная, аА₁, В₁– любые предложения (в частности, может быть пустые или состоящие только из одного литерала). Правило выводаназываетсяправилом резолюции. ПредложенияАиВназываютсярезольвируемыми(или родительскими), предложениеА₁В₁ – резольвентой, а формулыР, Р–контрарными литералами.

Теорема.Правило резолюции логично, т.е. резольвента является логическим следствием резольвируемых предложений.

Доказательство. ПустьI(A)=И иI(B)=И при некоторой интерпретации. Тогда еслиI(Р)=И, тоВ₁иI(В₁)=И, а значитI(А₁ В₁)=И. Если жеI(Р)=Л, тоА₁иI(А₁)=И, а значитI(А₁ В₁)=И.

Пусть нужно установить выводимость Г├ _LF. Воспользуемся доказательством от противного и будем доказывать выводимостьГ, F├ _L  с помощью метода резолюций. Для этого каждая формула множестваГи формулаFнезависимо преобразуются в множества предложений. В полученном совокупном множестве предложений отыскиваются резольвируемые предложения, к ним применяется правило резолюции и резольвента добавляется во множество предложений до тех пор, пока не будет получено пустое предложение. При этом возможны два случая:

• Среди текущего множества предложений нет резольвируемых. Это означает, что теорема опровергнута, т.е. формула Fне выводима из множества формулГ.

• В результате очередного применения правила резолюции получено пустое предложение. Это означает, что теорема доказана, т.е. Г├ _LF.

Пример 7. Докажем методом резолюций теорему

├ _L (X&Y&Z)(XY)&(XZ).

Преобразуем во множество предложений отрицание целевой формулы

((X&Y&Z)(XY)&(XZ))

((X&Y&Z)(XY)&(XZ))

(XYZ(XY)&(XZ))

X&Y&Z&((XY)&(XZ))

X&Y&Z&((XY)(XZ))

X&Y&Z&(X&YX&Z)

X&Y&Z&X&(YZ)

X&Y&Z&(YZ)

Таким образом, множество предложений состоит из X, Y, Z, (YZ).Теперь производим резольвирование

1	X
2	Y
3	Z
4	(YZ)
5	Z	ПР из 2 и 4
6		ПР из 3 и 5

Поскольку получено пустое предложение, то исходная формула выводима в ИВ.

Пример 8. Докажем методом резолюций выводимость

(X&Y&Z) ├ _L (XY)&(XZ).

Преобразуем во множество предложений отдельно гипотезу и отрицание целевой функции. Гипотеза дает предложения {X, Y, Z}. Отрицание целевой формулы дает следующие предложения { X, (YZ)}, поскольку

((XY)&(XZ))

(XY)(XZ)

(X&Y)( X&Z)

X&(YZ)

Таким образом общее множество предложений X, Y, Z, (YZ).Далее резольвируем как в примере 7.

Пример 9.Проверим методом резолюций выводимость

├ _L X((XY)(XZ)).

Применим к выводимости теорему дедукции. Получим