editar
Por meio das regras de inferência diretas e hipotéticas podemos demonstrar vários raciocínios bastante recorrentes. Estes raciocíonios, uma vez demonstrados, podem ser usados como regras de inferência diretas. Elas não são necessárias, mas são bastante úteis, tornando nossas derivações muito mais sucintas. Anteriormente demonstramos dois raciocínios que nos serão úteis como regras de inferência derivadas:
Dupla Negação em ambas direções (DN)
¬
¬
φ
φ
¯
{\displaystyle {\frac {\neg \neg \varphi \,}{\overline {\varphi \quad \;\,}}}}
Silogismo Hipotético (SH)
α
→
β
{\displaystyle \alpha \to \beta }
β
→
γ
_
{\displaystyle {\underline {\beta \to \gamma }}}
α
→
γ
{\displaystyle \alpha \to \gamma }
Vamos ampliar nossa lista de regras de inferência derivadas, demonstrado uma por uma:
α
⊢
α
{\displaystyle \alpha \vdash \alpha }
1.
α
{\displaystyle \alpha }
Premissa
2.
¬
¬
α
{\displaystyle \neg \neg \alpha }
1 DN
3.
α
{\displaystyle \alpha }
2 DN
{
α
→
β
,
¬
β
}
⊢
¬
α
{\displaystyle \left\{\alpha \to \beta ,\neg \beta \right\}\vdash \neg \alpha }
1.
α
→
β
{\displaystyle \alpha \to \beta }
Premissa
2.
¬
β
{\displaystyle \neg \beta }
Premissa
3.
α
{\displaystyle \alpha }
Hipótese
4.
β
{\displaystyle \beta }
1,3 MP
5.
β
∧
¬
β
{\displaystyle \beta \land \neg \beta }
2,4 C
6.
¬
α
{\displaystyle \neg \alpha }
3,5 RAA
α
⊢
β
→
α
{\displaystyle \alpha \vdash \beta \to \alpha }
1.
α
{\displaystyle \alpha }
Premissa
2.
β
{\displaystyle \beta }
Hipótese
3.
α
{\displaystyle \alpha }
1 R
4.
β
→
α
{\displaystyle \beta \to \alpha }
2,3 RPC
Aproveitaremos o Modus Tollens como regra de inferência.
α
→
β
⊢
¬
β
→
¬
α
{\displaystyle \alpha \to \beta \vdash \neg \beta \to \neg \alpha }
1.
α
→
β
{\displaystyle \alpha \to \beta }
Premissa
2.
¬
β
{\displaystyle \neg \beta }
Hipótese
3.
¬
α
{\displaystyle \neg \alpha }
1,2 MT
4.
¬
β
→
¬
α
{\displaystyle \neg \beta \to \neg \alpha }
2,3 RPC
Agora tente você provar a recíproca, ou seja, que
¬
β
→
¬
α
⊢
α
→
β
{\displaystyle \neg \beta \to \neg \alpha \vdash \alpha \to \beta }
Confira aqui sua resposta .
{
α
,
¬
α
}
⊢
β
{\displaystyle \left\{\alpha ,\neg \alpha \right\}\vdash \beta }
1.
α
{\displaystyle \alpha }
Premissa
2.
¬
α
{\displaystyle \neg \alpha }
Premissa
3.
α
∨
β
{\displaystyle \alpha \lor \beta }
1 E
4.
β
{\displaystyle \beta }
2,3 SD
¬
α
⊢
α
→
β
{\displaystyle \neg \alpha \vdash \alpha \to \beta }
1.
¬
α
{\displaystyle \neg \alpha }
Premissa
2.
α
{\displaystyle \alpha }
Hipótese
3.
β
{\displaystyle \beta }
1,2 CTR
4.
α
→
β
{\displaystyle \alpha \to \beta }
2,3 RPC
Prove que também vale
α
⊢
¬
α
→
β
{\displaystyle \alpha \vdash \neg \alpha \to \beta }
Confira aqui sua resposta .
¬
(
α
∨
β
)
⊢
¬
α
∧
¬
β
{\displaystyle \neg \left(\alpha \lor \beta \right)\vdash \neg \alpha \land \neg \beta }
01.
¬
(
α
∨
β
)
{\displaystyle \neg \left(\alpha \lor \beta \right)}
Premissa
02.
α
{\displaystyle \alpha }
Hipótese
03.
α
∨
β
{\displaystyle \alpha \lor \beta }
2 E
04.
(
α
∨
β
)
∧
¬
(
α
∨
β
)
{\displaystyle \left(\alpha \lor \beta \right)\land \neg \left(\alpha \lor \beta \right)}
1,3 C
05.
¬
α
{\displaystyle \neg \alpha }
2,4 RAA
06.
β
{\displaystyle \beta }
Hipótese
07.
α
∨
β
{\displaystyle \alpha \lor \beta }
6 E
08.
(
α
∨
β
)
∧
¬
(
α
∨
β
)
{\displaystyle \left(\alpha \lor \beta \right)\land \neg \left(\alpha \lor \beta \right)}
1,7 C
09.
¬
β
{\displaystyle \neg \beta }
6,8 RAA
10.
¬
α
∧
¬
β
{\displaystyle \neg \alpha \land \neg \beta }
5,9 C
Agora tente você provar a recíproca, ou seja, que
¬
α
∧
¬
β
⊢
¬
(
α
∨
β
)
{\displaystyle \neg \alpha \land \neg \beta \vdash \neg \left(\alpha \lor \beta \right)}
Confira aqui sua resposta
¬
(
α
∧
β
)
⊢
¬
α
∨
¬
β
{\displaystyle \neg \left(\alpha \land \beta \right)\vdash \neg \alpha \lor \neg \beta }
01.
¬
(
α
∧
β
)
{\displaystyle \neg \left(\alpha \land \beta \right)}
Premissa
02.
¬
(
¬
α
∨
¬
β
)
{\displaystyle \neg \left(\neg \alpha \lor \neg \beta \right)}
Hipótese
03.
¬
α
{\displaystyle \neg \alpha }
Hipótese
04.
¬
α
∨
¬
β
{\displaystyle \neg \alpha \lor \neg \beta }
3 E
05.
(
¬
α
∨
¬
β
)
∧
¬
(
¬
α
∨
¬
β
)
{\displaystyle \left(\neg \alpha \lor \neg \beta \right)\land \neg \left(\neg \alpha \lor \neg \beta \right)}
5,2 C
06.
¬
¬
α
{\displaystyle \neg \neg \alpha }
3,5 RAA
07.
α
{\displaystyle \alpha }
6 DN
08.
¬
β
{\displaystyle \neg \beta }
Hipótese
09.
¬
α
∨
¬
β
{\displaystyle \neg \alpha \lor \neg \beta }
8 E
10.
(
¬
α
∨
¬
β
)
∧
¬
(
¬
α
∨
¬
β
)
{\displaystyle \left(\neg \alpha \lor \neg \beta \right)\land \neg \left(\neg \alpha \lor \neg \beta \right)}
9,2 C
11.
¬
¬
β
{\displaystyle \neg \neg \beta }
8,10 RAA
12.
β
{\displaystyle \beta }
11 DN
13.
α
∧
β
{\displaystyle \alpha \land \beta }
7,12 C
14.
(
α
∧
β
)
∧
¬
(
α
∧
β
)
{\displaystyle \left(\alpha \land \beta \right)\land \neg \left(\alpha \land \beta \right)}
13,1 C
15.
¬
¬
(
¬
α
∨
¬
β
)
{\displaystyle \neg \neg \left(\neg \alpha \lor \neg \beta \right)}
2,14 RAA
16.
¬
α
∨
¬
β
{\displaystyle \neg \alpha \lor \neg \beta }
15 DN
Tente você agora provar a recíprova, ou seja, que
¬
α
∨
¬
β
⊢
¬
(
α
∧
β
)
{\displaystyle \neg \alpha \lor \neg \beta \vdash \neg \left(\alpha \land \beta \right)}
Confira aqui sua resposta
Lista das Regras Derivadas
editar
Valendo-se das regras derivadas, prove que:
{
(
A
∧
B
)
→
C
,
¬
C
}
⊢
¬
A
∨
¬
B
{\displaystyle \left\{\left(A\land B\right)\to C,\neg C\right\}\vdash \neg A\lor \neg B}
¬
(
A
∧
¬
B
)
⊢
A
→
B
{\displaystyle \neg \left(A\land \neg B\right)\vdash A\to B}
¬
A
→
B
⊢
A
∨
B
{\displaystyle \neg A\to B\vdash A\lor B}
{
A
→
C
,
B
→
C
}
⊢
(
A
∨
B
)
→
C
{\displaystyle \left\{A\to C,B\to C\right\}\vdash \left(A\lor B\right)\to C}
¬
(
A
→
B
)
⊢
A
∧
¬
B
{\displaystyle \neg \left(A\to B\right)\vdash A\land \neg B}
A
→
B
⊢
(
A
∨
C
)
→
(
B
∨
C
)
{\displaystyle A\to B\vdash \left(A\lor C\right)\to \left(B\lor C\right)}
Resolução dos Exercícios
Agora não temos mais premissas para trabalhar, devemos nos limitar às hipóteses. Algumas estratégias para provar teoremas podem ser traçadas:
Para provar
¬
φ
{\displaystyle \neg \varphi }
φ
{\displaystyle \varphi }
Para provar
φ
{\displaystyle \varphi }
¬
φ
{\displaystyle \neg \varphi }
Por regra para condicionais Para provar
φ
→
ψ
{\displaystyle \varphi \to \psi }
φ
{\displaystyle \varphi }
ψ
{\displaystyle \psi }
Para provar
φ
↔
ψ
{\displaystyle \varphi \leftrightarrow \psi }
φ
→
ψ
{\displaystyle \varphi \to \psi }
ψ
→
φ
{\displaystyle \psi \to \varphi }
⊢
¬
(
A
∧
¬
A
)
{\displaystyle \vdash \neg \left(A\land \neg A\right)}
1.
A
∧
¬
A
{\displaystyle A\land \neg A}
Hipótese
2.
¬
(
A
∧
¬
A
)
{\displaystyle \neg \left(A\land \neg A\right)}
1 RAA
⊢
A
∨
¬
A
{\displaystyle \vdash A\lor \neg A}
1.
¬
(
A
∨
¬
A
)
{\displaystyle \neg \left(A\lor \neg A\right)}
Hipótese
2.
¬
A
∧
¬
¬
A
{\displaystyle \neg A\land \neg \neg A}
1 DM
3.
¬
¬
(
A
∨
¬
A
)
{\displaystyle \neg \neg \left(A\lor \neg A\right)}
1,2 RAA
4.
A
∨
¬
A
{\displaystyle A\lor \neg A}
3 DN
⊢
(
A
→
(
A
→
B
)
)
→
(
A
→
B
)
{\displaystyle \vdash \left(A\to \left(A\to B\right)\right)\to \left(A\to B\right)}
1.
A
→
(
A
→
B
)
{\displaystyle A\to \left(A\to B\right)}
Hipótese
2.
A
{\displaystyle A}
Hipótese
3.
A
→
B
{\displaystyle A\to B}
1,2 MP
4.
B
{\displaystyle B}
3,2 MP
5.
A
→
B
{\displaystyle A\to B}
2,6 RPC
6.
(
A
→
(
A
→
B
)
)
→
(
A
→
B
)
{\displaystyle \left(A\to \left(A\to B\right)\right)\to \left(A\to B\right)}
1,7 RPC
⊢
(
A
→
B
)
∨
(
B
→
A
)
{\displaystyle \vdash \left(A\to B\right)\lor \left(B\to A\right)}
01.
¬
(
(
A
→
B
)
∨
(
B
→
A
)
)
{\displaystyle \neg \left(\left(A\to B\right)\lor \left(B\to A\right)\right)}
Hipótese
02.
¬
(
A
→
B
)
∧
¬
(
B
→
A
)
{\displaystyle \neg \left(A\to B\right)\land \neg \left(B\to A\right)}
1 DM
03.
¬
(
A
→
B
)
{\displaystyle \neg \left(A\to B\right)}
2 S
04.
¬
(
B
→
A
)
{\displaystyle \neg \left(B\to A\right)}
2 S
05.
A
{\displaystyle A}
Hipótese
06.
B
→
A
{\displaystyle B\to A}
5 PRF
07.
¬
(
B
→
A
)
∧
(
B
→
A
)
{\displaystyle \neg \left(B\to A\right)\land \left(B\to A\right)}
4,5 C
08.
¬
A
{\displaystyle \neg A}
5,7 RAA
09.
A
→
B
{\displaystyle A\to B}
8 DS
10.
(
A
→
B
)
∧
¬
(
A
→
B
)
{\displaystyle \left(A\to B\right)\land \neg \left(A\to B\right)}
9,3 C
11.
¬
¬
(
(
A
→
B
)
∨
(
B
→
A
)
)
{\displaystyle \neg \neg \left(\left(A\to B\right)\lor \left(B\to A\right)\right)}
1,10 RAA
12.
(
A
→
B
)
∨
(
B
→
A
)
{\displaystyle \left(A\to B\right)\lor \left(B\to A\right)}
11 DN
⊢
(
(
P
→
Q
)
→
P
)
→
P
{\displaystyle \vdash \left(\left(P\to Q\right)\to P\right)\to P}
01.
(
P
→
Q
)
→
P
{\displaystyle \left(P\to Q\right)\to P}
Hipótese
02.
¬
P
{\displaystyle \neg P}
Hipótese
03.
P
{\displaystyle P}
Hipótese
04.
¬
Q
{\displaystyle \neg Q}
Hipótese
05.
P
∧
¬
P
{\displaystyle P\land \neg P}
3,2 C
06.
¬
¬
Q
{\displaystyle \neg \neg Q}
4,5 RAA
07.
Q
{\displaystyle Q}
6 DN
08.
P
→
Q
{\displaystyle P\to Q}
3,7 RPC
09.
P
{\displaystyle P}
1,8 MP
10.
¬
P
∧
P
{\displaystyle \neg P\land P}
2,9 C
11.
¬
¬
P
{\displaystyle \neg \neg P}
2, 10 RAA
12.
P
{\displaystyle P}
11 DN
13.
(
(
P
→
Q
)
→
P
)
→
P
{\displaystyle \left(\left(P\to Q\right)\to P\right)\to P\,\!}
1, 12 RPC
⊢
(
(
A
∧
B
)
→
C
)
↔
(
A
→
(
B
→
C
)
)
{\displaystyle \vdash \left(\left(A\land B\right)\to C\right)\leftrightarrow \left(A\to \left(B\to C\right)\right)}
01.
(
A
∧
B
)
→
C
{\displaystyle \left(A\land B\right)\to C}
Hipótese
02.
A
{\displaystyle A}
Hipótese
03.
B
{\displaystyle B}
Hipótese
04.
A
∧
B
{\displaystyle A\land B}
2,3 C
05.
C
{\displaystyle C}
1,4 MP
06.
B
→
C
{\displaystyle B\to C}
3,5 RPC
07.
A
→
(
B
→
C
)
{\displaystyle A\to \left(B\to C\right)}
2,6 RPC
08.
(
(
A
∧
B
)
→
C
)
→
(
A
→
(
B
→
C
)
)
{\displaystyle \left(\left(A\land B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)}
1,7 RPC
09.
A
→
(
B
→
C
)
{\displaystyle A\to \left(B\to C\right)}
Hipótese
10.
A
∧
B
{\displaystyle A\land B}
Hipótese
11.
A
{\displaystyle A}
10 S
12.
B
→
C
{\displaystyle B\to C}
9,11 MP
13.
B
{\displaystyle B}
10 S
14.
C
{\displaystyle C}
12,13 MP
15.
(
A
∧
B
)
→
C
{\displaystyle \left(A\land B\right)\to C}
10,14 RPC
16.
(
A
→
(
B
→
C
)
)
→
(
(
A
∧
B
)
→
C
)
{\displaystyle \left(A\to \left(B\to C\right)\right)\to \left(\left(A\land B\right)\to C\right)}
9,15 RPC
17.
(
(
A
∧
B
)
→
C
)
↔
(
A
→
(
B
→
C
)
)
{\displaystyle \left(\left(A\land B\right)\to C\right)\leftrightarrow \left(A\to \left(B\to C\right)\right)}
8,16 CB
Prove os seguintes teoremas por dedução natural:
⊢
A
↔
A
{\displaystyle \vdash A\leftrightarrow A}
⊢
A
↔
¬
¬
A
{\displaystyle \vdash A\leftrightarrow \neg \neg A}
⊢
¬
(
A
↔
¬
A
)
{\displaystyle \vdash \neg \left(A\leftrightarrow \neg A\right)}
⊢
A
→
(
B
→
A
)
{\displaystyle \vdash A\to \left(B\to A\right)}
⊢
(
¬
A
→
A
)
→
A
{\displaystyle \vdash \left(\neg A\to A\right)\to A}
⊢
P
→
(
Q
→
(
P
∧
Q
)
)
{\displaystyle \vdash P\to \left(Q\to \left(P\land Q\right)\right)}
⊢
(
(
A
∧
B
)
→
C
)
↔
(
(
A
∧
¬
C
)
→
¬
B
)
{\displaystyle \vdash \left(\left(A\land B\right)\to C\right)\leftrightarrow \left(\left(A\land \neg C\right)\to \neg B\right)}
⊢
(
A
→
(
B
→
C
)
)
→
(
(
A
→
B
)
→
(
A
→
C
)
)
{\displaystyle \vdash \left(A\to \left(B\to C\right)\ \right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)}
⊢
(
D
→
(
B
→
A
)
)
→
(
B
→
(
D
→
A
)
)
{\displaystyle \vdash \left(D\to \left(B\to A\right)\right)\to \left(B\to \left(D\to A\right)\right)}
⊢
(
P
→
Q
)
→
(
(
P
→
¬
Q
)
→
¬
P
)
{\displaystyle \vdash \left(P\to Q\right)\to \left(\left(P\to \neg Q\right)\to \neg P\right)}
⊢
(
A
→
B
)
→
(
(
C
→
B
)
→
(
(
A
∨
C
)
→
B
)
)
{\displaystyle \vdash \left(A\to B\right)\to \left(\left(C\to B\right)\to \left(\left(A\lor C\right)\to B\right)\right)}
Resolução dos Exercícios
