Differenze tra le versioni di "Logica intuizionista"

m
(wiificazione)
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.
 
Una formalizzazione rigorosa della logica intuiziosta richiede una [[teoria dei modelli]] ed una teoria della dimostrazione adeguate. La [[sintassi]] delle formule intuizioniste è simile alla [[logica proposizionale]] (o del primo ordine). Naturalmente molte [[tautologia|tautologie]] della logica classica non possono più esser dimostrate nell'intuizionismo; non solo il principio del terzo escluso, ma anche la [[legge di Peirce]] ed unauno delledei [[legge di De Morgan|leggiteoremi di De Morgan]].
 
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.
7 985

contributi