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 $\mathrm{\Delta }$ o conjunto dos axiomas e todas suas instâncias, se $\mathrm{\Delta }⊢\alpha$, então $⊢\alpha$. Ou seja, se $\alpha$ é dedutível dos axiomas, então $\alpha$ é teorema.

E seja $\mathrm{\Gamma }$ um conjunto qualquer de fórmulas, se $\mathrm{\Delta }\cup \mathrm{\Gamma }⊢\alpha$ então $\mathrm{\Gamma }⊢\alpha$. Ou seja, se $\alpha$ é dedutível de um conjunto $\mathrm{\Gamma }$ de fórmulas juntamente com os axiomas, então um raciocínio que tenha $\mathrm{\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 (B\to A)$
THEN-2: $(A\to (B\to C))\to ((A\to B)\to (A\to C))$
THEN-3: $(A\to (B\to C))\to (B\to (A\to C))$
FRG-1: $(A\to B)\to (\mathrm{\neg }B\to \mathrm{\neg }A)$
FRG-2: $\mathrm{\neg }\mathrm{\neg }A\to A$
FRG-3: $A\to \mathrm{\neg }\mathrm{\neg }A$

• Regra de Inferência

MP: $\{P,P\to Q\}⊢Q$

Regra THEN-1*: $A⊢(B\to A)$

#	wff	razão
1.	$A$	premissa
2.	$A\to (B\to A)$	THEN-1
3.	$B\to A$	MP 1,2.

Regra THEN-2*: $A\to (B\to C)⊢(A\to B)\to (A\to C)$

#	wff	razão
1.	$A\to (B\to C)$	premissa
2.	$(A\to (B\to C))\to ((A\to B)\to (A\to C))$	THEN-2
3.	$(A\to B)\to (A\to C)$	MP 1,2.

Regra THEN-3*: $A\to (B\to C)⊢B\to (A\to C)$

#	wff	razão
1.	$A\to (B\to C)$	premissa
2.	$(A\to (B\to C))\to (B\to (A\to C))$	THEN-3
3.	$B\to (A\to C)$	MP 1,2.

Regra FRG-1*: $A\to B⊢\mathrm{\neg }B\to \mathrm{\neg }A$

#	wff	razão
1.	$(A\to B)\to (\mathrm{\neg }B\to \mathrm{\neg }A)$	FRG-1
2.	$A\to B$	premissa
3.	$\mathrm{\neg }B\to \mathrm{\neg }A$	MP 2,1.

Regra TH1*: $A\to B,B\to C⊢A\to C$

#	wff	razão
1.	$B\to C$	premissa
2.	$(B\to C)\to (A\to (B\to C))$	THEN-1
3.	$A\to (B\to C)$	MP 1,2
4.	$(A\to (B\to C))\to ((A\to B)\to (A\to C))$	THEN-2
5.	$(A\to B)\to (A\to C)$	MP 3,4
6.	$A\to B$	premissa
7.	$A\to C$	MP 6,5.

Teorema TH1: $(A\to B)\to ((B\to C)\to (A\to C))$

#	wff	razão
1.	$(B\to C)\to (A\to (B\to C))$	THEN-1
2.	$(A\to (B\to C))\to ((A\to B)\to (A\to C))$	THEN-2
3.	$(B\to C)\to ((A\to B)\to (A\to C))$	TH1* 1,2
4.	$((B\to C)\to ((A\to B)\to (A\to C)))\to ((A\to B)\to ((B\to C)\to (A\to C)))$	THEN-3
5.	$(A\to B)\to ((B\to C)\to (A\to C))$	MP 3,4.

Teorema TH2: $A\to (\mathrm{\neg }A\to \mathrm{\neg }B)$

#	wff	razão
1.	$A\to (B\to A)$	THEN-1
2.	$(B\to A)\to (\mathrm{\neg }A\to \mathrm{\neg }B)$	FRG-1
3.	$A\to (\mathrm{\neg }A\to \mathrm{\neg }B)$	TH1* 1,2.

Teorema TH3: $\mathrm{\neg }A\to (A\to \mathrm{\neg }B)$

#	wff	razão
1.	$A\to (\mathrm{\neg }A\to \mathrm{\neg }B)$	TH 2
2.	$(A\to (\mathrm{\neg }A\to \mathrm{\neg }B))\to (\mathrm{\neg }A\to (A\to \mathrm{\neg }B))$	THEN-3
3.	$\mathrm{\neg }A\to (A\to \mathrm{\neg }B)$	MP 1,2.

Teorema TH4: $\mathrm{\neg }(A\to \mathrm{\neg }B)\to A$

#	wff	razão
1.	$\mathrm{\neg }A\to (A\to \mathrm{\neg }B)$	TH3
2.	$(\mathrm{\neg }A\to (A\to \mathrm{\neg }B))\to (\mathrm{\neg }(A\to \mathrm{\neg }B)\to \mathrm{\neg }\mathrm{\neg }A)$	FRG-1
3.	$\mathrm{\neg }(A\to \mathrm{\neg }B)\to \mathrm{\neg }\mathrm{\neg }A$	MP 1,2
4.	$\mathrm{\neg }\mathrm{\neg }A\to A$	FRG-2
5.	$\mathrm{\neg }(A\to \mathrm{\neg }B)\to A$	TH1* 3,4.

Teorema TH5: $(A\to \mathrm{\neg }B)\to (B\to \mathrm{\neg }A)$

#	wff	razão
1.	$(A\to \mathrm{\neg }B)\to (\mathrm{\neg }\mathrm{\neg }B\to \mathrm{\neg }A)$	FRG-1
2.	$((A\to \mathrm{\neg }B)\to (\mathrm{\neg }\mathrm{\neg }B\to \mathrm{\neg }A))\to (\mathrm{\neg }\mathrm{\neg }B\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }A))$	THEN-3
3.	$\mathrm{\neg }\mathrm{\neg }B\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }A)$	MP 1,2
4.	$B\to \mathrm{\neg }\mathrm{\neg }B$	FRG-3, with A := B
5.	$B\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }A)$	TH1* 4,3
6.	$(B\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }A))\to ((A\to \mathrm{\neg }B)\to (B\to \mathrm{\neg }A))$	FRG-1
7.	$(A\to \mathrm{\neg }B)\to (B\to \mathrm{\neg }A)$	MP 5,6.

