Quelle  AnselmGod.thy

section ‹Introduction›

theory AnselmGod
imports Main
begin

text ‹This paper presents an automated verification of Anselm's ontological argument, as
  by Paul Oppenheimer and Edward Zalta cite‹"oppenheimer_logic_1991"›, in
 /HOL, an interactive theorem prover for higher-order logic. Previously, the argument has being
  by Oppenheimer and Zalta in Prover9 cite‹"oppenheimer_computationally-discovered_2011"›,
  automated theorem prover for first-order logic, and by John Rushby in PVS
 cite‹"rushby_ontological_2013"›, an automated theorem prover for higher-order logic. Automations of
  versions of the argument include cite‹"benzmuller_godels_2013"›, cite‹"rushby_mechanized_2016"›
  cite‹"fuenmayor_types_2017"›. My purpose here is to present a basis for comparison in the spirit
  cite‹"wiedijk_seventeen_2006"›, which compares automated proofs of the irrationality
  $\sqrt 2$.›

text ‹Oppenheimer and Zalta's reconstruction is based on the idea of treating `that than
  nothing greater can be conceived' as a definite description, and treating definite
  as singular terms. But in Isabelle/HOL all terms, including definite descriptions,
  assumed to denote. So the main task is to embed a free logic for definite descriptions within
 /HOL. (Previously, a free logic has been embedded into Isabelle/HOL by Christoph
  and Dana Scott cite‹"benzmuller_automating_2016"›. But theirs differs from Zalta
  Oppenheimer's in several ways). Once Isabelle/HOL is equipped with free definite descriptions,
  the argument is straightforward.›

section ‹Free Logic›

text ‹Isabelle treats definite descriptions as singular terms of the form @{term "THE x. φ x"}.
 , all terms in Isabelle are assumed to denote, and so from universal elimination we have
  validity of the argument form:›

lemma "∀ x. ψ x ==> ψ (THE x. φ x)" by (rule allE)

text ‹In the presence of definite descriptions which do not denote, this argument form is invalid;
  example, from `everyone has hair' we should not infer `the present King of France has hair',
  the present King of France does not exist.›

text ‹This problem can be avoided by introducing a null individual @{term "n"} to serve as the
  of non-denoting definite descriptions, as follows:›

typedecl i ― ‹the type of individuals›
consts n:: "i" (‹n›) ― ‹the null individual›

text ‹Then the universal and particular quantifiers can be restricted to
  excluding the null-individual as follows, where the new free quantifiers
  distinguished from the classical quantifiers by bold type:›
abbreviation universal_quantifier:: "(i ==> bool) ==> bool" (‹\∀›) 
  where "\<forall> φ ≡ ∀x::i. (¬ x = n ⟶ φ x)"
abbreviation universal_syntax:: "(i ==> bool) ==> bool" (binder ‹\∀› [8] 9)
  where "\<forall> x. φ x ≡ \<forall> φ"

abbreviation particular_quantifier:: "(i ==> bool) ==> bool" (‹\∃›)
  where "\<exists> φ ≡ ∃x::i. (x ≠ n ∧ φ x)"
abbreviation particular_syntax:: "(i ==> bool) ==> bool" (binder ‹\∃› [8] 9)
  where "\<exists> x. φ x ≡ \<exists> φ"    
text ‹Note that the quantifiers here range over both existent and non-existent individuals, whereas
  quantifiers in cite‹"benzmuller_automating_2016"› range only over existent individuals.›

text ‹In the free logic employed by Oppenheimer and Zalta, statements of identity in which terms
  not denote are always false cite‹"oppenheimer_logic_1991"›, p. 511. So the domain of the identity
  should be restricted to exclude the null-individual:›

abbreviation identity:: "i ==> i ==> bool" (‹is›)
  where "is x y ≡ x ≠ n ∧ x = y"
abbreviation identity_syntax:: "i ==> i ==> bool" (infix ‹=› 50 )
  where "x = y ≡ is x y"

text ‹Once identity is introduced, the uniqueness quantifier can then be defined in the usual way:›
abbreviation uniqueness_quantifier:: "(i ==> bool) ==> bool" (‹unique›)
 where "unique φ ≡ (\<exists> x::i. φ x ∧ (\<forall> y::i. φ y ⟶ x = y))"
abbreviation uniqueness_syntax:: "(i ==> bool) ==> bool" (binder ‹unique› [8] 9)
  where "unique x. φ x ≡ unique φ"

text ‹Finally, the logic employed by Oppenheimer and Zalta is a negative free logic, in that
  of atomic predicates to non-denoting terms are always false
 cite‹"oppenheimer_logic_1991"›, p. 511. So it's necessary to introduce a higher-order predicate
  between atomic and non-atomic predicates, and to introduce an axiom stipulating that
  atomic predicate is true of the null individual:›

consts atomic_predicates:: "(i ==> bool) ==> bool " (‹atomic›)
axiomatization where negativity_constraint: "atomic φ ==> ¬ φ n"

text ‹In addition, it has to be stated that identity is atomic:›
axiomatization where identity_atomic: "∧ x. atomic (is x)"

text ‹One of the most controversial premises of the ontological argument is that `exists'
  a genuine or atomic predicate. But surprisingly, we shall see below that the argument
  not require this premise.›

section ‹Definite Descriptions›

text ‹The main idea of Oppenheimer and Zalta's reconstruction of the ontological argument is to
  definite descriptions as genuine singular terms, which leads to the following syntax in
 /HOL:›
consts definite_description:: "(i ==> bool) ==> i" (‹\τ›)
abbreviation description_syntax:: "(i ==> bool) ==> i" (binder ‹\τ› [8] 9)
where "\<tau> x. φ x ≡ \<tau> φ"

text ‹In Oppenheimer and Zalta's reconstruction of the argument, definite descriptions
  governed by the Russellian axiom schema cite‹"oppenheimer_logic_1991"›, p. 513:›
axiomatization where description_axiom:
"atomic ψ ==> ψ (\<tau> x. φ x) ≡ (\<exists> x. φ x ∧ (\<forall> y. φ y ⟶ x = y) ∧ ψ x)"

text ‹From this axiom schema, Oppenheimer and Zalta derive two intermediary theorems
 to be used in the reconstruction of their argument cite‹"oppenheimer_logic_1991"›, pp. 513-4.
  to the first:›
theorem  description_theorem_1: "unique x. φ x ==> \<exists> y. y = (\<tau> x. φ x)"
using description_axiom identity_atomic by blast

text ‹The second theorem follows directly from the following lemma:›

lemma lemma_1: "a = (\<tau> x. φ x) ==> φ (\<tau> x. φ x)"
using description_axiom identity_atomic by blast

theorem description_theorem_2: "\<exists> x. x = (\<tau> x. φ x) ==> φ (\<tau> x. φ x)"
by (simp add: lemma_1)

text ‹In the course of verifying the argument using Prover9, Oppenheimer and Zalta discovered
  simplified proof which uses instead cite‹"oppenheimer_computationally-discovered_2011"›, p. 345:›
theorem description_theorem_3:
"atomic ψ ==> ψ (\<tau> x. φ x) ==> \<exists> y. y = (\<tau> x. φ x)" 
using negativity_constraint by fastforce

text ‹Notice that it is only this last theorem which presupposes the negativity constraint,
  the first two theorems depend only on the atomicity of identity.›

section ‹Anselm's Argument›

text ‹The argument proper employs the following non-logical vocabulary:›
consts existence:: "i ==> bool" (‹E›) ― ‹exists in reality›
consts greater_than:: "i==>i==>bool" (‹G›) ― ‹is greater than›
consts conceivable:: "i==>bool" (‹C›) ― ‹exists in the understanding›
text ‹Note that @{term "E a"} is not intended by Oppenheimer and Zalta to be equivalent to
 {term "\∃ x. a = x"} since according to their reading of the argument, some things do not exist
  reality cite‹"oppenheimer_logic_1991"›, p. 514.›

text ‹Finally, the presentation of the argument is simplified by introducing
  following abbreviation for the predicate `is a being greater than which none can be conceived':›
abbreviation none_greater_than :: "i==>bool" (‹Φ›)
where "Φ x ≡ (C x ∧ ¬(\<exists> y. G y x ∧ C y))"
  
text ‹With this vocabulary in place, a name for God can be introduced as an abbreviation
  the description `the being greater than which none can be conceived':›

definition g :: "i" where "g ≡ (\<tau> x. Φ x)"

text ‹In Oppenheimer and Zalta's presentation every name is assumed to denote, so a name for
  cannot be introduced until it is proved that the description @{term "(\τ x. Φ x)"} denotes
 cite‹"oppenheimer_logic_1991"›, p, 520. But since it's not assumed in this presentation that every
  denotes or, in other words, since it's not assumed that no names denote the null individual,
 it's not necessary to postpone this step.›

text ‹The final quasi-logical premise in Oppenheimer and Zalta's reconstruction of the argument
  the connectivity of `is greater than', which is used in the proof of the following lemma
 cite‹"oppenheimer_logic_1991"›, p. 518:›
  
lemma lemma_2:
  assumes connectivity: "\<forall> x. \<forall> y. G x y ∨ G y x ∨ x = y"
  shows "\<exists> x. Φ x ==> unique x. Φ x"
  using connectivity by blast 

text ‹Note that ‹connectivity› disallows any ties with respect to greatness. This is
 , since you and I, for example, may be equally great, without being the same person. So
 ‹connectivity› should not be thought of as merely stipulative, and a weaker premise would
  desirable.›    
    
text ‹With this vocabulary in place, Anselm's ontological argument, as reconstructed by
  and Zalta, can be stated as follows:›
theorem 
  assumes premise_1:  "\<exists> x. Φ x"
 ― ‹there exists in the understanding a being greater than which
  can be conceived›
and premise_2:  "¬ E (\<tau> x. Φ x) ⟶ (\<exists> y. G y (\<tau> x. Φ x) ∧ C y)"
 ― ‹if the being greater than which none can be conceived does not exist in reality,
  a being exists in the understanding which is greater than the being greater than
  none can be conceived›
and connectivity: "\<forall> x. \<forall> y. G x y ∨ G y x ∨ x = y"
shows "E g" ― ‹God exists.›

  text ‹Isabelle can verify the argument in one line with the command ‹using premise_1 premise_2 connectivity lemma_1 g_def description_theorem_1 by smt›.
  since proofs in Isabelle using ‹smt› are currently considered impermanent, I instead give Zalta
  Oppenheimer's handwritten proof cite‹"oppenheimer_computationally-discovered_2011"›, p. 337:›
proof (rule ccontr)
  assume atheism: "¬ E g"
  from premise_1 and connectivity and lemma_2 have "unique x. Φ x" by simp
  with description_theorem_1 have "\<exists> y. y = (\<tau> x. Φ x)" by simp
  with description_theorem_2 have "Φ (\<tau> x. Φ x)" by simp
  hence god_is_greatest: "¬(\<exists> y. G y (\<tau> x. Φ x) ∧ C y)" by (rule conjE)
  from  atheism and premise_2 and g_def have "(\<exists> y. G y (\<tau> x. Φ x) ∧ C y)" by simp
  with god_is_greatest show False..
qed  
text ‹Note that neither Oppenheimer and Zalta's proof nor the one line ‹smt› proof
  on the negativity constraint or whether any of the non-logical vocabulary is atomic
 though they do depend indirectly on the atomicity of identity).›
  
