di Pasquale Guarino
Nella giornata del 10 febbraio, presso il “Lamaro Pozzani”, Thomas Waring, dottorando in matematica presso l’Università degli Studi Roma Tre, ha presentato ai collegiali il suo ambito di ricerca. L’incontro ha offerto ai partecipanti un’interessante esplorazione del legame tra teoria della dimostrazione e computazione, un tema che affonda le radici nella logica matematica e si sviluppa fino alle moderne teorie informatiche.
Il relatore ha aperto il suo intervento con una panoramica storica sulla logica, sottolineandone il ruolo fondativo nella filosofia e nella matematica. Partendo dal contributo di Gottlob Frege, che nel XIX secolo introdusse il concetto di un “linguaggio formale per il pensiero puro modellato su quello dell’aritmetica”. Ha poi ricordato il progetto di David Hilbert, volto a costruire un sistema assiomatico capace di garantire la coerenza della matematica. “Il problema della risolvibilità deve essere posto a principio di ogni questione matematica”, sosteneva Hilbert, evidenziando la necessità di dimostrare l’assenza di contraddizioni all’interno di ogni sistema assiomatico.
L’esposizione è poi entrata nel cuore della teoria degli insiemi, a partire dai lavori di Georg Cantor e dal concetto di comprensione degli insiemi. Ma gli insiemi, da soli, non bastano come fondamento della logica; Waring ce lo ha illustrato con il celebre paradosso di Bertrand Russell: se in una città il barbiere rade tutti gli uomini che non si radono da soli, non si riesce a stabilire chi rada il barbiere, giacché se radesse se stesso allora non potrebbe essere raso dal barbiere, ossia se stesso. Benché ci siano scappatoie dall’antinomia di Russell, il problema con gli insiemi è più profondo: Kurt Gödel (1931) dimostra i celebri teoremi di incompletezza, mostrando che ogni sistema coerente non può essere completo, e quindi esistono proposizioni vere ma non dimostrabili. Con buona pace di Hilbert, il suo progetto fondazionale è un’utopia, destinato a rimanere irrealizzato in virtù degli stretti vincoli della logica.
Dall’analisi del “perché” di un sistema logico, Waring ha poi guidato i presenti alla scoperta del “come” delle dimostrazioni, facendo riferimento all’interpretazione BHK (sigla che racchiude i nomi di Brouwer, Heyting e Kolmogorov). Questo approccio costruttivo alla logica sposta l’attenzione dalla verità astratta alla costruzione esplicita delle prove: per dimostrare un enunciato del tipo “A e B”, ad esempio, occorre fornire una dimostrazione di A e una di B; per un enunciato “A o B” è sufficiente dimostrare uno dei due.
La discussione ha poi toccato il tema della funzione in logica e della sua applicazione nella teoria della computazione. Attraverso il calcolo λ di Church e il concetto di macchina di Turing, Waring ha spiegato come dimostrazioni e programmi informatici siano due facce della stessa medaglia, come espresso dalla corrispondenza Curry-Howard. In questo quadro, il teorema centrale di Gerhard Gentzen sulla “eliminazione del cut” diventa un ponte tra la logica e la computazione: tutto ciò che si può dimostrare attraverso l’uso di cuts si può dimostrare anche senza, garantendo così una maggiore efficienza nella costruzione delle prove e nell’esecuzione dei programmi.
Il seminario si è concluso con una riflessione sul legame tra logica e informatica, prendendo come esempio il problema della terminazione, formulato da Turing nel 1937. Così come il paradosso di Russell metteva in crisi la teoria degli insiemi, il problema della terminazione dimostra che non esiste un algoritmo generale in grado di stabilire se un qualsiasi programma terminerà o meno la sua esecuzione. La somiglianza tra questi due risultati sottolinea ancora una volta l’intima connessione tra dimostrazione e computazione.
L’incontro ha rappresentato un’occasione stimolante per approfondire un tema complesso ma di grande attualità. Durante la sessione di domande, è stata posta la questione relativa all’applicazione nel computing del lavoro di Waring in matematica. Thomas ha spiegato che la teoria della dimostrazione, pur essendo un campo teorico, possa potenzialmente influenzare profondamente l’informatica, specialmente dati i più recenti sviluppi.