Differenze tra le versioni di "Logica intuizionista"

m (segnalazione stub)
==Logica intuizionistica come calcolo formale e logico==
 
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 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 una delle leggi 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.
 
Osservare che molte tautologie classicamente valide non sono teoremi della logica intuizionista indebolisce la teoria della dimostrazione della logica classica. Gerhard Gentzen ottenne una versione più debole del suo calcolo dei sequenti (LK), noto come LJ, che è una teoria intuizionisticamente sostenibile.
 
La semantica intuizionista è più complicata della semantica classica. Una teoria dei modelli può essere rappresentata dall'algebra di Heyting o dalla semantica di Kripke.
 
[[Categoria:Logica]]
73

contributi