Dedução Natural: Alexandre, Liège e Danilo

De Wiki DAINF
(Diferença entre revisões)
(Nova página: '''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica no...)
 
Linha 2: Linha 2:
  
 
Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.
 
Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.
 +
  
 
'''Motivação'''
 
'''Motivação'''
Linha 8: Linha 9:
  
 
Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.
 
Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.
 +
  
 
'''O Método'''
 
'''O Método'''
Linha 14: Linha 16:
  
 
As regras básicas de inferência são postuladas (aceitas sem demonstração).  Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.
 
As regras básicas de inferência são postuladas (aceitas sem demonstração).  Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.
 +
  
 
'''Regras de Inferência'''
 
'''Regras de Inferência'''
Linha 25: Linha 28:
  
 
Exemplos:
 
Exemplos:
 
+
[[Imagem:Regras.jpeg]]
Dupla Negação (DN):
+
 
+
<nowiki>Dupla Negação (DN):       Modus Ponens (MP):              Conjunção (C):
+
            ¬¬  
+
  
+
  
+
 
+
  Separação (S):   Expansão (E): Silogismo Disjuntivo (SD):
+
    
+
  ¬¬
+
 
+
 
+
Condicionais para Bicondicional (CB):   Bicondicional para Condicionais (BC):
+
                     
+
 
+

+
</nowiki>
+

Edição de 14h55min de 30 de março de 2009

Dedução natural é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.


Motivação


O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.


O Método


Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.


Regras de Inferência


Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.


Regras de Inferência Diretas

Exemplos: Regras.jpeg

Ferramentas pessoais