28 aprile 2018

Sistemi formali: un’introduzione asistematica (parte seconda)

[leggi la prima parte]

 

Nel 1672, il padre del calcolo infinitesimale e della Monadologia, G. W. Leibniz, ideò la Stepped Reckoner , la prima calcolatrice meccanica in grado di svolgere le quattro operazioni aritmetiche. Le ambizioni del suo inventore andavano ben oltre il semplice calcolo aritmetico. Leibniz sognava di realizzare un sistema formale onnicomprensivo, la characteristica universalis , in grado di esprimere concetti matematici, scientifici, e addirittura filosofici. Questa prodigiosa invenzione avrebbe posto fine ad annose dispute intellettuali, che si sarebbero risolte nella revisione di calcoli. Negli Scritti di Logica , Leibniz dirà:

Sento che le controversie non finirebbero mai e che non si potrebbe mai imporre il silenzio alle sette, se non ci riportassimo dai ragionamenti complicati ai calcoli semplici, dai vocaboli di significato vago ed incerto ai caratteri determinati ... Una volta fatto ciò, quando sorgeranno controversie, non ci sarà maggior bisogno di discussione tra due filosofi di quanto ce ne sia tra due calcolatori. Sarà sufficiente, infatti, che essi prendano la penna in mano, si siedano a tavolino, e si dicano reciprocamente (chiamato, se loro piace, un amico): calculemus .

In ambito strettamente matematico, Leibniz formulò l’ Entscheidungsproblem , ovvero il “problema della decisione”, che consiste nel determinare il valore di verità (vero o falso) di un enunciato matematico con un algoritmo di calcolo. L’ Entscheidungsproblem è uno dei cardini del programma di Hilbert , formulato nel secolo scorso.

 

L’8 agosto 1900 Hilbert presentò una lista di ventitré problemi aperti al Congresso Internazionale dei Matematici di Parigi. La sua iniziativa ha avuto un notevole impatto sulla matematica del XX secolo, ed è stata emulata dal Clay Institute, che il 24 maggio 2000 ha proposto sette « problemi per il millennio » .

 

Il secondo problema di Hilbert consiste nella dimostrazione della coerenza degli assiomi dell’aritmetica, formalizzata da Peano. Un insieme di assiomi è coerente se da esso non si può ricavare una formula falsa.

 

Negli anni successivi, Hilbert formulò un programma più articolato, dedicato esclusivamente ai fondamenti della matematica (anche detti metamatematica ). Possiamo riassumere il programma nell’elaborazione di un sistema formale dotato delle seguenti caratteristiche:

 

- Completezza: si può derivare ogni enunciato matematico vero all’interno del sistema formale.

 

- Coerenza: non si possono ricavare enunciati matematici falsi all’interno del sistema formale.

 

- Decidibilità: si può determinare in un numero finito di passaggi se un enunciato è un teorema.

 

Osserviamo, incidentalmente, che la completezza di un sistema formale per il calcolo dei predicati (e delle proposizioni) è stata dimostrata da Gӧdel, tuttavia il programma di Hilbert ha una pretesa più generale: la formalizzazione della matematica, non semplicemente di una sua branca.

 

Gli assiomi di Peano per l'aritmetica sono il punto di partenza per la realizzazione del programma di Hilbert. Gödel dimostrò come in questa struttura elementare si annidi un'incompletezza essenziale.

 

Hofstadter ha paragonato l'aritmetica ad una massa critica. Alcuni fenomeni fisici, come una reazione nucleare a catena, si manifestano solo se le dimensioni del sistema eccedono una certa massa. In modo analogo, se un sistema formale è abbastanza espressivo da contenere l'aritmetica, esiste necessariamente almeno una formula vera ma indimostrabile.  Consideriamo ora il sistema MIU. Possiamo costruire una corrispondenza tra i teoremi di MIU e i numeri naturali, associando ad ogni simbolo un nuovo simbolo.  Le regole di deduzione sono esprimibili attraverso enunciati aritmetici. Ad esempio si può sostituire la regola “Da XI possiamo ricavare XIU” con “Un numero può venire moltiplicato per 10, se nella divisione per 10 il suo resto è 1”.    

Questo procedimento, detto gödelizzazione , si può applicare anche all’aritmetica di Peano. Dunque l’aritmetica di Peano è un sistema formale che descrive i numeri naturali, che a loro volta descrivono formule dell’aritmetica di Peano. Questa autoreferenzialità gioca un ruolo di primo piano nei due teoremi di incompletezza di Gödel, pubblicati nel 1931.

In ogni formalizzazione coerente della matematica, che sia sufficientemente da definire la struttura dei numeri naturali dotati delle operazioni di somma e prodotto, è possibile costruire una proposizione sintatticamente corretta, che non può essere né dimostrata, né confutata all'interno dello stesso sistema. Nessun sistema, che sia abbastanza espressivo da contenere l'aritmetica e coerente, può essere utilizzato per dimostrare la sua stessa coerenza.

Diamo ora una traccia di dimostrazione del primo teorema, esprimendola in un linguaggio “informale”, consapevoli di poter restituire, in questo modo, soltanto un'impressione sbiadita della magistrale opera di Gödel.    

 

