Axiomas
As sentenças seguintes são consideradas teoremas $\forall P,Q,R$.
- $P\implies (Q\implies P)$
- $(P \implies (Q \implies R)) \implies ((P\implies Q) \implies (P \implies R))$
- $ (\neg A \implies B) \implies ((\neg A \implies \neg B) \implies A) $
Regra de inferência
Se $A$ e $A\implies B$ são teoremas do cálculo proposicional, então $B$ é um teorema do cálculo proposicional. Temos, portanto $$ \left\{A , (A \implies B) \right\} \vdash B .$$
Essa regra de inferência é denominada modus ponens (MP).
Teoremas
Seguem teoremas considerados (por mim) importantes:
Teorema 1 (Reflexividade da implicação)
É possível deduzir a fórmula $A\implies A$ sem tomar hipóteses (além dos axiomas), ou seja, $\vdash A\implies A$. Segue a demonstração:
- $A\implies ((A \implies A ) \implies A)$ (Axioma 1)
- $(A \implies ((A \implies A) \implies A)) \implies ((A\implies (A \implies A)) \implies (A \implies A))$ (Axioma 2)
- $(A\implies (A \implies A)) \implies (A \implies A) $ (MP 1,2)
- $A \implies (A \implies A)$ (Axioma 1)
- $A\implies A$ (MP 4,3)
Teorema da dedução (volta)
Se $\Gamma \vdash A \implies B$ , então $\Gamma\cup \{A\}\vdash B$. Se $\Gamma \vdash A \implies B$, temos que $A \implies B$ é deduzível dos axiomas e de um conjunto de hipóteses $\Gamma$. Então temos:
- $\Gamma$ (Hipótese)
- $A$ (Hipótese)
- $A\implies B$ ( 1 e ($\Gamma \vdash A \implies B$))
- $B$ (MP 2,3)
Teorema da dedução
Se $\Gamma\cup \{A\}\vdash B$, então $\Gamma \vdash A \implies B$. A demonstração e sua importância estão presentes aqui.