Does Gödel's ontological proof succeed in its formal formulation with higher-order modal logic axioms, and what technical criticisms have been directed against it?

This question lies at the heart of contemporary mathematical logic and philosophy of religion. Kurt Gödel—the greatest logician of the twentieth century—formulated in the 1970s an ontological proof using higher-order modal logic, which was not published until after his death (1995). The proof represents the most formally precise formulation of the ontological argument and has sparked intense technical debate among logicians and philosophers about its validity and soundness.

Inadequate Responses to Avoid

From some defenders of theism:

"Gödel is a mathematical genius, therefore his proof is correct." Argument from authority. Gödel's genius in mathematical logic does not guarantee the correctness of his ontological proof. Even geniuses can err, especially when transitioning from pure logic to metaphysics.

"The proof is purely formal, therefore irrefutable." Confusion between formal validity and soundness. A proof can be formally valid (its conclusions follow from its premises) but unsound (its premises are questionable). Most criticism targets the axioms, not the inference.

"Computer verification has proven the proof's correctness." Half-truth. Computer verification (Benzmüller & Paleo 2014) proved the formal validity of the inference, but it does not address the question of accepting the metaphysical axioms.

From some critics:

"The proof is merely symbol manipulation without content." Misleading oversimplification. The proof translates deep metaphysical intuitions (perfection, necessity, positiveness) into formal formulation. The symbols are not empty but carry specific philosophical meanings.

"Sobel proved that the proof leads to modal collapse." Exaggeration. Sobel showed that a particular version of the proof (with particular axioms) leads to modal collapse. But later modifications (Anderson 1990, Bjørdal 2018) avoid this collapse.

Why These Responses Are Inadequate

They fail to engage with the technical complexity of the proof. Gödel's proof is not an "ordinary philosophical argument" but a sophisticated logical structure requiring precise understanding of higher-order modal logic, property theory, and possible semantics. Serious criticism requires delving into these details.

Technical Structure of Gödel's Proof

The proof employs:
- Higher-order modal logic (S5 with quantification over properties)
- The concept of "positive property" as a primitive notion
- Definition of God: The being that possesses all and only positive properties

Basic Axioms:

A1: If φ is positive and φ necessarily entails ψ, then ψ is positive.
A2: If φ is positive, then its negation ¬φ is not positive.
A3: The property "being divine" (G) is positive.
A4: If φ is positive, then it is necessarily positive.
A5: Necessary existence is a positive property.

Definitions:
- D1: x is divine (Gx) ≡ all properties of x are positive
- D2: φ is an essence of x ≡ x has φ and every property of x follows necessarily from φ
- D3: x exists necessarily ≡ every essence of x is necessarily exemplified

Steps of Inference:

1. From A1 and A2: The system of positive properties is consistent
2. From A3: Divine existence is possible (◇∃xGx)
3. From A4 and definition of G: If God exists, then God has an essence
4. From A5 and previous steps: If God possibly exists, then God necessarily exists
5. From S5: What is possibly necessary is necessary
6. Conclusion: God necessarily exists (□∃xGx)

Main Technical Criticisms

First: Sobel's Modal Collapse (Sobel 1987)

Howard Sobel showed that with strong A2 (every property is either positive or its negation is positive), one can derive that all truths are necessary—a "modal collapse" where □p ↔ p for every proposition p. This makes modalities meaningless.

Technical proof: If every property or its negation is positive, and God possesses all positive properties and exists necessarily, then every truth becomes necessary because it follows from God's necessary existence.

Second: Problem of Incompatible Properties (Oppy 1995, 2000)

Graham Oppy asks: What guarantees that all positive properties are compatible? Two properties might both be "positive" in some sense, but a single being cannot possess both (such as "being unchangeable" and "being temporally active").

Third: Circularity of Defining Positiveness (Grim 2000)

Patrick Grim argues that the concept of "positive property" is not independently defined. If we define it based on what we want to prove about God, the proof becomes circular.

Fourth: Problem of Necessary Exemplification (Pruss 2009)

Even if we accept that God has an essence, why must this essence be "necessarily exemplified"? God might have an essence without this entailing necessary existence.

Developments and Responses

Anderson's Modification (1990): Removing strong A2 and replacing it with a weaker version that avoids Sobel's collapse. But this weakens the proof and requires additional axioms.

