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

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

Г влечет 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), удаление ∨􀀀