Open main menu

Changes

1,040 bytes added ,  20:59, 15 October 2020
(Abreviatura: DN = Dedução Natural)= Derivações ==
* '''Componentes do formalismo dedutivo ''' da DNDedução Natural: ''regras '' (primitivas e derivações[VIDEO]* Elementos constitutivos das árvores de derivação em DNderivadas / casos particulares: nós, folhas, descendentes diretos (axiomas e justificativasteoremas), raize ''derivações''<!--[VIDEO]--><p>{{#ev:youtube|By6E_g2xf1Q}}</p>* Definição formal de derivação a partir O '''conjunto das derivações''' de um sistema de DNDedução Natural<!--[VIDEO]--><p>{{#ev:youtube|c4gdWh7vBwQ}}</p>* O conjunto das '''Notação DN<sup>Tree</sup>''': derivações como indutivamente definido[VIDEO]* Definição formal de árvores de derivação do tipo DN (árvores rotulada por fórmulas, com descarte de hipóteses)<!--[VIDEO]--><p>{{#ev:youtube|UdA2l5BK960}}</p>* Árvores de derivaçãoDerivações: manipulando ''manipulando fórmulas'' ou ''sequentes''?<!----><p>{{#ev:youtube|TyFDAjvSBgM}}</p> == Derivabilidade e admissibilidade ==[VIDEO]* Definição formal '''Derivabilidade''' e '''admissibilidade''' de consequência dedutiva a partir de um sistema de DNregras<!--[VIDEO]--><p>{{#ev:youtube|2KzJ3hB9a-Q}}</p>* Uso de '''lemas'''<!--[VIDEO]--><p>{{#ev:youtube|9BdeXjhyJWs}}</p>* Regras admissíveis[AGUARDEDa ''derivabilidade das regras estruturais'' na notação DN<sup>Tree</sup><!]--* Regras deriváveis--><p>{{#ev:youtube|jdHxUb2koy8}}</p>[VIDEO]* [[Estratégias == Noção de demonstração]]consequência dedutiva == * Conjunto das derivações Definição formal e principais meta-propriedades da '''relação de consequência dedutiva''' associada a um sistema de DN[VIDEO]Dedução Natural<!--* Notação para DN--><p>{{#ev: derivações como árvores de fórmulas[VIDEO]youtube|C9G_kswh-z4}}</p>
== Para reflexão ==
* Qual o ''significado lógico'' e o ''uso matemático'' da regra estrutural (𝕋)?* Como demonstrar que uma certa regra (ou um certo sequente) ''não é derivável '' na lógica clássica?* Como demonstrar que uma certa regra (ou um certo sequente) classicamente derivável não é derivável ''na lógica intuicionista''?* Se R é uma ''regra admissível'' em '''Nat''', o que ocorre se você ''adicionar'' esta regra ao estoque de regras primitivas de '''Nat'''? E por quê ''regras deriváveis são sempre admissíveis''?* Note que, em geral, os sistemas dedutivos no formalismo da Dedução Natural contêm regras de ''introdução'' e de ''eliminação''. Não há nada chamado "regras de ''inclusão''" ou "regras de ''exclusão''"!
== Veja também ==
* [[DN Dedução Natural para a Lógica Proposicional Intuicionista]]* [[DN Dedução Natural para a Lógica Proposicional Clássica]]* [[DN Dedução Natural para a Lógica de Primeira Ordem Intuicionista]]* [[Dedução Natural para a Lógica de Primeira Ordem Clássica]]* [[Estratégias de demonstração]]
* [[Relação de consequência]]
* [[Correção e completude]]
* [[Introdução Computacional à Lógica Matemática]]
== Links externos ==
*[http://pt.wikipedia.org/wiki/Dedu%C3%A7%C3%A3o_natural Dedução natural]