Dimostrata la prova ontologica di Godel dell’esistenza di Dio ?

Il logico, matematico e filosofo Kurt Gödel, nato a Brno il 28 aprile 1906, austriaco poi divenuto cittadino americano, è conosciuto sia per i suoi due Teoremi di incompletezza, da lui pubblicati nel 1931, quando aveva solo venticinque anni, sia per i suoi studi sull’Ipotesi del Continuo, sia per aver elaborato, nel 1970, una sua prova ontologica della esistenza di Dio; un modello logico, un teorema basato su sei assiomi e su principi di logica modale, che potesse spiegare l’esistenza del Creatore, solo modo per giustificare la realtà dell’universo, e le leggi matematiche che ne sono alla base.
in questi giorni sono apparsi alcuni articoli e notizie su uno studio realizzato da due ricercatori, il tedesco Christoph Benzmueller e l’austriaco Bruno Woltzenlogel Paleo, i quali utilizzando alcuni software e un MacBook Pro della Apple (quindi un computer portatile che, per quanto molto potente, è di semplice reperibilità), avrebbero dimostrato la veridicità del cosiddetto Teorema di Dio definito da Gödel.
Il loro lavoro, denominata Formalizzazione, Meccanizzazione e Automatizzazione della Prova di Godel dell’Esistenza di Dio (Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence), è stato pubblicato su Arxiv il 21 agosto di quest’anno, con ultima revisione il 10 di settembre.
Interessante notare come su alcuni giornali la ricerca sia stata descritta come una sorta di prova informatica dell’esistenza di Dio. Altri, come ad esempio La Repubblica, hanno più correttamente descritto la ricerca, anche se non così chiaramente forse nel titolo (“Sì, il teorema di Dio è corretto”: due matematici fanno rivivere l’opera di Gödel).
In realtà, come affermato dai due studiosi, e come illustrato già nel titolo dello studio, oltre che maggiormente descritto nella pagina dove è accessibile l’articolo, si è trattato di una analisi automatizzata della logica e coerenza interna del teorema e dei suoi assiomi, realizzata utilizzando alcuni software e piattaforme già esistenti, come TPTP, Nitpick, Leo II, Satallax, Isabelle, Coq.
Lo stesso Benzmueller ha spiegato gli obiettivi “la prova ontologica dell’esistenza di Dio di Gödel era più che altro un buon esempio di qualcosa di inaccessibile in matematica o per l’intelligenza artificiale, che con l’attuale tecnologia abbiamo risolto”.
Link Arxiv