Proving the existence of God using a computer

My friend and colleague George Constantinides wrote an interesting post on his blog recently where he formalises St Anselm’s argument for the existence of God. Since I’m teaching a course on the Isabelle proof assistant this term, I thought I’d see if I could recreate that argument using Isabelle.

Here goes…

theory God imports Main begin

(* We assume a fixed set of "beings". *)
typedecl Being

  (* Some beings exist in reality. The others
  exist only in the mind. *)
  fixes exists_in_reality :: "Being set"

  (* Suppose that the idea of "greatness" imposes
  a (strict) partial order on the set Being. That is, 
  some beings are greater than other beings. The 
  order is only partial, which means that it is 
  not always possible to compare the greatness of
  two beings. NB: strict partial order = 
  transitive + irreflexive. *)
  fixes greater_than :: "Being rel"
  assumes "trans greater_than"
  assumes "irrefl greater_than"

  (* We shall say that a being is godlike if
  there is no being that is greater than it. *)
  fixes godlike :: "Being set"
  assumes "∀b ∈ godlike. 
    ∄b'. (b',b) ∈ greater_than"

  (* The concept of god exists in the mind and 
  so is a member of Being. *)
  assumes "godlike ≠ {}"

  (* If two beings are identical except that one 
  exists in reality and one does not, then the 
  one that exists in reality is greater than the 
  one that doesn't. I've formalised a weaker 
  version: for every being that does not exist 
  in reality, there exists another being that 
  does exist in reality, and is greater. *)
  assumes "∀b. b ∉ exists_in_reality ⟶ 
    (∃b' ∈ exists_in_reality. 
      (b',b) ∈ greater_than)"

  (* God exists. *)
  shows "∃g ∈ godlike. g ∈ exists_in_reality"
  using assms by blast


As can be seen by the brevity of the final “using assms by blast” line, Isabelle didn’t have much trouble accepting this argument once all of the premises were laid out precisely. Then again, as for whether all of those premises are reasonable, I’m not so sure! I think St Anselm was taking some liberties in his original version, and I’m sure I’ve introduced some oversimplications in my own formulation.

Perhaps this is a theorem where a constructive proof would be more convincing…


4 thoughts on “Proving the existence of God using a computer”

  1. I clearly need to learn some Isabelle. Suggestions for a Quickstart tutorial?

    I think in your formulation, the transitive and irreflexive properties of greater_than are irrelevant to the argument, are they not?
    Because in the statement of your theorem, if g ∈ exists_in_reality were not true then by one of your assumptions, ∃b’. (b’,b) ∈ greater_than, right?. But this would contradict your other assumption ∀b ∈ godlike. ∄b’. (b’,b) ∈ greater_than.

    Also, can I not drop the ∃b’ ∈ exists_in_reality from one of your assumes and get away with the weaker ∀b. b ∉ exists_in_reality ⟶ (∃b’. (b’,b) ∈ greater_than)?

  2. Thanks George. Regarding Isabelle tutorials, I’m rather fond of this one.

    Yes you’re right that greater_than doesn’t need to be transitive or irreflexive for the proof to go through; I guess greater_than just felt like a partial order to me. And yes, it does indeed suffice to say that “if a being doesn’t exist in reality then there exists a greater being” without “… that does exist”. Having finished the proof I should have gone back to check whether any of my assumptions could be weakened or removed!

  3. Well I hear the author is a good bloke, so I’ll check it out. Thanks.

  4. Was pondering this phrase further this morning: “If two beings are identical except that one exists in reality and one does not”. Still not very sure I know what it means (I know you simplified it away).
    My thinking: can I imagine not just a unicorn u, but “a unicorn that exists-in-reality v”? I can imagine (an extension of) your construction saying “sure you can, but that doesn’t mean v exists in reality just because you imagined it to”. But on the other hand if I told you I can imagine not only a unicorn u but “a rainbow coloured unicorn v”, then it appears we’d this time accept that v is rainbow coloured given the interpretation of your Being set.
    I did a quick search on this question and found that — as with most interesting things — it appears Russell may have been here before us, and Kant before him 🙂 Will need to read:,

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s