Quelle  GoedelGod.thy

(*<*) 
theory GoedelGod
imports Main 

begin
(*>*)

section ‹Introduction›

 text ‹Dana Scott's version cite‹"ScottNotes"› (cf.~Fig.~1)
 of G\"odel's proof of God's existence cite‹"GoedelNotes"› is
 formalized in quantified modal logic KB (QML KB) within the proof assistant Isabelle/HOL.
 QML KB is modeled as a fragment of classical higher-order logic (HOL);
 thus, the formalization is essentially a formalization in HOL. The employed embedding
 of QML KB in HOL is adapting the work of Benzm\"uller and Paulson cite‹"J23" and "B9"›.
 Note that the QML KB formalization employs quantification over individuals and
 quantification over sets of individuals (properties).

 The gaps in Scott's proof have been automated
 with Sledgehammer cite‹"Sledgehammer"›, performing remote calls to the higher-order automated
 theorem prover LEO-II cite‹"LEO-II"›. Sledgehammer suggests the
 Metis cite‹"Metis"› calls, which result in proofs that are verified by Isabelle/HOL.
 For consistency checking, the model finder Nitpick cite‹"Nitpick"› has been employed.
 The successfull calls to Sledgehammer
 are deliberately kept as comments in the file for demonstration purposes
 (normally, they are automatically eliminated by Isabelle/HOL).
 
 Isabelle is described in the textbook by Nipkow,
 Paulson, and Wenzel cite‹"Isabelle"› and in tutorials available
 at: @{url "http://isabelle.in.tum.de"}.
 
 subsection{Related Work}

 The formalization presented here is related to the THF cite‹"J22"› and
 Coq cite‹"Coq"› formalizations at
 @{url "https://github.com/FormalTheology/GoedelGod/tree/master/Formalizations/"}.
 
 An older ontological argument by Anselm was formalized in PVS by John Rushby cite‹"rushby"›.
 ›

section ‹An Embedding of QML KB in HOL›

text ‹The types ‹i› for possible worlds and $\mu$ for individuals are introduced.›

  typedecl i    ― ‹the type for possible worlds›
  typedecl μ    ― ‹the type for indiviuals›      

text ‹Possible worlds are connected by an accessibility relation ‹r›.›

  consts r :: "i ==> i ==> bool" (infixr ‹r› 70)    ― ‹accessibility relation r›   

text ‹QML formulas are translated as HOL terms of type @{typ "i ==> bool"}.
  type is abbreviated as ‹σ›.›

  type_synonym σ = "(i ==> bool)"
 
text ‹The classical connectives $\neg, \wedge, \rightarrow$, and $\forall$
 over individuals and over sets of individuals) and $\exists$ (over individuals) are
  to type $\sigma$. The lifted connectives are ‹m¬›, ‹m∧›, ‹m→›,
 ‹∀›, and ‹∃› (the latter two are modeled as constant symbols).
  connectives can be introduced analogously. We exemplarily do this for ‹m∨› ,
 ‹m≡›, and ‹mL=› (Leibniz equality on individuals). Moreover, the modal
  ‹◻› and ‹♢› are introduced. Definitions could be used instead of
 .›

  abbreviation mnot :: "σ ==> σ" (‹m¬›) where "m¬ φ ≡ (λw. ¬ φ w)"    
  abbreviation mand :: "σ ==> σ ==> σ" (infixr ‹m∧› 65) where "φ m∧ ψ ≡ (λw. φ w ∧ ψ w)"   
  abbreviation mor :: "σ ==> σ ==> σ" (infixr ‹m∨› 70) where "φ m∨ ψ ≡ (λw. φ w ∨ ψ w)"   
  abbreviation mimplies :: "σ ==> σ ==> σ" (infixr ‹m→› 74) where "φ m→ ψ ≡ (λw. φ w ⟶ ψ w)"  
  abbreviation mequiv:: "σ ==> σ ==> σ" (infixr ‹m≡› 76) where "φ m≡ ψ ≡ (λw. φ w ⟷ ψ w)"  
  abbreviation mforall :: "('a ==> σ) ==> σ" (‹∀›) where "∀ Φ ≡ (λw. ∀x. Φ x w)"   
  abbreviation mexists :: "('a ==> σ) ==> σ" (‹∃›) where "∃ Φ ≡ (λw. ∃x. Φ x w)"
  abbreviation mLeibeq :: "μ ==> μ ==> σ" (infixr ‹mL=› 90) where "x mL= y ≡ ∀(λφ. (φ x m→ φ y))"
  abbreviation mbox :: "σ ==> σ" (‹◻›) where "◻ φ ≡ (λw. ∀v. w r v ⟶ φ v)"
  abbreviation mdia :: "σ ==> σ" (‹♢›) where "♢ φ ≡ (λw. ∃v. w r v ∧ φ v)" 
  
text ‹For grounding lifted formulas, the meta-predicate ‹valid› is introduced.›

  (*<*) unbundle no list_enumeration_syntax (*>*) 
  abbreviation valid :: "σ ==> bool" (‹[_]›) where "[p] ≡ ∀w. p w"
  
section ‹G\"odel's Ontological Argument›  
  
text ‹Constant symbol ‹P› (G\"odel's `Positive') is declared.›

  consts P :: "(μ ==> σ) ==> σ"  

text ‹The meaning of ‹P› is restricted by axioms ‹A1(a/b)›: $\all \phi
 P(\neg \phi) \biimp \neg P(\phi)]$ (Either a property or its negation is positive, but not both.)
  ‹A2›: $\all \phi \all \psi [(P(\phi) \wedge \nec \all x [\phi(x) \imp \psi(x)])
 imp P(\psi)]$ (A property necessarily implied by a positive property is positive).›

  axiomatization where
    A1a: "[∀(λΦ. P (λx. m¬ (Φ x)) m→ m¬ (P Φ))]" and
    A1b: "[∀(λΦ. m¬ (P Φ) m→ P (λx. m¬ (Φ x)))]" and
    A2:  "[∀(λΦ. ∀(λΨ. (P Φ m∧ ◻ (∀(λx. Φ x m→ Ψ x))) m→ P Ψ))]"

text ‹We prove theorem T1: $\all \phi [P(\phi) \imp \pos \ex x \phi(x)]$ (Positive
  are possibly exemplified). T1 is proved directly by Sledgehammer with command ‹sledgehammer [provers = remote_leo2]›.
  suggests to call Metis with axioms A1a and A2.
  sucesfully generates a proof object
  is verified in Isabelle/HOL's kernel.›
 
  theorem T1: "[∀(λΦ. P Φ m→ ♢ (∃ Φ))]"  
  ― ‹sledgehammer [provers = remote\_leo2]›
  by (metis A1a A2)

text ‹Next, the symbol ‹G› for `God-like' is introduced and defined
  $G(x) \biimp \forall \phi [P(\phi) \to \phi(x)]$ \\ (A God-like being possesses
  positive properties).›

  definition G :: "μ ==> σ" where "G = (λx. ∀(λΦ. P Φ m→ Φ x))"   

text ‹Axiom ‹A3› is added: $P(G)$ (The property of being God-like is positive).
  and Metis then prove corollary ‹C›: $\pos \ex x G(x)$
 Possibly, God exists).›
 
  axiomatization where A3:  "[P G]" 

  corollary C: "[♢ (∃ G)]" 
  ― ‹sledgehammer [provers = remote\_leo2]›
  by (metis A3 T1)

text ‹Axiom ‹A4› is added: $\all \phi [P(\phi) \to \Box \; P(\phi)]$
 Positive properties are necessarily positive).›

  axiomatization where A4:  "[∀(λΦ. P Φ m→ ◻ (P Φ))]" 

text ‹Symbol ‹ess› for `Essence' is introduced and defined as
 $\ess{\phi}{x} \biimp \phi(x) \wedge \all \psi (\psi(x) \imp \nec \all y (\phi(y)
 imp \psi(y)))$$ (An \emph{essence} of an individual is a property possessed by it and necessarily implying any of its properties).›

  definition ess :: "(μ ==> σ) ==> μ ==> σ" (infixr ‹ess› 85) where
    "Φ ess x = Φ x m∧ ∀(λΨ. Ψ x m→ ◻ (∀(λy. Φ y m→ Ψ y)))"

