Logica matematica/Calcolo delle proposizioni/La deduzione naturale: differenze tra le versioni
Riga 57: | Riga 57: | ||
<td> |
<td> |
||
<math>{\Phi \vee \Psi \quad \chi} \over \chi</math> |
<math>{\Phi \vee \Psi \quad {\stackrel{(\Phi)}{\chi}}{\stackrel{(\Psi)}{\chi}}} \over \chi</math> |
||
</td> |
</td> |
||
Riga 65: | Riga 65: | ||
</td> |
</td> |
||
</tr> |
</tr> |
||
<tr> |
|||
<td> |
|||
<math>\stackrel{(\Phi)}{\Psi} \over {\Phi \rightarrow \Psi}</math> |
|||
</td> |
|||
<td> |
|||
</td> |
|||
<td> |
|||
Introduzione di <math>\rightarrow</math> |
|||
</td> |
|||
<td> |
|||
<math>{\Phi \quad \Phi \rightarrow \Psi} \over \Psi</math> |
|||
</td> |
|||
<td></td> |
|||
<td> |
|||
Eliminazione di <math>\rightarrow</math> |
|||
</td> |
|||
</tr> |
|||
Versione delle 19:24, 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:
|
Introduzione di |
|
|
Eliminazione di |
|
|
|
Introduzione di |
|
Eliminazione di |
|
|
Introduzione di |
|
Eliminazione di |