Dedução

Dedução natural é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Foram introduzidos pela primeira vez, nos anos 30, por Gentzen. Para poder realizar uma derivação formal, é necessário formalizar a expressão que queremos demonstrar. Formalizar significa traduzir da forma lingüística usual para uma notação lógica, uma forma que é entendível para qualquer um, independente da língua que fala, e que também reduz o espaço ocupado pela frase escrita, tendo em vista que podemos utilizar uma notação mais econômica, a lógica.

Na notação formal utilizamos conectivos lógicos, operadores que realizam a ligação entre os átomos (os menores objetos). São eles:

\neg - Negação (não é um conectivo, simplesmente nega a fórmula ou átomo ligado)
\and - Conjunção
\or - Disjunção
\rightarrow - Implicação
\leftrightarrow - Bi-implicação
No caso da lógica clássica de primeira ordem, temos ainda os quantificadores:

\forall - Universal
\exists - Existencial
Também utilizamos alguns símbolos extras para auxiliar:

\vdash - Derivação
\vDash - Consequência semântica
\top - Top (Verdade)
\bot - Bottom (Absurdo, falsidade)
Motivação[editar | editar código-fonte]
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. A forma moderna da dedução natural, porém, 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