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.

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)
• $\land$ - Conjunção
• $\lor$ - 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

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.

Sistema de dedução natural

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.

Cada passo, ou seja, cada derivação realizada, na árvore, deve ser baseada em uma das regras do sistema. É como um jogo, em que devemos seguir todas as regras para podermos concluí-lo de maneira correta e vencer.

Os sistemas que trataremos aqui serão o Sistema intuitivo(Lógica Intuicionista), Sistema N_p (Lógica Clássica Proposicional) e o Sistema N_c(Lógica Clássica de Primeira Ordem).

Sistema intuitivo

No sistema intuitivo possuímos regras que tratam de conectivos, assim como o sistema N_p apresentado abaixo. A grande diferença entre o sistema intuitivo e o sistema N_p é 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: $\neg \neg \alpha \vdash \alpha ,$ facilmente derivadas no sistema N_p ou N_c da lógica clássica. Com exceção do citado, podemos utilizar as mesmas regras do sistema N_p.

Sistema N_p

No sistema N_p possuímos regras que tratam de conectivos. Abaixo está a apresentação do conjunto de regras do Sistema N_p:

Regras de eliminação

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").

Eliminação da conjunção

$A\land B \over A$ $\land Ed$ Eliminação da conjunção à direita.

$A\land B \over B$ $\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.

Exemplos:

$\left(\alpha \rightarrow \beta \right)\land \beta \vdash \alpha \rightarrow \beta$

${\left(\alpha \rightarrow \beta \right)\land \beta }^{1} \over \alpha \rightarrow \beta$ $\land Ed$

$\left(\alpha \rightarrow \beta \right)\land \beta \vdash \beta$

${\left(\alpha \rightarrow \beta \right)\land \beta }^{1} \over \beta$ $\land Ee$

Eliminação da implicação

$A\quad A\rightarrow B \over B$ $\rightarrow E$ Eliminação da implicação

A regra de eliminação da implicação diz que se temos uma implicação de $A$ em $B$ e sabemos quem é o $A,$ logo saberemos quem é o $B.$

Exemplo:

$\alpha ,\ \alpha \rightarrow \beta ,\ \beta \rightarrow \gamma \land \theta \vdash \gamma \land \theta$

${\cfrac {{\cfrac {\alpha ^{0}\qquad {\alpha \rightarrow \beta }^{1}}{\beta }}\ \rightarrow {E}\qquad {\beta \rightarrow \gamma \land \theta }^{2}}{\gamma \land \theta }}\ \rightarrow {E}$

Eliminação da disjunção

$\left[A\right]^{n}\left[B\right]^{m}$

$\vdots \qquad \vdots$

$A\lor B\quad C\quad C \over C$ $\lor E\ n,m$ Eliminação da disjunção com hipóteses $n$ e $m$

A regra de eliminação da disjunção diz que, se temos um $A$ derivando um $C$ e um $B$ derivando um $C$ e uma disjunção entre $A$ e $B,$ podemos eliminar a disjunção e ficar só com o $C,$ como é mostrado acima. Nessa regra podemos também transformar o $A$ e o $B$ em hipóteses, fechando as folhas.

Exemplo:

$\alpha \lor \beta ,\ \alpha \rightarrow \gamma ,\ \beta \rightarrow \gamma \vdash \gamma$

${\cfrac {{\alpha \lor \beta }^{3}\qquad {\cfrac {[\alpha ]^{1}\quad {\alpha \rightarrow \gamma }^{4}}{\gamma }}\ \rightarrow _{E}\qquad {\cfrac {[\beta ]^{2}\quad {\beta \rightarrow \gamma }^{5}}{\gamma }}\ \rightarrow _{E}}{\gamma }}\ \lor _{E,1,2}$

Regras de absurdo

As regras de absurdo partem da premissa que da falsidade podemos derivar qualquer coisa, ou seja, do absurdo podemos derivar qualquer coisa.

Absurdo clássico

$\left[\neg A\right]^{n}$

$\vdots$