text ‹Next, Sledgehammer and Metis prove theorem ‹T2›: $\all x [G(x) \imp \ess{G}{x}]$ \\
 Being God-like is an essence of any God-like being).›

  theorem T2: "[∀(λx. G x m→ G ess x)]"
  ― ‹sledgehammer [provers = remote\_leo2]›
  by (metis A1b A4 G_def ess_def)

text ‹Symbol ‹NE›, for `Necessary Existence', is introduced and
  as $$\NE(x) \biimp \all \phi [\ess{\phi}{x} \imp \nec \ex y \phi(y)]$$ (Necessary
  of an individual is the necessary exemplification of all its essences).›

  definition NE :: "μ ==> σ" where "NE = (λx. ∀(λΦ. Φ ess x m→ ◻ (∃ Φ)))"

text ‹Moreover, axiom ‹A5› is added: $P(\NE)$ (Necessary existence is a positive
 ).›

  axiomatization where A5:  "[P NE]"

text ‹The ‹B› axiom (symmetry) for relation r is stated. ‹B› is needed only
  proving theorem T3 and for corollary C2.›

  axiomatization where sym: "x r y ⟶ y r x" 

text ‹Finally, Sledgehammer and Metis prove the main theorem ‹T3›: $\nec \ex x G(x)$ \\
 Necessarily, God exists).›

  theorem T3: "[◻ (∃ G)]" 
  ― ‹sledgehammer [provers = remote\_leo2]›
  by (metis A5 C T2 sym G_def NE_def)

text ‹Surprisingly, the following corollary can be derived even without the ‹T› axiom
 reflexivity).›

  corollary C2: "[∃ G]" 
  ― ‹sledgehammer [provers = remote\_leo2]›
  by (metis T1 T3 G_def sym)

text ‹The consistency of the entire theory is confirmed by Nitpick.›

  lemma True nitpick [satisfy, user_axioms, expect = genuine] oops


section ‹Additional Results on G\"odel's God.›  

text ‹G\"odel's God is flawless: (s)he does not have non-positive properties.›

  theorem Flawlessness: "[∀(λΦ. ∀(λx. (G x m→ (m¬ (P Φ) m→ m¬ (Φ x)))))]"
  ― ‹sledgehammer [provers = remote\_leo2]›
  by (metis A1b G_def) 
  
text ‹There is only one God: any two God-like beings are equal.›   
  
  theorem Monotheism: "[∀(λx.∀(λy. (G x m→ (G y m→ (x mL= y)))))]"
  ― ‹sledgehammer [provers = remote\_leo2]›
  by (metis Flawlessness G_def) 

section ‹Modal Collapse›  

text ‹G\"odel's axioms have been criticized for entailing the so-called
  collapse. The prover Satallax cite‹"Satallax"› confirms this.
 , sledgehammer is not able to determine which axioms,
  and previous theorems are used by Satallax;
  it suggests to call Metis using everything, but this (unsurprinsingly) fails.
  to use `Sledegehammer min' to minimize Sledgehammer's suggestion does not work.
  Metis with ‹T2›, ‹T3› and ‹ess_def› also does not work.›

  lemma MC: "[∀(λΦ.(Φ m→ (◻ Φ)))]"  
  ― ‹sledgehammer [provers = remote\_satallax]›
  ― ‹by (metis T2 T3 ess\_def)›
  oops
(*<*) 
end
(*>*)