Changes

=== Derivabilidade de sequentes ===

====<math>\varphi \land \psi \vdash \psi \land \varphi</math>====

====<math>(\varphi \land \psi) \land \delta \vdash \varphi \land (\psi \land \delta)</math>====

====<math>\varphi \vdash \varphi \land \varphi</math>====

====<math>\alpha \land \beta, \gamma \land \delta \vdash \gamma \land \beta</math>====

====<math>\alpha \to (\beta \to \gamma) \vdash \beta \to (\alpha \to \gamma)</math>====

====<math>\vdash \alpha \to (\beta \to \alpha)</math>====

====<math>\vdash \alpha \to \alpha</math>====

====<math>\alpha \to \beta \vdash \alpha \to (\alpha \to \beta)</math>====

====<math>\alpha \to (\alpha \to \beta) \vdash \alpha \to \beta</math>====

====<math>\gamma \to \alpha, \gamma \to \beta \vdash \gamma \to (\alpha \land \beta)</math>====

====<math>\beta \lor (\alpha \land \beta) \vdash \beta</math>====

====<math>(\alpha \lor \beta) \to \gamma \vdash (\alpha \to \gamma) \land (\beta \to \gamma)</math>====

====<math>\alpha \lor \beta \not\vdash \alpha \land \beta</math>====

====<math>\alpha \vdash \neg\neg\alpha</math>====

====<math>\beta \to \alpha, \beta \to \neg\alpha \vdash \neg\beta</math>====

====<math>\alpha, \neg\alpha \vdash \neg\beta</math>====

====<math>\alpha\lor\beta, \neg\alpha\lor\gamma \vdash \beta\lor\gamma</math>====

====<math> \alpha\to\beta \vdash \neg\beta\to\neg\alpha</math>====

====<math>\neg(\alpha \lor \beta) \dashv\vdash \neg\alpha\land\neg\beta</math>====

===Derivabilidade de regras===

==== <math>\mathrm{(DNE)}</math> a partir de <math>\mathrm{DN_{int}}</math> + (<math>\mathrm{\bot E_{cls}}</math>) ====

==== <math>(\mathrm{\bot E_{cls}})</math> a partir de <math>\mathrm{DN_{int}}</math> + <math>\mathrm{(DNE)}</math> ====

==== <math>(\mathbb{M})</math> ====

==== <math>(\mathbb{R})</math> ====

==== <math>(\mathbb{T})</math> ====

==Dedução Natural para a Lógica Proposicional Clássica==

====Terceiro Excluído / ''Tertium Non Datur'': <math>\vdash\varphi\lor\neg\varphi</math>====

-->''Tarefa:'' Demonstrar a mesma fórmula, invertendo a ordem de aplicação das regras de introdução da disjunção.

==== <math>\neg\neg\alpha \vdash \alpha</math> ====

==== <math>\neg\beta\to\alpha, \neg\beta\to\neg\alpha \vdash \beta</math> ====

==== <math>\neg\alpha\to\neg\beta \vdash \beta\to\alpha</math> ====

==== <math>\vdash (\alpha \to \beta) \lor (\beta \to \alpha)</math>, via raciocínio por absurdo ====

==== <math>\vdash (\alpha \to \beta) \lor (\beta \to \alpha)</math>, via terceiro excluído ====

===Derivabilidade de regras===

====Raciocínio por casos: <math>\Gamma_1, \neg\varphi\vdash\psi; \Gamma_2, \varphi\vdash\psi \, / \, \Gamma_1, \Gamma_2 \vdash \psi</math>====

====Raciocínio por redução ao absurdo: <math>\Gamma_1, \neg\varphi\vdash\neg\psi; \Gamma_2, \neg\varphi\vdash\psi \, / \, \Gamma_1, \Gamma_2 \vdash \varphi</math>====

==Para reflexão==