A recent headline claimed that Computer Scientists ‘Prove’ God Exists. What is the real story beneath the headline? Who wrote the proof? How did the scientists prove that God exists? Finally – just what is “modal logic”?
Gödel’s Proof that God Exists
Christoph Benzmüller and Bruno W Paleo wrote a brief article describing the verification of Kurt Gödel’s proof of God’s existence.
Sometime between 1941 and the 1970s, Gödel wrote a brief mathematical proof that God exists. Later, Dana Scott edited the original proof. Decoded Science offers a brief summary of this proof, which has five axioms that we assume to be true:
- Any “property”, or the negation of that property, is “positive”; but it is impossible that both the property and negation are positive.
- If one positive property implies that some property necessarily exists, then the implied property is positive.
- The property of being God-like is positive.
- Positive properties are necessarily positive.
- The property of necessarily existing is positive.
Gödel added three definitions along the way:
- A “God-like” being has all positive properties.
- An “essence” of a being is a property that the being possesses, and that property necessarily implies any property of that being.
- The “necessary existence” of a being means that it is necessary that all the essences of that being exist (“are exemplified”).
Gödel proved intermediate theorems and one corollary in the course of his proof. The first two axioms led to “Positive properties may possibly exist (“be exemplified”). After adding the third axiom, God, the God-like being, may possibly exist. With the help of the fourth axiom, Gödel stated that “being God-like” is one essence of any God-like being.
After adding the final axiom, Gödel concluded that it is necessary that God exists.
Both Gödel and Euclid Used Axioms and Logic
The ancient Greek philosopher and mathematician Euclid laid the foundations of geometry in exactly the same way that Gödel constructed his proof that God exists. Euclid also provided axioms and definitions, then built theorem upon theorem by applying logic. Euclid’s results are still valid; mathematicians still use his approach.
If Gödel’s logic stands up to scrutiny, then the only logical way to attack his conclusion is to disagree with one or more axioms. We welcome our readers’ comments on this.
Euclid offers an intriguing “parallel” case. His “parallel postulate,” an axiom, states that there can be only one straight line, ‘S’, through a given point ‘G’ that is not on a different straight line ‘L’ such that line ‘S’ never intersects line ‘L’. That’s true on a flat surface, but not on a sphere such as the planet Earth, where parallel lines of longitude cross at the North and South Poles. Euclid defined “plane geometry” on a flat surface; but changing this one axiom changes many results and creates geometry on a sphere.
Would changing one of Gödel’s axioms eliminate God? Certainly this could invalidate the current proof.
Modern Computing Verified Gödel’s Proof
A team of logicians and computer scientists collaborated to encode Gödel’s proof and verify it with several computer programs. These particular programs had to deal with “modal logic”, which can handle statements about “possibility” and “necessity.”
These sophisticated programs have somewhat understated names such as “Nitpick,” “Sledgehammer” and “Metis.” Apparently a MacBook computer can be powerful enough to run them.
What is Modal Logic?
Modal logic deals with statements, or propositions, that express “possibility” and “necessity.”
Many of us are more familiar with less expressive “propositional logic,” limited to “if something exists” or “if all somethings have this property.”
Benzmüller and Paleo’s paper states that they used several different modal logic systems to verify Gödel’s proof. Those are different logic systems, not just different computer programs. The logic systems were:
- ‘K’, a “weak” logical system named for logician Saul Kripke; see the next paragraph.
- ‘B’ logic adds “A implies the necessity of the possibility of A” to ‘K’ logic.
- ‘S4’ and ‘S5’ logic allow some simplification of repeated “possibility” and “necessity” operations; see below.
‘K’ logic extends typical propositional logic by adding two axioms for necessity and also the concept of possibility:
- If A is a theorem in ‘K’, then “the necessity of A” is also a theorem in ‘K’.
- If it is necessary that “A implies B“, then “the necessity of A ” implies “B is necessary”.
- The “possibility of A” is equivalent to “it is not necessary that A is false”.
‘S4’ logic permits reducing a string of repeated necessities to one necessity, and a string of repeated possibilities to a single possibility.
‘S5’ logic permits reducing any string of repeated necessities and/or possibilities to just the final operation, whether it is possibility or necessity.