Formalizing St. Anselm's ontological argument

Stream: general

[Bulhwi Cha]

This might be the first second attempt in the Lean community to formalize an ontological argument for the existence of God in Lean. It's a modified version of the formulation of St. Anselm's ontological argument by Alvin Plantinga. (See 9.1 Formulation 1 of the SEP entry "Ontological Arguments.")

1. God exists in the understanding but not in reality. (Assumption for reductio)
2. Existence in reality is greater than existence in the understanding alone. (Premise)
3. There exists a being in reality that can be conceived. (Modified premise)
4. A being that exists in reality and can be conceived is greater than God. (From (1) and (2).)
5. There exists a being that can be conceived and is greater than God. (From (3) and (4).)
6. No being greater than God can be conceived. (From the definition of “God”.)
7. Hence, it is false that God exists in the understanding but not in reality. (From (1), (5), (6).)
8. God exists in the understanding. (Premise, to which even the Fool agrees.)
9. Hence God exists in reality. (From (7), (8).)

• Git repository: https://git.sr.ht/~chabulhwi/lean-notes
• Lean code: https://git.sr.ht/~chabulhwi/lean-notes/tree/master/item/Notes/Anselm.lean
• English documentation: https://git.sr.ht/~chabulhwi/lean-notes/tree/master/item/docs/en/Anselm.md
• Korean documentation: https://git.sr.ht/~chabulhwi/lean-notes/tree/master/item/docs/ko/Anselm.md

Lean code (flawed)

import Mathlib.Order.Basic

section

variable {α : Type u} [LinearOrder α]

def isMax (x : α) (p : α → Prop) := p x ∧ ∀ {y : α}, p y → y ≤ x

theorem isMax_unique {x y : α} (p : α → Prop) : isMax x p ∧ isMax y p → x = y := by
  intro ⟨hx, hy⟩
  have x_le_y : x ≤ y := hy.2 hx.1
  have y_le_x : y ≤ x := hx.2 hy.1
  exact le_antisymm x_le_y y_le_x

end

theorem isMax_property (α : Type u) [LinearOrder α] {x : α} (p q : α → Prop) (hmx : isMax x p)
    (hlt : ∀ {y : α}, ¬ q x → q y → x < y) (hex : ∃ (y : α), p y ∧ q y) : q x := by
  have hnnqx : ¬¬ q x := by
    intro hnqx
    rcases hex with ⟨y, hpy, hqy⟩
    have x_lt_y : x < y := hlt hnqx hqy
    have y_le_x : y ≤ x := hmx.2 hpy
    exact not_le_of_lt x_lt_y y_le_x
  exact of_not_not hnnqx

namespace Anselm

class Conceivable (α : Sort u) where
  conceivable : α → Prop

export Conceivable (conceivable)

class InUnderstanding (α : Sort u) where
  inUnderstanding : α → Prop

export InUnderstanding (inUnderstanding)

class InReality (α : Sort u) where
  inReality : α → Prop

export InReality (inReality)

variable {Being : Type u} [LinearOrder Being] [Conceivable Being] [InUnderstanding Being]
  [InReality Being]

def isGod (x : Being) : Prop := isMax x conceivable

axiom lt_of_inUnderstanding_not_inReality_inReality {x y : Being} : inUnderstanding x →
  ¬ inReality x → inReality y → x < y

axiom isGod_inUnderstanding : ∀ {x : Being}, isGod x → inUnderstanding x

axiom exists_conceivable_and_inReality : ∃ (x : Being), conceivable x ∧ inReality x

theorem isGod_inReality : ∀ {x : Being}, isGod x → inReality x := by
  intro x hgx
  refine isMax_property Being conceivable inReality hgx ?_ ?_
  · intro y
    exact lt_of_inUnderstanding_not_inReality_inReality (isGod_inUnderstanding hgx)
  · exact exists_conceivable_and_inReality

#print axioms isGod_inReality
/- 'Anselm.isGod_inReality' depends on axioms: [Classical.choice, Quot.sound, propext,
Anselm.lt_of_inUnderstanding_not_inReality_inReality, Anselm.isGod_inUnderstanding,
Anselm.exists_conceivable_and_inReality] -/

end Anselm

Reference

Oppy, Graham, "Ontological Arguments", The Stanford Encyclopedia of Philosophy (Fall 2023 Edition), Edward N. Zalta & Uri Nodelman (eds.), URL = <https://plato.stanford.edu/archives/fall2023/entries/ontological-arguments/>.

[Bulhwi Cha]

I'll write more messages later. I don't think St. Anselm's demonstrates shows God's existence.

[Eric Wieser]

Unfortunately this argument is contradictory as formalized:

example : False :=
  letI : Conceivable Unit := ⟨fun _ => True⟩
  letI : InUnderstanding Unit := ⟨fun _ => False⟩
  isGod_inUnderstanding (x := ()) ⟨trivial, fun _ => trivial⟩

