Regras Derivadas

$MT RA TE$

Certas regras facilitam e reduzem significativamente o número de passos numa prova.

Modus Tollens ( $MT$ )

$MT : p \to q, \neg q ⊢ \neg p$ ou $\frac{p \to q \neg q}{\neg p} (MT) .$

Demonstração.

Linha	Proposição	Regra	Hipóteses
1	$p \to q$	$H$
2	$\neg q$	$H$
3	$p$	$H$	(6)
4	$q$	$MP$	3, 1
5	$⊥$	$⊥^{+}$	4, 2
6	$\neg p$	$\neg^{+}$	3 - 5

Redução ao Absurdo ( $RA$ )

$RA : [\neg p ⊢ ⊥] ⊢ p$ ou $\frac{\neg p ⋮ ⊥ H}{p} (RA) .$

Demonstração.

Linha	Proposição	Regra	Hipóteses
1	$\neg p \to ⊥$	$H$
2	$\neg p$	$H$	(4)
3	$⊥$	$MP$	1, 2
4	$\neg\neg p$	$\neg^{+}$	2-3
5	$p$	$\neg \neg^{-}$	4

Terceiro Excluído ( $TE$ )

$TE : ⊢ p \lor \neg p$ ou $p \lor \neg p (TE) .$

Demonstração.

Linha	Proposição	Regra	Hipóteses
1	$\neg (p \lor \neg p)$	$H$	(8)
2	$p$	$H$	(5)
3	$p \lor \neg p$	$\lor_{1}^{+}$	2
4	$⊥$	$⊥^{+}$	1, 3
5	$\neg p$	$\neg^{+}$	2-4
6	$p \lor \neg p$	$\lor_{2}^{+}$	5
7	$⊥$	$⊥^{+}$	1, 6
8	$\neg\neg (p \lor \neg p)$	$\neg^{+}$	1-7
9	$p \lor \neg p$	$\neg \neg^{-}$	8

Exemplo. Regras Derivadas

A regra $\neg \neg^{+} : p ⊢ \neg\neg p$ como resultado de $⊥^{-}, ⊥^{+}$ .

Demonstração.

Linha	Proposição	Regra	Hipóteses
1	$p$	$H$
2	$\neg p$	$H$	(4)
3	$⊥$	$⊥^{+}$	1, 2
4	$\neg\neg p$	$⊥^{-}$	2 - 3

Isto é $p ⊢ \neg\neg p$ ou $\frac{p}{\neg\neg p} (\neg \neg^{+})$

Lógica e Computação