La seconda rivoluzione scientifica: matematica e logica. L'intuizionismo di Brouwer

Storia della Scienza (2004)

La seconda rivoluzione scientifica: matematica e logica. L'intuizionismo di Brouwer

Anne L. Troelstra

L'intuizionismo di Brouwer

Nella dissertazione Over de Grondslagen der Wiskunde (I fondamenti della scienza, 1907) il matematico olandese Luitzen Egbertus Jan Brouwer (1881-1966) difese, in maniera più radicale e decisa dei semiintuizionisti, la concezione intuizionista della matematica. La filosofia della matematica di Brouwer è inserita in un sistema filosofico generale, ai punti essenziali del quale egli restò fedele per tutta la vita. Rispetto alla matematica i concetti fondamentali espressi da Brouwer sono i seguenti:

a) la matematica non è formale; i suoi oggetti sono costruzioni mentali del matematico ideale. Soltanto le costruzioni pensate dal matematico ideale sono esatte;

b) la matematica è indipendente dall'esperienza del mondo esterno e, in linea di principio, anche dal linguaggio. La comunicazione mediante il linguaggio può servire a suggerire ad altri costruzioni di pensiero analoghe alle proprie, ma non c'è alcuna garanzia che tali altre costruzioni siano le stesse. Questo è un elemento solipsistico nella filosofia di Brouwer;

c) la matematica non dipende dalla logica; per contro, la logica è una componente della matematica.

Questi concetti condussero a un programma di ricostruzione della matematica basato su principî intuizionisti (il cosiddetto programma di Brouwer).

Nella fase iniziale, negli anni compresi grosso modo fra il 1907 e il 1913, Brouwer fu prevalentemente impegnato a realizzare la parte principale della sua opera nel campo della topologia (classica) e si dedicò in maniera assai limitata al proprio programma. In questi anni la sua visione del continuo e degli insiemi numerabili era molto simile a quella di Borel; egli scrive infatti: "Il continuo come totalità ci è dato intuitivamente; una costruzione del continuo, un atto che sia capace di creare 'tutte' le sue parti così come sono individualizzate dall'intuizione matematica è impensabile e impossibile. L'intuizione matematica non è in grado di creare altro che quantità numerabili in maniera individualizzata" (Brouwer 1907, p. 62).

D'altra parte appaiono sin da questa prima fase evidenti le differenze tra le concezioni dei due matematici. Brouwer non seguì Borel nel suo intersoggettivismo pragmatico e cercò di spiegare i numeri naturali e il continuo come due aspetti di una singola intuizione ('l'intuizione primigenia').

Un'altra differenza importante consiste nel fatto che Brouwer, subito dopo avere completato la propria tesi, si rese conto che la logica classica non poteva essere applicata alla sua matematica; nondimeno fino al 1913 ca. egli condivise alcune delle idee dei semiintuizionisti, dai quali non si dissociò pubblicamente.

Controesempi deboli e soggetto creativo

Brouwer introdusse sin dal 1908 un genere di controesempio tipicamente intuizionista rispetto a determinate asserzioni della matematica classica: non controesempi in senso stretto, tali cioè da provare una contraddizione nell'asserzione A, bensì esempi i quali mostravano che, assumendo la possibilità di dimostrare A intuizionisticamente, si sarebbe pervenuti a una soluzione per un problema irrisolto. L'eccessiva attenzione nei confronti di tali esempi ha spesso suscitato tra i non intuizionisti l'impressione erronea che l'intuizionismo fosse sostanzialmente un'attività negativa volta a criticare la matematica classica.

Un tipico caso di controesempio debole è il seguente: si consideri l'insieme X≡{x:x=1⋁(x=2∧F)} dove F è una asserzione matematica ancora non dimostrata, come l'ipotesi di Riemann. X è un sottoinsieme dell'insieme finito {1, 2}, ma non possiamo provare che X è finito, poiché ciò ci costringerebbe a decidere se X abbia uno oppure due elementi e per questo dovremmo dimostrare F (intuizionisticamente un insieme è finito se può essere costruttivamente posto in corrispondenza biunivoca con una parte iniziale dei numeri naturali). Abbiamo così trovato un controesempio debole all'asserzione 'un sottoinsieme di un insieme finito è finito'.