Teorema TH6: $\mathrm{\neg }(A\to \mathrm{\neg }B)\to B$

#	wff	razão
1.	$\mathrm{\neg }(B\to \mathrm{\neg }A)\to B$	TH4, with A := B, B := A
2.	$(B\to \mathrm{\neg }A)\to (A\to \mathrm{\neg }B)$	TH5, with A := B, B := A
3.	$((B\to \mathrm{\neg }A)\to (A\to \mathrm{\neg }B))\to (\mathrm{\neg }(A\to \mathrm{\neg }B)\to \mathrm{\neg }(B\to \mathrm{\neg }A))$	FRG-1
4.	$\mathrm{\neg }(A\to \mathrm{\neg }B)\to \mathrm{\neg }(B\to \mathrm{\neg }A)$	MP 2,3
5.	$\mathrm{\neg }(A\to \mathrm{\neg }B)\to B$	TH1* 4,1.

Teorema TH7: $A\to A$

#	wff	razão
1.	$A\to \mathrm{\neg }\mathrm{\neg }A$	FRG-3
2.	$\mathrm{\neg }\mathrm{\neg }A\to A$	FRG-2
3.	$A\to A$	TH1* 1,2.

Teorema TH8: $A\to ((A\to B)\to B)$

#	wff	razão
1.	$(A\to B)\to (A\to B)$	TH7, com A := $A\to B$
2.	$((A\to B)\to (A\to B))\to (A\to ((A\to B)\to B))$	THEN-3
3.	$A\to ((A\to B)\to B)$	MP 1,2.

Teorema TH9: $B\to ((A\to B)\to B)$

#	wff	razão
1.	$B\to ((A\to B)\to B)$	THEN-1, com A := B, B := $A\to B$.

Teorema TH10: $A\to (B\to \mathrm{\neg }(A\to \mathrm{\neg }B))$

#	wff	razão
1.	$(A\to \mathrm{\neg }B)\to (A\to \mathrm{\neg }B)$	TH7
2.	$((A\to \mathrm{\neg }B)\to (A\to \mathrm{\neg }B))\to (A\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }B))$	THEN-3
3.	$A\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }B)$	MP 1,2
4.	$((A\to \mathrm{\neg }B)\to \mathrm{\neg }B)\to (B\to \mathrm{\neg }(A\to \mathrm{\neg }B))$	TH5
5.	$A\to (B\to \mathrm{\neg }(A\to \mathrm{\neg }B))$	TH1* 3,4.

