Implicação

$${\to }^{-},\mathbb{MP}{\to }^{+}$$

Eliminação da Implicação

Eliminação da Implicação ou Modus Ponens (${\to }^{-},\mathbb{MP}$)

$${\to }^{-}\text{ou}\mathbb{MP}:\left\{p,p\to q\right\}⊢q$$ ou $$\frac{\begin{array}{c}pp\to q\end{array}}{q}\left({\to }^{-}\text{ou}\mathbb{MP}\right)$$

Modus Ponens é uma expressão latina e designa uma das primeiras, e mais importantes, regras de inferência.

Sobre o Modus Ponens:

1. "está frio."
2. "se está frio então levo cachecol."
3. portanto "levo cachecol".

Em tabela:

Exemplo. Cadeia de Implicações I

$$p,p\to q,q\to r⊢r$$

Introdução da Implicação

Nesta regra aparece um tipo novo de hipótese, uma sub-prova com hipóteses locais, representada por $\left[\cdots \right]$ na forma horizontal e por $\boxed{⋮}$ na forma vertical.

Introdução da Implicação (${\to }^{+}$)

$${\to }^{+}:\left\{\left[p⊢q\right]\right\}⊢p\to q$$ ou $$\frac{\begin{array}{c}\boxed{\begin{array}{cc}p& H\\ ⋮& \\ q& \end{array}}\end{array}}{p\to q}\left({\to }^{+}\right).$$

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⊢p\to r$$

Este exemplo ilustra o processo de descarte das hipóteses locais de uma sub-prova:

1. Na linha 3 é introduzida a hipótese $p$.
2. As linhas 4 e 5 dependem dessa hipótese.
3. Na linha 6 é a aplicada a regra ${\to }^{+}$, em que
   1. A sub-prova da hipótese desta regra ocorre nas linhas 3 - 5 da prova.
      • E escreve-se 3 - 5 na coluna "Hipóteses".
   2. 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.

Exemplo. Cadeia de Implicações III

$$p\to q⊢\left(q\to r\right)\to \left(p\to r\right)$$

Este exemplo continua o anterior: Na linha 7 ocorre uma nova aplicação da regra ${\to }^{+}$.

1. Esta aplicação usa as linhas 2 - 6 como sub-prova.
2. A hipótese da linha 2 é descartada, sendo indicado que esse descarte é feito na linha 7.