Gödel's Ontological Argument

Kurt Gödel, in Dana Scott's version

The argument is valid.

Every inference was checked by machine. All 2 objections are answered.

Open in the playground

flowchart TD
    classDef axiom fill:#f6efd9,stroke:#a8842a,color:#23212b;
    classDef premise fill:#e7edf7,stroke:#1f4e9c,color:#23212b;
    classDef deduction fill:#f3f4f1,stroke:#5b6b85,color:#23212b;
    classDef conclusion fill:#d6e1f3,stroke:#1f4e9c,stroke-width:3px,color:#23212b;
    classDef objection fill:#f7e3e1,stroke:#b3261e,color:#23212b;
    classDef reply fill:#f3f4f1,stroke:#7a5c2e,color:#23212b;
    classDef imported stroke-dasharray:4 3;
    classDef defeated fill:#f3f4f1,stroke:#b3261e,stroke-dasharray:6 3,color:#8a8796;
    classDef undecided stroke-dasharray:2 2;
    classDef overruled fill:#f3f4f1,stroke:#c9ccc6,color:#8a8796;
    Godel(["Godel: Kurt Gödel, Ontologischer Beweis, 1970"]):::axiom
    Scott(["Scott: Dana Scott, notes on Gödel's<br/>ontological proof, 1972"]):::axiom
    A1["<b>A1</b>: Necessarily, a property is positive<br/>exactly when its negation is not.<br/><i>□∀F:prop. Positive(λx. ¬F(x)) ↔<br/>¬Positive(F)</i>"]:::premise
    A2["<b>A2</b>: Necessarily, a property necessarily<br/>entailed by a positive property is<br/>positive.<br/><i>□∀F:prop. ∀H:prop. Positive(F) ∧<br/>□∀x. F(x) → H(x) → Positive(H)</i>"]:::premise
    A3["<b>A3</b>: Necessarily, being God-like (having<br/>every positive property) is positive.<br/><i>□Positive(G)</i>"]:::premise
    A4["<b>A4</b>: Necessarily, a positive property is<br/>necessarily positive.<br/><i>□∀F:prop. Positive(F) → □Positive(F)</i>"]:::premise
    A5["<b>A5</b>: Necessarily, necessary existence is<br/>positive.<br/><i>□Positive(NE)</i>"]:::premise
    T1["<b>T1</b>: A positive property is possibly<br/>exemplified.<br/><i>∀F:prop. Positive(F) → ◇∃x. F(x)</i>"]:::deduction
    Cor["<b>Cor</b>: Possibly, a God-like being exists.<br/><i>◇∃x. G(x)</i>"]:::deduction
    T2["<b>T2</b>: Necessarily, being God-like is the<br/>essence of any God-like being.<br/><i>□∀x. G(x) → Ess(G, x)</i>"]:::deduction
    T3["<b>T3</b>: Necessarily, a God-like being exists.<br/><i>□∃x. G(x)</i>"]:::conclusion
    O1{{"<b>O1</b>: Gödel never defines a positive<br/>property, so nothing guarantees the<br/>axioms describe anything coherent."}}:::objection
    R1{{"<b>R1</b>: Automated model finders have exhibited<br/>models of Scott's axioms (Benzmüller<br/>and Woltzenlogel Paleo, 2014), so they<br/>are consistent."}}:::reply
    O2{{"<b>O2</b>: Sobel showed that the axioms entail<br/>modal collapse: every truth becomes a<br/>necessary truth."}}:::objection
    R2{{"<b>R2</b>: Emended axiom systems, such as<br/>Anderson's, block the collapse while<br/>keeping the conclusion."}}:::reply
    class O1 overruled
    class O2 overruled
    Godel -.-> A1
    Scott -.-> A1
    Godel -.-> A2
    Scott -.-> A2
    Godel -.-> A3
    Scott -.-> A3
    Godel -.-> A4
    Scott -.-> A4
    Godel -.-> A5
    Scott -.-> A5
    A1 --> T1
    A2 --> T1
    T1 --> Cor
    A3 --> Cor
    A1 --> T2
    A4 --> T2
    Cor --> T3
    T2 --> T3
    A5 --> T3
    O1 -. objects .-> A1
    R1 -. replies .-> O1
    O2 -. objects .-> T3
    R2 -. replies .-> O2

Sources

Godel

Kurt Gödel, Ontologischer Beweis, 1970

Scott

Dana Scott, notes on Gödel's ontological proof, 1972

Definitions

G(x)

∀F:prop. Positive(F) → F(x)

Ess(F, x)

F(x) ∧ (∀H:prop. H(x) → □∀y. F(y) → H(y))

NE(x)

∀F:prop. Ess(F, x) → □∃y. F(y)

The argument

Objections and replies