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".
THEN-1:
A
→
(
B
→
A
)
{\displaystyle A\to \left(B\to A\right)}
THEN-2:
(
A
→
(
B
→
C
)
)
→
(
(
A
→
B
)
→
(
A
→
C
)
)
{\displaystyle \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:
(
A
→
(
B
→
C
)
)
→
(
B
→
(
A
→
C
)
)
{\displaystyle \left(A\to \left(B\to C\right)\right)\to \left(B\to \left(A\to C\right)\right)}
FRG-1:
(
A
→
B
)
→
(
¬
B
→
¬
A
)
{\displaystyle \left(A\to B\right)\to \left(\neg B\to \neg A\right)}
FRG-2:
¬
¬
A
→
A
{\displaystyle \neg \neg A\to A\,\!}
FRG-3:
A
→
¬
¬
A
{\displaystyle A\to \neg \neg A\,\!}
MP:
{
P
,
P
→
Q
}
⊢
Q
{\displaystyle \left\{P,P\to Q\right\}\vdash Q}
Regra THEN-1*:
A
⊢
(
B
→
A
)
{\displaystyle A\vdash \left(B\to A\right)}
#
wff
razão
1.
A
{\displaystyle A\,\!}
premissa
2.
A
→
(
B
→
A
)
{\displaystyle A\to \left(B\to A\right)}
THEN-1
3.
B
→
A
{\displaystyle B\to A\,\!}
MP 1,2.
Regra THEN-2*:
A
→
(
B
→
C
)
⊢
(
A
→
B
)
→
(
A
→
C
)
{\displaystyle A\to \left(B\to C\right)\vdash \left(A\to B\right)\to \left(A\to C\right)}
#
wff
razão
1.
A
→
(
B
→
C
)
{\displaystyle A\to \left(B\to C\right)}
premissa
2.
(
A
→
(
B
→
C
)
)
→
(
(
A
→
B
)
→
(
A
→
C
)
)
{\displaystyle \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.
(
A
→
B
)
→
(
A
→
C
)
{\displaystyle \left(A\to B\right)\to \left(A\to C\right)}
MP 1,2.
Regra THEN-3*:
A
→
(
B
→
C
)
⊢
B
→
(
A
→
C
)
{\displaystyle A\to \left(B\to C\right)\vdash B\to \left(A\to C\right)}
#
wff
razão
1.
A
→
(
B
→
C
)
{\displaystyle A\to \left(B\to C\right)}
premissa
2.
(
A
→
(
B
→
C
)
)
→
(
B
→
(
A
→
C
)
)
{\displaystyle \left(A\to \left(B\to C\right)\right)\to \left(B\to \left(A\to C\right)\right)}
THEN-3
3.
B
→
(
A
→
C
)
{\displaystyle B\to \left(A\to C\right)}
MP 1,2.
Regra FRG-1*:
A
→
B
⊢
¬
B
→
¬
A
{\displaystyle A\to B\vdash \neg B\to \neg A}
#
wff
razão
1.
(
A
→
B
)
→
(
¬
B
→
¬
A
)
{\displaystyle \left(A\to B\right)\to \left(\neg B\to \neg A\right)}
FRG-1
2.
A
→
B
{\displaystyle A\to B}
premissa
3.
¬
B
→
¬
A
{\displaystyle \neg B\to \neg A}
MP 2,1.
Regra TH1*:
A
→
B
,
B
→
C
⊢
A
→
C
{\displaystyle A\to B,B\to C\vdash A\to C}
#
wff
razão
1.
B
→
C
{\displaystyle B\to C}
premissa
2.
(
B
→
C
)
→
(
A
→
(
B
→
C
)
)
{\displaystyle \left(B\to C\right)\to \left(A\to \left(B\to C\right)\right)}
THEN-1
3.
A
→
(
B
→
C
)
{\displaystyle A\to \left(B\to C\right)}
MP 1,2
4.
(
A
→
(
B
→
C
)
)
→
(
(
A
→
B
)
→
(
A
→
C
)
)
{\displaystyle \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.
(
A
→
B
)
→
(
A
→
C
)
{\displaystyle \left(A\to B\right)\to \left(A\to C\right)}
MP 3,4
6.
A
→
B
{\displaystyle A\to B}
premissa
7.
A
→
C
{\displaystyle A\to C}
MP 6,5.
Teorema TH1:
(
A
→
B
)
→
(
(
B
→
C
)
→
(
A
→
C
)
)
{\displaystyle \left(A\to B\right)\to \left(\left(B\to C\right)\to \left(A\to C\right)\right)}
#
wff
razão
1.
(
B
→
C
)
→
(
A
→
(
B
→
C
)
)
{\displaystyle \left(B\to C\right)\to \left(A\to \left(B\to C\right)\right)}
THEN-1
2.
(
A
→
(
B
→
C
)
)
→
(
(
A
→
B
)
→
(
A
→
C
)
)
{\displaystyle \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.
(
B
→
C
)
→
(
(
A
→
B
)
→
(
A
→
C
)
)
{\displaystyle \left(B\to C\right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)}
TH1* 1,2
4.
(
(
B
→
C
)
→
(
(
A
→
B
)
→
(
A
→
C
)
)
)
→
(
(
A
→
B
)
→
(
(
B
→
C
)
→
(
A
→
C
)
)
)
{\displaystyle \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.
(
A
→
B
)
→
(
(
B
→
C
)
→
(
A
→
C
)
)
{\displaystyle \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
→
(
¬
A
→
¬
B
)
{\displaystyle A\to \left(\neg A\to \neg B\right)}
#
wff
razão
1.
A
→
(
B
→
A
)
{\displaystyle A\to \left(B\to A\right)}
THEN-1
2.
(
B
→
A
)
→
(
¬
A
→
¬
B
)
{\displaystyle \left(B\to A\right)\to \left(\neg A\to \neg B\right)}
FRG-1
3.
A
→
(
¬
A
→
¬
B
)
{\displaystyle A\to \left(\neg A\to \neg B\right)}
TH1* 1,2.
Teorema TH3:
¬
A
→
(
A
→
¬
B
)
{\displaystyle \neg A\to \left(A\to \neg B\right)}
#
wff
razão
1.
A
→
(
¬
A
→
¬
B
)
{\displaystyle A\to \left(\neg A\to \neg B\right)}
TH 2
2.
(
A
→
(
¬
A
→
¬
B
)
)
→
(
¬
A
→
(
A
→
¬
B
)
)
{\displaystyle \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.
¬
A
→
(
A
→
¬
B
)
{\displaystyle \neg A\to \left(A\to \neg B\right)}
MP 1,2.
Teorema TH4:
¬
(
A
→
¬
B
)
→
A
{\displaystyle \neg \left(A\to \neg B\right)\to A}
#
wff
razão
1.
¬
A
→
(
A
→
¬
B
)
{\displaystyle \neg A\to \left(A\to \neg B\right)}
TH3
2.
(
¬
A
→
(
A
→
¬
B
)
)
→
(
¬
(
A
→
¬
B
)
→
¬
¬
A
)
{\displaystyle \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.
¬
(
A
→
¬
B
)
→
¬
¬
A
{\displaystyle \neg \left(A\to \neg B\right)\to \neg \neg A}
MP 1,2
4.
¬
¬
A
→
A
{\displaystyle \neg \neg A\to A}
FRG-2
5.
¬
(
A
→
¬
B
)
→
A
{\displaystyle \neg \left(A\to \neg B\right)\to A}
TH1* 3,4.
Teorema TH5:
(
A
→
¬
B
)
→
(
B
→
¬
A
)
{\displaystyle \left(A\to \neg B\right)\to \left(B\to \neg A\right)}
#
wff
razão
1.
(
A
→
¬
B
)
→
(
¬
¬
B
→
¬
A
)
{\displaystyle \left(A\to \neg B\right)\to \left(\neg \neg B\to \neg A\right)}
FRG-1
2.
(
(
A
→
¬
B
)
→
(
¬
¬
B
→
¬
A
)
)
→
(
¬
¬
B
→
(
(
A
→
¬
B
)
→
¬
A
)
)
{\displaystyle \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.
¬
¬
B
→
(
(
A
→
¬
B
)
→
¬
A
)
{\displaystyle \neg \neg B\to \left(\left(A\to \neg B\right)\to \neg A\right)}
MP 1,2
4.
B
→
¬
¬
B
{\displaystyle B\to \neg \neg B}
FRG-3, with A := B
5.
B
→
(
(
A
→
¬
B
)
→
¬
A
)
{\displaystyle B\to \left(\left(A\to \neg B\right)\to \neg A\right)}
TH1* 4,3
6.
(
B
→
(
(
A
→
¬
B
)
→
¬
A
)
)
→
(
(
A
→
¬
B
)
→
(
B
→
¬
A
)
)
{\displaystyle \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.
(
A
→
¬
B
)
→
(
B
→
¬
A
)
{\displaystyle \left(A\to \neg B\right)\to \left(B\to \neg A\right)}
MP 5,6.
Teorema TH6:
¬
(
A
→
¬
B
)
→
B
{\displaystyle \neg \left(A\to \neg B\right)\to B}
#
wff
razão
1.
¬
(
B
→
¬
A
)
→
B
{\displaystyle \neg \left(B\to \neg A\right)\to B}
TH4, with A := B, B := A
2.
(
B
→
¬
A
)
→
(
A
→
¬
B
)
{\displaystyle \left(B\to \neg A\right)\to \left(A\to \neg B\right)}
TH5, with A := B, B := A
3.
(
(
B
→
¬
A
)
→
(
A
→
¬
B
)
)
→
(
¬
(
A
→
¬
B
)
→
¬
(
B
→
¬
A
)
)
{\displaystyle \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.
¬
(
A
→
¬
B
)
→
¬
(
B
→
¬
A
)
{\displaystyle \neg \left(A\to \neg B\right)\to \neg \left(B\to \neg A\right)}
MP 2,3
5.
¬
(
A
→
¬
B
)
→
B
{\displaystyle \neg \left(A\to \neg B\right)\to B}
TH1* 4,1.
Teorema TH7:
A
→
A
{\displaystyle A\to A}
#
wff
razão
1.
A
→
¬
¬
A
{\displaystyle A\to \neg \neg A}
FRG-3
2.
¬
¬
A
→
A
{\displaystyle \neg \neg A\to A}
FRG-2
3.
A
→
A
{\displaystyle A\to A}
TH1* 1,2.
Teorema TH8:
A
→
(
(
A
→
B
)
→
B
)
{\displaystyle A\to \left(\left(A\to B\right)\to B\right)}
#
wff
razão
1.
(
A
→
B
)
→
(
A
→
B
)
{\displaystyle \left(A\to B\right)\to \left(A\to B\right)}
TH7, com A :=
A
→
B
{\displaystyle A\to B}
2.
(
(
A
→
B
)
→
(
A
→
B
)
)
→
(
A
→
(
(
A
→
B
)
→
B
)
)
{\displaystyle \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
→
(
(
A
→
B
)
→
B
)
{\displaystyle A\to \left(\left(A\to B\right)\to B\right)}
MP 1,2.
Teorema TH9:
B
→
(
(
A
→
B
)
→
B
)
{\displaystyle B\to \left(\left(A\to B\right)\to B\right)}
#
wff
razão
1.
B
→
(
(
A
→
B
)
→
B
)
{\displaystyle B\to \left(\left(A\to B\right)\to B\right)}
THEN-1, com A := B, B :=
A
→
B
{\displaystyle A\to B}
Teorema TH10:
A
→
(
B
→
¬
(
A
→
¬
B
)
)
{\displaystyle A\to \left(B\to \neg \left(A\to \neg B\right)\right)}
#
wff
razão
1.
(
A
→
¬
B
)
→
(
A
→
¬
B
)
{\displaystyle \left(A\to \neg B\right)\to \left(A\to \neg B\right)}
TH7
2.
(
(
A
→
¬
B
)
→
(
A
→
¬
B
)
)
→
(
A
→
(
(
A
→
¬
B
)
→
¬
B
)
)
{\displaystyle \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
→
(
(
A
→
¬
B
)
→
¬
B
)
{\displaystyle A\to \left(\left(A\to \neg B\right)\to \neg B\right)}
MP 1,2
4.
(
(
A
→
¬
B
)
→
¬
B
)
→
(
B
→
¬
(
A
→
¬
B
)
)
{\displaystyle \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
→
(
B
→
¬
(
A
→
¬
B
)
)
{\displaystyle A\to \left(B\to \neg \left(A\to \neg B\right)\right)}
TH1* 3,4.
Teorema TH11:
(
A
→
B
)
→
(
(
A
→
¬
B
)
→
¬
A
)
{\displaystyle \left(A\to B\right)\to \left(\left(A\to \neg B\right)\to \neg A\right)}
#
wff
razão
1.
A
→
(
B
→
¬
(
A
→
¬
B
)
)
{\displaystyle A\to \left(B\to \neg \left(A\to \neg B\right)\right)}
TH10
2.
(
A
→
(
B
→
¬
(
A
→
¬
B
)
)
)
→
(
(
A
→
B
)
→
(
A
→
¬
(
A
→
¬
B
)
)
)
{\displaystyle \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.
(
A
→
B
)
→
(
A
→
¬
(
A
→
¬
B
)
)
{\displaystyle \left(A\to B\right)\to \left(A\to \neg \left(A\to \neg B\right)\right)}
MP 1,2
4.
(
A
→
¬
(
A
→
¬
B
)
)
→
(
(
A
→
¬
B
)
→
¬
A
)
{\displaystyle \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.
(
A
→
B
)
→
(
(
A
→
¬
B
)
→
¬
A
)
{\displaystyle \left(A\to B\right)\to \left(\left(A\to \neg B\right)\to \neg A\right)}
TH1* 3,4.
Teorema TH12:
(
(
A
→
B
)
→
C
)
→
(
A
→
(
B
→
C
)
)
{\displaystyle \left(\left(A\to B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)}
#
wff
razão
1.
B
→
(
A
→
B
)
{\displaystyle B\to \left(A\to B\right)}
THEN-1
2.
(
B
→
(
A
→
B
)
)
→
(
(
(
A
→
B
)
→
C
)
→
(
B
→
C
)
)
{\displaystyle \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.
(
(
A
→
B
)
→
C
)
→
(
B
→
C
)
{\displaystyle \left(\left(A\to B\right)\to C\right)\to \left(B\to C\right)}
MP 1,2
4.
(
B
→
C
)
→
(
A
→
(
B
→
C
)
)
{\displaystyle \left(B\to C\right)\to \left(A\to \left(B\to C\right)\right)}
THEN-1
5.
(
(
A
→
B
)
→
C
)
→
(
A
→
(
B
→
C
)
)
{\displaystyle \left(\left(A\to B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)}
TH1* 3,4.
Teorema TH13:
(
B
→
(
B
→
C
)
)
→
(
B
→
C
)
{\displaystyle \left(B\to \left(B\to C\right)\right)\to \left(B\to C\right)}
#
wff
razão
1.
(
B
→
(
B
→
C
)
)
→
(
(
B
→
B
)
→
(
B
→
C
)
)
{\displaystyle \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.
(
B
→
B
)
→
(
(
B
→
(
B
→
C
)
)
→
(
B
→
C
)
)
{\displaystyle \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
→
B
{\displaystyle B\to B}
TH7
4.
(
B
→
(
B
→
C
)
)
→
(
B
→
C
)
{\displaystyle \left(B\to \left(B\to C\right)\right)\to \left(B\to C\right)}
MP 3,2.
Regra TH14*:
{
A
→
(
B
→
P
)
,
P
→
Q
}
⊢
A
→
(
B
→
Q
)
{\displaystyle \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
→
Q
{\displaystyle P\to Q\,\!}
premissa
2.
(
P
→
Q
)
→
(
B
→
(
P
→
Q
)
)
{\displaystyle \left(P\to Q\right)\to \left(B\to \left(P\to Q\right)\right)}
THEN-1
3.
B
→
(
P
→
Q
)
{\displaystyle B\to \left(P\to Q\right)}
MP 1,2
4.
(
B
→
(
P
→
Q
)
)
→
(
(
B
→
P
)
→
(
B
→
Q
)
)
{\displaystyle \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.
(
B
→
P
)
→
(
B
→
Q
)
{\displaystyle \left(B\to P\right)\to \left(B\to Q\right)}
MP 3,4
6.
(
(
B
→
P
)
→
(
B
→
Q
)
)
→
(
A
→
(
(
B
→
P
)
→
(
B
→
Q
)
)
)
{\displaystyle \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
→
(
(
B
→
P
)
→
(
B
→
Q
)
)
{\displaystyle A\to \left(\left(B\to P\right)\to \left(B\to Q\right)\right)}
MP 5,6
8.
(
A
→
(
B
→
P
)
)
→
(
A
→
(
B
→
Q
)
)
{\displaystyle \left(A\to \left(B\to P\right)\right)\to \left(A\to \left(B\to Q\right)\right)}
THEN-2* 7
9.
A
→
(
B
→
P
)
{\displaystyle A\to \left(B\to P\right)}
premissa
10.
A
→
(
B
→
Q
)
{\displaystyle A\to \left(B\to Q\right)}
MP 9,8.
Teorema TH15:
(
(
A
→
B
)
→
(
A
→
C
)
)
→
(
A
→
(
B
→
C
)
)
{\displaystyle \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.
(
(
A
→
B
)
→
(
A
→
C
)
)
→
(
(
(
A
→
B
)
→
A
)
→
(
(
A
→
B
)
→
C
)
)
{\displaystyle \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.
(
(
A
→
B
)
→
C
)
→
(
A
→
(
B
→
C
)
)
{\displaystyle \left(\left(A\to B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)}
TH12
3.
(
(
A
→
B
)
→
(
A
→
C
)
)
→
(
(
(
A
→
B
)
→
A
)
→
(
A
→
(
B
→
C
)
)
)
{\displaystyle \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.
(
(
A
→
B
)
→
A
)
→
(
(
(
A
→
B
)
→
(
A
→
C
)
)
→
(
A
→
(
B
→
C
)
)
)
{\displaystyle \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
→
(
(
A
→
B
)
→
A
)
{\displaystyle A\to \left(\left(A\to B\right)\to A\right)}
THEN-1
6.
A
→
(
(
(
A
→
B
)
→
(
A
→
C
)
)
→
(
A
→
(
B
→
C
)
)
)
{\displaystyle 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.
(
(
A
→
B
)
→
(
A
→
C
)
)
→
(
A
→
(
A
→
(
B
→
C
)
)
)
{\displaystyle \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.
(
A
→
(
A
→
(
B
→
C
)
)
)
→
(
A
→
(
B
→
C
)
)
{\displaystyle \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.
(
(
A
→
B
)
→
(
A
→
C
)
)
→
(
A
→
(
B
→
C
)
)
{\displaystyle \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:
(
¬
A
→
¬
B
)
→
(
B
→
A
)
{\displaystyle \left(\neg A\to \neg B\right)\to \left(B\to A\right)}
#
wff
razão
1.
(
¬
A
→
¬
B
)
→
(
¬
¬
B
→
¬
¬
A
)
{\displaystyle \left(\neg A\to \neg B\right)\to \left(\neg \neg B\to \neg \neg A\right)}
FRG-1
2.
¬
¬
B
→
(
(
¬
A
→
¬
B
)
→
¬
¬
A
)
{\displaystyle \neg \neg B\to \left(\left(\neg A\to \neg B\right)\to \neg \neg A\right)}
THEN-3* 1
3.
B
→
¬
¬
B
{\displaystyle B\to \neg \neg B}
FRG-3
4.
B
→
(
(
¬
A
→
¬
B
)
→
¬
¬
A
)
{\displaystyle B\to \left(\left(\neg A\to \neg B\right)\to \neg \neg A\right)}
TH1* 3,2
5.
(
¬
A
→
¬
B
)
→
(
B
→
¬
¬
A
)
{\displaystyle \left(\neg A\to \neg B\right)\to \left(B\to \neg \neg A\right)}
THEN-3* 4
6.
¬
¬
A
→
A
{\displaystyle \neg \neg A\to A}
FRG-2
7.
(
¬
¬
A
→
A
)
→
(
B
→
(
¬
¬
A
→
A
)
)
{\displaystyle \left(\neg \neg A\to A\right)\to \left(B\to \left(\neg \neg A\to A\right)\right)}
THEN-1
8.
B
→
(
¬
¬
A
→
A
)
{\displaystyle B\to \left(\neg \neg A\to A\right)}
MP 6,7
9.
(
B
→
(
¬
¬
A
→
A
)
)
→
(
(
B
→
¬
¬
A
)
→
(
B
→
A
)
)
{\displaystyle \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.
(
B
→
¬
¬
A
)
→
(
B
→
A
)
{\displaystyle \left(B\to \neg \neg A\right)\to \left(B\to A\right)}
MP 8,9
11.
(
¬
A
→
¬
B
)
→
(
B
→
A
)
{\displaystyle \left(\neg A\to \neg B\right)\to \left(B\to A\right)}
TH1* 5,10.
Teorema TH17:
(
¬
A
→
B
)
→
(
¬
B
→
A
)
{\displaystyle \left(\neg A\to B\right)\to \left(\neg B\to A\right)}
#
wff
razão
1.
(
¬
A
→
¬
¬
B
)
→
(
¬
B
→
A
)
{\displaystyle \left(\neg A\to \neg \neg B\right)\to \left(\neg B\to A\right)}
TH16, com B := \neg B
2.
B
→
¬
¬
B
{\displaystyle B\to \neg \neg B}
FRG-3
3.
(
B
→
¬
¬
B
)
→
(
¬
A
→
(
B
→
¬
¬
B
)
)
{\displaystyle \left(B\to \neg \neg B\right)\to \left(\neg A\to \left(B\to \neg \neg B\right)\right)}
THEN-1
4.
¬
A
→
(
B
→
¬
¬
B
)
{\displaystyle \neg A\to \left(B\to \neg \neg B\right)}
MP 2,3
5.
(
¬
A
→
(
B
→
¬
¬
B
)
)
→
(
(
¬
A
→
B
)
→
(
¬
A
→
¬
¬
B
)
)
{\displaystyle \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.
(
¬
A
→
B
)
→
(
¬
A
→
¬
¬
B
)
{\displaystyle \left(\neg A\to B\right)\to \left(\neg A\to \neg \neg B\right)}
MP 4,5
7.
(
¬
A
→
B
)
→
(
¬
B
→
A
)
{\displaystyle \left(\neg A\to B\right)\to \left(\neg B\to A\right)}
TH1* 6,1.
Teorema TH18:
(
(
A
→
B
)
→
B
)
→
(
¬
A
→
B
)
{\displaystyle \left(\left(A\to B\right)\to B\right)\to \left(\neg A\to B\right)}
#
wff
razão
1.
(
A
→
B
)
→
(
¬
B
→
(
A
→
B
)
)
{\displaystyle \left(A\to B\right)\to \left(\neg B\to \left(A\to B\right)\right)}
THEN-1
2.
(
¬
B
→
¬
A
)
→
(
A
→
B
)
{\displaystyle \left(\neg B\to \neg A\right)\to \left(A\to B\right)}
TH16
3.
(
¬
B
→
¬
A
)
→
(
¬
B
→
(
A
→
B
)
)
{\displaystyle \left(\neg B\to \neg A\right)\to \left(\neg B\to \left(A\to B\right)\right)}
TH1* 2,1
4.
(
(
¬
B
→
¬
A
)
→
(
¬
B
→
(
A
→
B
)
)
)
→
(
¬
B
→
(
¬
A
→
(
A
→
B
)
)
)
{\displaystyle \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.
¬
B
→
(
¬
A
→
(
A
→
B
)
)
{\displaystyle \neg B\to \left(\neg A\to \left(A\to B\right)\right)}
MP 3,4
6.
(
¬
A
→
(
A
→
B
)
)
→
(
¬
(
A
→
B
)
→
A
)
{\displaystyle \left(\neg A\to \left(A\to B\right)\right)\to \left(\neg \left(A\to B\right)\to A\right)}
TH17
7.
¬
B
→
(
¬
(
A
→
B
)
→
A
)
{\displaystyle \neg B\to \left(\neg \left(A\to B\right)\to A\right)}
TH1* 5,6
8.
(
¬
B
→
(
¬
(
A
→
B
)
→
A
)
)
→
(
(
¬
B
→
¬
(
A
→
B
)
)
→
(
¬
B
→
A
)
)
{\displaystyle \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.
(
¬
B
→
¬
(
A
→
B
)
)
→
(
¬
B
→
A
)
{\displaystyle \left(\neg B\to \neg \left(A\to B\right)\right)\to \left(\neg B\to A\right)}
MP 7,8
10.
(
(
A
→
B
)
→
B
)
→
(
¬
B
→
¬
(
A
→
B
)
)
{\displaystyle \left(\left(A\to B\right)\to B\right)\to \left(\neg B\to \neg \left(A\to B\right)\right)}
FRG-1
11.
(
(
A
→
B
)
→
B
)
→
(
¬
B
→
A
)
{\displaystyle \left(\left(A\to B\right)\to B\right)\to \left(\neg B\to A\right)}
TH1* 10,9
12.
(
¬
B
→
A
)
→
(
¬
A
→
B
)
{\displaystyle \left(\neg B\to A\right)\to \left(\neg A\to B\right)}
TH17
13.
(
(
A
→
B
)
→
B
)
→
(
¬
A
→
B
)
{\displaystyle \left(\left(A\to B\right)\to B\right)\to \left(\neg A\to B\right)}
TH1* 11,12.
Teorema TH19:
(
A
→
C
)
→
(
(
B
→
C
)
→
(
(
(
A
→
B
)
→
B
)
→
C
)
)
{\displaystyle \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.
¬
A
→
(
¬
B
→
¬
(
¬
A
→
¬
¬
B
)
)
{\displaystyle \neg A\to \left(\neg B\to \neg \left(\neg A\to \neg \neg B\right)\right)}
TH10
2.
B
→
¬
¬
B
{\displaystyle B\to \neg \neg B}
FRG-3
3.
(
B
→
¬
¬
B
)
→
(
¬
A
→
(
B
→
¬
¬
B
)
)
{\displaystyle \left(B\to \neg \neg B\right)\to \left(\neg A\to \left(B\to \neg \neg B\right)\right)}
THEN-1
4.
¬
A
→
(
B
→
¬
¬
B
)
{\displaystyle \neg A\to \left(B\to \neg \neg B\right)}
MP 2,3
5.
(
¬
A
→
(
B
→
¬
¬
B
)
)
→
(
(
¬
A
→
B
)
→
(
¬
A
→
¬
¬
B
)
)
{\displaystyle \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.
(
¬
A
→
B
)
→
(
¬
A
→
¬
¬
B
)
{\displaystyle \left(\neg A\to B\right)\to \left(\neg A\to \neg \neg B\right)}
MP 4,5
7.
¬
(
¬
A
→
¬
¬
B
)
→
¬
(
¬
A
→
B
)
{\displaystyle \neg \left(\neg A\to \neg \neg B\right)\to \neg \left(\neg A\to B\right)}
FRG-1* 6
8.
¬
A
→
(
¬
B
→
¬
(
¬
A
→
B
)
)
{\displaystyle \neg A\to \left(\neg B\to \neg \left(\neg A\to B\right)\right)}
TH14* 1,7
9.
(
(
A
→
B
)
→
B
)
→
(
¬
A
→
B
)
{\displaystyle \left(\left(A\to B\right)\to B\right)\to \left(\neg A\to B\right)}
TH18
10.
¬
(
¬
A
→
B
)
→
¬
(
(
A
→
B
)
→
B
)
{\displaystyle \neg \left(\neg A\to B\right)\to \neg \left(\left(A\to B\right)\to B\right)}
FRG-1* 9
11.
¬
A
→
(
¬
B
→
¬
(
(
A
→
B
)
→
B
)
)
{\displaystyle \neg A\to \left(\neg B\to \neg \left(\left(A\to B\right)\to B\right)\right)}
TH14* 8,10
12.
¬
C
→
(
¬
A
→
(
¬
B
→
¬
(
(
A
→
B
)
→
B
)
)
)
{\displaystyle \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.
(
¬
C
→
¬
A
)
→
(
¬
C
→
(
¬
B
→
¬
(
(
A
→
B
)
→
B
)
)
)
{\displaystyle \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.
(
¬
C
→
(
¬
B
→
¬
(
(
A
→
B
)
→
B
)
)
)
→
(
(
¬
C
→
¬
B
)
→
(
¬
C
→
¬
(
(
A
→
B
)
→
B
)
)
)
{\displaystyle \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.
(
¬
C
→
¬
A
)
→
(
(
¬
C
→
¬
B
)
→
(
¬
C
→
¬
(
(
A
→
B
)
→
B
)
)
)
{\displaystyle \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.
(
A
→
C
)
→
(
¬
C
→
¬
A
)
{\displaystyle \left(A\to C\right)\to \left(\neg C\to \neg A\right)}
FRG-1
17.
(
A
→
C
)
→
(
(
→
C
→
¬
B
)
→
(
¬
C
→
¬
(
(
A
→
B
)
→
B
)
)
)
{\displaystyle \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.
(
¬
C
→
¬
(
(
A
→
B
)
→
B
)
)
→
(
(
(
A
→
B
)
→
B
)
→
C
)
{\displaystyle \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.
(
A
→
C
)
→
(
(
¬
C
→
¬
B
)
→
(
(
(
A
→
B
)
→
B
)
→
C
)
)
{\displaystyle \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.
(
B
→
C
)
→
(
¬
C
→
¬
B
)
{\displaystyle \left(B\to C\right)\to \left(\neg C\to \neg B\right)}
FRG-1
21.
(
(
B
→
C
)
→
(
¬
C
→
¬
B
)
)
→
(
(
(
¬
C
→
¬
B
)
→
(
(
(
A
→
B
)
→
B
)
→
C
)
)
→
(
(
B
→
C
)
→
(
(
(
A
→
B
)
→
B
)
→
C
)
)
)
{\displaystyle \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.
(
(
¬
C
→
¬
B
)
→
(
(
(
A
→
B
)
→
B
)
→
C
)
)
→
(
(
B
→
C
)
→
(
(
(
A
→
B
)
→
B
)
→
C
)
)
{\displaystyle \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.
(
A
→
C
)
→
(
(
B
→
C
)
→
(
(
(
A
→
B
)
→
B
)
→
C
)
)
{\displaystyle \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:
(
A
→
¬
A
)
→
¬
A
{\displaystyle \left(A\to \neg A\right)\to \neg A}
#
wff
razão
1.
(
A
→
A
)
→
(
(
A
→
¬
A
)
→
¬
A
)
{\displaystyle \left(A\to A\right)\to \left(\left(A\to \neg A\right)\to \neg A\right)}
TH11
2.
A
→
A
{\displaystyle A\to A}
TH7
3.
(
A
→
¬
A
)
→
¬
A
{\displaystyle \left(A\to \neg A\right)\to \neg A}
MP 2,1.
Teorema TH21:
A
→
(
¬
A
→
B
)
{\displaystyle A\to \left(\neg A\to B\right)}
#
wff
razão
1.
A
→
(
¬
A
→
¬
¬
B
)
{\displaystyle A\to \left(\neg A\to \neg \neg B\right)}
TH2, com B := ~B
2.
¬
¬
B
→
B
{\displaystyle \neg \neg B\to B}
FRG-2
3.
A
→
(
¬
A
→
B
)
{\displaystyle A\to \left(\neg A\to B\right)}
TH14* 1,2.
Prova de que o terceiro axioma é dedutível dos dois primeiros
editar
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
→
(
Q
→
P
)
{\displaystyle P\to \left(Q\to P\right)}
THEN-2:
(
P
→
(
Q
→
R
)
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
{\displaystyle \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:
(
(
Q
→
R
)
→
(
P
→
(
Q
→
R
)
)
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
{\displaystyle \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.
(
(
(
P
→
(
Q
→
R
)
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
)
→
(
(
Q
→
R
)
→
(
(
P
→
(
Q
→
R
)
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
)
)
)
{\displaystyle \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.
(
P
→
(
Q
→
R
)
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
{\displaystyle \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.
(
(
Q
→
R
)
→
(
P
→
(
Q
→
R
)
)
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
{\displaystyle \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
/
(
P
→
(
Q
→
R
)
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
{\displaystyle 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
→
R
{\displaystyle Q/Q\to R}
Tese 2:
(
(
Q
→
R
)
→
(
P
→
(
Q
→
R
)
)
)
→
(
(
Q
→
R
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
)
{\displaystyle \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.
(
(
(
Q
→
R
)
→
(
(
P
→
(
Q
→
R
)
)
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
)
)
→
(
(
(
Q
→
R
)
→
(
P
→
(
Q
→
R
)
)
)
→
(
Q
→
R
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
)
{\displaystyle \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.
(
(
Q
→
R
)
→
(
P
→
(
Q
→
R
)
)
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
{\displaystyle \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.
(
(
Q
→
R
)
→
(
P
→
(
Q
→
R
)
)
)
→
(
(
Q
→
R
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
)
{\displaystyle \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
→
R
{\displaystyle P/Q\to R}
*
Q
/
P
→
(
Q
→
R
)
{\displaystyle Q/P\to \left(Q\to R\right)}
*
R
/
(
P
→
Q
)
→
(
P
→
R
)
{\displaystyle R/\left(P\to Q\right)\to \left(P\to R\right)}
Tese 3:
(
Q
→
R
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
{\displaystyle \left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)}
#
wff
razão
1.
(
(
Q
→
R
)
→
(
P
→
(
Q
→
R
)
)
)
→
(
(
Q
→
R
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
)
{\displaystyle \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.
(
Q
→
R
)
→
(
P
→
(
Q
→
R
)
)
{\displaystyle \left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)}
THEN-1*
3.
(
Q
→
R
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
{\displaystyle \left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)}
MP 1,2.
*
P
/
Q
→
R
{\displaystyle P/Q\to R}
*
Q
/
P
{\displaystyle Q/P\,\!}
Tese 4:
(
(
Q
→
R
)
→
(
P
→
Q
)
)
→
(
(
Q
→
R
)
→
(
P
→
R
)
)
{\displaystyle \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.
(
(
Q
→
R
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
)
→
(
(
(
Q
→
R
)
→
(
P
→
Q
)
)
→
(
(
Q
→
R
)
→
(
P
→
R
)
)
)
{\displaystyle \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.
(
Q
→
R
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
{\displaystyle \left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)}
Prop.3
3.
(
(
Q
→
R
)
→
(
P
→
Q
)
)
→
(
(
Q
→
R
)
→
(
P
→
R
)
)
{\displaystyle \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
→
R
{\displaystyle P/Q\to R}
*
Q
/
P
→
Q
{\displaystyle Q/P\to Q}
*
R
/
P
→
R
{\displaystyle R/P\to R}
Tese 5:
R
→
(
P
→
(
Q
→
P
)
)
{\displaystyle R\to \left(P\to \left(Q\to P\right)\right)}
#
wff
razão
1.
(
P
→
(
Q
→
P
)
)
→
(
R
→
(
P
→
(
Q
→
P
)
)
)
{\displaystyle \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
→
(
Q
→
P
)
{\displaystyle P\to \left(Q\to P\right)}
THEN-1
3.
R
→
(
P
→
(
Q
→
P
)
)
{\displaystyle R\to \left(P\to \left(Q\to P\right)\right)}
MP 1,2.
*
P
/
P
→
(
Q
→
P
)
{\displaystyle P/P\to \left(Q\to P\right)}
*
Q
/
R
{\displaystyle Q/R\,\!}
Tese 6:
(
(
P
→
Q
)
→
R
)
→
(
Q
→
R
)
{\displaystyle \left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)}
#
wff
razão
1.
(
(
(
P
→
Q
)
→
R
)
→
(
Q
→
(
P
→
Q
)
)
)
→
(
(
(
P
→
Q
)
→
R
)
→
(
Q
→
R
)
)
{\displaystyle \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.
(
(
P
→
Q
)
→
R
)
→
(
Q
→
(
P
→
Q
)
)
{\displaystyle \left(\left(P\to Q\right)\to R\right)\to \left(Q\to \left(P\to Q\right)\right)}
Prop.5**
3.
(
(
P
→
Q
)
→
R
)
→
(
Q
→
R
)
{\displaystyle \left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)}
MP 1,2.
*
Q
/
P
→
Q
{\displaystyle Q/P\to Q}
*
P
/
Q
{\displaystyle P/Q\,\!}
**
R
/
(
P
→
Q
)
→
R
{\displaystyle R/\left(P\to Q\right)\to R}
**
P
/
Q
{\displaystyle P/Q\,\!}
**
Q
/
P
{\displaystyle Q/P\,\!}
Tese 7:
(
S
→
(
(
P
→
Q
)
→
R
)
)
→
(
S
→
(
Q
→
R
)
)
{\displaystyle \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.
(
(
(
P
→
Q
)
→
R
)
→
(
Q
→
R
)
)
→
(
(
S
→
(
(
P
→
Q
)
→
R
)
)
→
(
S
→
(
Q
→
R
)
)
)
{\displaystyle \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.
(
(
P
→
Q
)
→
R
)
→
(
Q
→
R
)
{\displaystyle \left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)}
Prop.6
3.
(
S
→
(
(
P
→
Q
)
→
R
)
)
→
(
S
→
(
Q
→
R
)
)
{\displaystyle \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
/
(
P
→
Q
)
→
R
{\displaystyle Q/\left(P\to Q\right)\to R}
*
R
/
Q
→
R
{\displaystyle R/Q\to R}
*
P
/
S
{\displaystyle P/S\,\!}
THEN-3:
(
P
→
(
Q
→
R
)
)
→
(
Q
→
(
P
→
R
)
)
{\displaystyle \left(P\to \left(Q\to R\right)\right)\to \left(Q\to \left(P\to R\right)\right)}
#
wff
razão
1.
(
(
P
→
(
Q
→
R
)
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
)
→
(
(
P
→
(
Q
→
R
)
)
→
(
Q
→
(
P
→
R
)
)
)
{\displaystyle \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.
(
P
→
(
Q
→
R
)
)
→
(
(
P
→
Q
)
→
(
P
→
R
)
)
{\displaystyle \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.
(
P
→
(
Q
→
R
)
)
→
(
Q
→
(
P
→
R
)
)
{\displaystyle \left(P\to \left(Q\to R\right)\right)\to \left(Q\to \left(P\to R\right)\right)}
MP 1,2.
*
S
/
P
→
(
Q
→
R
)
{\displaystyle S/P\to \left(Q\to R\right)}
*
R
/
P
→
R
{\displaystyle R/P\to R}
Q
u
o
d
E
r
a
t
D
e
m
o
n
s
t
r
a
n
d
u
m
{\displaystyle {\mathfrak {Quod\ Erat\ Demonstrandum}}}
