(*<*) 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"}. 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 abbreviations.› 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.› (*<*) 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. 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 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 property).› 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 (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 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)› oops (*<*) end (*>*)