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

Edição de 15h00min 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 de Inferência Hipotéticas

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

Regra de Prova Condicional

Arquivo:Regra1.jpeg