Consideriamo il paradosso del mentitore, che fu fonte di ispirazione per il logico austriaco:

Questa frase è falsa.

La frase, attribuita ad Epimenide, non è né vera, né falsa. Secondo Aristotele, il paradosso nasce dalla confusione tra uso e menzione e la frase deve essere semplicemente cassata, perché priva di significato.  Per dimostrare il primo teorema, Gödel utilizzò la proposizione « Io non sono dimostrabile » . Se la proposizione fosse dimostrabile, sarebbe falsa. Viceversa, se fosse vera sarebbe dimostrabile. Quindi l’aritmetica di Peano è necessariamente incoerente o incompleta.

 

I teoremi di incompletezza di Gödel e il teorema di Turing hanno influenzato profondamente la nostra concezione della matematica e dell'informatica. La conoscenza di prima mano degli specialisti è filtrata attraverso ampi strati della società: il lettore di questo articolo, quantunque privo di conoscenze tecniche, possiede già la "preparazione psicologica" necessaria. Lo stesso non si può dire dei contemporanei di Gödel, che furono ridestati bruscamente dal secolare sogno di Leibniz . L’approccio logicista era stato scalfito dall’interno.

 

Diversi pensatori si sono cimentati nell'ardua impresa di investigare le implicazioni filosofiche dei teoremi di Gödel e Turing, soffermandosi sul rapporto tra menti e macchine. La principale difficoltà consiste nel delineare un modello matematico, seppur grossolano, della mente.  Il filosofo J. R. Lucas, nel suo celebre articolo Menti, macchine e Gödel , sostiene che le menti e le macchine non sono tra loro equivalenti; pertanto, il meccanicismo è falso.  Un essere umano può simulare le operazioni svolte da un computer usando carta e penna. L’ovvia differenza sta nel numero di operazioni svolte al secondo: su questo fronte non c’è partita per gli umani, ma l’equivalenza discussa da Lucas è qualitativa, non quantitativa.

 

D’altro canto, potremmo chiederci se un computer può simulare il comportamento di un essere umano. Lucas afferma che ciò è impossibile: una macchina può replicare singoli aspetti dell’intelligenza umana, ma non simulare tutte le caratteristiche della mente contemporaneamente.  L’argomento di Lucas fa uso del primo teorema di Gödel: gli esseri umani sanno che la formula   « Io non sono dimostrabile » è vera, mentre le macchine, assimilabili a dei sistemi formali, possono discernere le formule vere dalle formule false solo applicando la regola di deduzione. Come per la formula MU, è necessario “uscire dal sistema”: è una prerogativa degli esseri umani.

 

Una mente, quindi, è una macchina con un componente addizionale: l’ operatore gödelizzante .

 

Vi è anche una differenza “dialettica” tra le macchine e le menti. Queste ultime possono contemplare idee contraddittorie senza perdere il senno, mentre l’esistenza di una singola contraddizione pregiudica irrimediabilmente le macchine: da un sistema formula contraddittorio si può dedurre qualsiasi formula.  Sebbene le idee di Lucas siano lusinghiere e rassicuranti per il genere umano, non sono universalmente condivise.  La formula che abbiamo chiamato, informalmente, « Io non sono dimostrabile » assumerà una certa espressione nel linguaggio del sistema formale in esame. Indichiamola con G. Se aggiungiamo G agli assiomi del nostro sistema, abbiamo eluso, temporaneamente, l’operatore gödelizzante.

 

A questo punto, l’operatore gödelizzante può determinare una nuova formula G’ vera, ma non dimostrabile. In Gӧdel, Escher e Bach , Hofstadter osserva che i sistemi formali costruiti in questo modo diventano via via più complessi, fino ad eccedere la capacità degli esseri umani di determinarne la formula vera, ma non dimostrabile.

 

Altrettanto interessanti per noi umani sono le implicazioni del teorema di Turing sul tema del libero arbitrio. Molte persone, pur avendo una concezione meccanicista della realtà, credono nel libero arbitrio. Seth Lloyd, fisico e informatico statunitense, afferma che quest’atteggiamento è del tutto razionale. In una prospettiva meccanicista, le menti sono assimilabili a delle macchine di Turing, incapaci di determinare se un programma avrà termine o meno. Ne consegue che è impossibile rispondere alla domanda “Quale decisione sto per prendere?”. Sarebbe necessario simulare il processo decisionale, ma, in linea di principio, la simulazione potrebbe anche procedere per un tempo indefinito e non terminare mai.  Il teorema di Turing non risolve il problema del libero arbitrio, ma spiega, secondo Seth Lloyd, perché ci sentiamo liberi.

 

 

Per saperne di più:

L'articolo fa riferimento soprattutto al saggio Gödel, Escher, Bach: un'eterna ghirlanda brillante di Douglas Hofstadter, Adelphi, 1990.

Photo by bhupendrasingh on Pixabay - CC0 Creative Commons: libera per usi commerciali, attribuzione non richiesta.

© Istituto della Enciclopedia Italiana - Riproduzione riservata