Logica matematica/Calcolo delle proposizioni/La deduzione naturale: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
Nessun oggetto della modifica |
|||
Riga 14: | Riga 14: | ||
Per ogni connettivo sono specificate delle regole di inferenza che permettono di introdurre o eliminare una operazione logica nel corso della dimostrazione. |
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: |
|||
<math>\Phi \quad\quad \Psi</math> |
|||
<math>----------------</math> |
|||
<math>\Phi \wedge \Psi</math> |
Versione delle 18:57, 18 nov 2007
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: