Difference between revisions of "Exercícios de Dedução Natural"
Jump to navigation
Jump to search
Tag: 2017 source edit |
Tag: 2017 source edit |
||
Line 79: | Line 79: | ||
==== <math>(\forall x_1)(\forall x_2)R(x_1,x_2) \vdash (\forall x_2)(\forall x_1)R(x_1,x_2)</math> ==== | ==== <math>(\forall x_1)(\forall x_2)R(x_1,x_2) \vdash (\forall x_2)(\forall x_1)R(x_1,x_2)</math> ==== | ||
: {{#ev:youtube|B7fFRZF_wao|||||start=1303}} | : {{#ev:youtube|B7fFRZF_wao|||||start=1303}} | ||
− | ==== <math>(\forall x) \ | + | ==== <math>(\forall x) \varphi_1 \land \varphi_2 \dashv\vdash (\forall x) \varphi_1 \land (\forall x)\varphi_2<math> ==== |
: {{#ev:youtube|B7fFRZF_wao|||||start=1678}} | : {{#ev:youtube|B7fFRZF_wao|||||start=1678}} | ||
Revision as of 15:29, 11 October 2020
Contents
- 1 Dedução Natural para a Lógica Proposicional Intuicionista
- 2 Dedução Natural para a Lógica Proposicional Clássica
- 3 Dedução Natural para a Lógica de Primeira Ordem Intuicionista
- 3.1 Derivabilidade de sequentes
- 3.1.1
- 3.1.2
- 3.1.3
- 3.1.4 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 (\forall x) \varphi_1 \land \varphi_2 \dashv\vdash (\forall x) \varphi_1 \land (\forall x)\varphi_2<math> ==== : {{#ev:youtube|B7fFRZF_wao|||||start=1678}} ==Dedução Natural para a Lógica de Primeira Ordem Clássica== [AGUARDE!] ===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}
- 3.1.5 Raciocínio por redução ao absurdo:
- 3.1 Derivabilidade de sequentes
- 4 Para reflexão
- 5 Veja também
- 6 Links externos
Dedução Natural para a Lógica Proposicional Intuicionista
Derivabilidade de sequentes
Derivabilidade de regras
a partir de + ()
a partir de +
Dedução Natural para a Lógica Proposicional Clássica
Derivabilidade de sequentes
Terceiro Excluído / Tertium Non Datur:
- Tarefa: Demonstrar a mesma fórmula, invertendo a ordem de aplicação das regras de introdução da disjunção.
, via raciocínio por absurdo
, via terceiro excluído
Dedução Natural para a Lógica de Primeira Ordem Intuicionista
[AGUARDE!]
Derivabilidade de sequentes
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 (\forall x) \varphi_1 \land \varphi_2 \dashv\vdash (\forall x) \varphi_1 \land (\forall x)\varphi_2<math> ==== : {{#ev:youtube|B7fFRZF_wao|||||start=1678}} ==Dedução Natural para a Lógica de Primeira Ordem Clássica== [AGUARDE!] ===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}
Raciocínio por redução ao absurdo:
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
adicionarmos uma regra da forma
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 adicionarmos a seguinte regra de consequentia mirabilis?
(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 adicionarmos a regra