Bjørdal's Formulation (Bjørdal 2018): Using modal logic weaker than S5 to avoid collapse. But this weakens the final conclusion.

Computer Verification (Benzmüller & Paleo 2014): Using automated theorem proving systems (Isabelle/HOL) to verify formal validity. Confirmed the validity of inference but revealed extreme sensitivity to axioms.

Kovač's Formulation (Kovač 2003): Developing a version using "perfection" instead of "positiveness" and avoiding some criticisms. But it faces similar problems.

The Deeper Philosophical Problem

Behind the technicalities lies a philosophical question: Can formal logic prove real existence? Kant argued that existence is not a real predicate. Even if we accept that existence is a predicate in higher-order logic, the question remains: Is logical consistency sufficient for real existence?

Wittgenstein in his notes on Gödel (published 2016) points out that the proof might show the consistency of a certain concept of God, but cannot prove that this concept refers to reality.

Current Consensus (2024)

- Logicians: Appreciate the proof as a technical achievement but see its limitations
- Analytic philosophers: Divided between those who see value in formal formulation and those who find it misleading
- Theologians: Cautious about relying on a complex technical proof to establish God

From the Perspective of Rational Weighing (rajḥān ʿaqlī)

Gödel's proof shows the possibility of formally formulating ontological intuition, but it does not settle the debate. The real value:
- Clarifies the logical structure of the ontological argument
- Reveals implicit assumptions (especially about necessity and possibility)
- Shows the limits of formalization in metaphysics

The proof is technically successful within its limited scope, but "success" here does not mean proving God's existence, but proving the consistency of a certain concept of God within a certain logical system. The transition from logical consistency to real existence remains a philosophical leap requiring independent justification.

Where We Stand in This Debate Today

The period 2020-2026 has witnessed notable developments. Benzmüller continued expanding automated verification to include multiple versions of the proof in different modal systems (K, S4, S5), showing that results are extremely sensitive to the choice of underlying system—a minor modification in a single axiom produces radically different results. Cantini and Tedman (2021) presented alternative formulations that avoid Sobel's collapse without weakening the conclusion to the extent Anderson did. In contrast, Oppy (2020) developed his criticism to include what he calls the "equivalence problem": one can construct structurally similar proofs for contradictory beings, weakening the persuasive force of any formal ontological proof. Current debate centers on two questions: Can the concept of "positiveness" be defined non-circularly and non-arbitrarily? Does modal logic S5 reflect the true structure of metaphysical necessity or is it merely a formal tool? There is no consensus, but the prevailing assessment is that the proof is a highly significant technical achievement that reveals the structure of the ontological argument more than it settles it.

From the Perspective of Rational Weighing (rajḥān ʿaqlī)

Gödel's proof plays a specific role in the cumulative method that should neither be inflated nor diminished:
─ The proof establishes that the concept of a necessary perfect being is logically consistent within powerful formal systems. This is not trivial: many seemingly reasonable concepts turn out to be contradictory upon formalization.
─ Proving logical consistency removes an obstacle to theism (the claim that the concept of God is self-contradictory), but it does not prove real existence by itself.
─ The transition from consistency to existence requires independent data: the universe, fine-tuning, consciousness, objective morality. Here the value of accumulation becomes apparent.
─ The proof reveals that the weakest point in the ontological argument is not the inference but the metaphysical axioms—and this is a general methodological lesson.

Rational weighing (rajḥān ʿaqlī) says: Gödel's proof is a real building block in the cumulative construction, strengthening the reasonableness of theism without being sufficient alone to prove it. Its value is multiplied when paired with other data pointing in the same direction.

For Reading

- Kurt Gödel, "Ontological Proof" in Collected Works III (1995)
- C. Anthony Anderson, "Some Emendations of Gödel's Ontological Proof" (1990)
- Jordan Howard Sobel, Logic and Theism (2004), Ch. 6
- Graham Oppy, Ontological Arguments and Belief in God (1995)
- Benzmüller & Paleo, "Automating Gödel's Ontological Proof" (2014)
- Frode Bjørdal, "Understanding Gödel's Ontological Argument" (2018)
- Srećko Kovač, "Some Weakened Gödelian Ontological Systems" (2003)
- "Formulation: Modal Ontological Arguments" page on the website
- "Scholar: Kurt Gödel" page on the website