theory God imports Main begin

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

theorem 
  (* 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 "\<forall>b \<in> godlike. 
    \<nexists>b'. (b',b) \<in> greater_than"

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

  (* 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 "\<forall>b. b \<notin> exists_in_reality \<longrightarrow> 
    (\<exists>b' \<in> exists_in_reality. 
      (b',b) \<in> greater_than)"

  (* God exists. *)
  shows "\<exists>g \<in> godlike. g \<in> exists_in_reality"
  using assms by blast

end