Scegliendo in modo opportuno i problemi irrisolti è anche possibile fornire un controesempio debole all'enunciato: 'per ogni numero reale x, x⟨0 oppure x=0 oppure x>0'. Brouwer utilizzò questi esempi per mostrare la necessità di una revisione intuizionista di molti concetti matematici e per dimostrare quanto definizioni equivalenti nella matematica classica corrispondessero invece a nozioni intuizioniste distinte.

George F.C. Griss, in una serie di pubblicazioni edite tra il 1944 e il 1955, promosse una forma di matematica intuizionista senza negazione, sostenendo che non si può avere una concezione chiara di cosa significhi fornire la dimostrazione di una proposizione che si riveli contraddittoria.

In risposta a Griss, nel 1948 Brouwer pubblicò un esempio di asserzione in forma di negazione che non era possibile sostituire con un'asserzione positiva. L'esempio di Brouwer considerava un numero reale definito da un esplicito riferimento ai vari livelli nell'attività del matematico ideale che cerca di dimostrare un'asserzione A ancora irrisolta. Una componente essenziale dell'argomentazione di Brouwer è che il matematico ideale (il 'soggetto creativo', secondo la sua terminologia) è certo che a nessun livello futuro della sua attività matematica troverà che A è vera; ciò significa che egli sa che è vera ¬A (Brouwer utilizzava esempi di questo genere nelle sue conferenze sin dal 1927).

L'argomentazione illustra le estreme conseguenze solipsistiche dell'intuizionismo di Brouwer. A causa dell'effetto da essi suscitato nel dibattito filosofico questi esempi generarono una notevole quantità di discussioni e stimolarono alcune ricerche metamatematiche, ma la loro influenza sul programma di Brouwer risultò molto limitata, sostanzialmente nulla.

Il programma di Brouwer

Dopo il 1912, anno in cui ricevette un incarico come professore presso l'Università di Amsterdam, Brouwer iniziò con impegno a lavorare al suo programma e ben presto scoprì che, perché la ricostruzione dell'analisi fosse efficace, era necessario che egli rivedesse le sue idee sul continuo. Intorno al 1913 Brouwer si rese conto che la nozione di sequenza di scelta (che compare in un contesto piuttosto diverso nella discussione di Borel sull'assioma di scelta) poteva essere legittimata dal suo punto di vista offrendo tutti i vantaggi di una 'teoria aritmetica' del continuo. Il primo scritto di Brouwer in cui tale nozione viene effettivamente utilizzata è del 1919.

A partire dal 1928 egli ricostruì alcune parti della teoria della topologia generale nonché della teoria delle funzioni, sviluppò inoltre una teoria dei buoni ordinamenti numerabili e, insieme al suo studente Barend de Loor, fornì una dimostrazione intuizionista del teorema fondamentale dell'algebra. Le idee di Brouwer cominciarono a essere più ampiamente conosciute soltanto dopo il 1920, quando egli tenne una serie di conferenze in molte sedi diverse, soprattutto in Germania.

Successivamente al 1928 la sua attività matematica si ridusse moltissimo, presumibilmente a causa di un conflitto insorto nel comitato editoriale dei "Mathematische Annalen". A partire dal 1923 proseguirono il programma di Brouwer Maurits Joost Belinfante (1896-1944) e Arend Heyting (1898-1980) e, in seguito, anche gli allievi di quest'ultimo. Belinfante indagò negli anni Trenta la teoria intuizionista delle funzioni complesse; Heyting si occupò di geometria proiettiva intuizionista e di algebra (in particolare di algebra lineare e teoria dell'eliminazione). Tra il 1952 e il 1967 sei degli studenti di dottorato di Heyting scrissero, da un punto di vista intuizionista, tesi su argomenti quali la topologia, la teoria della misura, la teoria degli spazi di Hilbert, l'integrale di Radon e la geometria affine. Dopo il 1974 interessanti contributi sono stati forniti da Willem H.M. Veldman, che ha studiato fra l'altro la gerarchia analitica intuizionista.

La scoperta, negli anni Trenta, di una nozione precisa di algoritmo ‒ la nozione di funzione ricorsiva (generale), risultato del lavoro di Alonzo Church, Kurt Gödel, Jacques Herbrand, Alan M. Turing e Stephen C. Kleene ‒ non influì sull'intuizionismo; ciò tuttavia non deve sorprendere, in quanto la maggior parte di queste caratterizzazioni descrive algoritmi specificando un linguaggio ristretto nel quale possono essere espressi, e ciò è assolutamente estraneo alla visione di Brouwer della matematica come attività non linguistica del matematico ideale. L'analisi di Turing non è legata a uno specifico formalismo, tuttavia per la generalità della sua nozione di algoritmo egli basa le sue argomentazioni informali sulla manipolazione di simboli e considera le limitazioni fisiche del calcolo; tali idee non concordano con quelle di Brouwer sulla matematica come 'libera creazione'.

Senza gli sforzi prolungati compiuti da Heyting per spiegare e divulgare le idee di Brouwer, l'interesse per l'intuizionismo avrebbe potuto esaurirsi negli anni Trenta; ma, a dispetto degli intenti dello stesso Heyting, tale interesse si rivolgeva più alla metamatematica dell'intuizionismo che non al programma di Brouwer. Fu solo con la pubblicazione della sua monografia (Heyting 1956), che Heyting riuscì a suscitare uno studio più attento della matematica intuizionista.

Logica e aritmetica intuizioniste

All'epoca della propria dissertazione Brouwer non si era ancora reso conto del fatto che il suo approccio alla matematica rendeva necessario rivedere i principî della logica classica ma, nel 1908, egli comprese chiaramente che l'intuizionismo richiedeva una logica differente. In particolare, Brouwer sottolineò che il principio del terzo escluso non era intuizionisticamente valido. In maniera implicita, naturalmente, il significato degli operatori logici era stato adattato al contesto intuizionista e quindi il significato intuizionista di un'asserzione della forma A⋁¬A è diverso da quello classico.

Un primo significativo contributo tecnico alla logica intuizionista consiste nell'osservazione che ¬¬¬A→¬A è una legge intuizionisticamente valida.

L'interpretazione Brouwer-Heyting-Kolmogorov

Nella logica intuizionista l'interpretazione informale standard degli operatori logici è la cosiddetta interpretazione di Brouwer-Heyting-Kolmogorov (detta in breve BHK). La formalizzazione della logica intuizionista prese avvio prima che tale interpretazione venisse effettivamente formulata, ma in questa sede è preferibile dare la precedenza all'interpretazione BHK, perché in tal modo si agevola la comprensione dei risultati più tecnici. Nell'interpretazione BHK il significato di un'asserzione A è dato dalla spiegazione di ciò che costituisce una dimostrazione di A e la dimostrazione di A per A logicamente composta è spiegata in termini di ciò che significa fornire una dimostrazione dei suoi costituenti. Dunque, per la logica proposizionale:

1)una dimostrazione di AB è data presentando una dimostrazione di A e una dimostrazione di B;

2)una dimostrazione di AB è data presentando una dimostrazione di A o una dimostrazione di B;

3)una dimostrazione di AB è una costruzione che trasforma qualsiasi dimostrazione di A in dimostrazione di B;

4)l'assurdità ⊥ ('la contraddizione') non ha dimostrazione; una dimostrazione di ¬A è una costruzione che trasforma qualsiasi dimostrazione ipotizzata di A in dimostrazione di ⊥.

Una tale interpretazione è implicita negli scritti di Brouwer e fu esplicitata da Heyting per la logica predicativa (Heyting 1934) e da Andrej Nikolaevič Kolmogorov (Kolmogorov 1932a) per la logica proposizionale.

Kolmogorov formulò un'interpretazione che è essenzialmente la stessa in termini diversi: egli considerò le proposizioni come problemi e le asserzioni logicamente composte come problemi spiegati nei termini di problemi più semplici: per esempio, AB rappresenta il problema di ridurre la soluzione di B alla soluzione di A. Inizialmente Heyting e Kolmogorov considerarono come distinte le loro rispettive interpretazioni; Kolmogorov sottolineava che la sua aveva un senso anche in un contesto classico. In seguito Heyting si rese conto che, quanto meno in ambito intuizionista, le due interpretazioni coincidevano.

Logica intuizionista formale e aritmetica fino al 1940

L'articolo di Kolmogorov del 1925, scritto in lingua russa, è la prima formalizzazione pubblicata di una parte della logica intuizionista e rappresenta un risultato notevole; ciononostante esso influì in misura molto limitata sugli sviluppi successivi (era infatti ancora sconosciuto a Gödel nel 1933 e non letto da Heyting nel 1934). Kolmogorov non assume l''ex falso sequitur quodlibet' P→(¬PQ), che trova giustificazione sulla base dell'interpretazione BHK. Il sistema della logica intuizionista privato dell''ex falso' (successivamente noto come logica minimale) riveste un certo interesse in rapporto a problemi di completezza.

Valerij Ivanovič Glivenko (1897-1940) presentò nel 1928 una formalizzazione (incompleta) della logica proposizionale intuizionista derivando informalmente ¬¬(¬PP), ¬¬¬P→¬P, (¬PP→¬Q)→¬Q; egli utilizzò questi teoremi per mostrare l'insostenibilità dell'interpretazione della logica di Brouwer, secondo la quale una proposizione può assumere intuizionisticamente tre valori di verità; si tratta di un buon esempio dell'uso della formalizzazione per risolvere una disputa filosofica.

Heyting scrisse un eccellente saggio sulla formalizzazione della matematica intuizionista, che fu premiato dall'associazione matematica olandese nel 1928 e pubblicato in una versione rivista nel 1930. Il primo dei tre articoli (Heyting 1930) contiene una formalizzazione della logica proposizionale intuizionista, mentre il secondo tratta di logica predicativa e aritmetica. La logica predicativa non appare ancora nella sua forma definitiva, a causa del trattamento incompleto della sostituzione e della presenza in embrione di elementi (non del tutto coerenti) di una teoria che permetta l'impiego di termini non denotanti; l'aritmetica presentata nel secondo articolo è una parte dell'aritmetica di Heyting così come viene intesa oggi, in quanto presenta assiomi per l'addizione (in forma di definizione) ma non per la moltiplicazione. Il terzo articolo, infine, tratta dell'analisi. Il sistema appare molto debole per via della mancanza di assiomi di esistenza per insiemi e funzioni.

Nel 1929 Glivenko, in esito al suo rapporto epistolare con Heyting, formulò e dimostrò il 'teorema di Glivenko': nella logica proposizionale ¬¬A è dimostrabile intuizionisticamente se e soltanto se A è dimostrabile classicamente.

Kolmogorov nell'articolo del 1925 descrive una immersione della logica proposizionale classica nella (sua parte di) logica proposizionale intuizionista ‒ anticipando in tal modo i lavori di Gödel (1933) e di Gerhard Gentzen (1909-1945), risalente anch'esso al 1933 ma pubblicato solamente nel 1965 ‒ e sostiene che tale immersione può essere generalizzata a sistemi più forti. L'immersione di Gödel è formulata per l'aritmetica, ma è evidente la possibilità di adattarla alla logica predicativa. Nella versione di Gentzen formule prime P sono per la prima volta sostituite da ¬¬P e gli operatori …⋁… e ∃x… da ¬(¬…∧¬…) e ¬∀x¬… rispettivamente. Nella versione di Kolmogorov l'operatore ¬¬ è inserito simultaneamente davanti a ciascuna sottoformula. Le varie immersioni sono logicamente equivalenti.

Se * è una di queste immersioni, A*→A classicamente; A* è dimostrabile intuizionisticamente se e soltanto se A è dimostrabile classicamente.

Il risultato di Gödel rese evidente che i metodi intuizionisti vanno al di là del finitismo, proprio perché consentono l'impiego di nozioni astratte. Ciò risulta evidente, per esempio, dalla clausola che spiega l'implicazione intuizionista nell'interpretazione BHK, poiché in essa le nozioni astratte di dimostrazione costruttiva e costruzione sono utilizzate come fondamentali. Fino a quel momento la scuola di Hilbert non se n'era resa conto; Paul Bernays (1888-1977) fu il primo ad afferrare le implicazioni del risultato di Gödel.

Importante per la teoria della dimostrazione della logica intuizionista fu la formulazione (Gentzen 1935) del calcolo dei sequenti LK e LJ. Usando il suo teorema di eliminazione del taglio Gentzen mostrò che per IQC (calcolo dei predicati intuizionista) vale la proprietà disgiuntiva DP: se ⊦AB, allora ⊦A o ⊦B. Lo stesso, identico metodo produce la proprietà di definibilità esplicita o di esistenza ED: se ⊦∃x A(x) allora ⊦A(t) per qualche termine t. Queste proprietà sono in evidente contrasto con la logica classica e sono state ampiamente indagate e definite per tutti i comuni sistemi formali intuizionisti. La semantica per IPC (calcolo proposizionale intuizionista), che si deve a Stanisław Jaśkowski, Marshall H. Stone, Alfred Tarski, Garrett Birkhoff e Toziro Ogasawara negli anni 1936-1940, era una semantica algebrica, con la semantica topologica come importante caso particolare. Nella semantica algebrica i valori di verità per le proposizioni sono elementi di un'algebra di Heyting (nota anche come reticolo brouweriano, reticolo pseudo-complementato, algebra pseudo-booleana o reticolo residuato con minimo). Un'algebra di Heyting è un reticolo con massimo e minimo e un'operazione supplementare → tale che abc se abc, per tutti gli elementi a,b,c del reticolo. Un importante caso speciale di un'algebra di Heyting è la collezione degli insiemi aperti di uno spazio topologico T ordinato per inclusione, dove UV:=Interno (V (T U)). Le operazioni logiche ∧, ⋁, →, ¬ corrispondono alle operazioni di reticolo ∧, ⋁, → e all'operazione definita ¬a:=a→0, dove 0 è l'elemento minimo del reticolo (un'algebra booleana è un caso speciale di un'algebra di Heyting).

Metamatematica della logica e dell'aritmetica intuizioniste dopo il 1940

Agli inizi degli anni Quaranta Kleene concepì un'interpretazione che stabiliva una connessione fra la nozione di funzione calcolabile (ricorsiva) e logica intuizionista, l'interpretazione di realizzabilità (Kleene 1945). L'idea dell'interpretazione è di codificare in modo ereditario informazioni sulla realizzazione esplicita di disgiunzioni e quantificatori esistenziali, ricorsivamente in parametri numerici. La definizione è per induzione sul numero di simboli logici di un enunciato (formule senza variabili libere): a ogni formula A si associa un predicato 'x realizza A', dove x è un numero naturale. Clausole tipiche sono

n realizza t=s se e solo se t=s è vero;

n realizza AB se e solo se per ogni m che realizza A, nm realizza B;

n realizza ∃mB(m) se e solo se n è una coppia (m,k) e k realizza B(m).

Qui ∙ è l'operazione di applicazione tra un numero e il codice di una funzione ricorsiva parziale. Kleene stabilì la correttezza di questa interpretazione: se HA ⊦A, allora esiste un numero n che realizza A. In particolare è realizzabile la seguente versione della tesi di Church:

