Logica intuizionista

La logica intuizionista, o logica costruttiva, è la logica dell'intuizionismo matematico e di altre forme di costruttivismo matematico.

Secondo la prospettiva intuizionista, la logica e la matematica sono le applicazioni di metodi internamente coerenti per la realizzazione di costrutti mentali di complessità crescente. La logica intuizionista si propone come una rigorosa e formale logica matematica. Benché non sia chiaro se un calcolo logico formale esaurisca gli aspetti più spiccatamente filosofici dell'intuizionismo, esso mostra delle proprietà piuttosto utili nella pratica scientifica.

Logica intuizionistica come paradigma del ragionamento logico

Nella logica intuizionista sono rifiutati passi epistemologicamente inadeguati nelle dimostrazioni. Nella logica classica, un asserto A significa che "A è vero". Nell'intuizionismo, una tale formula è considerata vera nel solo caso in cui se ne possa esibire una dimostrazione. Un'esempio di questa differenza è, ad esempio, il principio del terzo escluso (Tertium non datur, vedi anche principio di bivalenza: $A\vee \neg A$); questo principio è rigettato dalla logica intuizionista perché, in un linguaggio che permetta tale formula, è possibile concludere che ($P\vee \neg P$) senza che sia chiaro se P sia vero o falso. Nella logica intuizionista, il principio del terzo escluso significa soltanto che almeno uno tra P e ¬P può essere dimostrato; una formulazione più forte del corrispettivo classico, che considera vera la sola disgiunzione. La tesi fondamentale è che la validità di un costrutto mentale dipenda dalla sola coerenza dell'asserto nel contesto. La logica intuizionista sostituisce la nozione di verità con quella di giustificazione nel suo calcolo logico. Una dimostrazione corretta non preserva dunque la validità nel passaggio dalle premesse alle conclusioni, bensì la giustificabilità.

La logica intuizionista ha dato supporto filosofico a diverse scuole filosofiche, tra cui l'antirealismo di Michael Dummett.

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 ∃xP(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 uno dei teoremi 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 Arend Heyting o dalla semantica di Saul Kripke.