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

[Matt Diamond]

https://arxiv.org/abs/2202.06264

Neat paper! I put together a proof that combines some ideas in there:

import Mathlib

opaque individual : Type

abbrev property : Type := individual → Prop
abbrev metaproperty : Type := property → Prop

-- Positive
opaque P : metaproperty
-- God-like
opaque G : property

notation "~" p => Not ∘ p

-- Either a property or its negation is positive, but not both
axiom axiom_1 : ∀ (ϕ : property), P (~ϕ) ↔ ¬P ϕ

-- A property entailed by a positive property is positive
axiom axiom_2 : ∀ ϕ ψ, (P ϕ ∧ (∀ x, (ϕ x → ψ x))) → P ψ

-- being God-like is a Positive property
axiom axiom_3 : P G

lemma not_top_eq_bot : (¬⊤) = ⊥ :=
by rw [Prop.top_eq_true, Prop.bot_eq_false, not_true_eq_false]

theorem empty_property_not_positive : ¬P (fun _ => ⊥) :=
by
  intro h1
  have h2 : P (fun _ => ⊤)
  · apply axiom_2 (fun _ => ⊥) _
    use h1
    intros
    trivial
  have h3 := axiom_1 (fun _ => ⊤)
  rw [Function.comp_def, not_top_eq_bot] at h3
  rw [h3] at h1
  exact h1 h2

theorem all_positive_properties_exemplified : P ϕ → ∃ x, ϕ x := by
  intro ϕ_pos
  by_contra h
  apply empty_property_not_positive
  apply axiom_2 ϕ _
  use ϕ_pos
  intros x hx
  exact (h ⟨x, hx⟩).elim

theorem god_exists : ∃ x, G x := all_positive_properties_exemplified axiom_3

[Matt Diamond]

axiom_2 is pretty obviously the weak point... this shouldn't convince anyone but it was a fun little exercise

[Kyle Miller]

@Matt Diamond That's fun. I've switched it over to the language of sets. There, it's sort of like that P has most of the axioms of an ultrafilter. axiom_2 is "upwards closed", axiom_3 is "nonempty", and axiom_1 is the ultrafilter property. What's missing is that pairwise intersections of positive properties are still positive. Even without it, the point is that the ultrafilter property implies that the empty set can't be in it, since it contradicts upwards closure applied to nonemptiness. Hence the G set is nonempty.

import Mathlib

opaque individual : Type

abbrev property : Type := Set individual
abbrev metaproperty : Type := Set property

-- Positive
opaque P : metaproperty
-- God-like
opaque G : property

-- Either a property or its negation is positive, and not both
axiom axiom_1 : ∀ (ϕ : property), P ϕᶜ ↔ ¬P ϕ

-- A property entailed by a positive property is positive
axiom axiom_2 : ∀ ϕ ψ, ϕ ⊆ ψ → P ϕ → P ψ

-- being God-like is a Positive property
axiom axiom_3 : P G

theorem univ_positive : P Set.univ :=
  axiom_2 G _ (Set.subset_univ _) axiom_3

theorem empty_property_not_positive : ¬P ∅ := by
  rw [← axiom_1, Set.compl_empty]
  exact univ_positive

theorem all_positive_properties_exemplified {ϕ : property} (hϕ : P ϕ) : ϕ.Nonempty := by
  by_contra! h
  cases h
  exact empty_property_not_positive hϕ

theorem god_exists : G.Nonempty := all_positive_properties_exemplified axiom_3

[Matt Diamond]

nice!

[Johan Commelin]

In the paper, it seems that G is a definition, instead of an axiom.

[David Michael Roberts]

I was thinking about how this works in constructive logic and you get a "not-not-exists" in that setting.

[Matt Diamond]

so constructively we can't prove God exists, but we can disprove atheism :big_smile:

[Matt Diamond]

@Johan Commelin re: the definition, that's true... I left it out because it was irrelevant to the proof

[Johan Commelin]

Fair enough. The benefit of defining it, is that it is one less axiom to dispute.

[Johan Commelin]

Matt Diamond said:

so constructively we can't prove God exists, but we can disprove atheism :big_smile:

Fun fact: there is a subfield of theology known as apophatic theology or negative theology (https://en.wikipedia.org/wiki/Apophatic_theology). It focuses on describing what God is not, as opposed to describing what God is.

For we explain not what God is but candidly confess that we have not exact knowledge concerning Him. For in what concerns God to confess our ignorance is the best knowledge

(Quoting Saint Cyril of Jerusalem, via the Wiki page.)

[Johan Commelin]

(Full disclosure: I believe in God. I also think that ontological arguments and existence-of-God proofs are missing the point.)

[Jeremy Tan]

(I believe that God does not exist)

[David Michael Roberts]

Amusingly, Anselm used the phrase "it cannot be nonexistent" (albeit not in English, of course....)

[Kyle Miller]

Matt Diamond said:

I left it out because it was irrelevant to the proof

I just looked at the paper, and it seems that this formalization is dropping the modal operators. This might be the proof if your modal operators have "modal collapse"?

If I understand it right, then this formalization is essentially adding in the additional hypothesis that we only care about this world and no other possible worlds.