Contents
1 Dedução Natural para a Lógica Proposicional Intuicionista
1.1 Derivabilidade de sequentes
1.1.1
φ
∧
ψ
⊢
ψ
∧
φ
{\displaystyle \varphi \land \psi \vdash \psi \land \varphi }
1.1.2
(
φ
∧
ψ
)
∧
δ
⊢
φ
∧
(
ψ
∧
δ
)
{\displaystyle (\varphi \land \psi )\land \delta \vdash \varphi \land (\psi \land \delta )}
1.1.3
φ
⊢
φ
∧
φ
{\displaystyle \varphi \vdash \varphi \land \varphi }
1.1.4
α
∧
β
,
γ
∧
δ
⊢
γ
∧
β
{\displaystyle \alpha \land \beta ,\gamma \land \delta \vdash \gamma \land \beta }
1.1.5
α
→
(
β
→
γ
)
⊢
β
→
(
α
→
γ
)
{\displaystyle \alpha \to (\beta \to \gamma )\vdash \beta \to (\alpha \to \gamma )}
1.1.6
⊢
α
→
(
β
→
α
)
{\displaystyle \vdash \alpha \to (\beta \to \alpha )}
1.1.7
⊢
α
→
α
{\displaystyle \vdash \alpha \to \alpha }
1.1.8
α
→
β
⊢
α
→
(
α
→
β
)
{\displaystyle \alpha \to \beta \vdash \alpha \to (\alpha \to \beta )}
1.1.9
α
→
(
α
→
β
)
⊢
α
→
β
{\displaystyle \alpha \to (\alpha \to \beta )\vdash \alpha \to \beta }
1.1.10
γ
→
α
,
γ
→
β
⊢
γ
→
(
α
∧
β
)
{\displaystyle \gamma \to \alpha ,\gamma \to \beta \vdash \gamma \to (\alpha \land \beta )}
1.1.11
β
∨
(
α
∧
β
)
⊢
β
{\displaystyle \beta \lor (\alpha \land \beta )\vdash \beta }
1.1.12
(
α
∨
β
)
→
γ
⊢
(
α
→
γ
)
∧
(
β
→
γ
)
{\displaystyle (\alpha \lor \beta )\to \gamma \vdash (\alpha \to \gamma )\land (\beta \to \gamma )}
1.1.13
α
∨
β
⊬
α
∧
β
{\displaystyle \alpha \lor \beta \not \vdash \alpha \land \beta }
1.1.14
α
⊢
¬
¬
α
{\displaystyle \alpha \vdash \neg \neg \alpha }
1.1.15
β
→
α
,
β
→
¬
α
⊢
¬
β
{\displaystyle \beta \to \alpha ,\beta \to \neg \alpha \vdash \neg \beta }
1.1.16
α
,
¬
α
⊢
¬
β
{\displaystyle \alpha ,\neg \alpha \vdash \neg \beta }
1.1.17
α
∨
β
,
¬
α
∨
γ
⊢
β
∨
γ
{\displaystyle \alpha \lor \beta ,\neg \alpha \lor \gamma \vdash \beta \lor \gamma }
1.1.18
α
→
β
⊢
¬
β
→
¬
α
{\displaystyle \alpha \to \beta \vdash \neg \beta \to \neg \alpha }
1.1.19
¬
(
α
∨
β
)
⊣⊢
¬
α
∧
¬
β
{\displaystyle \neg (\alpha \lor \beta )\dashv \vdash \neg \alpha \land \neg \beta }
1.2 Derivabilidade de regras
2 Dedução Natural para a Lógica Proposicional Clássica
2.1 Derivabilidade de sequentes 2.2 Derivabilidade de regras
2.2.1 Raciocínio por casos:
Γ
1
,
¬
φ
⊢
ψ
;
Γ
2
,
φ
⊢
ψ
/
Γ
1
,
Γ
2
⊢
ψ
{\displaystyle \Gamma _{1},\neg \varphi \vdash \psi ;\Gamma _{2},\varphi \vdash \psi \,/\,\Gamma _{1},\Gamma _{2}\vdash \psi }
2.2.2 Raciocínio por redução ao absurdo:
Γ
1
,
¬
φ
⊢
¬
ψ
;
Γ
2
,
¬
φ
⊢
ψ
/
Γ
1
,
Γ
2
⊢
φ
{\displaystyle \Gamma _{1},\neg \varphi \vdash \neg \psi ;\Gamma _{2},\neg \varphi \vdash \psi \,/\,\Gamma _{1},\Gamma _{2}\vdash \varphi }
3 Para reflexão 4 Veja também 5 Links externos
Dedução Natural para a Lógica Proposicional Intuicionista Derivabilidade de sequentes
φ
∧
ψ
⊢
ψ
∧
φ
{\displaystyle \varphi \land \psi \vdash \psi \land \varphi }
(
φ
∧
ψ
)
∧
δ
⊢
φ
∧
(
ψ
∧
δ
)
{\displaystyle (\varphi \land \psi )\land \delta \vdash \varphi \land (\psi \land \delta )}
φ
⊢
φ
∧
φ
{\displaystyle \varphi \vdash \varphi \land \varphi }
α
∧
β
,
γ
∧
δ
⊢
γ
∧
β
{\displaystyle \alpha \land \beta ,\gamma \land \delta \vdash \gamma \land \beta }
α
→
(
β
→
γ
)
⊢
β
→
(
α
→
γ
)
{\displaystyle \alpha \to (\beta \to \gamma )\vdash \beta \to (\alpha \to \gamma )}
⊢
α
→
(
β
→
α
)
{\displaystyle \vdash \alpha \to (\beta \to \alpha )}
⊢
α
→
α
{\displaystyle \vdash \alpha \to \alpha }
α
→
β
⊢
α
→
(
α
→
β
)
{\displaystyle \alpha \to \beta \vdash \alpha \to (\alpha \to \beta )}
α
→
(
α
→
β
)
⊢
α
→
β
{\displaystyle \alpha \to (\alpha \to \beta )\vdash \alpha \to \beta }
γ
→
α
,
γ
→
β
⊢
γ
→
(
α
∧
β
)
{\displaystyle \gamma \to \alpha ,\gamma \to \beta \vdash \gamma \to (\alpha \land \beta )}
β
∨
(
α
∧
β
)
⊢
β
{\displaystyle \beta \lor (\alpha \land \beta )\vdash \beta }
(
α
∨
β
)
→
γ
⊢
(
α
→
γ
)
∧
(
β
→
γ
)
{\displaystyle (\alpha \lor \beta )\to \gamma \vdash (\alpha \to \gamma )\land (\beta \to \gamma )}
α
∨
β
⊬
α
∧
β
{\displaystyle \alpha \lor \beta \not \vdash \alpha \land \beta }
α
⊢
¬
¬
α
{\displaystyle \alpha \vdash \neg \neg \alpha }
β
→
α
,
β
→
¬
α
⊢
¬
β
{\displaystyle \beta \to \alpha ,\beta \to \neg \alpha \vdash \neg \beta }
α
,
¬
α
⊢
¬
β
{\displaystyle \alpha ,\neg \alpha \vdash \neg \beta }
α
∨
β
,
¬
α
∨
γ
⊢
β
∨
γ
{\displaystyle \alpha \lor \beta ,\neg \alpha \lor \gamma \vdash \beta \lor \gamma }
α
→
β
⊢
¬
β
→
¬
α
{\displaystyle \alpha \to \beta \vdash \neg \beta \to \neg \alpha }
¬
(
α
∨
β
)
⊣⊢
¬
α
∧
¬
β
{\displaystyle \neg (\alpha \lor \beta )\dashv \vdash \neg \alpha \land \neg \beta }
Derivabilidade de regras
(
D
N
E
)
{\displaystyle \mathrm {(DNE)} }
D
N
i
n
t
{\displaystyle \mathrm {DN_{int}} }
⊥
E
c
l
s
{\displaystyle \mathrm {\bot E_{cls}} }
(
⊥
E
c
l
s
)
{\displaystyle (\mathrm {\bot E_{cls}} )}
D
N
i
n
t
{\displaystyle \mathrm {DN_{int}} }
(
D
N
E
)
{\displaystyle \mathrm {(DNE)} }
(
M
)
{\displaystyle (\mathbb {M} )}
(
R
)
{\displaystyle (\mathbb {R} )}
(
T
)
{\displaystyle (\mathbb {T} )}
Dedução Natural para a Lógica Proposicional Clássica Derivabilidade de sequentes Terceiro Excluído / Tertium Non Datur :
⊢
φ
∨
¬
φ
{\displaystyle \vdash \varphi \lor \neg \varphi }
Tarefa: Demonstrar a mesma fórmula, invertendo a ordem de aplicação das regras de introdução da disjunção.
¬
¬
α
⊢
α
{\displaystyle \neg \neg \alpha \vdash \alpha }
¬
β
→
α
,
¬
β
→
¬
α
⊢
β
{\displaystyle \neg \beta \to \alpha ,\neg \beta \to \neg \alpha \vdash \beta }
¬
α
→
¬
β
⊢
β
→
α
{\displaystyle \neg \alpha \to \neg \beta \vdash \beta \to \alpha }
⊢
(
α
→
β
)
∨
(
β
→
α
)
{\displaystyle \vdash (\alpha \to \beta )\lor (\beta \to \alpha )}
⊢
(
α
→
β
)
∨
(
β
→
α
)
{\displaystyle \vdash (\alpha \to \beta )\lor (\beta \to \alpha )}
Derivabilidade de regras Raciocínio por casos:
Γ
1
,
¬
φ
⊢
ψ
;
Γ
2
,
φ
⊢
ψ
/
Γ
1
,
Γ
2
⊢
ψ
{\displaystyle \Gamma _{1},\neg \varphi \vdash \psi ;\Gamma _{2},\varphi \vdash \psi \,/\,\Gamma _{1},\Gamma _{2}\vdash \psi }
Raciocínio por redução ao absurdo:
Γ
1
,
¬
φ
⊢
¬
ψ
;
Γ
2
,
¬
φ
⊢
ψ
/
Γ
1
,
Γ
2
⊢
φ
{\displaystyle \Gamma _{1},\neg \varphi \vdash \neg \psi ;\Gamma _{2},\neg \varphi \vdash \psi \,/\,\Gamma _{1},\Gamma _{2}\vdash \varphi }
Para reflexão O que ocorre se ao invés de adicionarmos ao sistema de Dedução Natural para a Lógica Intuicionista a regra
(
⊥
E
c
l
s
)
Γ
,
¬
φ
⊢
⊥
/
Γ
⊢
φ
{\displaystyle (\bot \mathrm {E} _{cls})\;\Gamma ,\neg \varphi \vdash \bot \,/\,\Gamma \vdash \varphi }
adicionarmos uma regra da forma
Γ
,
¬
(
α
#
β
)
⊢
⊥
/
Γ
⊢
α
#
β
{\displaystyle \Gamma ,\neg (\alpha \#\beta )\vdash \bot \,/\,\Gamma \vdash \alpha \#\beta }
para algum conectivo binário
#
{\displaystyle \#}
O que ocorre se ao invés de adicionarmos ao sistema de Dedução Natural para a Lógica Intuicionista a regra
(
⊥
E
c
l
s
)
{\displaystyle (\bot \mathrm {E} _{cls})}
consequentia mirabilis ?
(
¬
c
l
s
)
Γ
,
¬
α
⊢
α
/
Γ
⊢
α
{\displaystyle (\neg _{cls})\;\Gamma ,\neg \alpha \vdash \alpha \,/\,\Gamma \vdash \alpha }
(Podemos dizer, neste caso, que se trata de uma regra de introdução ou de eliminação? E quanta diferença isso faz?)
Veja também Links externos 
