# Lógica/Cálculo Proposicional Clássico/Axiomática
## Introdução

Uma outra forma de lidar sintáticamente com o CPC é axiomaticamente. Como você deve saber, axiomas são proposições tomadas como verdadeiras a partir das quais os teoremas são derivados.
Funciona assim:
Seja $\Delta \,\!$ o conjunto dos axiomas e todas suas instâncias, se $\Delta \vdash \alpha \,\!$, então $\vdash \alpha$. Ou seja, se $\alpha \,\!$ é dedutível dos axiomas, então $\alpha \,\!$ é teorema.
E seja $\Gamma \,\!$ um conjunto qualquer de fórmulas, se $\Delta \cup \Gamma \vdash \alpha$ então $\Gamma \vdash \alpha$. Ou seja, se $\alpha \,\!$ é dedutível de um conjunto $\Gamma \,\!$ de fórmulas juntamente com os axiomas, então um raciocínio que tenha $\Gamma \,\!$ como premissas e $\alpha \,\!$ como conclusão é válido.
A escolha adequada de axiomas e da regra de inferência primitiva confere ao sistema tanto a correção quanto a completude.

## Axiomática de Frege

Gottlob Frege usava apenas a implicação e a negação como operadores primitivos, definindo as demais operações por meio destes, mas sem criar símbolos para expressá-las. Sua axiomática do CPC tem seis axiomas e uma regra de inferência.
Por questões de economia, demonstraremos algumas regras de inferência derivadas e as aplicaremos.
Nas tabelas onde as deduções são expressas, "wff" significa "well formed formula", ou seja, "fórmula bem formada".
* Axiomas
THEN-1: $A\to \left(B\to A\right)$
THEN-2: $\left(A\to \left(B\to C\right)\right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)$
THEN-3: $\left(A\to \left(B\to C\right)\right)\to \left(B\to \left(A\to C\right)\right)$
FRG-1: $\left(A\to B\right)\to \left(\neg B\to \neg A\right)$
FRG-2: $\neg \neg A\to A\,\!$
FRG-3: $A\to \neg \neg A\,\!$
* Regra de Inferência
MP: $\left\{P,P\to Q\right\}\vdash Q$
Regra THEN-1*: $A\vdash \left(B\to A\right)$
| # | wff | razão |
| 1. | $A\,\!$ | premissa |
| 2. | $A\to \left(B\to A\right)$ | THEN-1 |
| 3. | $B\to A\,\!$ | MP 1,2. |
Regra THEN-2*: $A\to \left(B\to C\right)\vdash \left(A\to B\right)\to \left(A\to C\right)$
| # | wff | razão |
| 1. | $A\to \left(B\to C\right)$ | premissa |
| 2. | $\left(A\to \left(B\to C\right)\right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)$ | THEN-2 |
| 3. | $\left(A\to B\right)\to \left(A\to C\right)$ | MP 1,2. |
Regra THEN-3*: $A\to \left(B\to C\right)\vdash B\to \left(A\to C\right)$
| # | wff | razão |
| 1. | $A\to \left(B\to C\right)$ | premissa |
| 2. | $\left(A\to \left(B\to C\right)\right)\to \left(B\to \left(A\to C\right)\right)$ | THEN-3 |
| 3. | $B\to \left(A\to C\right)$ | MP 1,2. |
Regra FRG-1*: $A\to B\vdash \neg B\to \neg A$
| # | wff | razão |
| 1. | $\left(A\to B\right)\to \left(\neg B\to \neg A\right)$ | FRG-1 |
| 2. | $A\to B$ | premissa |
| 3. | $\neg B\to \neg A$ | MP 2,1. |
Regra TH1*: $A\to B,B\to C\vdash A\to C$
| # | wff | razão |
| 1. | $B\to C$ | premissa |
| 2. | $\left(B\to C\right)\to \left(A\to \left(B\to C\right)\right)$ | THEN-1 |
| 3. | $A\to \left(B\to C\right)$ | MP 1,2 |
| 4. | $\left(A\to \left(B\to C\right)\right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)$ | THEN-2 |
| 5. | $\left(A\to B\right)\to \left(A\to C\right)$ | MP 3,4 |
| 6. | $A\to B$ | premissa |
| 7. | $A\to C$ | MP 6,5. |
Teorema TH1: $\left(A\to B\right)\to \left(\left(B\to C\right)\to \left(A\to C\right)\right)$
| # | wff | razão |
| 1. | $\left(B\to C\right)\to \left(A\to \left(B\to C\right)\right)$ | THEN-1 |
| 2. | $\left(A\to \left(B\to C\right)\right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)$ | THEN-2 |
| 3. | $\left(B\to C\right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)$ | TH1* 1,2 |
| 4. | $\left(\left(B\to C\right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)\right)\to \left(\left(A\to B\right)\to \left(\left(B\to C\right)\to \left(A\to C\right)\right)\right)$ | THEN-3 |
| 5. | $\left(A\to B\right)\to \left(\left(B\to C\right)\to \left(A\to C\right)\right)$ | MP 3,4. |
Teorema TH2: $A\to \left(\neg A\to \neg B\right)$
| # | wff | razão |
| 1. | $A\to \left(B\to A\right)$ | THEN-1 |
| 2. | $\left(B\to A\right)\to \left(\neg A\to \neg B\right)$ | FRG-1 |
| 3. | $A\to \left(\neg A\to \neg B\right)$ | TH1* 1,2. |
Teorema TH3: $\neg A\to \left(A\to \neg B\right)$
| # | wff | razão |
| 1. | $A\to \left(\neg A\to \neg B\right)$ | TH 2 |
| 2. | $\left(A\to \left(\neg A\to \neg B\right)\right)\to \left(\neg A\to \left(A\to \neg B\right)\right)$ | THEN-3 |
| 3. | $\neg A\to \left(A\to \neg B\right)$ | MP 1,2. |
Teorema TH4: $\neg \left(A\to \neg B\right)\to A$
| # | wff | razão |
| 1. | $\neg A\to \left(A\to \neg B\right)$ | TH3 |
| 2. | $\left(\neg A\to \left(A\to \neg B\right)\right)\to \left(\neg \left(A\to \neg B\right)\to \neg \neg A\right)$ | FRG-1 |
| 3. | $\neg \left(A\to \neg B\right)\to \neg \neg A$ | MP 1,2 |
| 4. | $\neg \neg A\to A$ | FRG-2 |
| 5. | $\neg \left(A\to \neg B\right)\to A$ | TH1* 3,4. |
Teorema TH5: $\left(A\to \neg B\right)\to \left(B\to \neg A\right)$
| # | wff | razão |
| 1. | $\left(A\to \neg B\right)\to \left(\neg \neg B\to \neg A\right)$ | FRG-1 |
| 2. | $\left(\left(A\to \neg B\right)\to \left(\neg \neg B\to \neg A\right)\right)\to \left(\neg \neg B\to \left(\left(A\to \neg B\right)\to \neg A\right)\right)$ | THEN-3 |
| 3. | $\neg \neg B\to \left(\left(A\to \neg B\right)\to \neg A\right)$ | MP 1,2 |
| 4. | $B\to \neg \neg B$ | FRG-3, with A := B |
| 5. | $B\to \left(\left(A\to \neg B\right)\to \neg A\right)$ | TH1* 4,3 |
| 6. | $\left(B\to \left(\left(A\to \neg B\right)\to \neg A\right)\right)\to \left(\left(A\to \neg B\right)\to \left(B\to \neg A\right)\right)$ | FRG-1 |
| 7. | $\left(A\to \neg B\right)\to \left(B\to \neg A\right)$ | MP 5,6. |
Teorema TH6: $\neg \left(A\to \neg B\right)\to B$
| # | wff | razão |
| 1. | $\neg \left(B\to \neg A\right)\to B$ | TH4, with A := B, B := A |
| 2. | $\left(B\to \neg A\right)\to \left(A\to \neg B\right)$ | TH5, with A := B, B := A |
| 3. | $\left(\left(B\to \neg A\right)\to \left(A\to \neg B\right)\right)\to \left(\neg \left(A\to \neg B\right)\to \neg \left(B\to \neg A\right)\right)$ | FRG-1 |
| 4. | $\neg \left(A\to \neg B\right)\to \neg \left(B\to \neg A\right)$ | MP 2,3 |
| 5. | $\neg \left(A\to \neg B\right)\to B$ | TH1* 4,1. |
Teorema TH7: $A\to A$
| # | wff | razão |
| 1. | $A\to \neg \neg A$ | FRG-3 |
| 2. | $\neg \neg A\to A$ | FRG-2 |
| 3. | $A\to A$ | TH1* 1,2. |
Teorema TH8: $A\to \left(\left(A\to B\right)\to B\right)$
| # | wff | razão |
| 1. | $\left(A\to B\right)\to \left(A\to B\right)$ | TH7, com A := $A\to B$ |
| 2. | $\left(\left(A\to B\right)\to \left(A\to B\right)\right)\to \left(A\to \left(\left(A\to B\right)\to B\right)\right)$ | THEN-3 |
| 3. | $A\to \left(\left(A\to B\right)\to B\right)$ | MP 1,2. |
Teorema TH9: $B\to \left(\left(A\to B\right)\to B\right)$
| # | wff | razão |
| 1. | $B\to \left(\left(A\to B\right)\to B\right)$ | THEN-1, com A := B, B := $A\to B$. |
Teorema TH10: $A\to \left(B\to \neg \left(A\to \neg B\right)\right)$
| # | wff | razão |
| 1. | $\left(A\to \neg B\right)\to \left(A\to \neg B\right)$ | TH7 |
| 2. | $\left(\left(A\to \neg B\right)\to \left(A\to \neg B\right)\right)\to \left(A\to \left(\left(A\to \neg B\right)\to \neg B\right)\right)$ | THEN-3 |
| 3. | $A\to \left(\left(A\to \neg B\right)\to \neg B\right)$ | MP 1,2 |
| 4. | $\left(\left(A\to \neg B\right)\to \neg B\right)\to \left(B\to \neg \left(A\to \neg B\right)\right)$ | TH5 |
| 5. | $A\to \left(B\to \neg \left(A\to \neg B\right)\right)$ | TH1* 3,4. |
Teorema TH11: $\left(A\to B\right)\to \left(\left(A\to \neg B\right)\to \neg A\right)$
| # | wff | razão |
| 1. | $A\to \left(B\to \neg \left(A\to \neg B\right)\right)$ | TH10 |
| 2. | $\left(A\to \left(B\to \neg \left(A\to \neg B\right)\right)\right)\to \left(\left(A\to B\right)\to \left(A\to \neg \left(A\to \neg B\right)\right)\right)$ | THEN-2 |
| 3. | $\left(A\to B\right)\to \left(A\to \neg \left(A\to \neg B\right)\right)$ | MP 1,2 |
| 4. | $\left(A\to \neg \left(A\to \neg B\right)\right)\to \left(\left(A\to \neg B\right)\to \neg A\right)$ | TH5 |
| 5. | $\left(A\to B\right)\to \left(\left(A\to \neg B\right)\to \neg A\right)$ | TH1* 3,4. |
Teorema TH12: $\left(\left(A\to B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)$
| # | wff | razão |
| 1. | $B\to \left(A\to B\right)$ | THEN-1 |
| 2. | $\left(B\to \left(A\to B\right)\right)\to \left(\left(\left(A\to B\right)\to C\right)\to \left(B\to C\right)\right)$ | TH1 |
| 3. | $\left(\left(A\to B\right)\to C\right)\to \left(B\to C\right)$ | MP 1,2 |
| 4. | $\left(B\to C\right)\to \left(A\to \left(B\to C\right)\right)$ | THEN-1 |
| 5. | $\left(\left(A\to B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)$ | TH1* 3,4. |
Teorema TH13: $\left(B\to \left(B\to C\right)\right)\to \left(B\to C\right)$
| # | wff | razão |
| 1. | $\left(B\to \left(B\to C\right)\right)\to \left(\left(B\to B\right)\to \left(B\to C\right)\right)$ | THEN-2 |
| 2. | $\left(B\to B\right)\to \left(\left(B\to \left(B\to C\right)\right)\to \left(B\to C\right)\right)$ | THEN-3* 1 |
| 3. | $B\to B$ | TH7 |
| 4. | $\left(B\to \left(B\to C\right)\right)\to \left(B\to C\right)$ | MP 3,2. |
Regra TH14*: $\left\{A\to \left(B\to P\right),P\to Q\right\}\vdash A\to \left(B\to Q\right)$
| # | wff | razão |
| 1. | $P\to Q\,\!$ | premissa |
| 2. | $\left(P\to Q\right)\to \left(B\to \left(P\to Q\right)\right)$ | THEN-1 |
| 3. | $B\to \left(P\to Q\right)$ | MP 1,2 |
| 4. | $\left(B\to \left(P\to Q\right)\right)\to \left(\left(B\to P\right)\to \left(B\to Q\right)\right)$ | THEN-2 |
| 5. | $\left(B\to P\right)\to \left(B\to Q\right)$ | MP 3,4 |
| 6. | $\left(\left(B\to P\right)\to \left(B\to Q\right)\right)\to \left(A\to \left(\left(B\to P\right)\to \left(B\to Q\right)\right)\right)$ | THEN-1 |
| 7. | $A\to \left(\left(B\to P\right)\to \left(B\to Q\right)\right)$ | MP 5,6 |
| 8. | $\left(A\to \left(B\to P\right)\right)\to \left(A\to \left(B\to Q\right)\right)$ | THEN-2* 7 |
| 9. | $A\to \left(B\to P\right)$ | premissa |
| 10. | $A\to \left(B\to Q\right)$ | MP 9,8. |
Teorema TH15: $\left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(A\to \left(B\to C\right)\right)$
| # | wff | razão |
| 1. | $\left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(\left(\left(A\to B\right)\to A\right)\to \left(\left(A\to B\right)\to C\right)\right)$ | THEN-2 |
| 2. | $\left(\left(A\to B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)$ | TH12 |
| 3. | $\left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(\left(\left(A\to B\right)\to A\right)\to \left(A\to \left(B\to C\right)\right)\right)$ | TH14* 1,2 |
| 4. | $\left(\left(A\to B\right)\to A\right)\to \left(\left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(A\to \left(B\to C\right)\right)\right)$ | THEN-3* 3 |
| 5. | $A\to \left(\left(A\to B\right)\to A\right)$ | THEN-1 |
| 6. | $A\to \left(\left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(A\to \left(B\to C\right)\right)\right)$ | TH1* 5,4 |
| 7. | $\left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(A\to \left(A\to \left(B\to C\right)\right)\right)$ | THEN-3* 6 |
| 8. | $\left(A\to \left(A\to \left(B\to C\right)\right)\right)\to \left(A\to \left(B\to C\right)\right)$ | TH13 |
| 9. | $\left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(A\to \left(B\to C\right)\right)$ | TH1* 7,8. |
Teorema TH16: $\left(\neg A\to \neg B\right)\to \left(B\to A\right)$
| # | wff | razão |
| 1. | $\left(\neg A\to \neg B\right)\to \left(\neg \neg B\to \neg \neg A\right)$ | FRG-1 |
| 2. | $\neg \neg B\to \left(\left(\neg A\to \neg B\right)\to \neg \neg A\right)$ | THEN-3* 1 |
| 3. | $B\to \neg \neg B$ | FRG-3 |
| 4. | $B\to \left(\left(\neg A\to \neg B\right)\to \neg \neg A\right)$ | TH1* 3,2 |
| 5. | $\left(\neg A\to \neg B\right)\to \left(B\to \neg \neg A\right)$ | THEN-3* 4 |
| 6. | $\neg \neg A\to A$ | FRG-2 |
| 7. | $\left(\neg \neg A\to A\right)\to \left(B\to \left(\neg \neg A\to A\right)\right)$ | THEN-1 |
| 8. | $B\to \left(\neg \neg A\to A\right)$ | MP 6,7 |
| 9. | $\left(B\to \left(\neg \neg A\to A\right)\right)\to \left(\left(B\to \neg \neg A\right)\to \left(B\to A\right)\right)$ | THEN-2 |
| 10. | $\left(B\to \neg \neg A\right)\to \left(B\to A\right)$ | MP 8,9 |
| 11. | $\left(\neg A\to \neg B\right)\to \left(B\to A\right)$ | TH1* 5,10. |
Teorema TH17: $\left(\neg A\to B\right)\to \left(\neg B\to A\right)$
| # | wff | razão |
| 1. | $\left(\neg A\to \neg \neg B\right)\to \left(\neg B\to A\right)$ | TH16, com B := \neg B |
| 2. | $B\to \neg \neg B$ | FRG-3 |
| 3. | $\left(B\to \neg \neg B\right)\to \left(\neg A\to \left(B\to \neg \neg B\right)\right)$ | THEN-1 |
| 4. | $\neg A\to \left(B\to \neg \neg B\right)$ | MP 2,3 |
| 5. | $\left(\neg A\to \left(B\to \neg \neg B\right)\right)\to \left(\left(\neg A\to B\right)\to \left(\neg A\to \neg \neg B\right)\right)$ | THEN-2 |
| 6. | $\left(\neg A\to B\right)\to \left(\neg A\to \neg \neg B\right)$ | MP 4,5 |
| 7. | $\left(\neg A\to B\right)\to \left(\neg B\to A\right)$ | TH1* 6,1. |
Teorema TH18: $\left(\left(A\to B\right)\to B\right)\to \left(\neg A\to B\right)$
| # | wff | razão |
| 1. | $\left(A\to B\right)\to \left(\neg B\to \left(A\to B\right)\right)$ | THEN-1 |
| 2. | $\left(\neg B\to \neg A\right)\to \left(A\to B\right)$ | TH16 |
| 3. | $\left(\neg B\to \neg A\right)\to \left(\neg B\to \left(A\to B\right)\right)$ | TH1* 2,1 |
| 4. | $\left(\left(\neg B\to \neg A\right)\to \left(\neg B\to \left(A\to B\right)\right)\right)\to \left(\neg B\to \left(\neg A\to \left(A\to B\right)\right)\right)$ | TH15 |
| 5. | $\neg B\to \left(\neg A\to \left(A\to B\right)\right)$ | MP 3,4 |
| 6. | $\left(\neg A\to \left(A\to B\right)\right)\to \left(\neg \left(A\to B\right)\to A\right)$ | TH17 |
| 7. | $\neg B\to \left(\neg \left(A\to B\right)\to A\right)$ | TH1* 5,6 |
| 8. | $\left(\neg B\to \left(\neg \left(A\to B\right)\to A\right)\right)\to \left(\left(\neg B\to \neg \left(A\to B\right)\right)\to \left(\neg B\to A\right)\right)$ | THEN-2 |
| 9. | $\left(\neg B\to \neg \left(A\to B\right)\right)\to \left(\neg B\to A\right)$ | MP 7,8 |
| 10. | $\left(\left(A\to B\right)\to B\right)\to \left(\neg B\to \neg \left(A\to B\right)\right)$ | FRG-1 |
| 11. | $\left(\left(A\to B\right)\to B\right)\to \left(\neg B\to A\right)$ | TH1* 10,9 |
| 12. | $\left(\neg B\to A\right)\to \left(\neg A\to B\right)$ | TH17 |
| 13. | $\left(\left(A\to B\right)\to B\right)\to \left(\neg A\to B\right)$ | TH1* 11,12. |
Teorema TH19: $\left(A\to C\right)\to \left(\left(B\to C\right)\to \left(\left(\left(A\to B\right)\to B\right)\to C\right)\right)$
| # | wff | razão |
| 1. | $\neg A\to \left(\neg B\to \neg \left(\neg A\to \neg \neg B\right)\right)$ | TH10 |
| 2. | $B\to \neg \neg B$ | FRG-3 |
| 3. | $\left(B\to \neg \neg B\right)\to \left(\neg A\to \left(B\to \neg \neg B\right)\right)$ | THEN-1 |
| 4. | $\neg A\to \left(B\to \neg \neg B\right)$ | MP 2,3 |
| 5. | $\left(\neg A\to \left(B\to \neg \neg B\right)\right)\to \left(\left(\neg A\to B\right)\to \left(\neg A\to \neg \neg B\right)\right)$ | THEN-2 |
| 6. | $\left(\neg A\to B\right)\to \left(\neg A\to \neg \neg B\right)$ | MP 4,5 |
| 7. | $\neg \left(\neg A\to \neg \neg B\right)\to \neg \left(\neg A\to B\right)$ | FRG-1* 6 |
| 8. | $\neg A\to \left(\neg B\to \neg \left(\neg A\to B\right)\right)$ | TH14* 1,7 |
| 9. | $\left(\left(A\to B\right)\to B\right)\to \left(\neg A\to B\right)$ | TH18 |
| 10. | $\neg \left(\neg A\to B\right)\to \neg \left(\left(A\to B\right)\to B\right)$ | FRG-1* 9 |
| 11. | $\neg A\to \left(\neg B\to \neg \left(\left(A\to B\right)\to B\right)\right)$ | TH14* 8,10 |
| 12. | $\neg C\to \left(\neg A\to \left(\neg B\to \neg \left(\left(A\to B\right)\to B\right)\right)\right)$ | THEN-1* 11 |
| 13. | $\left(\neg C\to \neg A\right)\to \left(\neg C\to \left(\neg B\to \neg \left(\left(A\to B\right)\to B\right)\right)\right)$ | THEN-2* 12 |
| 14. | $\left(\neg C\to \left(\neg B\to \neg \left(\left(A\to B\right)\to B\right)\right)\right)\to \left(\left(\neg C\to \neg B\right)\to \left(\neg C\to \neg \left(\left(A\to B\right)\to B\right)\right)\right)$ | THEN-2 |
| 15. | $\left(\neg C\to \neg A\right)\to \left(\left(\neg C\to \neg B\right)\to \left(\neg C\to \neg \left(\left(A\to B\right)\to B\right)\right)\right)$ | TH1* 13,14 |
| 16. | $\left(A\to C\right)\to \left(\neg C\to \neg A\right)$ | FRG-1 |
| 17. | $\left(A\to C\right)\to \left(\left(\to C\to \neg B\right)\to \left(\neg C\to \neg \left(\left(A\to B\right)\to B\right)\right)\right)$ | TH1* 16,15 |
| 18. | $\left(\neg C\to \neg \left(\left(A\to B\right)\to B\right)\right)\to \left(\left(\left(A\to B\right)\to B\right)\to C\right)$ | TH16 |
| 19. | $\left(A\to C\right)\to \left(\left(\neg C\to \neg B\right)\to \left(\left(\left(A\to B\right)\to B\right)\to C\right)\right)$ | TH14* 17,18 |
| 20. | $\left(B\to C\right)\to \left(\neg C\to \neg B\right)$ | FRG-1 |
| 21. | $\left(\left(B\to C\right)\to \left(\neg C\to \neg B\right)\right)\to \left(\left(\left(\neg C\to \neg B\right)\to \left(\left(\left(A\to B\right)\to B\right)\to C\right)\right)\to \left(\left(B\to C\right)\to \left(\left(\left(A\to B\right)\to B\right)\to C\right)\right)\right)$ | TH1 |
| 22. | $\left(\left(\neg C\to \neg B\right)\to \left(\left(\left(A\to B\right)\to B\right)\to C\right)\right)\to \left(\left(B\to C\right)\to \left(\left(\left(A\to B\right)\to B\right)\to C\right)\right)$ | MP 20,21 |
| 23. | $\left(A\to C\right)\to \left(\left(B\to C\right)\to \left(\left(\left(A\to B\right)\to B\right)\to C\right)\right)$ | TH1* 19,22. |
Teorema TH20: $\left(A\to \neg A\right)\to \neg A$
| # | wff | razão |
| 1. | $\left(A\to A\right)\to \left(\left(A\to \neg A\right)\to \neg A\right)$ | TH11 |
| 2. | $A\to A$ | TH7 |
| 3. | $\left(A\to \neg A\right)\to \neg A$ | MP 2,1. |
Teorema TH21: $A\to \left(\neg A\to B\right)$
| # | wff | razão |
| 1. | $A\to \left(\neg A\to \neg \neg B\right)$ | TH2, com B := ~B |
| 2. | $\neg \neg B\to B$ | FRG-2 |
| 3. | $A\to \left(\neg A\to B\right)$ | TH14* 1,2. |

### Prova de que o terceiro axioma é dedutível dos dois primeiros

O lógico e filósofo polonês Jan Łukasiewicz, famoso por seus estudos em lógicas não-clássicas, provou que o THEN-3 é dedutível do THEN-1 e do THEN-2.

#### Tese 1: $\left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)$

| # | wff | razão |
| 1. | $\left(\left(\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\to \left(\left(Q\to R\right)\to \left(\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\right)\right)$ | THEN-1* |
| 2. | $\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)$ | THEN-2 |
| 3. | $\left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)$ | MP 1,2. |
* $P/\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)$
* $Q/Q\to R$

#### Tese 2: $\left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)$

| # | wff | razão |
| 1. | $\left(\left(\left(Q\to R\right)\to \left(\left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\right)\to \left(\left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)$ | THEN-2* |
| 2. | $\left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)$ | Prop. 1 |
| 3. | $\left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)$ | MP 1,2. |
*$P/Q\to R$
*$Q/P\to \left(Q\to R\right)$
*$R/\left(P\to Q\right)\to \left(P\to R\right)$

#### Tese 3: $\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)$

| # | wff | razão |
| 1. | $\left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)$ | Prop.2 |
| 2. | $\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)$ | THEN-1* |
| 3. | $\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)$ | MP 1,2. |
* $P/Q\to R$
* $Q/P\,\!$

