Difference between revisions of "Exercícios de Dedução Natural"

From Logic Wiki

Jump to navigation Jump to search

Revision as of 11:07, 23 July 2021

Contents

1 Dedução Natural para a Lógica Proposicional Intuicionista
- 1.1 Derivabilidade de sequentes
- 1.2 Derivabilidade de regras
2 Dedução Natural para a Lógica Proposicional Clássica
- 2.1 Derivabilidade de sequentes
3 Dedução Natural para a Lógica de Primeira Ordem Intuicionista
- 3.1 Derivabilidade de sequentes
4 Dedução Natural para a Lógica de Primeira Ordem Clássica
- 4.1 Derivabilidade de sequentes
  - 4.1.1 $\neg (\exists x)\neg \varphi \vdash (\forall x)\varphi$
  - 4.1.2 $\vdash (\exists x)(\forall y)(B(y)\lor \neg B(x))$
- 4.2 Derivabilidade de regras
5 Para reflexão
6 Veja também
7 Links externos

Dedução Natural para a Lógica Proposicional Intuicionista

Derivabilidade de sequentes

$\varphi \land \psi \vdash \psi \land \varphi$

$(\varphi \land \psi )\land \delta \vdash \varphi \land (\psi \land \delta )$

$\varphi \vdash \varphi \land \varphi$

$\alpha \land \beta ,\gamma \land \delta \vdash \gamma \land \beta$

$\alpha \to (\beta \to \gamma )\vdash \beta \to (\alpha \to \gamma )$

$\vdash \alpha \to (\beta \to \alpha )$

$\vdash \alpha \to \alpha$

$\alpha \to \beta \vdash \alpha \to (\alpha \to \beta )$

$\alpha \to (\alpha \to \beta )\vdash \alpha \to \beta$

$\gamma \to \alpha ,\gamma \to \beta \vdash \gamma \to (\alpha \land \beta )$

$\beta \lor (\alpha \land \beta )\vdash \beta$

$(\alpha \lor \beta )\to \gamma \vdash (\alpha \to \gamma )\land (\beta \to \gamma )$

$\alpha \vdash \neg \neg \alpha$

$\beta \to \alpha ,\beta \to \neg \alpha \vdash \neg \beta$

$\alpha ,\neg \alpha \vdash \neg \beta$

$\alpha \lor \beta ,\neg \alpha \lor \gamma \vdash \beta \lor \gamma$

$\alpha \to \beta \vdash \neg \beta \to \neg \alpha$

$\neg (\alpha \lor \beta )\dashv \vdash \neg \alpha \land \neg \beta$

Derivabilidade de regras

$\mathrm {(DNE)}$ a partir de $\mathrm {DN_{int}}$ + ( $\mathrm {\bot E_{cls}}$ )

$(\mathrm {\bot E_{cls}} )$ a partir de $\mathrm {DN_{int}}$ + $\mathrm {(DNE)}$

$(\mathbb {M} )$

$(\mathbb {R} )$

$(\mathbb {T} )$

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

Derivabilidade de sequentes

Terceiro Excluído / Tertium Non Datur: $\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.

$\neg \neg \alpha \vdash \alpha$

$\neg \beta \to \alpha ,\neg \beta \to \neg \alpha \vdash \beta$

$\neg \alpha \to \neg \beta \vdash \beta \to \alpha$

$\vdash (\alpha \to \beta )\lor (\beta \to \alpha )$ , via raciocínio por absurdo

$\vdash (\alpha \to \beta )\lor (\beta \to \alpha )$ , via terceiro excluído

Dedução Natural para a Lógica de Primeira Ordem Intuicionista

Derivabilidade de sequentes

$(\forall x)(\varphi \to \psi )\vdash (\forall x)\varphi \to (\forall x)\psi$

$(\forall x)Q(x)\vdash (\forall y)Q(y)$

$(\forall x_{1})(\forall x_{2})R(x_{1},x_{2})\vdash (\forall x_{2})(\forall x_{1})R(x_{1},x_{2})$

$(\forall x)\varphi _{1}\land \varphi _{2}\dashv \vdash (\forall x)\varphi _{1}\land (\forall x)\varphi _{2}$

$(\exists x)P(x),(\forall x)(\forall y)(P(x)\to Q(y))\vdash (\forall y)Q(y)$

$(\forall x)A(x),(\exists y)(A(y)\to B(y)),(\forall z)(A(z)\to C(z))\vdash (\exists w)(B(w)\land C(w))$

$(\exists x)(\varphi _{1}\lor \varphi _{2})\dashv \vdash (\exists x)\varphi _{1}\lor (\exists x)\varphi _{2}$

$(\exists x)(\forall y)\varphi \vdash (\forall y)(\exists x)\varphi$

$(\forall x)\neg \varphi \vdash \neg (\exists x)\varphi$

Dedução Natural para a Lógica de Primeira Ordem Clássica

[AGUARDE!]

Derivabilidade de sequentes

$\neg (\exists x)\neg \varphi \vdash (\forall x)\varphi$

$\vdash (\exists x)(\forall y)(B(y)\lor \neg B(x))$

Derivabilidade de regras

Raciocínio por casos: $\Gamma _{1},\neg \varphi \vdash \psi ;\Gamma _{2},\varphi \vdash \psi \,/\,\Gamma _{1},\Gamma _{2}\vdash \psi$

Raciocínio por redução ao absurdo: $\Gamma _{1},\neg \varphi \vdash \neg \psi ;\Gamma _{2},\neg \varphi \vdash \psi \,/\,\Gamma _{1},\Gamma _{2}\vdash \varphi$

$(\approx _{sim})\Gamma \vdash t_{1}\approx t_{2}/\Gamma \vdash t_{2}\approx t_{1}$

$(\approx _{trn})\Gamma _{1}\vdash t_{1}\approx t_{2};\Gamma _{2}\vdash t_{2}\approx t_{3}/\Gamma _{1},\Gamma _{2}\vdash t_{1}\approx t_{3}$

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
$(\bot \mathrm {E} _{cls})\;\Gamma ,\neg \varphi \vdash \bot \,/\,\Gamma \vdash \varphi$
adicionarmos uma regra da forma
$\Gamma ,\neg (\alpha \#\beta )\vdash \bot \,/\,\Gamma \vdash \alpha \#\beta$
para algum conectivo binário $\#$ da nossa linguagem?

O que ocorre se ao invés de adicionarmos ao sistema de Dedução Natural para a Lógica Intuicionista a regra $(\bot \mathrm {E} _{cls})$ adicionarmos a seguinte regra de consequentia mirabilis?
$(\neg _{cls})\;\Gamma ,\neg \alpha \vdash \alpha \,/\,\Gamma \vdash \alpha$
(Será que podemos dizer, neste caso, que se trata de uma regra de introdução ou de eliminação? E quanta diferença isso faz?)

O que ocorre se ao invés de adicionarmos ao sistema de Dedução Natural para a Lógica de Primeira Ordem Intuicionista a regra $(\bot \mathrm {E} _{cls})$ adicionarmos a regra
$(DNQ)\;\Gamma \vdash (\forall x)\neg \neg \varphi \,/\,\Gamma \vdash \neg \neg (\forall x)\varphi$

Veja também

Links externos

Retrieved from "http://carol.dimap.ufrn.br/logicwiki/index.php?title=Exercícios_de_Dedução_Natural&oldid=1516"