Teoria de la Prova: Deducció Natural de Gentzen

A les seccions anteriors s'han utilitzat tècniques que estudien la correcció dels raonaments en base al significat de les fórmules que contenen. Aquest conjunto de tècniques s'engloben en el que s'anomena teoria semàntica. Pel contrari, existeix altre conjunt de tècniques, conegut com a teoria de la prova, que prescindeix dels possibles valors de les fórmules i es centra únicament en la manipulació sintàctica de fórmules. Existeixen diversos estils com el sistema de Hilbert, la deducció natural, etc. Tots ells utilitzen un conjunt d'axiomes i un seguit de regles d'inferència que permeten obtenir teoremes a partir d'aquests axiomes o d'altres teoremes prèviament derivats.

En aquesta secció es presenta l'estil de deducció natural, desenvolupat per Gentzen el 1935 i que té per principal objectiu oferir un sistema que s'aproximi a les tècniques de demostració habituals. La deducció natural no conté axiomes i ofereix un seguit de regles d'inferència per a cada tipus de connectiva. Les regles d'inferència es mostren a continuació:

Regles d'introducció (I)

  1. A i B ⇒ (A ∧ B)
  2. A ⇒ (A ∨ B) i B ⇒ (A ∨ B)
  3. Deducció: de A es dedueix B ⇒ (A → B)
  4. Si A aleshores B i si B aleshores A ⇒ (A ↔ B)
  5. Demostració per contradicció: Si de A es dedueix B i no B ⇒ ¬A
  6. Medi exclòs: A o no A és sempre Veritat: (A ∨ ¬A) ≡ V
  7. Contradicció: A i no A és sempre F: (A ∧ ¬A) ≡ F

Regles d'eliminació (E)

  1. (A ∧ B) ⇒ A i (A ∧ B) ⇒ B
  2. Prova per casos: (A ∨ B) i (A → C) i (B → C) ⇒ C
  3. Modus ponens: A i (A → B ⇒ B
  4. Modus tollens: ¬B i (A → B) ⇒ ¬A
  5. (A ↔ B) ⇒ (A → B) i (B → A)
  6. Demostració per contradicció: Si de no A es dedueix B i no B ⇒ A
  7. V ⇒ (A ∨ ¬A)
  8. F ⇒ A

Exemple

▪ Demostrar que p ∧ q → q ∧ p

Per l'estudi de raonaments de la forma {P1, P2, ··· , Pn} ⇒ Q partim de les premisses i s'intenta arribar a la conclusió.

Exemple

▪ Demostrar que p ∧ q → p ∧ (q ∨ r)

La utilització de quadres permet visualitzar la idea de proves subordinades. En una prova subordinada, es realitza un supòsit i, un cop en tenim el resultat, es descarta el supòsit (es tanca el quadre) obtenint un resultat lliure de supòsits. Un exemple n'és la regla de deducció (I-3).

Exemples

▪ Demostrar que p → (q → r) ⇒ (p ∧ q) → r

▪ Demostrar que (p ∧ q) → r ⇒ p → (q → r)

▪ Demostrar que ¬p ⇒ p → q

▪ Demostrar que p ↔ ¬¬p

▪ Demostrar que ¬p ∨ q ⇒ p → q

▪ Demostrar que p → q ⇒ ¬p ∨ q