Logica matematica/Calcolo delle proposizioni/La deduzione naturale: differenze tra le versioni
m User-controlled Bot: table syntax updated |
|||
Riga 17: | Riga 17: | ||
Vediamo quindi le regole: |
Vediamo quindi le regole: |
||
⚫ | |||
<tr> |
|||
⚫ | |||
<td> |
|||
|----- |
|||
| |
|||
<math>{\Phi \quad\Psi} \over {\Phi \wedge \Psi}</math> |
<math>{\Phi \quad\Psi} \over {\Phi \wedge \Psi}</math> |
||
|
|| |
|||
</td> |
|||
<td> |
|||
</td> |
|||
<td> |
|||
Introduzione di <math>\wedge</math> |
Introduzione di <math>\wedge</math> |
||
| |
|||
</td> |
|||
<td> |
|||
<math>{\Phi \wedge \Psi} \over \Phi</math> |
<math>{\Phi \wedge \Psi} \over \Phi</math> |
||
| |
|||
</td> |
|||
<td> |
|||
<math>{\Phi \wedge \Psi} \over \Psi</math> |
<math>{\Phi \wedge \Psi} \over \Psi</math> |
||
| |
|||
</td> |
|||
<td> |
|||
Eliminazione di <math>\wedge</math> |
Eliminazione di <math>\wedge</math> |
||
|----- |
|||
</td> |
|||
| |
|||
</tr> |
|||
<tr> |
|||
<td> |
|||
<math>\Phi \over {\Phi \vee \Psi}</math> |
<math>\Phi \over {\Phi \vee \Psi}</math> |
||
| |
|||
</td> |
|||
<td> |
|||
<math>\Psi \over {\Phi \vee \Psi}</math> |
<math>\Psi \over {\Phi \vee \Psi}</math> |
||
| |
|||
</td> |
|||
<td> |
|||
Introduzione di <math>\vee</math> |
Introduzione di <math>\vee</math> |
||
| |
|||
</td> |
|||
<td> |
|||
<math>{\Phi \vee \Psi \quad {\stackrel{(\Phi)}{\chi}}{\stackrel{(\Psi)}{\chi}}} \over \chi</math> |
<math>{\Phi \vee \Psi \quad {\stackrel{(\Phi)}{\chi}}{\stackrel{(\Psi)}{\chi}}} \over \chi</math> |
||
|
|| |
|||
</td> |
|||
⚫ | |||
|----- |
|||
<td></td> |
|||
| |
|||
<td> |
|||
⚫ | |||
</td> |
|||
</tr> |
|||
<tr> |
|||
<td> |
|||
<math>\stackrel{(\Phi)}{\Psi} \over {\Phi \rightarrow \Psi}</math> |
<math>\stackrel{(\Phi)}{\Psi} \over {\Phi \rightarrow \Psi}</math> |
||
|
|| |
|||
</td> |
|||
<td> |
|||
</td> |
|||
<td> |
|||
Introduzione di <math>\rightarrow</math> |
Introduzione di <math>\rightarrow</math> |
||
| |
|||
</td> |
|||
<td> |
|||
<math>{\Phi \quad \Phi \rightarrow \Psi} \over \Psi</math> |
<math>{\Phi \quad \Phi \rightarrow \Psi} \over \Psi</math> |
||
|
|| |
|||
</td> |
|||
⚫ | |||
|} |
|||
<td></td> |
|||
<td> |
|||
⚫ | |||
</td> |
|||
</tr> |
|||
</table> |
|||
Vediamo come si utilizza questo schema prendendo come esempio la prima regola. |
Vediamo come si utilizza questo schema prendendo come esempio la prima regola. |
Versione delle 18:30, 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 |
Vediamo come si utilizza questo schema prendendo come esempio la prima regola. Questa ci dice che se abbiamo una dimostrazione di e una dimostrazione di (la riga sopra la barra orizzontale) possiamo derivare la frase che è da considerarsi dimostrata. La regola si può anche utilizzare in senso inverso, se devo dimostrare la congiunzione (frase sotto la riga orizzontale) devo procurarmi una dimostrazione delle due sentenze che la compongono (frasi sopra la riga).