Система натурального вывода

Основываясь на применяемых в математике способах рассуждения, можно сформулировать так называемые правила естественного вывода. Обычно логическое рассуждение имеет вид

Г влечет U (или из Г следует U),

где U – формула (утверждение), а Г – некоторое множество формул (утверждений). Рассуждение такого вида мы будем представлять записью Г⇒U (не приписывая пока знаку ⇒ какого бы то ни было смысла). Элементы множества Г будем называть гипотезами, U – заключением. Правила вывода устанавливают, как от одних рассуждений можно переходить к другим, основываясь только на их логической форме.

Прежде чем сформулировать правила, условимся об обозначениях. Далее Г будет обозначать некоторое множество формул. Если U – формула, вместо {U} будем писать просто U; вместо Г∪{U} будем писать Г, U. Правила мы будем записывать в виде двухэтажных выражений: над чертой (в «числителе») – исходные рассуждения, под чертой (в «знаменателе») – рассуждение, к которому от них можно перейти. Следующие два базисных правила формализуют принцип монотонности рассуждений:

∅

-----------

Γ, U ⇒ U

Γ ⇒ U

-----------

Γ, V ⇒ U

Содержательно их можно понимать так: первое – всегда допустимо (выводится из «ничего») рассуждение, в котором заключение является одной из гипотез; второе – если некоторый набор гипотез позволяет прийти к некоторому заключению, то и более широкий набор гипотез позволяет прийти к тому же заключению.

Теперь выпишем правила введения логических связок:

Γ ⇒ U; Γ ⇒ V

------------------

Γ ⇒ U∧V

Γ ⇒ U

-----------

Γ ⇒ U∨V

Γ ⇒ V

-----------

Γ ⇒ U∨V

Γ, U ⇒ V

-------------

Γ ⇒ U→V

Γ, U ⇒ V; Γ, U ⇒ V

----------------------------------------

Γ ⇒ U

Наконец, приведем правила удаления логических связок:

Γ ⇒ U∧V

-------------

Γ ⇒ U

Γ ⇒ U∧V

-------------

Γ ⇒ V

Γ ⇒ U∨V; Γ, U ⇒ W; Γ, V ⇒ W

----------------------------------------

Γ ⇒ W

Γ ⇒ U→V

--------------

Γ, U ⇒ V

Γ ⇒ U; Γ ⇒ U

------------------

Γ ⇒ V

Γ ⇒ U

------------------

Γ ⇒ U

Перечисленные правила составляют систему натурального вывода. Рассуждение выводимо в системе натурального вывода, если его можно получить из «ничего» (пустого рассуждения), применяя конечное число подходящих правил. Будем говорить, что формула логики высказываний U логически следует из гипотез Г, если формула U принимает значение «истина» для любой оценки переменных, для которой значение «истина» принимают все формулы из Г. Правила натурального вывода согласуются с логическим следованием. Если понимать ⇒ как логическое следование, то верный «числитель» приводит к верному «знаменателю». Более того, система правил натурального вывода полна: если U логически следует из Г, к этому можно прийти с помощью натурального вывода.

Пример. Приведем обоснование в системе натурального вывода метода доказательства разбором случаев:

из U, U→V₁∨V₂, V₁→W, V₂→W логически следует W

Доказательство. Обозначим для краткости набор гипотез через Г. Имеем:

(1) Г, U→V₁∨V₂ ⇒ U→V₁∨V₂ базисное правило

(2) Г ⇒ U→V₁∨V₂ базисное правило

(3) Г, U ⇒ V₁∨V₂ (2), удаление →

(4) Г ⇒ V₁∨V₂ базисное правило

(5) Г, V₁→W ⇒ V₁→W базисное правило

(6) Г ⇒ V₁→W базисное правило

(7) Г, V₁ ⇒ W (6), удаление →

(8) Г, V₂→W ⇒ V₂→W базисное правило

(9) Г ⇒ V₂→W (10) Г, V₂ ⇒ W (9), удаление →

(11) Г⇒ W (4), (7), (10), удаление ∨􀀀

Принцип резолюций

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

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

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

– сначала из формулы исключаются все импликации (используется равносильность U→V≅U∨V);

– необходимое число раз применяются законы де Моргана до тех пор, пока отрицания не будут относиться только к пропозициональным переменным; при этом снимаются двойные отрицания;

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

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

(X→Y)→(Z→(X∧Y)).

Имеем

(X→Y)→(Z→(X∧Y)) ≅ (X∨Y)∨(Z∨(X∧Y)) ≅

≅ (X∧Y)∨(Z∨(X∧Y)) ≅ (X∧Y)∨(Z∨(X∧Y)) ≅

≅ (X∧Y)∨((Z∨X)∧(Z∨Y)) ≅

≅ (X∨Z∨X) ∧ (Y∨Z∨X) ∧ (X∨Z∨Y) ∧ (Y ∨Z∨Y) ≅

≅ (X∨Z) ∧ (X∨Y∨Z) ∧ (X∨Y∨Z).􀀀

Двойственным образом определяются дизъюнктивные нормальные формы. Элементарной конъюнкцией называется конъюнкция нескольких пропозициональных переменных и/или их отрицаний. Дизъюнктивной нормальной формой (ДНФ) называется дизъюнкция конечного числа элементарных конъюнкций.

Следующее правило называется правилом резолюций. Пусть U и V дизъюнкты, а X – пропозициональная переменная. Тогда из формул X∨U и X∨V логически следует формула U∨V.

