Allemachtig!

Nieuws | de redactie
9 september 2013 | God bestaat. Kurt Gödel bracht het ontologische bewijs voor de existentie van een opperwezen, maar dat was voor velen natuurlijk nog niet adequaat. Het MacBook van de computerwetenschapper Christoph Benzmüller van de Freie Universität Berlin heeft nu de formules nog eens doorgenomen. En zie, het was licht.

Benzmüller beschrijft in zijn abstract wat hij heeft gedaan en de uitkomsten daarvan.

“Goedel’s ontological proof has been analysed for the first-time with an unprecedent degree of detail and formality with the help of higher-order theorem provers. The following has been done (and in this order): A detailed natural deduction proof. A formalization of the axioms, definitions and theorems in the TPTP THF syntax. Automatic verification of the consistency of the axioms and definitions with Nitpick. Automatic demonstration of the theorems with the provers LEO-II and Satallax. A step-by-step formalization using the Coq proof assistant. A formalization using the Isabelle proof assistant, where the theorems (and some additional lemmata) have been automated with Sledgehammer and Metis.”

Zelf zei Gödel kort voor zijn dood, dat hij tevreden was met de kwaliteit van zijn bewijsvoering, maar die toch maar voor zich hield, uit vrees voor een eeuwigheid aan misverstanden onder collega’s en anderen. Een studente liet hij wel meelezen en met haar aantekeningen kwam Gödels Godsbewijs toch naar buiten. Niet dat God nu bewijzen van feilbare wezens nodig zou hebben, maar noch Gödel, noch God zal daar echt mee zitten


«
Schrijf je in voor onze nieuwsbrief
ScienceGuide is bij wet verplicht je toestemming te vragen voor het gebruik van cookies.
Lees hier over ons cookiebeleid en klik op OK om akkoord te gaan
OK