Pin It

Viste le leggi di raccolta delle informazioni con cui il web ormai gestisce e determina la sopravvivenza delle testate giornalistiche, un risultato abbastanza minuscolo ottenuto da due informatici, Christoph Benzmüller della Freie Universität di Berlino e Bruno Woltzenlogel Paleo della Technische Universität di Vienna, caricato su arXiv ha raccolto una quantità incredibile di riscontri. A chi è capitato di leggerne qualcuno, suggerisco certamente di leggere anche questo articolo su Der Spiegel, dove ho trovato una spiegazione chiara di che cosa abbiano fatto i due ricercatori europei.

godel

Copia con disegno di Leo Ortolani di proprietà di Pino Rosolini del libro su questo teorema.

In brevissima sintesi, hanno verificato mediante alcuni dimostratori di teoremi (theorem provers) la cosiddetta “prova ontologica dell’esistenza del dio”, un esercizio in logica modale del second’ordine che interessò Kurt Gödel intorno al 1940 e che egli risolse, ma non pubblicò. Le due pagine con la soluzione scritte a mano da Gödel divennero note con la pubblicazione dell’opera completa del matematico (sono nel terzo volume uscito nel 1995). Anche se Gödel non aveva mandato ad una rivista specializzata il risultato (come membro permanente dell’Institute for Advanced Study a Princeton non sentiva alcuna pressione di produrre carta stampata), aveva mostrato la soluzione dell’esercizio a Dana Scott nel 1970. È proprio la riedizione di Dana Scott che viene verificata a computer da Benzmüller e Woltzenlogel Paleo. Chiaramente, la verifica non aggiunge nulla alla corretta soluzione dell’esercizio (come avrebbe detto un mio amico matematico: Gödel e Scott non sono mica dei pirla). Piuttosto offre un ulteriore spunto al tentativo di formalizzare mediante linguaggi meccanici i metodi e le strategie del ragionamento matematico, cercando di aumentare il successo che il calcolo formale automatico ha già ottenuto con linguaggi quali Mathematica, Cocoa, Singular, Coq, Isabelle e tanti altri.

Per chi sia interessato ad analizzare più a fondo i motivi che possono aver spinto Gödel a trattare un tale argomento (la prova ontologica dell’esistenza della divinità) – o a controllare di persona la correttezza delle dimostrazione – suggerisco l’eccellente pubblicazione “La prova matematica dell’esistenza di Dio“, curata da Gabriele Lolli e Piergiorgio Odifreddi per Bollati Boringhieri nel 2006.

Giuseppe “Pino” Rosolini

Pin It
this site uses the awesome footnotes Plugin