Дизъюнкт U∨V называется резольвентой дизъюнктов X∨U и X∨V.

На правиле резолюций основывается метод доказательства невыполнимости набора дизъюнктов Г (метод резолюций):

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

Пример. Покажем, используя метод резолюций, что из формул X∨Y, X∨Z, Y∨Z логически следует X. Доказываемое утверждение равносильно невыполнимости набора формул

X∨Y, X∨Z, Y∨Z, X.

Составим соответствующий список дизъюнктов (около резолюций в скобках указаны номера дизъюнктов, из которых они получены):

(1) X∨Y; (2) X∨Z; (3) Y∨Z; (4) X;

(5) Y (1,4); (6) Z (2,4); (7) Y (3,6); (8) Λ (5,7).􀀀

Без доказательства приведем следующую теорему.

Теорема. Пусть Г – множество дизъюнктов (возможно, бесконечное и содержащее бесконечное множество пропозициональных переменных). Если множество Г невыполнимо, это может быть установлено методом резолюций: существует конечная последовательность дизъюнктов, заканчивающаяся пустым дизъюнктом, в которой каждый дизъюнкт либо содержится в Г, либо получен из предыдущих по правилу резолюций.􀀀

Логика предикатов

Понятие предиката

Наряду с высказываниями в математике приходится иметь дело с высказывательными формами, которые превращаются в высказывания при замене в них переменных именами предметов. Например, записи x>5 нельзя приписать значение истинности, пока вместо x не подставлено число. Подставив вместо x число 7, мы получим истинное высказывание, подставив 3 – ложное. Подобные высказывательные формы называют предикатами. Дадим более точное определение.

Будем говорить, что на множестве X задан предикат P(x₁,x₂,…,x_n) от переменных x₁, x₂, …, x_n , если каждому набору значений этих переменных из множества X поставлено в соответствие значение истинности: 1 (истина) или 0 (ложь). Предикаты от одной переменной называют одноместными; от двух переменных – двухместными и т.д. Вообще, n-местный предикат можно рассматривать как отображение Xⁿ в {0,1}.

Для обозначения предикатов используются заглавные латинские буквы, дополненные списком переменных, от которых зависит предикат. Переменные в предикатах называют предметными, а множество, в котором они принимают значения, называют иногда предметной областью. Например, P(x,y) – предикат P, зависящий от предметных переменных x и y. Для обозначения высказываний, которые получаются после замены переменных конкретными значениями, используются стандартные функциональные обозначения, например P(2,3) и т.п. Некоторые предикаты, часто используемые в математической практике, имеют свои специфические обозначения. Например, x=y, x>y – предикаты от двух переменных.

Высказывания можно трактовать как нульместные предикаты, то есть постоянные предикаты, не зависящие от переменных.

Одноместный предикат P(x) на множестве X может трактоваться как свойство. Предмет x обладает свойством P, если P(x) истинно, и не обладает свойством P, если P(x) ложно.

Двухместный предикат P(x,y) на множестве X×Y может трактоваться как соответствие. Предмет y соответствует предмету x в том и только том случае, когда P(x,y) истинно. При X=Y предикат P(x,y) может трактоваться как бинарное отношение: предметы x и y находятся в отношении P, если истинно P(x,y).

Пусть P – n-местный предикат на множестве X. Обозначим через D_P множество всех тех наборов из Xⁿ, для которых этот предикат истинен. Множество D_P⊂Xⁿ называется областью истинности предиката P.

Пример. Уравнение или неравенство с одной неизвестной величиной является предикатом на своей области определения. Область истинности такого предиката – множество решений. Например, неравенство P(x): lg x>3 – это одноместный предикат на множестве положительных действительных чисел; D_P = (1000; +∞).􀀀

Одноместные предикаты можно в некотором смысле отождествить с характеристическими функциями. Пусть X – произвольное множество, и A⊂X – некоторое его подмножество. Областью истинности одноместного предиката x∈A на множестве X является A. Так что значения истинности предиката x∈A совпадают со значениями характеристической функции подмножества A. Обратно, всякий одноместный предикат P на множестве X принимает те же значения, что и предикат x∈D_P.

Иногда бывает удобно считать, что предметные переменные принимают свои значения в разных множествах. Например, для предиката P(x,l): «точка x лежит на прямой l», – удобно считать, что переменная x пробегает множество точек X, а переменная l – множество прямых L. В такой ситуации говорят, что предикат P определен на X×L и рассматривают его как отображение множества X×L в {0,1}.

Предикат P(x₁,x₂,…,x_n) на множестве X называется:

а) тождественно истинным (ложным), если он принимает значение «истина» («ложь») для любого набора значений его предметных переменных; б) выполнимым (опровержимым), если существует хотя бы один набор значений предметных переменных, для которого предикат P принимает значение «истина» («ложь»).

Пример. Предикат x²+y²≥0 тождественно истинен на множестве действительных чисел; предикат x²+y²<0 – тождественно ложен; предикат x²+y²>0 – одновременно выполним и опровержим.􀀀

Непосредственно из определений вытекает справедливость следующих утверждений.

Предикат P(x₁,x₂,…,x_n) на множестве X тождественно истинен (ложен) тогда и только тогда, когда D_P=Xⁿ (соотв. D_P=∅).

Предикат P(x₁,x₂,…,x_n) на множестве X выполним (опровержим) тогда и только тогда, когда D_P≠∅ (соотв. D_P≠Xⁿ).

Не нашли, что искали? Воспользуйтесь поиском: