Dedução natural
A Dedução Natural é um sistema dedutivo fundamental na Lógica, introduzido por Gentzen nos anos 30, para a construção de demonstrações formais. Para realizar uma derivação formal, é essencial formalizar a expressão a ser demonstrada, traduzindo-a da linguagem usual para uma notação lógica universal e concisa. Essa formalização torna a expressão compreensível independentemente do idioma e otimiza o espaço da escrita.
Pontos-chave
- A Dedução Natural é um sistema dedutivo para construir demonstrações formais em Lógica.
- Foi introduzida por Gentzen nos anos 30, motivado pela busca de consistência na teoria dos números.
- A formalização de expressões é crucial, traduzindo-as para uma notação lógica universal.
- O sistema serve para verificar a derivabilidade de uma expressão, usando métodos lineares ou árvores de derivação.
- É considerado válido por ser correto (deriva o que é verdadeiro semanticamente) e completo (deriva tudo que é demonstrado semanticamente).
O sistema de Dedução Natural surgiu da insatisfação com os sistemas de demonstração formal anteriores, desenvolvidos por Hilbert, Frege e Russell. Jaśkowski iniciou o desenvolvimento de um sistema mais natural em 1929, usando notação diagramática e atualizando sua proposta nos anos 30. A forma moderna foi proposta por G. Gentzen, um matemático alemão, em 1935, em sua dissertação na Universidade de Göttingen. Gentzen buscava estabilizar a consistência da teoria dos números, e embora tenha encontrado uso para seu cálculo, a complexidade inicial das demonstrações o levou a uma nova consistência em 1938. Prawitz, em 1965, desenvolveu uma monografia que apresentou o sistema de Dedução Natural em sua forma mais conhecida atualmente, incluindo aplicações para lógica modal e de segunda ordem, baseando-se fortemente no trabalho de Gentzen.
O sistema de Dedução Natural é utilizado para verificar a derivabilidade de uma expressão. Contudo, ele não gera contra-modelos nem mostra um conjunto de derivações possíveis; a árvore de derivação apresenta apenas uma das várias derivações existentes. As demonstrações podem ser escritas de forma linear ou através de árvores de derivação. Numa árvore, a raiz é a conclusão, e os filhos são as derivações que levam a essa conclusão. O sistema utiliza regras para unir árvores finitas, que são geradas a partir de um conjunto finito de premissas e hipóteses até derivar uma conclusão. As folhas da árvore representam hipóteses ou premissas; folhas abertas são premissas, enquanto as fechadas (marcadas com []) são hipóteses. Todas as folhas devem ter marcas (geralmente números naturais) para identificação, e conflitos de marcas devem ser evitados.
Sistema Intuitivo: Lógica Sem Absurdo Clássico
O sistema intuitivo possui regras para conectivos, semelhantes ao sistema Np. A principal diferença é a ausência da regra do absurdo clássico e de derivações baseadas nela. Isso significa que derivações como ¬ ¬ α ⊢ α, facilmente obtidas nos sistemas Np ou Nc da lógica clássica, não são possíveis. Com essa exceção, as demais regras do sistema Np podem ser utilizadas.
Sistema Np: Regras para Conectivos Proposicionais
O sistema Np contém regras específicas para o tratamento de conectivos. As regras de eliminação, por exemplo, demonstram como remover conectivos para gerar derivações. Elas são mais eficazes na construção de derivações 'de cima para baixo', partindo das hipóteses em direção à conclusão. Exemplos incluem: Eliminação da conjunção à direita (A ∧ B / A) e Eliminação da conjunção à esquerda (A ∧ B / B). Essas regras indicam que, dada uma conjunção, é possível extrair e eliminar uma de suas partes (direita ou esquerda).
Sistema Nc: Lógica Clássica de Primeira Ordem
O sistema Nc abrange todo o sistema Np e adiciona novas regras para trabalhar com fórmulas da Lógica Clássica de Primeira Ordem, incluindo as regras relativas aos quantificadores, que não existem na Lógica Proposicional. Um exemplo é a Eliminação do Universal (∀ x A / A [x := i]), que permite eliminar um quantificador universal substituindo-o por um termo 'i', desde que 'i' seja um termo livre para 'x' na fórmula 'A'. Recomenda-se aplicar essa regra o mais próximo possível das folhas da árvore de derivação.
Um sistema dedutivo é considerado válido se for simultaneamente correto e completo. A correção significa que tudo o que o sistema deriva pode ser demonstrado como verdadeiro através da semântica. A completude, por sua vez, implica que o sistema consegue derivar tudo o que é demonstrado semanticamente. O sistema de Dedução Natural é válido nos sistemas intuitivo, Np e Nc, o que significa que ele atende a ambos os critérios de correção e completude.
