Logica intuizionista: differenze tra le versioni

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 [[filosofia|filosofici]] dell'intuizionismo, esso mostra delle proprietà piuttosto utili nella pratica [[scienza|scientifica]].

Nella logica intuizionista sono rifiutati passi [[epistemologia|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, lail leggeprincipio del terzo escluso (''[[Tertium non datur]]'', vedi anche [[principio di bivalenza]]: <math>A \vee \neg A</math>); questo principio è rigettato dalla logica intuizinistaintuizionista perché, in un linguaggio che permetta tale formula, è possibile concludere che (<math>P \vee \neg P</math>) 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. L'assuntoLa 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 [[premessa|premesse]] alle conclusioni, bensì la ''giustificabilità''.

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

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 una delle [[legge di De Morgan|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 [[Arend Heyting]] o dalla semantica di [[Saul Kripke]].