Logica/Calcolo delle proposizioni/Sistema di Hilbert

Wikibooks, manuali e libri di testo liberi.

Indice

[modifica] Il metodo di Frege-Hilbert

Il primo sistema di dimostrazione che analizziamo è stato proposto in modo formale da Hilbert, ma era già in uso dall' opera di Frege, per cui lo indichiamo con i due nomi.

Il sistema prevede degli assiomi che sono sentenze che riteniamo vere e che possiamo utilizzare liberamente in ogni dimostrazione e delle regole di derivazione.

Si noti come questo sistema ricordi la geometria di Euclide: degli assiomi su cui non si discute e delle regole per derivare da questi nuove verità.

[modifica] Assiomi

Gli assiomi per il calcolo proposizionale nel sistema di Hilbert sono 3:

\Phi \rightarrow \left( \Psi \rightarrow \Phi \right)

\left(\Phi \rightarrow \left( \Psi \rightarrow \Omega \right) \right) \rightarrow \left( \left(\Phi \rightarrow \Psi \right) \rightarrow \left(\Phi \rightarrow \Omega \right) \right)

\left( \neg \Psi \rightarrow \neg \Phi \right) \rightarrow \left( \Phi \rightarrow \Psi \right)

[modifica] Modus Ponens

Il sistema di Hilbert ha una sola regola di inferenza, il modus ponens:

\quad\Phi

{\Phi \rightarrow \Psi} \over \Psi

cioè da \Phi\quad e \Phi \rightarrow \Psi è possibile derivare \Psi\quad.

[modifica] Esempi di dimostrazioni

Dimostriamo che

\Phi \rightarrow \Phi .

− − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − −

1. (\Phi \rightarrow ((\Psi\rightarrow\Phi) \rightarrow \Phi)) \rightarrow ((\Phi \rightarrow (\Psi\rightarrow\Phi)) \rightarrow (\Phi \rightarrow \Phi))  : Assioma 2 con \Phi\quad al posto di \Omega\quad e \Psi \rightarrow \Phi al posto di \Psi\quad

2. (\Phi \rightarrow ((\Psi \rightarrow \Phi)\rightarrow \Phi))  : Assioma 1 con \Psi \rightarrow \Phi al posto di \Psi\quad

3. (\Phi \rightarrow (\Psi \rightarrow \Phi)) \rightarrow (\Phi \rightarrow \Phi)  : Modus ponens tra 1 e 2

4. (\Phi \rightarrow (\Psi \rightarrow \Phi))  : Assioma 1

5. \Phi \rightarrow \Phi  : Modus ponens tra 3 e 4


Dimostriamo che

\Phi \rightarrow \Psi, \Psi \rightarrow \Omega \vdash \Phi \rightarrow \Omega .

− − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − − −

1. \Phi\quad : Ipotesi

2. \Phi \rightarrow \Psi : Ipotesi

3. \Psi\quad : Modus ponens tra 1 e 2

4. \Psi \rightarrow \Omega : Ipotesi

5. \Omega\quad : Modus ponens tra 4 e 3

così abbiamo dimostrato che

\Phi, \Phi \rightarrow \Psi, \Psi \rightarrow \Omega \vdash \Omega

applicando il teorema di deduzione (\Phi \vdash \Omega) \rightarrow (\vdash \Phi \rightarrow \Omega) otteniamo il risultato voluto, eliminando \Phi\quad dalle ipotesi che abbiamo utilizzato.

[modifica] Moduls Tollens

Il modus tollens e un'altra possibile regola di inferenza:

\neg\Psi

{\Phi \rightarrow \Psi} \over {\neg\Phi}


cioè da \neg\Psi e \Phi \rightarrow \Psi è possibile derivare \neg\Phi.

[modifica] L' assioma di Meredith

Un logico Irlandese, Carew Meredith, nel 1953 ha proposto un singolo assioma che può sostituire i tre assiomi che abbiamo utilizzato finora.

L' assioma e':

(((((\Phi \rightarrow \Psi) \rightarrow (\neg \chi \rightarrow \neg \Omega)) \rightarrow \chi) \rightarrow \tau) \rightarrow ((\tau \rightarrow \Phi) \rightarrow (\Omega \rightarrow \Phi)))

i logici credono, ma non è ancora stato provato, che questa sia la singola formula più corta possibile da cui può essere derivato l' intero calcolo delle proposizioni basato su implicazione e negazione e con la sola regola deduttiva del modus ponens.

Ricavato da "http://it.wikibooks.org/wiki/Logica/Calcolo_delle_proposizioni/Sistema_di_Hilbert"
Strumenti personali