I struggle with theories. They so rarely work out in practice. And though teachers tried to force-feed theories, theorems, and theologies down my throat when I was impressionable, these days nothing gets through.
Two Apple aficionados, however, decided to take on the Big Banging Theory -- whether God exists -- and claim they now have proof.
The theorem belongs originally to Anselm of Canterbury and was taken on by Austrian mathematician Kurt Godel. It goes like this: "God, by definition, is that for which no greater can be conceived. God exists in the understanding. If God exists in the understanding, we could imagine Him to be greater by existing in reality. Therefore, God must exist."
I am not going to enter into the finer points of this fine leap of logic. However, what's clear is that while I've been waiting for Godot, I should have been waiting for Gödel.
Gödel, you see, created a web of theorems and axioms. As we all (don't) know about theorems and axioms, they can be expressed as mathematical equations.
What can't these days?
So Christoph Benzmüller of Berlin's Free University and Bruno Woltzenlogel Paleo of the Technical University in Vienna whipped out their MacBook and tried to make the equations work. The idea was to see if Gödel's thinking can be confirmed on an Apple computer.
The result of their work is called "Formalization, Mechanization and Automation of Gödel's Proof of God's Existence."
Its abstract is anything but abstract. It makes for glorious reading, especially to those who understand it.
Here it is:
Goedel's ontological proof has been analyzed for the first-time with an unprecedented 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.
From Nitpick to Coq, culminating in a Sledgehammer.
I never thought I'd ever write a sentence like that. And I never thought that such words could bring us to a firmer understanding that God really, truly is somewhere out there. Or down here. Or everywhere.
I know that nitpickers will bring their own sledgehammers and attempt to declare that even the idea that God's existence might be formalized by math is a load of warmed-up coq au vin.
Or, in this case, a pile of schnitzel.
But we have to find whatever ways we can to at least touch certainty, as our reality has all the sureness of a paper sock.
In any case, the more practical significance of this work is that it might allow for a swifter and surer verification of any theorem by computers.
Indeed, Benzmüller told Der Spiegel that the God work opens vast horizons: "It's a very small, crisp thing, because we are just dealing with six axioms in a little theorem. There might be other things that use similar logic. Can we develop computer systems to check each single step and make sure they are now right?"
One day, perhaps, computers might totally shift the burdens of proof away from humans, so that the latter can focus on higher concept issues.
Until, that is, the computers and the humans become one and the same godly thing.