#### Tese 4: $\left(\left(Q\to R\right)\to \left(P\to Q\right)\right)\to \left(\left(Q\to R\right)\to \left(P\to R\right)\right)$

| # | wff | razão |
| 1. | $\left(\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\to \left(\left(\left(Q\to R\right)\to \left(P\to Q\right)\right)\to \left(\left(Q\to R\right)\to \left(P\to R\right)\right)\right)$ | THEN-2* |
| 2. | $\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)$ | Prop.3 |
| 3. | $\left(\left(Q\to R\right)\to \left(P\to Q\right)\right)\to \left(\left(Q\to R\right)\to \left(P\to R\right)\right)$ | MP 1,2. |
* $P/Q\to R$
* $Q/P\to Q$
* $R/P\to R$

#### Tese 5: $R\to \left(P\to \left(Q\to P\right)\right)$

| # | wff | razão |
| 1. | $\left(P\to \left(Q\to P\right)\right)\to \left(R\to \left(P\to \left(Q\to P\right)\right)\right)$ | THEN-1* |
| 2. | $P\to \left(Q\to P\right)$ | THEN-1 |
| 3. | $R\to \left(P\to \left(Q\to P\right)\right)$ | MP 1,2. |
* $P/P\to \left(Q\to P\right)$
* $Q/R\,\!$