Teorema TH11: $(A\to B)\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }A)$

#	wff	razão
1.	$A\to (B\to \mathrm{\neg }(A\to \mathrm{\neg }B))$	TH10
2.	$(A\to (B\to \mathrm{\neg }(A\to \mathrm{\neg }B)))\to ((A\to B)\to (A\to \mathrm{\neg }(A\to \mathrm{\neg }B)))$	THEN-2
3.	$(A\to B)\to (A\to \mathrm{\neg }(A\to \mathrm{\neg }B))$	MP 1,2
4.	$(A\to \mathrm{\neg }(A\to \mathrm{\neg }B))\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }A)$	TH5
5.	$(A\to B)\to ((A\to \mathrm{\neg }B)\to \mathrm{\neg }A)$	TH1* 3,4.

Teorema TH12: $((A\to B)\to C)\to (A\to (B\to C))$

#	wff	razão
1.	$B\to (A\to B)$	THEN-1
2.	$(B\to (A\to B))\to (((A\to B)\to C)\to (B\to C))$	TH1
3.	$((A\to B)\to C)\to (B\to C)$	MP 1,2
4.	$(B\to C)\to (A\to (B\to C))$	THEN-1
5.	$((A\to B)\to C)\to (A\to (B\to C))$	TH1* 3,4.

Teorema TH13: $(B\to (B\to C))\to (B\to C)$

#	wff	razão
1.	$(B\to (B\to C))\to ((B\to B)\to (B\to C))$	THEN-2
2.	$(B\to B)\to ((B\to (B\to C))\to (B\to C))$	THEN-3* 1
3.	$B\to B$	TH7
4.	$(B\to (B\to C))\to (B\to C)$	MP 3,2.

Regra TH14*: $\{A\to (B\to P),P\to Q\}⊢A\to (B\to Q)$

#	wff	razão
1.	$P\to Q$	premissa
2.	$(P\to Q)\to (B\to (P\to Q))$	THEN-1
3.	$B\to (P\to Q)$	MP 1,2
4.	$(B\to (P\to Q))\to ((B\to P)\to (B\to Q))$	THEN-2
5.	$(B\to P)\to (B\to Q)$	MP 3,4
6.	$((B\to P)\to (B\to Q))\to (A\to ((B\to P)\to (B\to Q)))$	THEN-1
7.	$A\to ((B\to P)\to (B\to Q))$	MP 5,6
8.	$(A\to (B\to P))\to (A\to (B\to Q))$	THEN-2* 7
9.	$A\to (B\to P)$	premissa
10.	$A\to (B\to Q)$	MP 9,8.

Teorema TH15: $((A\to B)\to (A\to C))\to (A\to (B\to C))$

#	wff	razão
1.	$((A\to B)\to (A\to C))\to (((A\to B)\to A)\to ((A\to B)\to C))$	THEN-2
2.	$((A\to B)\to C)\to (A\to (B\to C))$	TH12
3.	$((A\to B)\to (A\to C))\to (((A\to B)\to A)\to (A\to (B\to C)))$	TH14* 1,2
4.	$((A\to B)\to A)\to (((A\to B)\to (A\to C))\to (A\to (B\to C)))$	THEN-3* 3
5.	$A\to ((A\to B)\to A)$	THEN-1
6.	$A\to (((A\to B)\to (A\to C))\to (A\to (B\to C)))$	TH1* 5,4
7.	$((A\to B)\to (A\to C))\to (A\to (A\to (B\to C)))$	THEN-3* 6
8.	$(A\to (A\to (B\to C)))\to (A\to (B\to C))$	TH13
9.	$((A\to B)\to (A\to C))\to (A\to (B\to C))$	TH1* 7,8.

Teorema TH16: $(\mathrm{\neg }A\to \mathrm{\neg }B)\to (B\to A)$

