Deduzione naturale

La tabella di verità, gli algoritmi di Davis e Stålmarck non danno spiegazioni perché una formula è una tautologia. La deduzione naturale è un modo per costruire tautologie. Per tale costruzione, per ogni operatore ci sono delle regole per creare l'operatore (Introduzione) e delle regole per usare l'operatore (Eliminazione).

Congiunzione

Introduzione

A B A ∧ B

Eliminazione

A ∧ B A

A ∧ B B

Esempio

A ∧ B B A ∧ B A B ∧ A

Disgiunzione

Introduzione

A A ∨ B

B A ∨ B

Eliminazione

A ∨ B [A] . . C [B] . . C C

Esempio

A ∨ B A B ∨ A B B ∨ A B ∨ A

Implicazione

Introduzione

[A] . . B A ⇒ B

Eliminazione

A ⇒ B A B

Esempio

A ⇒ B A B B ⇒ C C A ⇒ C (B ⇒ C) ⇒ (A ⇒ C) (A ⇒ B) ⇒ (B ⇒ C) ⇒ (A ⇒ C)

Tutte le ipotesi della prova sono state introdotte dalla regola d'introduzione. Dunque la conclusione è una tautologia.

Equivalenze

Introduzione

[A] . . B [B] . . A A ≡ B

Eliminazione

A ≡ B A [B] . . C C A ≡ B B [A] . . C C

Esempio

A ≡ B B A A A ≡ B A B B B ≡ A B ≡ A A B B B ≡ A B A A A ≡ B (A ≡ B) ≡ (B ≡ A)

Falso

Eliminazione

False A

Negazione

Introduzione

[A] . . False ¬A

Eliminazione

A ¬A False

Esempio

(A ∨ ¬B) ∧ B A ∨ ¬B A (A ∨ ¬B) ∧ B B ¬B False A A ((A ∨ ¬B) ∧ B) ⇒ A

Esercizi

E1. Trovare una prova di ((A ∨ B) ⇒ C) ≡ ((A ⇒ C) ∧ (B ⇒ C)).

E2. Trovare una prova di (A ⇒ B) ⇒ (B ⇒ A).

E3. Trovare una prova di A ⇒ ¬¬A.

E4*. Trovare una prova di A ⇒ (A ∧A).

E5*. Trovare una prova di ((A ∨ B) ∧ (A ⇒ B)) ⇒ B.

E6*. Trovare una prova di (A ∨ B) ⇒ ((A ⇒ C) ⇒ ((B ⇒ C) ⇒ C)).

E7*. Trovare una prova di ((A ∧ B) ∧ C) ⇒ (A ∧ (B ∧ C)).

E8*. Trovare una prova di ((A ⇒ C) ∧ (B ⇒ C)) ⇒ ((A ∨ B) ⇒ C).

E9*. Trovare una prova di ((A ∨ B) ∧ (A ∨ ¬B)) ⇒ A.

E10*. Trovare una prova di ((A ∨ ¬B) ∧ B) ⇒ A.

E11*. Trovare una prova di ((A ⇒ B) ∧ (B ⇒ ¬A)) ⇒ ¬A.

E12*. Trovare una prova di ((A ⇒ ¬B) ∧ B) ⇒ ¬A.

Logica classica

Con le regole precedenti non abbiamo la logica usuale. Per avere tale logica, occorre che A ∨ ¬A sia vero per ogni formula A. Si cambia la regola :

False A

con:

[¬A] . . False A

Esempio

Adesso è possibile provare A ∨ ¬A:

¬A A ∨ ¬A ¬ (A ∨ ¬A) False A A A ∨ ¬A ¬ (A ∨ ¬A) False ¬A False A ∨ ¬A

Esercizi

E13. Trovare una prova di ¬¬A ⇒ A.

E14. Trovare una prova di ((A ⇒ B) ⇒ A) ⇒ A.

E15. Trovare una prova di ((A ⇒ B) ∨ C) ⇒ ((A ⇒ C) ∨ B).

Laurent Théry

Last modified: Tue Apr 30 01:38:21 MEST 2002