logica intuizionista
logica intuizionista
La più studiata rivale della logica classica sin da quando fu assiomatizzata da Arend Heyting nel 1930. Già Anchei M. Kolmogorov nel 1925 e Vasili I. Glivenko nel 1929 avevano cercato di codificare in un calcolo logico analogo a quello di David Hilbert e Wilhelm Ackemann per la logica classica i principi logici e le regole valide dal punto di vista brouweriano. L’idea base era l’interpretazione dei connettivi e dei quantificatori in termini di costruzioni che realizzano la verità di enunciati. Di qui la lettura di A→B in termini di esistenza di una costruzione che – data una qualsiasi costruzione d che realizza A – dà una costruzione d′ che realizza B o di ∀xA in termini di una costruzione che per ogni a dell’universo del discorso fornisce una costruzione che realizza A(a). Se – come proposto da Luifren Brouwer – interpretiamo ←A come A→⊥, dove ⊥ è la proposizione assurda (che nessuna costruzione può realizzare), si vede immediatamente come il terzo escluso A∨←A risulti falso o come sia falsificabile una formula quale ←∃x←A→∀xA. L’assiomatizzazione HI data da Heyting si ottiene quindi da quella per la logica classica semplicemente eliminando alcuni assiomi validi classicamente. I connettivi ∧,∨,→ risultano non definibili l’uno con gli altri come pure i quantificatori ∀,∃. Nel 1932, Kurt Gödel dimostra che il calcolo intuizionista non ha matrice caratteristica finita (non ha cioè una matrice finita che renda veri tutti e soli i teoremi) e nel 1936 Stanislaw Jaskowski dimostra che è possibile refutare ogni non teorema utilizzando una matrice finita. Questo garantisce la decidibilità della logica proposizionale intuizionista. Negli stessi anni Gerard Gentzen introduce un nuovo tipo di calcoli logici – i cosiddetti calcoli di sequenti LK e LJ, rispettivamente per la logica classica e intuizionista – che rendono molto più facile confrontare dimostrazioni classiche e intuizioniste, ottenendo oltre alla decidibilità proposizionale un risultato già provato da Gödel per cui se si traducono nel modo ovvio i connettivi in termini di ∧ e ← tutti i teoremi della logica classica – letti in questo modo – saranno teoremi anche di quella intuizionista. Il risultato estende un teorema di Glivenko per cui ogni teorema classico negativo ←A è teorema intuizionista. I calcoli di Gentzen sono risultati preziosi per lo studio dal punto di vista della teoria della dimostrazione delle numerose assiomatizzazioni di specifici settori della matematica intuizionista (teoria dei numeri, teoria delle successioni di libera scelta, teoria delle specie ecc.). Un passo decisivo sul piano dell’elaborazione semantica lo compie nel 1935 Alfred Tarski che prova che i teoremi proposizionali di HI coincidono con le formule vere (che hanno cioè come valore l’insieme massimo) in ogni valutazione v che assegna a ogni formula A un insieme v(A) nel reticolo O(T) degli aperti di uno spazio topologico, dove ∧ corrisponde all’intersezione, ∨ all’unione, ← all’interno del complemento. Le algebre di aperti sono reticoli relativamente pseudo complementati (noti oggi come algebre di Heyting) e poiché – come provato da Marshal Stone – ogni algebra di Heyting è isomorfa a un reticolo di aperti, i teoremi proposizionali di HI sono le formule vere in ogni interpretazione in algebre di Heyting. Con le tecniche introdotte da Tarski si possono dimostrare molte proprietà significative di HI, per es., che esso è interpretabile nel sistema modale S4 di Clarence I. Lewis dove ogni atomica A si legga come LA (L è il connettivo ‘è necessario che’), ∧ e ∨ siano tradotte letteralmente e (A→B) come L(A→B). Una svolta decisiva nello studio della semantica della logica intuizionista si è avuta negli anni Sessanta per opera di Saul Kripke che – sfruttando il fatto che ogni algebra di Heyting è isomorfa all’algebra dei coni su un albero – ha mostrato come essa si possa interpretare su alberi dove ogni vertice costituisce uno stato di conoscenze e il passaggio da un vertice a uno successivo nell’albero rappresenta un aumento di conoscenza. In quest’ottica affermare al livello j che A→B è vera significa affermare che per ogni livello successivo i>j non si potrà avere A e ¬B. Stesso discorso per ← e ∀. Nuovi orizzonti – all’interno della matematica classica – si sono aperti infine per le applicazioni della logica intuizionista quando in seguito ai lavori di F. William Lawvere si è verificato che essa è la logica opportuna una volta che si interpretino le formule (anche di linguaggi di ordine superiore) in categorie di prefasci o fasci e quindi in topoi generali.