#	wff	razão
1.	$(\mathrm{\neg }A\to \mathrm{\neg }B)\to (\mathrm{\neg }\mathrm{\neg }B\to \mathrm{\neg }\mathrm{\neg }A)$	FRG-1
2.	$\mathrm{\neg }\mathrm{\neg }B\to ((\mathrm{\neg }A\to \mathrm{\neg }B)\to \mathrm{\neg }\mathrm{\neg }A)$	THEN-3* 1
3.	$B\to \mathrm{\neg }\mathrm{\neg }B$	FRG-3
4.	$B\to ((\mathrm{\neg }A\to \mathrm{\neg }B)\to \mathrm{\neg }\mathrm{\neg }A)$	TH1* 3,2
5.	$(\mathrm{\neg }A\to \mathrm{\neg }B)\to (B\to \mathrm{\neg }\mathrm{\neg }A)$	THEN-3* 4
6.	$\mathrm{\neg }\mathrm{\neg }A\to A$	FRG-2
7.	$(\mathrm{\neg }\mathrm{\neg }A\to A)\to (B\to (\mathrm{\neg }\mathrm{\neg }A\to A))$	THEN-1
8.	$B\to (\mathrm{\neg }\mathrm{\neg }A\to A)$	MP 6,7
9.	$(B\to (\mathrm{\neg }\mathrm{\neg }A\to A))\to ((B\to \mathrm{\neg }\mathrm{\neg }A)\to (B\to A))$	THEN-2
10.	$(B\to \mathrm{\neg }\mathrm{\neg }A)\to (B\to A)$	MP 8,9
11.	$(\mathrm{\neg }A\to \mathrm{\neg }B)\to (B\to A)$	TH1* 5,10.

Teorema TH17: $(\mathrm{\neg }A\to B)\to (\mathrm{\neg }B\to A)$

#	wff	razão
1.	$(\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }B)\to (\mathrm{\neg }B\to A)$	TH16, com B := \neg B
2.	$B\to \mathrm{\neg }\mathrm{\neg }B$	FRG-3
3.	$(B\to \mathrm{\neg }\mathrm{\neg }B)\to (\mathrm{\neg }A\to (B\to \mathrm{\neg }\mathrm{\neg }B))$	THEN-1
4.	$\mathrm{\neg }A\to (B\to \mathrm{\neg }\mathrm{\neg }B)$	MP 2,3
5.	$(\mathrm{\neg }A\to (B\to \mathrm{\neg }\mathrm{\neg }B))\to ((\mathrm{\neg }A\to B)\to (\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }B))$	THEN-2
6.	$(\mathrm{\neg }A\to B)\to (\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }B)$	MP 4,5
7.	$(\mathrm{\neg }A\to B)\to (\mathrm{\neg }B\to A)$	TH1* 6,1.

Teorema TH18: $((A\to B)\to B)\to (\mathrm{\neg }A\to B)$

#	wff	razão
1.	$(A\to B)\to (\mathrm{\neg }B\to (A\to B))$	THEN-1
2.	$(\mathrm{\neg }B\to \mathrm{\neg }A)\to (A\to B)$	TH16
3.	$(\mathrm{\neg }B\to \mathrm{\neg }A)\to (\mathrm{\neg }B\to (A\to B))$	TH1* 2,1
4.	$((\mathrm{\neg }B\to \mathrm{\neg }A)\to (\mathrm{\neg }B\to (A\to B)))\to (\mathrm{\neg }B\to (\mathrm{\neg }A\to (A\to B)))$	TH15
5.	$\mathrm{\neg }B\to (\mathrm{\neg }A\to (A\to B))$	MP 3,4
6.	$(\mathrm{\neg }A\to (A\to B))\to (\mathrm{\neg }(A\to B)\to A)$	TH17
7.	$\mathrm{\neg }B\to (\mathrm{\neg }(A\to B)\to A)$	TH1* 5,6
8.	$(\mathrm{\neg }B\to (\mathrm{\neg }(A\to B)\to A))\to ((\mathrm{\neg }B\to \mathrm{\neg }(A\to B))\to (\mathrm{\neg }B\to A))$	THEN-2
9.	$(\mathrm{\neg }B\to \mathrm{\neg }(A\to B))\to (\mathrm{\neg }B\to A)$	MP 7,8
10.	$((A\to B)\to B)\to (\mathrm{\neg }B\to \mathrm{\neg }(A\to B))$	FRG-1
11.	$((A\to B)\to B)\to (\mathrm{\neg }B\to A)$	TH1* 10,9
12.	$(\mathrm{\neg }B\to A)\to (\mathrm{\neg }A\to B)$	TH17
13.	$((A\to B)\to B)\to (\mathrm{\neg }A\to B)$	TH1* 11,12.

Teorema TH19: $(A\to C)\to ((B\to C)\to (((A\to B)\to B)\to C))$

