Dedução natural
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 linguí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.
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 demonstrações, e em 1938 deu uma nova consistência às 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 sistema de dedução natural serve para verificar a derivabilidade de uma expressão. Não serve, porém, para gerar um contra-modelo nem para mostrar um conjunto de derivações possíveis, ou seja, a árvore de derivação nos mostra apenas uma, das várias derivações existentes para a expressão. Existem dois métodos de se escrever as demonstrações em dedução natural: através de um método linear ou através de árvores de derivação (árvores de dedução). A raiz da árvore é a conclusão, os filhos são as derivações que geram a conclusão. O sistema de dedução natural apresenta regras que unem árvores(finitas), que são geradas a partir de um conjunto finito de premissas e hipóteses até derivar uma certa conclusão. As folhas da árvore representam hipóteses ou premissas. As folhas abertas representam premissas, enquanto as fechadas representam hipóteses (marcadas com []). Todas as folhas devem possuir marcas e deve-se evitar o conflito de marcas, ou seja, ter duas fórmulas diferentes com uma mesma marca. A marca, geralmente, é um número natural, identificando as folhas.
Sistema intuitivo
No sistema intuitivo possuímos regras que tratam de conectivos, assim como o sistema Np apresentado abaixo. A grande diferença entre o sistema intuitivo e o sistema Np é que o sistema intuitivo não possui a regra do absurdo clássico e nenhuma derivação baseada nela. Sendo assim, não podemos fazer derivações como: ¬ ¬ α ⊢ α , {\displaystyle \neg \neg \alpha \vdash \alpha ,} facilmente derivadas no sistema Np ou Nc da lógica clássica. Com exceção do citado, podemos utilizar as mesmas regras do sistema Np.
Sistema Np
No sistema Np possuímos regras que tratam de conectivos. Abaixo está a apresentação do conjunto de regras do Sistema Np: As regras de eliminação mostram como retirar os conectivos para podermos gerar derivações. Elas são melhores utilizadas quando estamos construindo uma derivação a partir das hipóteses em direção a conclusão ("de cima para baixo"). A ∧ B A {\displaystyle A\land B \over A} ∧ E d {\displaystyle \land Ed} Eliminação da conjunção à direita. A ∧ B B {\displaystyle A\land B \over B} ∧ E e {\displaystyle \land Ee} Eliminação da conjunção à esquerda. As regras de eliminação da conjunção, como foram apresentadas acima, dizem que, se temos uma conjunção, podemos tirar um pedaço dela, a parte mais à direita (Ed) ou a parte mais à esquerda (Ee), e eliminá-lo.
Sistema Nc
O sistema Nc inclui todo o sistema Np mas adiciona algumas regras novas para que possamos trabalhar com fórmulas da Lógica Clássica de Primeira Ordem. As regras adicionais são as relativas aos quantificadores, inexistentes na Lógica Proposicional. Seguem as regras que eliminam os quantificadores utilizados em primeira ordem. ∀ x A A [ x := i ] {\displaystyle \forall xA \over A[x:=i]} ∀ E {\displaystyle \qquad \forall E} Eliminação do Universal Esta regra diz que se temos um quantificador universal podemos eliminá-lo substituindo-o por um termo i , {\displaystyle i,} se i {\displaystyle i} for um termo livre para x {\displaystyle x} na fórmula A . {\displaystyle A.} Recomenda-se a utilização dela o mais próximo das folhas possível.
Um sistema dedutivo pode ser considerado válido se o que ele deriva pode ser demonstrado, como verdadeiro, através da semântica, sendo assim considerado correto, e se ele conseguir derivar tudo que é demonstrado semanticamente, sendo assim considerado completo. Ou seja, o sistema dedutivo pode ser correto, completo e válido, mas para ser válido ele precisa ser correto e completo ao mesmo tempo. O sistema dedutivo nomeado dedução natural é válido nos sistemas mostrados acima(intuitivo, Np e Nc).
