Regras Derivadas
$$\Huge \ndMT \qquad \ndRA \qquad \ndTE $$
Certas regras facilitam e reduzem significativamente o número de passos numa prova.
- É necessário demonstrar que as regras novas resultam das anteriores.
- Também algumas regras anteriores são redundantes: umas resultam das restantes.
Modus Tollens ($\ndMT$)
$$\Large \ndMT: p \to q, \neg q \vdash \neg p $$ ou $$\Large \ndrule{p \to q & \neg q}{\neg p}{\ndMT}. $$
Demonstração.
| Linha | Proposição | Regra | Hipóteses |
|---|---|---|---|
| 1 | $p \to q$ | $H$ | |
| 2 | $\neg q $ | $H$ | |
| 3 | $p$ | $H$ | (6) |
| 4 | $q$ | $\ndMP$ | 3, 1 |
| 5 | $\bot$ | $\ndIContr$ | 4, 2 |
| 6 | $\neg p$ | $\ndINeg$ | 3 - 5 |
Redução ao Absurdo ($\ndRA$)
$$\Large \ndRA: \sbr{\neg p \vdash \bot} \vdash p $$ ou $$\Large \ndrule{\ndsub{\neg p & H \cr \vdots \cr\bot}}{p}{\ndRA}. $$
Demonstração.
| Linha | Proposição | Regra | Hipóteses |
|---|---|---|---|
| 1 | $\neg p \to \bot$ | $H$ | |
| 2 | $\qquad \neg p $ | $H$ | (4) |
| 3 | $\qquad \bot$ | $\ndMP$ | 1, 2 |
| 4 | $\neg \neg p$ | $\ndINeg$ | 2-3 |
| 5 | $p$ | $\ndEDNeg$ | 4 |
Terceiro Excluído ($\ndTE$)
$$\Large \ndTE: ~\vdash p \lor \neg p $$ ou $$\Large \ndrule{~}{p \lor \neg p}{\ndTE}. $$
Demonstração.
| Linha | Proposição | Regra | Hipóteses |
|---|---|---|---|
| 1 | $\qquad \neg( p \lor \neg p)$ | $H$ | (8) |
| 2 | $\qquad \qquad p$ | $H$ | (5) |
| 3 | $\qquad \qquad p \lor \neg p$ | $\ndIDisjL$ | 2 |
| 4 | $\qquad \qquad \bot$ | $\ndIContr$ | 1, 3 |
| 5 | $\qquad \neg p$ | $\ndINeg$ | 2-4 |
| 6 | $\qquad p \lor \neg p$ | $\ndIDisjR$ | 5 |
| 7 | $\qquad \bot$ | $\ndIContr$ | 1, 6 |
| 8 | $\neg\neg (p \lor \neg p)$ | $\ndINeg$ | 1-7 |
| 9 | $p \lor \neg p$ | $\ndEDNeg$ | 8 |
Exemplo: Regras Derivadas
A regra $\ndIDNeg: p \vdash \neg\neg p$ como resultado de $\ndEContr, \ndIContr$.
Demonstração.
| Linha | Proposição | Regra | Hipóteses |
|---|---|---|---|
| 1 | $p$ | $H$ | |
| 2 | $\qquad \neg p$ | $H$ | (4) |
| 3 | $\qquad \bot$ | $\ndIContr$ | 1, 2 |
| 4 | $\neg\neg p$ | $\ndEContr$ | 2 - 3 |
Isto é $p \vdash \neg\neg p$ ou $$\ndrule{p}{\neg\neg p}{\ndIDNeg}$$