Sistema dedutivo de dedução natural

Sistema Dedutivo de Dedução Natural

Este sistema dedutivo é bastante natural, pois reflete o raciocínio usado nas demonstrações informais em matemática ou em qualquer outro argumento lógico informal.

Para cada um dos símbolos lógicos existem duas regras, uma que introdução e outra de eliminação. As regras de introdução de conectivos inferem fórmulas cujo conectivo principal é aquele (por exemplo, a regra de introdução de  infere uma fórmula cujo conectivo principal é ), já as de eliminação de um conectivo, partem de fórmulas com aquele conectivo.Vamos representar a regra "de  e  infira " por  , 



Regras de inferência :

IP 



Introdução Eliminação

I E

,       

    

I E

 .  . [] []

      . .

. .

    



I E1 E2

[] [] ,  []

. .  .

. . .

  

 

I  E

[]   , 

. 

.



  

I E

  ,         

        

Chamamos de hipóteses (conclusões) da regra as fórmulas que ocorrem acima (abaixo) do travessão. Em algumas regras não temos simplesmente fórmulas acima do travessão, mas derivações, por exemplo, regras I  e I. Nestas regras, as fórmulas entre []’s são hipóteses usadas (localmente) naquelas derivações e não são consideradas como hipóteses das regras. Estas hipóteses entre parênteses são ditas "descarregadas".

Assim, na representação em forma de lista, uma prova de  a partir de um conjunto de premissas  é uma seqüência finita de fórmulas 1,2,3, ... , m tal que m é  e cada i=1…m, i ou é obtido pela aplicação de uma regra de inferência a j's com j<i.

Apesar de em um sistema dedutivo as regras de inferência terem um cunho essencialmente formal, podemos dar uma explicação semântica de seu uso. Assim, a regra I significa que se temos duas fórmulas  e , isto é, se  e  valem sua conjunção    também vale. A regra I reflete o raciocínio que fazemos nas provas de redução ao absurdo: se supondo  chegamos a um absurdo ( e  para algum ) então devemos ter A regra IP ( introdução de premissas) diz que supondo  podemos inferir 

As estratégias usadas para a obtenção das derivações não são indicadas nas derivações. A obtenção das derivações em geral é guiada pela aplicação da regra de introdução do conectivo principal das fórmulas a serem derivadas ao longo da derivação, e desta forma as derivações são obtidas de trás para frente, como será ilustrado nos exemplos ao longo desta seção.

Como as regras são usadas sucessivamente numa derivação e algumas fórmulas são usadas temporariamente como hipóteses para a aplicação de uma regra, numa representação linear de uma derivação o conceito de escôpo das hipóteses se torna útil, no sentido de que uma hipótese só pode ser usada dentro de seu escôpo. Podemos usar identação de fórmulas dentro de uma derivação para indicar em que escôpo elas estão sendo derivadas, isto é, de quais hipóteses elas dependem.

Exemplos de derivações:

1. Derive AD a partir das premissas A BC , A B e C D por dedução natural

1. A  B  C IP

2. A B IP

3. C D IP

4. [A] ( para I )

5. B  C 1,4 E

6. [B] (hipótese usada para E

7. B 2,4 E 

8. D 6,7 E1

9. [C] (para E 

10. D 3,9 E

11. D 6-7 e 9-10 E 

12. A D 4-8 I 

Observe que como a fórmula a ser derivada, A D, é um condicional, esta poderá ser obtida pela aplicação de I. Então o problema original se reduz a derivarD a partir de das premissas originais, A BC , A B, C D acrescidas da premissa A . Na derivação que obtemos no exemplo a fórmula D foi obtida a partir das premissas diretamente, mas tambem poderia ter sido obtida guiada por seu conectivbo, isto é, por aplicação da regra I.

Outra forma de representarmos a relação de dependência entre as fórmulas de uma derivação e as hipóteses das quais elas dependem é listar explicitamente as hipóteses, i. e. em cada linha, entre {}’, listamos os números das hipóteses das quais a fórmula da linha depende. Abaixo representamos a derivação dada anteriormente explicitando as hipóteses de cada linha.

{1} 1. A