section ‹The Prover9 Argument›

text ‹In the course of verifying the argument using Prover9, Oppenheimer and Zalta
  a simplified version which employs only ‹premise_2›, but not ‹premise_1›
  the connectivity of `greater than' cite‹"oppenheimer_computationally-discovered_2011"›.›

theorem
assumes premise_2:  "¬ E (\<tau> x. Φ x) ⟶ (\<exists> y. G y (\<tau> x. Φ x) ∧ C y)"
shows "E g" nitpick [user_axioms] oops

text ‹However, Isabelle not only fails to verify this argument, but finds a counterexample
  ‹nitpick›. The reason is that it needs to be specified that `greater than' is atomic,
  order for ‹description_theorem_3› to be applicable:›

theorem Prover9Argument:
assumes premise_2:  "¬ E (\<tau> x. Φ x) ⟶ (\<exists> y. G y (\<tau> x. Φ x) ∧ C y)"
and G_atomic: "∧ x. atomic (G x)"
shows "E g"
  text ‹Once the atomicity of `greater than' is added as a premise, a call to ‹sledgehammer›
  the following two-step proof, which Isabelle verifies easily:›
proof -
  have "C g ∧ (∀i. i = n ∨ ¬ G i g ∨ ¬ C i) ∨ n = g"
    by (metis (lifting, full_types) g_def lemma_1)
  then show ?thesis
    by (metis (lifting) G_atomic g_def negativity_constraint premise_2)
qed
    
text ‹If provided with all premises, ‹sledgehammer› still suggests a proof using only
 ‹premise_2›:›
theorem 
assumes connectivity:  "\<forall> x. \<forall> y. G x y ∨ G y x ∨ x = y"
and premise_1:  "\<exists> x. Φ x"
and premise_2:  "¬ E (\<tau> x. Φ x) ⟶ (\<exists> y. G y (\<tau> x. Φ x) ∧ C y)"
and G_atomic: "∧ x. atomic (G x)"
shows "E g"
proof -
  have "Φ g ∨ n = g"
    by (metis (lifting, full_types) g_def lemma_1)
  then show ?thesis
    by (metis (lifting) G_atomic g_def negativity_constraint premise_2)
qed

text ‹Note that this version of the argument does employ the ‹negativity_constraint›,
  well as the premise that identity is atomic via ‹lemma_1›. So although it has less
 -logical premises than the original version of the argument, it has more, and more
 , logical premises.›

section ‹Soundness›

text ‹Since ‹premise_1› and the connectivity of `is greater than' are both dispensable, and
  atomicity of `is greater than' is not especially controversial, the main non-logical premise
  the argument turns out to be ‹premise_2›. Note that ‹premise_2› is entailed
  God's existence:›

theorem
  assumes theism: "E g"
  shows "¬ E (\<tau> x. Φ x) ⟶ (\<exists> y. G y (\<tau> x. Φ x) ∧ C y)"
  using g_def theism by auto

text ‹So under the supposition that `is greater than' is atomic, ‹premise_2›
  equivalent to God's existence, suggesting an atheist might wish to reject it as question-begging
 see cite‹"oppenheimer_computationally-discovered_2011"›, pp. 348-9 and
 cite‹"garbacz_prover9s_2012"› for more detailed discussion of this point).›