$\bot \over A$ $\bot \ n$ Absurdo clássico com hipótese $n$

O absurdo clássico gera uma hipótese $\neg A.$ Se a partir dessa hipótese chegarmos a um absurdo, então podemos derivar A.

Exemplo:

$\alpha \rightarrow \beta ,\ \neg \beta \vdash \neg \alpha$

${\cfrac {{\cfrac {{\cfrac {{\cfrac {[\lnot \left(\lnot \alpha \right)]^{1}\quad [\lnot \alpha ]^{2}}{\bot }}\rightarrow E}{\alpha }}\bot ,2\quad {\alpha \rightarrow \beta }^{3}}{\beta }}\ \rightarrow {E}\qquad {\lnot \beta }^{4}}{{\cfrac {\bot }{\lnot \alpha }}\bot ,1}}\rightarrow E$

Note que, nesse exemplo, $\alpha \rightarrow \beta$ e $\lnot \beta$ são premissas.

Absurdo intuicionista

$\bot \over A$ $\bot \ int.$ Absurdo intuicionista

O absurdo intuicionista é menos poderoso que o absurdo clássico. Nele, não ganhamos hipótese alguma para utilizar, ou seja, temos que chegar a um absurdo através das premissas dadas para desse absurdo derivarmos outra coisa qualquer.

Regras de introdução

As regras de introdução introduzem conectivos lógicos nas derivações. Elas são melhores utilizadas quando estamos construindo uma derivação a partir da conclusão e em direção as hipóteses(metodologia bottom-up, ou "de baixo para cima").

Introdução da conjunção

$A\quad B \over A\land B$ $\quad \land I$ Introdução da conjunção

Se temos $A$ e $B$ podemos derivar $A\land B.$

Exemplo:

$[\alpha ]^{1}\quad \beta \rightarrow \gamma ^{2} \over \alpha \land \left(\beta \rightarrow \gamma \right)$ $\land I$

Introdução da implicação

$\left[A\right]^{n}$

$\vdots$

${B \over A\rightarrow B}{\begin{matrix}\rightarrow I\ n\end{matrix}}$ Introdução da implicação com hipótese $n$

Se chegamos a $B$ a partir de uma hipótese $A,$ derivamos: $A\rightarrow B$ e fechamos a hipótese $A.$

Exemplo:

${\cfrac {{\cfrac {[\alpha ]^{1}\quad \alpha \rightarrow \beta ^{2}}{\beta }}\rightarrow E}{{\cfrac {\beta \lor \gamma }{\alpha \rightarrow \left(\beta \lor \gamma \right)}}\rightarrow I,1}}\lor Id$

Note que nesse exemplo $\alpha \rightarrow \beta$ é uma premissa.

Introdução da disjunção

$A \over A\lor B$ $\qquad \lor Id$ Introdução da disjunção à direita

$A \over B\lor A$ $\quad \lor Ie$ Introdução da disjunção à esquerda

Se temos um $A$ então podemos adicionar à sua direita ou esquerda um disjunto qualquer.

Exemplos:

$\alpha ^{1} \over \alpha \lor \left(\beta \land \gamma \right)$ $\lor Id$

$\alpha ^{1} \over \left(\beta \land \gamma \right)\lor \alpha$ $\lor Ie$

Regras derivadas

São as regras criadas a partir de outras regras que, quando demonstradas válidas, podem ser utilizadas...

Abaixo temos dois exemplos de regras derivadas, uma de eliminação e outra de introdução, bastante utilizadas:

Eliminação da negação

$A\quad \neg A \over \bot$ $\neg E$ Eliminação da negação

A regra da eliminação da negação é uma regra feita a partir da eliminação da implicação, pois uma negação $\neg A$ pode ser apresentada como: $A\rightarrow \bot$ e se temos $A$ em conjunto dessa implicação podemos derivar $\bot .$ Ou seja, de $A$ e não $A,$ derivamos um absurdo.

Exemplo

$\alpha ,\ {\alpha \rightarrow {\neg \alpha }}\vdash \bot$

