Skip to content

Latest commit

 

History

History
101 lines (80 loc) · 4.43 KB

Anselm.md

File metadata and controls

101 lines (80 loc) · 4.43 KB
Raw

St. Anselm's ontological argument

The Anselm file 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).)

I formalized the three premises of the argument as follows:

  • lt_of_inUnderstanding_not_inReality_inReality {x y : Being} : InUnderstanding x → ¬InReality x → InReality y → x < y (Step 2)
  • exists_conceivable_and_inReality : ∃ (x : Being), Conceivable x ∧ InReality x (Step 3)
  • IsGod.inUnderstanding {x : Being} : IsGod x → InUnderstanding x (Step 8)

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.

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

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.

Theorem not_exists_int_isGod

A user named car_nap of Owl of Sogang, a Korean-speaking philosophy discussion forum, pointed out (in Korean) that I didn't prove that the statement ∃ (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).

So I proved a theorem named not_exists_int_isGod, which shows that there exist a universe level u, a type Being : Type u, and an instance of Anselm Being where the statement ∃ (x : Being), IsGod x is false.

Reference

Acknowledgements

The Lean community

I'd like to thank Eric Wieser and Alistair Tucker. Eric Wieser found inconsistency in my first and second drafts. Alistair Tucker commented on transcribing premise 3 of the original formulation by Alvin Plantinga. You can see my discussion with them in this link.

Alistair Tucker also told me how to prove that we can't deduce the statement ∃ (x : Being), IsGod x ∧ InReality x from the premises of St. Anselm's argument and the axioms of Lean's type theory.

Owl of Sogang

I want to thank car_nap for raising the issue mentioned above.