BRUNO WOLTZENLOGEL PALEO, Ph.D.
LOGICIAN, PROOF THEORIST, VERIFIER OF GÖDEL’S PROOF OF GOD
In 2012 and 2013, during a difficult period, Bruno’s mother encouraged him to attend a church in his home town in Brazil. To show his gratitude for the priest’s support, he decided to give him a gift. And what could be a better gift to a priest from a logician, and particularly a proof theorist like Bruno, than an ontological proof of God’s existence?
However, he quickly discovered that the proof he sought did not meet contemporary standards of rigor, precision, and quality in computational logic. Even Kurt Gödel’s decades-old manuscript was full of gaps. What was supposed to be a weekend-long personal project became a multi-year research program that he conducted first as a researcher at the Vienna University of Technology and later at the Australian National University.
In the project, Bruno collaborated with Christoph Benzmüller, from the Free University of Berlin, an expert in automated reasoning for higher-order logic, and Annika Kanckos, a philosopher at the University of Helsinki. They filled the gaps in the proof, formalized it in a modern, natural deduction calculus, and analyzed it, using a variety of modern computational logic tools. In a major success story for artificial intelligence, their computers uncovered a surprising mistake in Gödel’s manuscript, which caused his theory to be inconsistent. Fortunately, they quickly determined that most of the other modern variants of Gödel’s proof had already fixed the mistake.
Bruno’s work on ontological proofs would never have started without his mother’s encouragement. She also taught him the life lesson always to finish what you start. It took him five years to complete the work that he began in 2013, after which he switched his focus to research areas unrelated to ontological proofs. But, coincidentally, as he sat next to his mother in the hospital where she would pass away just a few days later, he received the invitation to contribute to this book. For all that and so much more, Bruno dedicates all of his work on ontological proofs to the memory of his mother, Claudia Zambello Woltzenlogel Paleo, whose faith was beyond proof.
Ontological Proofs (1)
BRUNO WOLTZENLOGEL PALEO, Ph.D.
Attempts to prove the existence of God by means of purely logical arguments are an old tradition in philosophy, theology, mathematics, and logic, dating back at least to 1078 CE, when St. Anselm of Canterbury proposed his famous ontological argument. Ontology is the branch of philosophy that is concerned with the concepts of being and existence. Thus, ontological arguments (2) for God’s existence are arguments that derive the conclusion that God exists from premises about the definition of being God.
The formulation that the famous logician Kurt Gödel (1906-1978) proposed (3) is a modern culmination of this tradition, addressing various shortcomings of earlier ontological arguments. For instance, Kant’s famous objection (that existence is not a property) does not apply to Gödel’s formulation, since Gödel properly uses an existential quantifier to express God’s existence.
Gödel worked on the argument for decades and shared a two-page manuscript with Dana Scott in 1970. There Gödel defined God as a being who possesses all positive properties.(4) “Positiveness” of a property is a primitive notion in Gödel’s theory. It is the only concept left undefined; however, its meaning is not arbitrary, but constrained by five axioms.(5) They are:
A1) Either a property or its negation is positive, but not both.
A2) A property necessarily implied by a positive property is positive.
A3) The conjunction of any number of positive properties is positive.
A4) Positive properties are necessarily positive.
A5) Necessary exemplification of an individual‘s essences is a positive property. (He defines an essence of an individual as a property that it possesses and that necessarily implies any property possessed by it.)
From axioms A1 and A2, we derive the first theorem, (6) stating that for any positive property, it is possible that there is a being who has this property. From A3 and the definition of God, it follows that the property of being God is itself a positive property. Hence, as a corollary (7) of the first theorem, it is possible that God exists.
The second part of the proof consists of proving a lemma (8) that shows that if God’s existence is possible, then it is necessary. Gödel achieves this by first showing, through A4, that the property of being God-like is an essence of any God, and then by using A5 together with a few modal logic (9) principles.
Finally, by using the lemma and the corollary of the first theorem, we conclude that the existence of a God-like being is necessary.
This proof has been formally verified to be logically correct. This means that, if you believe in the stated axioms and accept the logical rules of deductive reasoning, you must believe in the conclusion as well.
Footnotes:
1. A proof is a sequence of logical statements, which are either axioms or theorems.
2. cf. Stanford Encyclopedia of Philosophy's entry on Ontological Arguments: https://plato.stanford.edu/entries/ ontological-arguments/
3. For the Full Proof in Natural Deduction Calculus, see the images and derivations in this paper: https://gitlab.com/ aossie/ComputationalPhilosophy/-/blob/master/Papers/2016/StudiaLogica-NaturalDeduction/GodProof-ND.pdf
4. Higher-order logics are logics where it is possible to express statements not only about objects (e.g. "there are objects that are yellow" or "all objects that are triangles have internal angles with a sum of 180 degrees"), but also about properties (e.g. "for every property, if the property is positive then God has it").
5. An axiom is a logical statement that is assumed to be true.
6. A theorem is a logical statement that is derived from other previous logical statements in the proof according to the rules of logic.
7. A corollary is a theorem that is trivially derived from another theorem in the proof.
8. A lemma is a theorem that is a significant step in a proof of another major theorem.
9. Modal logics are logics where the logical statements can have modal operators such as “it is possible that...” and “it is necessary that...“Modal logics typically have a possible worlds semantics where, for instance, we interpret “it is possible that...” as “there is a world where...” and “it is necessary that...” as “in all worlds...”