8

SISTEMA 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 de introdução e outra de eliminação. As regras de introdução de conectivos inferem fórmulas cujo conectivo principal é o próprio (por exemplo, a regra de introdução do ∧ infere uma fórmula cujo conectivo principal é ∧).
As regras de eliminação de um conectivo partem de fórmulas com aquele conectivo.

1.1 REGRAS NÃO HIPOTÉTICAS DE INFERÊNCIA

O Sistema de Dedução Natural (SDN) não é axiomático. Para as provas, não se parte de axiomas, mas sim de premissas dadas ou de hipóteses formuladas.
Quanto às regras de dedução/inferência, existem 10 eliminação e introdução de cada conectivo/operador.

regras

básicas, correspondendo à

(i) Eliminação da implicação (Modus Ponens ou MP)
De uma implicação e seu antecedente (α→β), pode-se concluir seu conseqüente (β).
Ex.: Prove: ¬P → (Q → R), ¬P, Q R
1.
2.
3.
4.
5.

¬P →(Q → R)
¬P
Q
(Q → R)
R

[premissa]
[premissa]
[premissa]
[1,2 MP]
[3,4 MP]

(ii) Eliminação da negação (E ¬)
De uma FBF na forma ¬¬α, pode-se inferir α.
Ex.: Prove: (¬P → ¬¬Q), ¬¬¬P  Q
1.
2.
3.
4.
5.

(¬P → ¬¬Q), [ premissa ]
¬¬¬P
[ premissa ]
(¬P
[ 2 E¬ ]
¬¬Q
[ 1,3 MP ]
Q
[ 4 E¬ ]

(iii) Introdução da Conjunção (I ∧)
De qualquer FBF’s α e β, pode-se inferir (α∧β).

(iv) Eliminação de conjunção ( E∧ )
De uma FBF da forma ( α∧β ) pode-se inferir qualquer elemento da conjunção.
Ex.: Prove: (P → (Q ∧ R)), P (P ∧ Q)
1.
2.
3.
4.
5.

(P → (Q ∧ R))
P
(Q ∧ R)
Q
(P ∧ Q)

[premissa]
[premissa]
[1,2 MP]
[3 E∧]
[2,4 I∧]

(v) Introdução da Disjunção ( I ∨ )
De uma FBF α, pode-se inferir a disjunção de α com qualquer FBF. primeiro ou o segundo elemento da disjunção.
Ex.: PROVE: P  ((P ∨ Q) ∧ (P ∨ R))
1.
2.
3.
4.

P
(P ∨ Q)
(P ∨ R)
(P ∨ Q) ∧

[premissa]
[1, I ∨ ]
[1, I ∨ ]
(P ∨ R)

[2, 3 I∧ ]

α pode ser o

(vi) Eliminação