Введение и Исключение Конъюнкций и Дизъюнкций

Одна из техник классической логики заключается во введении и исключении конъюнктов и дизъюнктов. Хотя эти техники выполняются более или менее интуитивно, их обоснование не совсем тривиально, но их можно вывести из правил пропозициональной логики, которые мы уже доказали на предыдущих занятиях. Формально техники введения и исключения конъюнктов и дизъюнктов следующие:

Их доказательства из пропозициональной логики следующие:

∨-Введение

∨-Исключение

∧-Введение

∧-Исключение

Техники Противоречий и Тавтологий

Правило Исключённого Третьего или Тавтология (tau)

Другое известное свойство классической логики — это закон исключённого третьего (tertium non datur). В нем утверждается, что если имеются два утверждения, одно из которых отрицает другое, то одно из них обязательно должно быть истинным; иначе говоря, конъюнкция двух утверждений, одно из которых отрицает другое, является тавтологией. Формально это выражается следующим образом:

\vdash (\neg\alpha \vee\alpha)

И его доказательство легко получить.

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

\vdash \neg(\neg\alpha \wedge \alpha)

Это свойство не нуждается в доказательстве, не потому что оно самоочевидно, а потому что оно получается непосредственно из применения определения конъюнкции к принципу исключённого третьего.

Правило Противоречия или Принцип Взрыва

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

\{(\neg\alpha \wedge \alpha)\}\vdash \beta

\{\alpha, \neg\alpha\}\vdash \beta

Доказательство этого правила простое:

∨-Исключение3

Modus ponens может быть записан двумя способами. Один из известных нам способов — \{\alpha,(\alpha \rightarrow \beta)\}\vdash \beta. Другой менее привычен:

\{\alpha\}\vdash\beta \; \wedge \; \vdash \alpha \; \Longrightarrow \; \vdash \beta

Сосредоточившись на втором способе, можно визуализировать расширение для этого правила, которое мы называем ∨-Исключение3, потому что оно похоже на упрощение, получаемое из дизъюнкции. Оно утверждает, что если \gamma можно вывести из \alpha и из \beta (обоих одновременно), и дизъюнкция между \alpha и \beta является теоремой, то \gamma является теоремой. Это формально записывается следующим образом:

\{\alpha\}\vdash\gamma\; \wedge \; \{\beta\}\vdash\gamma \; \wedge \; \vdash (\alpha \vee \beta) \Longrightarrow \vdash \gamma

Доказательство этой техники классической логики следующее:

Доказательство от противного (cas)

Другая техника классической логики — это доказательство от противного. Если выражение \beta можно вывести как из другого выражения \alpha, так и из его отрицания, то выражение \beta является теоремой. Это формально выражается так: \alpha \vdash \beta \; \wedge \; \neg\alpha \vdash \beta \Longrightarrow \vdash \beta. Его доказательство следующее:

\begin{array}{rll} (1) & \alpha \vdash \beta &; Премиса\\ (2) & \neg \alpha \vdash \beta &; Премиса \\ (3) & \vdash \alpha \vee \neg\alpha &; TAU \\ (4) & \vdash \beta &; \vee-Исключение3(1,2,3) \end{array}

Приведение к Абсурду (absurdo)

Одна из наиболее используемых техник классической логики в доказательствах, особенно в математике, — это приведение к абсурду. Она заключается в том, что если из выражения \alpha следует противоречие (утверждение и его отрицание), то отрицание \alpha является тавтологией. Формально это выражается следующим образом: \{\alpha\}\vdash \beta \; \wedge \; \{\alpha\}\vdash \neg\beta \Longrightarrow \vdash \neg\alpha. И это можно доказать следующим образом: