Theory GoedelGod

theory GoedelGod
imports Main 


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 ""}.
\subsection{Related Work}

 The formalization presented here is related to the THF cite"J22" and
 Coq cite"Coq" formalizations at 
 @{url ""}.
 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"}. 
This 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
lifted to type $\sigma$. The lifted connectives are m¬›, m∧›, m→›,
∀›, and ∃› (the latter two are modeled as constant symbols). 
Other connectives can be introduced analogously. We exemplarily do this for m∨› , 
m≡›, and mL=› (Leibniz equality on individuals). Moreover, the modal 
operators □› and ◇›  are introduced. Definitions could be used instead of 

  abbreviation mnot :: "σ  σ" ("") where " φ  (λ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.›

  (*<*) no_syntax "_list" :: "args  'a list" ("[(_)]") (*>*) 
  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.) 
and 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.  (Φ x)) m→  (P Φ))]" and
    A1b: "[(λΦ.  (P Φ) m→ P (λx.  (Φ 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 
properties are possibly exemplified). T1 is proved directly by Sledgehammer with command sledgehammer [provers = remote_leo2]›. 
Sledgehammer suggests to call Metis with axioms A1a and A2. 
Metis sucesfully generates a proof object 
that 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 
as $G(x) \biimp \forall \phi [P(\phi) \to \phi(x)]$ \\ (A God-like being possesses 
all 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).
Sledgehammer 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
defined as $$\NE(x) \biimp \all \phi [\ess{\phi}{x} \imp \nec \ex y \phi(y)]$$ (Necessary 
existence 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 
for 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 

  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→ ( (P Φ) 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 
modal collapse. The prover Satallax cite"Satallax" confirms this. 
However, sledgehammer is not able to determine which axioms, 
definitions and previous theorems are used by Satallax;
hence it suggests to call Metis using everything, but this (unsurprinsingly) fails.
Attempting to use `Sledegehammer min' to minimize Sledgehammer's suggestion does not work.
Calling Metis with T2›, T3› and ess_def› also does not work.› 

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