Lógica: Cálculo Proposicional Clássico: Axiomática

acima: Voltar para o índice de Cálculo Proposicional Clássico
anterior: Dedução Natural - Parte II | próximo: Cálculo de Sequêntes

Introdução

Uma outra forma de lidar sintáticamente com o CPC é axiomáticamente. 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.

THEN-1: $P\to \left(Q\to P\right)$

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

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 \,\!$