Dedução Natural: Alexandre, Liège e Danilo
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:
