Quando la logica è da premio internazionale

“Eccellenza della scrittura espositiva nel campo della logica”. Con questa motivazione il professore dell’Università Cattolica del Sacro Cuore Sergio Galvan ha ricevuto lo Shoenfield Prize Recipients, il premio che porta il nome dell’eminente logico scomparso nel 2000 e apprezzato da generazioni di studiosi per i suoi scritti considerati modelli di lucidità ed eleganza. Una sorta di “Premio Nobel” per chi in ambito filosofico si occupa di logica, è assegnato ogni tre anni dall’Association for Symbolic Logic, la più antica e importante associazione a livello internazionale, fondata nel 1936 in un momento in cui tale disciplina stava facendo grandi progressi. Basti pensare alla scoperta dei famosi teoremi di Gödel nel 1931.

Il professor Galvan è stato insignito del riconoscimento assieme a Paolo Mancosu, dell’Università di Berkeley, in California, e Richard Zach, dell’Università di Calgary autori con lui del libro “An Introduction to Proof Theory-Normalization, Cut-Elimination, and Consistency Proofs” (Oxford University Press, 2021). Il volume, che ha ottenuto subito gli apprezzamenti della comunità scientifica per la chiarezza in cui è illustrata la teoria della dimostrazione, quella branca della logica che ha come oggetto di studio le capacità dimostrative dei sistemi formali, «è il risultato del lavoro di tre studiosi uniti non solo da una comune visione della logica e della sua importanza, ma da una non comune esperienza di formazione», commenta il professor Galvan, a lungo docente di Logica e di Filosofia della scienza in Cattolica. Ma è anche «un riconoscimento del lavoro svolto in questo ambito fin dai tempi in cui ho scritto i miei primi libri sui sistemi dell’aritmetica e sui teoremi di Gödel».

Com’è nata l’idea di questo lavoro? «L’iniziativa di scrittura a sei mani è venuta a Paolo Mancosu, uno dei miei primi allievi, laureatosi con me in Cattolica negli anni in cui insegnavo Logica Matematica nella Facoltà di Lettere e Filosofia. Paolo è da molti anni professore di Logica e Filosofia nella prestigiosa università di Berkeley, dove ha avuto come allievo Richard Zach che si addottorò con lui svolgendo una tesi su temi hilbertiani della teoria della dimostrazione. Richard ora insegna Logica nella Università di Calgary. In questi anni siamo sempre stati in contatto e l’idea di fare un libro introduttivo alla teoria della dimostrazione si è sviluppata in concomitanza con le nostre esperienze didattiche».

Di cosa si occupa il volume? «Il libro rappresenta una introduzione avanzata alla proof theory, vale a dire la teoria della dimostrazione, un’area centrale della logica matematica di particolare interesse per la filosofia. Ognuno di noi ha messo a disposizione le specifiche competenze per coprire i tre filoni principali della teoria ispirata all’opera di Gentzen, ovvero le tecniche di normalizzazione nella deduzione naturale, di eliminazione del taglio nel calcolo dei sequenti e le prove di consistenza».

Cosa s’intende per teoria della dimostrazione? «È quella branca della logica, fondata dal matematico Hilbert - e dai suoi allievi - allo scopo di studiare la struttura logica delle teorie formali e le loro proprietà, come la non contraddittorietà, la correttezza, la decidibilità, la completezza. Nel contesto della logica contemporanea ognuna di queste proprietà ha un significato preciso, il che permette di stabilire se una teoria - come, ad esempio, l’aritmetica, l’analisi o la geometria - gode o meno di esse».

Qual è la questione centrale? «La determinazione della non contraddittorietà - o coerenza - di una teoria è il problema fondamentale della teoria della dimostrazione, dal momento che la coerenza è il requisito minimale di una teoria: se in una teoria è derivabile la contraddizione la teoria cessa di essere tale. Per superare la crisi dei fondamenti della matematica - che ebbe luogo tra la fine dell’Ottocento e l’inizio del Novecento - la dimostrazione della coerenza dell’aritmetica, mediante procedure assolutamente sicure, diventò l’obiettivo fondamentale della teoria della dimostrazione. I teoremi di Gödel segnarono una battuta d’arresto ai tentativi compiuti da Hilbert e dai suoi allievi per raggiungere questo scopo. Gentzen, però, attraverso il suo “Hauptsatz” , cioè il suo fondamentale teorema di eliminazione del taglio, riuscì a dimostrare la coerenza dell’aritmetica, usando principi più astratti e potenti di quelli usati da Hilbert. Il nostro libro, quindi, presenta i sistemi logici ideati da Hilbert e i sistemi della deduzione naturale e dei sequenti ideati da Gentzen, dimostra il teorema di normalizzazione per i sistemi di deduzione naturale e quello di eliminazione del taglio per i sistemi dei sequenti. Infine, esamina a fondo le dimostrazioni di consistenza dell’aritmetica ideate da Gentzen».

Si tratta di un testo rivolto esclusivamente a studiosi o fruibile anche dai non addetti ai lavori? «Come risulta dalla prefazione il libro nasce dal desiderio di consentire agli studenti, soprattutto quelli di filosofia, che hanno un background minimale in matematica e in logica, di comprendere i più importanti risultati della teoria della dimostrazione classica. Per questo non ha la natura di un libro divulgativo, quanto piuttosto quella di un trattato di teoria della dimostrazione, che introduce, partendo da una base minima di conoscenze logiche e matematiche, ai temi centrali della teoria della dimostrazione stessa. È fornito di un ampio apparato di esercizi e di approfondimenti locali, che hanno la funzione di rendere maggiormente accessibili i singoli argomenti e si propone di esibire i dettagli più riposti delle dimostrazioni. Cionondimeno, presenta alcuni dei teoremi più difficili della teoria della dimostrazione – come il menzionato teorema di eliminazione del taglio – per cui la sua lettura richiede un impegno notevole».

Per quanto possa apparire ostico, lo studio della logica è fondamentale, soprattutto nella nostra epoca sempre più alle prese con algoritmi e intelligenza artificiale… «La logica è una disciplina antica, ma tra la fine dell’Ottocento e l’inizio del Novecento è stata, per così dire, rifondata grazie all’introduzione di metodi formali rigorosi, ideati in gran parte per affrontare la problematica dei fondamenti della matematica. Il termine “logica simbolica” è stato coniato proprio per indicare tale tipo nuovo di logica, basato su una completa formalizzazione dei mezzi di dimostrazione. Per quanto allora la logica fosse intesa soprattutto come logica della matematica, la sua natura di logica formale le consentì di estendersi a tutti i campi in cui fosse importante il ragionamento rigoroso. Così, il progresso in molteplici aree della scienza moderna come l’informatica, la linguistica e le scienze cognitive, è stato spesso ispirato dalla logica. Anzi, alcune branche della scienza contemporanea, come la computer science o l’intelligenza artificiale, non sarebbero potute nascere senza la logica simbolica. Già questo dovrebbe essere sufficiente per comprendere l’utilità della logica e del suo studio. Ma a me preme sottolinearne l’importanza a tutti i livelli dell’apprendimento. La logica insegna a comprendere a fondo la natura dei problemi e, spesso, a individuare la strada per la loro soluzione in tutti i campi del sapere, dai più piccoli e limitati ai più grandi, perché dove c’è attività del pensiero conoscitivo o pratico lì c’è logica».

Foto di Kaleidico su Unsplash