CT0nmA(n,m)→∃knA(n,km),

un principio chiaramente incompatibile con la logica classica. La realizzabilità e le sue molte varianti sono divenute uno strumento molto efficace nello studio della metamatematica di sistemi costruttivi.

La semantica algebrica fu estesa alla logica predicativa e Andrzej Mostowski (1913-1975) nel 1949 fu il primo ad applicare modelli topologici per ottenere risultati di indimostrabilità dall'IQC; questa direzione di indagine culminò nel 1963 nella monografia di Helena Rasiowa e Roman Sikorski. Benché la semantica algebrica si sia dimostrata utile nella ricerca metamatematica, essa costituisce ‒ per così dire ‒ solamente la versione algebrica della sintassi, come testimonia il fatto che l'IPC stessa può essere trasformata in un'algebra di Heyting (l'algebra di Lindenbaum dell'IPC). Più importanti dal punto di vista concettuale sono altre due semantiche, i modelli di Beth (Beth 1956, 1959) e quelli di Kripke (Kripke 1965), che si devono rispettivamente a Evert Willem Beth e Saul Kripke.

Entrambe queste semantiche sono basate su insiemi parzialmente ordinati. Chiamiamo nodi gli elementi di un insieme parzialmente ordinato. Nei modelli di Kripke l'ordine parziale è arbitrario, in quelli di Beth è un albero ramificato in maniera finita. L'interesse per questi modelli risiede nell'interpretazione intuitiva dell'ordine parziale: nei modelli di Beth ciascun nodo rappresenta uno stato di informazione in un dato momento e un nodo più in alto rappresenta un possibile stato di informazione in un tempo successivo. La ramificazione dell'albero riflette il fatto che nel futuro le nostre conoscenze hanno diverse possibilità di estensione. Nei modelli di Kripke è più naturale pensare che i nodi rappresentino diversi livelli di conoscenza; un nodo più in alto nell'ordine corrisponde a un'estensione delle nostre conoscenze. In altri termini, nel modello di Kripke passare a un momento successivo nel tempo non costringe a muoversi verso l'alto, come avviene invece nel caso in cui si verifichi un ampliamento delle conoscenze. In questi modelli si ha la nozione di 'A è vero nel nodo k' oppure 'k forza A'. La falsità di ⊥ non è forzata in alcun nodo. È possibile interpretare i modelli di Beth e di Kripke come modelli topologici per spazi speciali.

Un aspetto importante dei modelli di Beth è la connessione con la validità intuizionista intuitiva.

Da osservazioni di Georg Kreisel nel 1958 si può dedurre che, per la logica proposizionale, la validità in un modello di Beth è equivalente alla validità intuitiva.

Beth e Kripke dimostrarono la completezza dei rispettivi tipi di semantica utilizzando metodi classici (originariamente Beth aveva creduto di disporre per la propria semantica anche di una dimostrazione intuizionista di completezza). Veldman fu in grado di mostrare che, se si estende la nozione di modello di Beth a quella di modello di Beth fallibile, dove in certi nodi è permessa la forzatura della falsità, è possibile ottenere una dimostrazione di completezza intuizionista per la semantica di Kripke; l'idea fu trasferita alla semantica di Kripke da Henricus Cornelis Maria de Swart. Per la parte di logica intuizionista senza falsità e negazione i modelli fallibili sono semplicemente modelli ordinari. Per la logica minimale, dove ⊥ è considerato una lettera proposizionale arbitraria indimostrabile, si ha completezza intuizionista relativamente ai modelli di Beth ordinari. I migliori risultati in questa direzione si possono trarre dal lavoro di Harvey Friedman a partire dal 1976 circa.

Craig A. Smoryn′ski utilizzò con grande virtuosismo i modelli di Kripke applicandoli allo studio della metamatematica dell'aritmetica intuizionista.

CATEGORIE