Sistema Dedutivo de Dedução Natural

...

α ↔ β α → β β → α

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

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 → B ∨ C IP

{2} 2. A → ¬ B IP

{3} 3. C → ¬ D IP

{4} 4. [A] (para I →)

{1,4} 5. B ∨ C 1,4E →

{6} 6. [B] (para E ∨)

{2,4} 7. ¬ B 2,4 E →

{2,4,6} 8. ¬ D 6,7 E¬1

{9} 9. [C] (para E ∨)

{3,9} 10. ¬ D 3,9 T

{1,2,3,4} 11. ¬ D 6-7 e 9-10 E ∨

{1,2,3} 12. A → ¬ D 4-11 I →

Note que ao descarregarmos as hipótese das linhas 6 e 7, na lista das hipóteses da linha 8 fizemos a união do conjuntos das hipóteses das linhas 10, 8 e 5, eliminando as hipóteses da linha 6 e 9. Também ao eliminarmos a hipótese da linha 4 para obtermos as hipótese da linha 12, mantivemos as hipóteses da linha 11 menos as da linha 4.

2. Obtenha ¬E a partir de {A → (B→ C ), C→ ¬ D, ¬ D→ ¬ E, A ∧ B } por dedução natural (vamos representar as hipóteses e fazer a identação das fórmulas).

{1} 1. Α → (Β → C ) IP

{2} 2. C→ ¬ D IP

{3} 3. ¬ D→ ¬ E IP

{4 } 4. A∧B IP

{5 } 5. [E] (para I¬)

{4} 6. A 4 E∧

{1,4} 7. Β→ C 1,7 E →

{4} 8. Β 4 E∧

{1,4} 9. C 1,7

{1,4,2} 10. ¬D 3,2 E →

{1,4,2,3} 11. ¬E 5,3 E →

{1, 2, 3, 4, 5} 12. E∧¬ E 11,5 I∧

{1,2,3,4} 13. ¬ E 3-12 I¬

As derivações também podem ser representadas em forma de árvore, para tal usaremos a seguinte notação:

- D para indicar uma derivação de α

α

- η para indicar uma derivação de α usando η como uma das hipóteses.

D

α

-