#	wff	razão
1.	$\mathrm{\neg }A\to (\mathrm{\neg }B\to \mathrm{\neg }(\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }B))$	TH10
2.	$B\to \mathrm{\neg }\mathrm{\neg }B$	FRG-3
3.	$(B\to \mathrm{\neg }\mathrm{\neg }B)\to (\mathrm{\neg }A\to (B\to \mathrm{\neg }\mathrm{\neg }B))$	THEN-1
4.	$\mathrm{\neg }A\to (B\to \mathrm{\neg }\mathrm{\neg }B)$	MP 2,3
5.	$(\mathrm{\neg }A\to (B\to \mathrm{\neg }\mathrm{\neg }B))\to ((\mathrm{\neg }A\to B)\to (\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }B))$	THEN-2
6.	$(\mathrm{\neg }A\to B)\to (\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }B)$	MP 4,5
7.	$\mathrm{\neg }(\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }B)\to \mathrm{\neg }(\mathrm{\neg }A\to B)$	FRG-1* 6
8.	$\mathrm{\neg }A\to (\mathrm{\neg }B\to \mathrm{\neg }(\mathrm{\neg }A\to B))$	TH14* 1,7
9.	$((A\to B)\to B)\to (\mathrm{\neg }A\to B)$	TH18
10.	$\mathrm{\neg }(\mathrm{\neg }A\to B)\to \mathrm{\neg }((A\to B)\to B)$	FRG-1* 9
11.	$\mathrm{\neg }A\to (\mathrm{\neg }B\to \mathrm{\neg }((A\to B)\to B))$	TH14* 8,10
12.	$\mathrm{\neg }C\to (\mathrm{\neg }A\to (\mathrm{\neg }B\to \mathrm{\neg }((A\to B)\to B)))$	THEN-1* 11
13.	$(\mathrm{\neg }C\to \mathrm{\neg }A)\to (\mathrm{\neg }C\to (\mathrm{\neg }B\to \mathrm{\neg }((A\to B)\to B)))$	THEN-2* 12
14.	$(\mathrm{\neg }C\to (\mathrm{\neg }B\to \mathrm{\neg }((A\to B)\to B)))\to ((\mathrm{\neg }C\to \mathrm{\neg }B)\to (\mathrm{\neg }C\to \mathrm{\neg }((A\to B)\to B)))$	THEN-2
15.	$(\mathrm{\neg }C\to \mathrm{\neg }A)\to ((\mathrm{\neg }C\to \mathrm{\neg }B)\to (\mathrm{\neg }C\to \mathrm{\neg }((A\to B)\to B)))$	TH1* 13,14
16.	$(A\to C)\to (\mathrm{\neg }C\to \mathrm{\neg }A)$	FRG-1
17.	$(A\to C)\to ((\to C\to \mathrm{\neg }B)\to (\mathrm{\neg }C\to \mathrm{\neg }((A\to B)\to B)))$	TH1* 16,15
18.	$(\mathrm{\neg }C\to \mathrm{\neg }((A\to B)\to B))\to (((A\to B)\to B)\to C)$	TH16
19.	$(A\to C)\to ((\mathrm{\neg }C\to \mathrm{\neg }B)\to (((A\to B)\to B)\to C))$	TH14* 17,18
20.	$(B\to C)\to (\mathrm{\neg }C\to \mathrm{\neg }B)$	FRG-1
21.	$((B\to C)\to (\mathrm{\neg }C\to \mathrm{\neg }B))\to (((\mathrm{\neg }C\to \mathrm{\neg }B)\to (((A\to B)\to B)\to C))\to ((B\to C)\to (((A\to B)\to B)\to C)))$	TH1
22.	$((\mathrm{\neg }C\to \mathrm{\neg }B)\to (((A\to B)\to B)\to C))\to ((B\to C)\to (((A\to B)\to B)\to C))$	MP 20,21
23.	$(A\to C)\to ((B\to C)\to (((A\to B)\to B)\to C))$	TH1* 19,22.

Teorema TH20: $(A\to \mathrm{\neg }A)\to \mathrm{\neg }A$

#	wff	razão
1.	$(A\to A)\to ((A\to \mathrm{\neg }A)\to \mathrm{\neg }A)$	TH11
2.	$A\to A$	TH7
3.	$(A\to \mathrm{\neg }A)\to \mathrm{\neg }A$	MP 2,1.