text ‹However, Ted Parent has pointed out that ‹premise_2› need not stand on its own,
  may be further supported by the following argument cite‹"parent_prover9_2015"›,
 p. 478:›

lemma
assumes premise_3: "\<forall> y. \<forall> z. ((E y ∧ ¬ E z) ⟶ ((y = (\<tau> x. Φ x) ∨ z = (\<tau> x. Φ x)) ⟶ y = (\<tau> x. Φ x)))" and something_exists: "\<exists> x. E x" and god_is_conceivable: "C g" and C_atomic: "atomic C"
shows "¬ E (\<tau> x. Φ x) ⟶ (\<exists> y. C y ∧ G y (\<tau> x. Φ x))"
by (metis (no_types, lifting) C_atomic description_theorem_3 g_def god_is_conceivable premise_3 something_exists)

text ‹But as Parent says, the premise that `exists in the understanding' is atomic is
  questionable. If `exists in the understanding' is atomic, then it follows from
 ‹description_theorem_3› that, for example, if the largest positive integer exists in
  understanding, then something is the largest positive integer. But since `the largest positive
 ' is a grammatical description, there is a case to be made that the largest positive integer
  exist in the understanding, even though nothing is the largest positive integer
 cite‹"parent_prover9_2015"›, p. 480-1.›

section ‹Conclusion›

text ‹The main difference between Oppenheimer and Zalta's reconstruction of the argument in
  and the reconstruction presented here in Isabelle/HOL is that whereas Prover9 employs
 -order logic, Isabelle/HOL employs higher-order logic. That means that the Russellian
 ‹description_axiom› schema can be stated directly in Isabelle/HOL, whereas in Prover9
  has to be represented indirectly using first-order quantifiers ranging over predicates and
  cite‹"oppenheimer_computationally-discovered_2011"›, pp. 338-41.›

text ‹Because of the way Oppenheimer and Zalta carry out this embedding, it is presupposed
  their presentation that all the non-logical predicates which occur in their argument are
 . In contrast, in the presentation in Isabelle/HOL, whenever the assumption that a certain
  is atomic is needed, this has to be made explicit as a premise of the argument. This
  not a merely practical matter since, as Parent points out, the question of whether `exists
  the understanding' is an atomic predicate turns out to be crucial.›

text ‹Abstracting from the peculiarities of different software, a surprising result is that
  every version of the argument requires the premise that identity is atomic, and some
  require the additional premises that `is greater than' is atomic and `exists in the
 ' is atomic, no version of the argument requires the premises that `exists in
 ', or in other words `exists' simpliciter, is atomic. This is in spite of the fact that
 the question of whether `exists' is a genuine predicate has historically being one of the most
  questions raised by Anselm's argument.›

end
  
section ‹Acknowledgements›

text ‹I thank Bob Beddor, Christoph Benzmuller, Dana Goswick, Frank Jackson, Paul Oppenheimer,
  Pelczar, Abelard Podgorski, Hsueh Qu, Neil Sinhababu, Weng-Hong Tang, Jennifer Wang,
  Wilson and an audience at the University of Sydney for comments on this paper.
 ›