Theory GoedelGod
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
typedecl μ
text ‹Possible worlds are connected by an accessibility relation ‹r›.›
consts r :: "i ⇒ i ⇒ bool" (infixr "r" 70)
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→ ◇ (∃ Φ))]"
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)]"
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)]"
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)]"
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]"
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)))))]"
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)))))]"
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→ (□ Φ)))]"
oops
end