[Damiano Testa]

Rather than "unfortunately", I guess you meant "and hence the proof of existence of God is complete", right?

[Eric Wieser]

Of course, what I should have said is "here's a much shorter proof":

def key :=
  letI : Conceivable Unit := ⟨fun _ => True⟩
  letI : InUnderstanding Unit := ⟨fun _ => False⟩
  isGod_inUnderstanding (x := ()) ⟨trivial, fun _ => trivial⟩

theorem isGod_inReality : ∀ {x : Being}, isGod x → inReality x := key.elim
theorem not_isGod_inReality : ∀ {x : Being}, isGod x → ¬inReality x := key.elim

[Bulhwi Cha]

@Eric Wieser What if I remove variable {Being : Type u} and add the axiom axiom Being.{u} : Type u?

Fixed code (still flawed)

import Mathlib.Order.Basic

section

variable {α : Type u} [LinearOrder α]

def isMax (x : α) (p : α → Prop) := p x ∧ ∀ {y : α}, p y → y ≤ x

theorem isMax_unique {x y : α} (p : α → Prop) : isMax x p ∧ isMax y p → x = y := by
  intro ⟨hx, hy⟩
  have x_le_y : x ≤ y := hy.2 hx.1
  have y_le_x : y ≤ x := hx.2 hy.1
  exact le_antisymm x_le_y y_le_x

end

theorem isMax_property (α : Type u) [LinearOrder α] {x : α} (p q : α → Prop) (hmx : isMax x p)
    (hlt : ∀ {y : α}, ¬ q x → q y → x < y) (hex : ∃ (y : α), p y ∧ q y) : q x := by
  have hnnqx : ¬¬ q x := by
    intro hnqx
    rcases hex with ⟨y, hpy, hqy⟩
    have x_lt_y : x < y := hlt hnqx hqy
    have y_le_x : y ≤ x := hmx.2 hpy
    exact not_le_of_lt x_lt_y y_le_x
  exact of_not_not hnnqx

namespace Anselm

class Conceivable (α : Sort u) where
  conceivable : α → Prop

export Conceivable (conceivable)

class InUnderstanding (α : Sort u) where
  inUnderstanding : α → Prop

export InUnderstanding (inUnderstanding)

class InReality (α : Sort u) where
  inReality : α → Prop

export InReality (inReality)

axiom Being.{u} : Type u

variable [LinearOrder Being] [Conceivable Being] [InUnderstanding Being] [InReality Being]

def isGod (x : Being) : Prop := isMax x conceivable

axiom lt_of_inUnderstanding_not_inReality_inReality {x y : Being} : inUnderstanding x →
  ¬ inReality x → inReality y → x < y

axiom isGod_inUnderstanding : ∀ {x : Being}, isGod x → inUnderstanding x

axiom exists_conceivable_and_inReality : ∃ (x : Being), conceivable x ∧ inReality x

theorem isGod_inReality : ∀ {x : Being}, isGod x → inReality x := by
  intro x hgx
  refine isMax_property Being conceivable inReality hgx ?_ ?_
  · intro y
    exact lt_of_inUnderstanding_not_inReality_inReality (isGod_inUnderstanding hgx)
  · exact exists_conceivable_and_inReality

#print axioms isGod_inReality
/- 'Anselm.isGod_inReality' depends on axioms: [Anselm.Being, Classical.choice, Quot.sound, propext,
Anselm.lt_of_inUnderstanding_not_inReality_inReality, Anselm.isGod_inUnderstanding,
Anselm.exists_conceivable_and_inReality] -/

end Anselm

[Eric Wieser]

Nope:

def key : False :=
  letI : Conceivable Being.{0} := ⟨fun _ => False⟩
  letI : InReality Being := ⟨fun _ => False⟩
  let ⟨b, h⟩ := exists_conceivable_and_inReality
  h.2.elim

theorem isGod_inReality : ∀ {x : Being}, isGod x → inReality x := key.elim
theorem not_isGod_inReality : ∀ {x : Being}, isGod x → ¬inReality x := key.elim

[Bulhwi Cha]

Hmm, I should understand how letI works. After all, It's just an exercise. Thanks anyway.

[Damiano Testa]

Gödel also had a proof of existence of God: maybe we should have a God folder in Mathlib.

[Eric Wieser]

letI is irrelevant here, this works fine without it:

def key : False :=
  let ⟨b, h⟩ := @exists_conceivable_and_inReality.{0} ⟨fun _ => False⟩ ⟨fun _ => False⟩
  h.2.elim

[Bulhwi Cha]

I actually want to make a counterargument to St. Anselm's argument. But I guess I can't formalize the modified version of the proof correctly in Lean.

[Bulhwi Cha]

Will replacing type classes with axioms fix my formalization?

[Eric Wieser]

I think so, but it would probably be better to put the axioms in a typeclass instead

[Eric Wieser]

If you use axioms, then if they're false you can prove anything. If you use a typeclass and get something wrong, you can prove that the typeclass cannot exist but it doesn't break trust anywhere else

[Bulhwi Cha]

Eric Wieser said:

I think so, but it would probably be better to put the axioms in a typeclass instead

Okay, I'll try that!

[Bulhwi Cha]

I made a new type class, Anselm:

class Anselm (Being : Type u) extends LinearOrder Being where
  conceivable : Being → Prop
  inUnderstanding : Being → Prop
  inReality : Being → Prop
  lt_of_inUnderstanding_not_inReality_inReality {x y : Being} : inUnderstanding x → ¬ inReality x →
    inReality y → x < y
  isMax_conceivable_inUnderstanding {x : Being} : isMax x conceivable → inUnderstanding x
  exists_conceivable_and_inReality : ∃ (x : Being), conceivable x ∧ inReality x

Fixed code (final)

import Mathlib.Order.Basic

section

variable {α : Type u} [LinearOrder α]

def isMax (x : α) (p : α → Prop) := p x ∧ ∀ (y : α), p y → y ≤ x

theorem isMax_unique {x y : α} (p : α → Prop) : isMax x p ∧ isMax y p → x = y := by
  intro ⟨hx, hy⟩
  have x_le_y : x ≤ y := hy.2 x hx.1
  have y_le_x : y ≤ x := hx.2 y hy.1
  exact le_antisymm x_le_y y_le_x

theorem isMax_mt {x y : α} (p : α → Prop) (hmx : isMax x p) (hlt : x < y) : ¬ p y :=
  mt (hmx.2 y) (not_le_of_lt hlt)

end

theorem isMax_property (α : Type u) [LinearOrder α] {x : α} (p q : α → Prop) (hmx : isMax x p)
    (hlt : ∀ {y : α}, ¬ q x → q y → x < y) (hex : ∃ (y : α), p y ∧ q y) : q x := by
  have hnnqx : ¬¬ q x := by
    intro hnqx
    rcases hex with ⟨y, hpy, hqy⟩
    have x_lt_y : x < y := hlt hnqx hqy
    have y_le_x : y ≤ x := hmx.2 y hpy
    exact not_le_of_lt x_lt_y y_le_x
  exact of_not_not hnnqx

class Anselm (Being : Type u) extends LinearOrder Being where
  conceivable : Being → Prop
  inUnderstanding : Being → Prop
  inReality : Being → Prop
  lt_of_inUnderstanding_not_inReality_inReality {x y : Being} : inUnderstanding x → ¬ inReality x →
    inReality y → x < y
  isMax_conceivable_inUnderstanding {x : Being} : isMax x conceivable → inUnderstanding x
  exists_conceivable_and_inReality : ∃ (x : Being), conceivable x ∧ inReality x

namespace Anselm

variable {Being : Type u} [Anselm Being]

def isGod (x : Being) := isMax x conceivable

theorem isGod_unique {x y : Being} : isGod x ∧ isGod y → x = y := isMax_unique conceivable

theorem isGod_mt {x y : Being} (hgx : isGod x) (hlt : x < y) : ¬ conceivable y :=
  isMax_mt conceivable hgx hlt

theorem isGod_inUnderstanding {x : Being} : isGod x → inUnderstanding x :=
  isMax_conceivable_inUnderstanding

theorem isGod_conceivable {x : Being} : isGod x → conceivable x := And.left

theorem isGod_inReality {x : Being} (hgx : isGod x) : inReality x := by
  refine isMax_property Being conceivable inReality hgx ?_ ?_
  · intro y
    exact lt_of_inUnderstanding_not_inReality_inReality (isGod_inUnderstanding hgx)
  · exact exists_conceivable_and_inReality

#print axioms isGod_inReality
-- 'Anselm.isGod_inReality' depends on axioms: [Classical.choice, Quot.sound, propext]

end Anselm

[Bulhwi Cha]

Bulhwi Cha said:

3. There exists a being in reality that can be conceived. (Modified premise)

Step 3 of the original formulation by Alvin Plantinga is the following premise: "A being having all of God’s properties plus existence in reality can be conceived." This premise is redundant. Since God is the greatest being that can be conceived, God itself can be conceived. Therefore, a being having all of God's properties can be conceived.

theorem isGod_conceivable {x : Being} : isGod x → conceivable x := And.left

[Bulhwi Cha]

I think we can only conclude from St. Anselm's argument that the following statement is true:

theorem isGod_inReality {x : Being} : isGod x → inReality x

This theorem doesn't state that God exists in reality. It merely says that if a being is God, it exists in reality. In order to prove the existence of God in reality, you need to show that ∃ (x : Being), isGod x ∧ inReality x.

For this reason, I think St. Anselm's argument doesn't show God's existence. Of course, I might have formalized it wrong.

[Chris Hughes]

The existence of god has been proven in Isabelle. Google shows me a couple of formalisations. But IIRC, there was some problem with the hypotheses being inconsistent, similar to what Eric found.

[Bulhwi Cha]

Thanks. I'll check those out when I have more time. I hope we see a future where more philosophers try out Lean and use it to formalize subdisciplines of philosophy.

[Ruben Van de Velde]

I have a feeling we already have plenty of doctors of philosophy here

[Alistair Tucker]

Bulhwi Cha said:

Step 3 of the original formulation by Alvin Plantinga is the following premise: "A being having all of God’s properties plus existence in reality can be conceived." This premise is redundant. Since God is the greatest being that can be conceived, God itself can be conceived. Therefore, a being having all of God's properties can be conceived.

The way I see it, we are being asked to conceive of beings with a separated property of existence/nonexistence in reality, for which we may use a Bool. Then premise 3 does have content:

class Anselm (Being : Type u) extends LinearOrder (Being × Bool) where
  Conceivable : Being × Bool → Prop
  premise3 : ∀ x : Being × Bool, IsMax x Conceivable → Conceivable (x.1, true)

[Alistair Tucker]

The ordering on Being × Bool also makes it possible to transcribe premise 2 more faithfully

  premise2 : ∀ x : Being, (x, false) < (x, true)

[Bulhwi Cha]

@Alistair Tucker If we adopt your view, inReality should also be a predicate on Being × Bool, not Being.

def inReality (x : Being × Bool) := x.2 = true

Then we can't say that "Bulhwi exists in reality," since I'm not a pair of a being and its existence property. I'm a being. So I think inReality should be a predicate on Being.

[Alistair Tucker]

Bulhwi Cha said:

Then we can't say that "Bulhwi exists in reality," since I'm not a pair of a being and its existence property. I'm a being. So I think inReality should be a predicate on Being.

I don't understand this point. You may well be a hallucination of mine i.e. (bulhwi, false). If not then (bulhwi, true).

[Bulhwi Cha]

My point is that Bulhwi is neither ⟨Bulhwi, true⟩ nor ⟨Bulhwi, false⟩. I'm a being, not a pair of a being and its existence property. Bulhwi's type is and should be Being, not Being × Bool.

[Alistair Tucker]

Well you need some way to map between an object not having the existence property to one that does, which currently you don't have.

[Bulhwi Cha]

How would you do that?

[Alistair Tucker]

I have outlined one way. I'm sure there are others.

[Bulhwi Cha]

I don't feel like creating a type, say, BeingNoExist, of "beings separated from their existence properties" and considering the type Being to be equal to BeingNoExist × Bool. It presupposes that ∃ (α : Type u), Being = α × Bool.

[Hypatia du Bois-Marie]

I was thinking of something similar this week! https://github.com/analytic-bias/agora

[Hypatia du Bois-Marie]

Eric Wieser said:

Unfortunately this argument is contradictory as formalized:

example : False :=
  letI : Conceivable Unit := ⟨fun _ => True⟩
  letI : InUnderstanding Unit := ⟨fun _ => False⟩
  isGod_inUnderstanding (x := ()) ⟨trivial, fun _ => trivial⟩

I think that's exactly the point: formal methods yielding fierce recognition of human fallacies.

[Bulhwi Cha]

Bulhwi Cha said:

I think we can only conclude from St. Anselm's argument that the following statement is true:

theorem isGod_inReality {x : Being} : isGod x → inReality x

A user of a Korean-speaking philosophy discussion forum said, "You didn't prove that ∃ (x : Being), isGod x ∧ inReality x is not a theorem of a theory whose axioms are the premises of St. Anselm's argument (and the axioms of Lean's type theory)."

[Bulhwi Cha]

That's true. So I'll rephrase my opinion:

I think the conclusion of St. Anselm's argument is the following statement:

theorem isGod_inReality {x : Being} : isGod x → inReality x

[Uranus Testing]

Interesting to see another approach to the ontological proof. I tried once (original version was written in Lean 3, later ported to 4) “classical” modal version: https://github.com/forked-from-1kasper/ground_zero/blob/9f83f7c6224eee8905b16aeebc4c234b4b216031/GroundZero/Theorems/Ontological.lean#L520-L521

[Uranus Testing]

Chris Hughes said:

The existence of god has been proven in Isabelle. Google shows me a couple of formalisations. But IIRC, there was some problem with the hypotheses being inconsistent, similar to what Eric found.

There are actually several versions of original Gödel’s proof that correct this issue.

[David Michael Roberts]

Cf https://arxiv.org/abs/2202.06264