Implicação
$$\Huge \ndEImpl, \ndMP \qquad \ndIImpl $$
Eliminação da Implicação
Eliminação da Implicação ou Modus Ponens ($\ndEImpl, \ndMP$)
$$\Large \ndEImpl \text{ ou } \ndMP: \cbr{p, p \to q} \vdash q $$ ou $$\Large \ndrule{p \quad p \to q}{q}{\ndEImpl\text{ ou }\ndMP} $$
Modus Ponens é uma expressão latina e designa uma das primeiras, e mais importantes, regras de inferência.
Sobre o Modus Ponens:
- “está frio.”
- “se está frio então levo cachecol.”
- portanto “levo cachecol”.
Em tabela:
| Linha | Proposição | Regra | Hipóteses |
|---|---|---|---|
| 1 | $\lit{está frio}$ | $H$ | |
| 2 | $\lit{está frio}\to\lit{levo cachecol}$ | $H$ | |
| 3 | $\lit{levo cachecol}$ | $\ndMP$ | 1, 2 |
Exemplo. Cadeia de Implicações I
$$ p, p \to q, q \to r \vdash r $$
| Linha | Proposição | Regra | Hipóteses |
|---|---|---|---|
| 1 | $p$ | $H$ | |
| 2 | $p \to q $ | $H$ | |
| 3 | $q \to r $ | $H$ | |
| 4 | $q$ | $\ndMP$ | 1, 2 |
| 5 | $r$ | $\ndMP$ | 4, 3 |
Introdução da Implicação
Nesta regra aparece um tipo novo de hipótese, uma sub-prova com hipóteses locais, representada por $\sbr{\cdots}$ na forma horizontal e por $\boxed{\vdots~}~$ na forma vertical.
Introdução da Implicação ($\ndIImpl$)
$$\Large \ndIImpl: \cbr{ \sbr{p \vdash q} } \vdash p \to q $$ ou $$\Large \ndrule{\ndsub{p & H\cr \vdots\cr q}}{p \to q}{\ndIImpl}. $$
As hipóteses locais duma sub-prova são descartadas com a aplicação da regra.
Exemplo. Cadeia de Implicações II
$$p \to q, q \to r \vdash p \to r$$
| Linha | Proposição | Regra | Hipóteses |
|---|---|---|---|
| 1 | $p \to q$ | $H$ | |
| 2 | $q \to r$ | $H$ | |
| 3 | $p$ | $H$ | (6) |
| 4 | $q$ | $\ndMP$ | 3, 1 |
| 5 | $r$ | $\ndMP$ | 4, 2 |
| 6 | $p \to r$ | $\ndIImpl$ | 3 - 5 |
Este exemplo ilustra o processo de descarte das hipóteses locais de uma sub-prova:
- Na linha 3 é introduzida a hipótese $p$.
- As linhas 4 e 5 dependem dessa hipótese.
- Na linha 6 é a aplicada a regra $\ndIImpl$, em que
- A sub-prova da hipótese desta regra ocorre nas linhas 3 - 5 da prova.
- E escreve-se 3 - 5 na coluna “Hipóteses”.
- A aplicação desta regra descarta toda a sub-prova.
- E escreve-se (6) na coluna “Hipóteses” da linha 3, onde inicia a sub-prova.
- A sub-prova da hipótese desta regra ocorre nas linhas 3 - 5 da prova.
Exemplo. Cadeia de Implicações III
$$p \to q \vdash \del{q \to r} \to \del{p \to r}$$
| Linha | Proposição | Regra | Hipóteses |
|---|---|---|---|
| 1 | $p \to q$ | $H$ | |
| 2 | $q \to r$ | $H$ | (7) |
| 3 | $p$ | $H$ | (6) |
| 4 | $q$ | $\ndMP$ | 3, 1 |
| 5 | $r$ | $\ndMP$ | 4, 2 |
| 6 | $p \to r$ | $\ndIImpl$ | 3 - 5 |
| 7 | $(q \to r) \to (p \to r)$ | $\ndIImpl$ | 2 - 6 |
Este exemplo continua o anterior: Na linha 7 ocorre uma nova aplicação da regra $\ndIImpl$.
- Esta aplicação usa as linhas 2 - 6 como sub-prova.
- A hipótese da linha 2 é descartada, sendo indicado que esse descarte é feito na linha 7.