${{\alpha ^{1}\qquad {{\alpha ^{1}\quad {\alpha \rightarrow {\neg \alpha }}^{0}} \over {\neg \alpha }}\rightarrow _{E}} \over {\bot }}\neg _{E}$

Introdução da negação

${\begin{matrix}[A]^{n}\\\vdots \end{matrix}}$

$\bot \over \neg A$ $\neg I\ n$ Introdução da negação com hipótese $n$

A partir de uma hipótese $A,$ se chegarmos a um absurdo podemos derivar $\neg A.$ Essa regra se justifica através da regra do absurdo clássico e do fato que $\neg \neg A$ é o mesmo que $A.$

Sobre a bi-implicação

A bi-implicação ($A\leftrightarrow B$) pode ser introduzida como uma abreviatura para: $(A\rightarrow B)\land (B\rightarrow A)$

Sistema N_c

O sistema N_c inclui todo o sistema N_p 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.

Regras de eliminação

Seguem as regras que eliminam os quantificadores utilizados em primeira ordem.

Eliminação do universal

$\forall xA \over A[x:=i]$ $\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,$ se $i$ for um termo livre para $x$ na fórmula $A.$ Recomenda-se a utilização dela o mais próximo das folhas possível.

Exemplo:

$\forall x\left(P(x)\rightarrow Q(x)\right)^{1} \over P(a)\rightarrow Q(a)$ $\qquad \forall E$

Eliminação do existencial

${\begin{matrix}\ &[A[x:=i]]^{n}\\\ &\vdots \end{matrix}}$

$\exists xA\quad B \over B$ $\qquad \exists E\ n$ Eliminação do existencial

Algumas restrições devem ser efeitas sobre a aplicação dessa regra: $i$ não pode ocorrer livre nas hipóteses abertas que derivam $B,$ nem em $B$ e a marca n aplica-se apenas às hipóteses com a forma da hipótese fechada.

Regras de introdução

Abaixo estão as regras que introduzem os quantificadores utilizados em primeira ordem.

Introdução do universal

$A[x:=i] \over \forall xA$ $\forall I$ Introdução do universal

Se tivermos um i não-livre nas hipóteses abertas que derivam $A[x:=i],$ então podemos introduzir o quantificador universal. Recomenda-se a utilização desta regra o mais próximo da conclusão possível.

Introdução do existencial

$A[x:=i] \over \exists xA$ $\exists I$ Introdução do existencial

Se possuirmos um termo livre $i$ para a variável $x$ na fórmula $A,$ podemos então introduzir o quantificador existencial.

Exemplo:

${\cfrac {{\cfrac {[\forall x\left(P(x)\rightarrow Q(x)\right)]^{1}}{P(a)\rightarrow Q(a)}}\ \forall {E}\qquad [P(a)]^{2}}{{\cfrac {Q(a)}{\exists xQ(x)}}\exists I}}\ \rightarrow {E}$

Note que nesse exemplo, $\forall x\left(P(x)\rightarrow Q(x)\right)$ e $P(a)$ são premissas.

Validade do sistema

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, N_p e N_c).

Bibliografia

• Bedregal, Benjamín René Callejas, e Acióly, Benedito Melo (2002), Lógica para a Ciência da Computação, Versão Preliminar, Natal, RN.
• F. Miguel Dionísio, Paula Gouveia, João Marcos. Lógica Computacional. Versão preliminar, 2006.
• Introduction to natural deduction. Acesso em: 11:20 h. 18 de junho, 2007. Disponível em: http://www.danielclemente.com/logica/dn.en.html .

Ver também

• Álgebra booleana
• Axioma
• Cálculo proposicional implicacional
• Equivalência lógica
• Forma normal conjuntiva

• Forma normal disjuntiva
• Fórmula atômica
• História da lógica
• Lógica aristotélica
• Lógica combinacional

• Lógica proposicional
• Operação
• Princípio da resolução
• Tabela verdade

Ligações externas

• Planetmath - Natural Deduction