#### Tese 6: $\left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)$

| # | wff | razão |
| 1. | $\left(\left(\left(P\to Q\right)\to R\right)\to \left(Q\to \left(P\to Q\right)\right)\right)\to \left(\left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)\right)$ | Prop.4* |
| 2. | $\left(\left(P\to Q\right)\to R\right)\to \left(Q\to \left(P\to Q\right)\right)$ | Prop.5** |
| 3. | $\left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)$ | MP 1,2. |
* $Q/P\to Q$
* $P/Q\,\!$
** $R/\left(P\to Q\right)\to R$
** $P/Q\,\!$
** $Q/P\,\!$

#### Tese 7: $\left(S\to \left(\left(P\to Q\right)\to R\right)\right)\to \left(S\to \left(Q\to R\right)\right)$

| # | wff | razão |
| 1. | $\left(\left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)\right)\to \left(\left(S\to \left(\left(P\to Q\right)\to R\right)\right)\to \left(S\to \left(Q\to R\right)\right)\right)$ | Prop.3* |
| 2. | $\left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)$ | Prop.6 |
| 3. | $\left(S\to \left(\left(P\to Q\right)\to R\right)\right)\to \left(S\to \left(Q\to R\right)\right)$ | MP 1,2. |
* $Q/\left(P\to Q\right)\to R$
* $R/Q\to R$
* $P/S\,\!$

