Logica intuizionista: differenze tra le versioni

Da un punto di vista pratico, c'è un buon motivo per usare la logica intuizionista. Nella [[programmazione]], infatti, delle mere asserzioni di [[esistenza]] sono poco interessanti. Un programma per [[computer]] è compilato per fornire una risposta, non per affermare che ne esiste (o non ne esiste) una. Sarebbe infatti strano che un sistema fornisse una dimostrazione per ∃''x''P(''x'') ma non potesse provare P(''b'') per qualsiasi ''b'' che non sia una variabile libera.

 

 

Un altro esempio di una tautologia classica rifiutata dalla logica intuizionista riguarda l'eliminazione della [[doppia negazione]]. Nella logica classica, sia P → ¬¬P che ¬¬P → P sono teoremi. La logica intuizionista accetta solo il primo: la doppia negazione può essere introdotta ma non eliminata. Questo perché la nozione intuizionista di negazione è differente dal suo equivalente classico. Se la logica classica intende ¬P come 'P è falso', nella logica intuizionista ¬P afferma che esiste una dimostrazione che provi l'inesistenza di una dimostrazione di P. L'asimmetria tra le due implicazioni è evidente. Se P è dimostrabile, allora è certamente impossibile provare che non esiste una dimostrazione di P (introduzione della doppia negazione); ma l'eliminazione della doppia negazione è intuizionisticamente insostenibile: se non c'è una dimostrazione che non esiste una dimostrazione di P, non è possibile concludere che esista una dimostrazione di P. Tuttavia è possibile dimostrare una versione più debole dell'eliminazione della doppia negazione tale che da ¬¬¬P si concluda ¬P.