Teorema TH21: $A\to (\mathrm{\neg }A\to B)$

#	wff	razão
1.	$A\to (\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }B)$	TH2, com B := ~B
2.	$\mathrm{\neg }\mathrm{\neg }B\to B$	FRG-2
3.	$A\to (\mathrm{\neg }A\to B)$	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 (Q\to P)$

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

• Tese 1: $((Q\to R)\to (P\to (Q\to R)))\to ((P\to Q)\to (P\to R))$

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

* $P/(P\to (Q\to R))\to ((P\to Q)\to (P\to R))$

* $Q/Q\to R$

• Tese 2: $((Q\to R)\to (P\to (Q\to R)))\to ((Q\to R)\to ((P\to Q)\to (P\to R)))$

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

*$P/Q\to R$

*$Q/P\to (Q\to R)$

*$R/(P\to Q)\to (P\to R)$

• Tese 3: $(Q\to R)\to ((P\to Q)\to (P\to R))$

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

* $P/Q\to R$

* $Q/P$

• Tese 4: $((Q\to R)\to (P\to Q))\to ((Q\to R)\to (P\to R))$

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

* $P/Q\to R$

* $Q/P\to Q$

* $R/P\to R$

• Tese 5: $R\to (P\to (Q\to P))$

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

* $P/P\to (Q\to P)$

* $Q/R$

• Tese 6: $((P\to Q)\to R)\to (Q\to R)$

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

* $Q/P\to Q$

* $P/Q$

** $R/(P\to Q)\to R$

** $P/Q$

** $Q/P$

• Tese 7: $(S\to ((P\to Q)\to R))\to (S\to (Q\to R))$

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

* $Q/(P\to Q)\to R$

* $R/Q\to R$

* $P/S$

• THEN-3: $(P\to (Q\to R))\to (Q\to (P\to R))$

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

* $S/P\to (Q\to R)$

* $R/P\to R$

$𝔔𝔲𝔬𝔡𝔈𝔯𝔞𝔱𝔇𝔢𝔪𝔬𝔫𝔰𝔱𝔯𝔞𝔫𝔡𝔲𝔪$

Axiomática de 5 operadores

• THEN-1: $\phi \to (\chi \to \phi )$
• THEN-2: $(\phi \to (\chi \to \psi ))\to ((\phi \to \chi )\to (\phi \to \psi ))$
• AND-1: $(\phi \wedge \chi )\to \phi$
• AND-2: $(\phi \wedge \chi )\to \chi$
• AND-3: $\phi \to (\chi \to (\phi \wedge \chi ))$
• OR-1: $\phi \to (\phi \vee \chi )$
• OR-2: $\chi \to (\phi \vee \chi )$
• OR-3: $(\phi \to \psi )\to ((\chi \to \psi )\to ((\phi \vee \chi )\to \psi ))$
• NOT-1: $(\phi \to \chi )\to ((\phi \to \mathrm{\neg }\chi )\to \mathrm{\neg }\phi )$
• NOT-2: $\phi \to (\mathrm{\neg }\phi \to \chi )$
• NOT-3: $\phi \vee \mathrm{\neg }\phi$
• IFF-1: $(\phi \leftrightarrow \chi )\to (\phi \to \chi )$
• IFF-2: $(\phi \leftrightarrow \chi )\to (\chi \to \phi )$
• IFF-3: $(\phi \to \chi )\to ((\chi \to \phi )\to (\phi \leftrightarrow \chi ))$

Alguns Teoremas

• $\alpha \to \alpha$

#	wff	razão
1.	$\alpha \to (\alpha \to \alpha )$	THEN-1*
2.	$\alpha \to ((\alpha \to \alpha )\to \alpha )$	THEN-1**
3.	$(\alpha \to ((\alpha \to \alpha )\to \alpha ))\to ((\alpha \to (\alpha \to \alpha ))\to (\alpha \to \alpha ))$	THEN-2***.
4.	$((\alpha \to (\alpha \to \alpha ))\to (\alpha \to \alpha ))$	2,3 MP.
5.	$\alpha \to \alpha$	1,4 MP.

* $\phi /\alpha$ , $\chi /\alpha$

** $\phi /\alpha$ , $\chi /\alpha \to \alpha$

*** $\phi /\alpha$ , $\chi /\alpha \to \alpha$ , $\psi /\alpha$