#### THEN-3: $\left(P\to \left(Q\to R\right)\right)\to \left(Q\to \left(P\to R\right)\right)$

| # | wff | razão |
| 1. | $\left(\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\to \left(\left(P\to \left(Q\to R\right)\right)\to \left(Q\to \left(P\to R\right)\right)\right)$ | Prop.7* |
| 2. | $\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)$ | THEN-2 |
| 3. | $\left(P\to \left(Q\to R\right)\right)\to \left(Q\to \left(P\to R\right)\right)$ | MP 1,2. |
* $S/P\to \left(Q\to R\right)$
* $R/P\to R$
${\mathfrak {Quod\ Erat\ Demonstrandum}}$

## Axiomática de 5 operadores

* THEN-1: $\varphi \to \left(\chi \to \varphi \right)$
* THEN-2: $\left(\varphi \to \left(\chi \to \psi \right)\right)\to \left(\left(\varphi \to \chi \right)\to \left(\varphi \to \psi \right)\right)$
* AND-1: $\left(\varphi \land \chi \right)\to \varphi$
* AND-2: $\left(\varphi \land \chi \right)\to \chi$
* AND-3: $\varphi \to \left(\chi \to \left(\varphi \land \chi \right)\right)$
* OR-1: $\varphi \to \left(\varphi \lor \chi \right)$
* OR-2: $\chi \to \left(\varphi \lor \chi \right)$
* OR-3: $\left(\varphi \to \psi \right)\to \left(\left(\chi \to \psi \right)\to \left(\left(\varphi \lor \chi \right)\to \psi \right)\right)$
* NOT-1: $\left(\varphi \to \chi \right)\to \left(\left(\varphi \to \neg \chi \right)\to \neg \varphi \right)$
* NOT-2: $\varphi \to \left(\neg \varphi \to \chi \right)$
* NOT-3: $\varphi \lor \neg \varphi$
* IFF-1: $\left(\varphi \leftrightarrow \chi \right)\to \left(\varphi \to \chi \right)$
* IFF-2: $\left(\varphi \leftrightarrow \chi \right)\to \left(\chi \to \varphi \right)$
* IFF-3: $\left(\varphi \to \chi \right)\to \left(\left(\chi \to \varphi \right)\to \left(\varphi \leftrightarrow \chi \right)\right)$

### Alguns Teoremas

* $\alpha \to \alpha \,\!$
| # | wff | razão |
| 1. | $\alpha \to \left(\alpha \to \alpha \right)$ | THEN-1* |
| 2. | $\alpha \to \left(\left(\alpha \to \alpha \right)\to \alpha \right)$ | THEN-1** |
| 3. | $\left(\alpha \to \left(\left(\alpha \to \alpha \right)\to \alpha \right)\right)\to \left(\left(\alpha \to \left(\alpha \to \alpha \right)\right)\to \left(\alpha \to \alpha \right)\right)$ | THEN-2***. |
| 4. | $\left(\left(\alpha \to \left(\alpha \to \alpha \right)\right)\to \left(\alpha \to \alpha \right)\right)$ | 2,3 MP. |
| 5. | $\alpha \to \alpha \,\!$ | 1,4 MP. |
* $\varphi /\alpha \,\!$ , $\chi /\alpha \,\!$
** $\varphi /\alpha \,\!$ , $\chi /\alpha \to \alpha \,\!$
*** $\varphi /\alpha \,\!$ , $\chi /\alpha \to \alpha \,\!$ , $\psi /\alpha \,\!$