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 3 Veja também 4 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)} }
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 }
Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (\alpha \to \beta) \lor (\beta \to \alpha), via raciocínio por absurdo}
Failed to parse (syntax error): {\displaystyle (\alpha \to \beta) \lor (\beta \to \alpha), via terceiro excluído}
Derivabilidade de regras Nenhum exemplo ainda para esta seção.
Veja também Links externos 
