Logica matematica/Calcolo delle proposizioni/La deduzione naturale

La deduzione naturale

Gerhard Gentzen ha notato che il sistema assiomatico di Hilbert è molto lontano da modo di ragionare che applicano i matematici nella loro attività quotidiana.

Riasalire agli assiomi o partire dagli assiomi non è semplice e spesso è molto poco intuitivo, in fondo l' unico esempio significativo di nteoria assiomatica che ci è giunta da tempi lontani è la geometria di Euclide.

Gentzen ha cercato un sistema di dimostrazione che fosse semplice ed intuitivo, arrivando alla "deduzione naturale", un sistema di dimostrazione senza assiomi e con 7 regole.

Le regole

Per ogni connettivo sono specificate delle regole di inferenza che permettono di introdurre o eliminare una operazione logica nel corso della dimostrazione.

Vediamo quindi le regole:

${\Phi \quad \Psi } \over {\Phi \wedge \Psi }$		Introduzione di $\wedge$	${\Phi \wedge \Psi } \over \Phi$	${\Phi \wedge \Psi } \over \Psi$	Eliminazione di $\wedge$
$\Phi \over {\Phi \vee \Psi }$	$\Psi \over {\Phi \vee \Psi }$	Introduzione di $\vee$	${\Phi \vee \Psi \quad {\stackrel {(\Phi )}{\chi }}{\stackrel {(\Psi )}{\chi }}} \over \chi$		Eliminazione di $\vee$
${\stackrel {(\Phi )}{\Psi }} \over {\Phi \rightarrow \Psi }$		Introduzione di $\rightarrow$	${\Phi \quad \Phi \rightarrow \Psi } \over \Psi$		Eliminazione di $\rightarrow$