(* Christoph Benzmüller and Bruno Woltzenlogel-P., February 2016 *) theory Scott imports QML begin (* Gödel's Ontological Argument: Variant of Scott *) (* We work in logic S5. *) axiomatization where S5: "S5_sem" consts P :: "(\ \ \) \ \" axiomatization where (* Either a property or its negation is positive, but not both. *) A1a: "\\<^bold>\\. P(\<^sup>\\) \<^bold>\ \<^bold>\(P \)\" and A1b: "\\<^bold>\\. \<^bold>\(P \) \<^bold>\ P (\<^sup>\\)\" and (* A property necessarily implied by a positive property is positive. *) A2: "\\<^bold>\\. \<^bold>\\. (P \ \<^bold>\ \<^bold>\ (\<^bold>\x. \ x \<^bold>\ \ x)) \<^bold>\ P \\" (* Positive properties are possibly exemplified. *) theorem T1: "\\<^bold>\\. P \ \<^bold>\ \<^bold>\ (\<^bold>\ \)\" sledgehammer using A1a A2 by blast (* A God-like being possesses all positive properties. *) definition G :: "\ \ \" where "G = (\x. \<^bold>\(\\. P \ \<^bold>\ \ x))" (* The property of being God-like is positive. *) axiomatization where A3: "\P G\" (* Possibly, God exists. *) corollary C: "\\<^bold>\ (\<^bold>\ G)\" sledgehammer by (simp add: A3 T1) (* Positive properties are necessarily positive). *) axiomatization where A4: "\\<^bold>\\. P \ \<^bold>\ \<^bold>\(P \)\" (* An 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 \<^bold>\ (\<^bold>\\. \ x \<^bold>\ \<^bold>\(\<^bold>\y. \ y \<^bold>\ \ y))" (* Being God-like is an essence of any God-like being. *) theorem T2: "\\<^bold>\(\x. G x \<^bold>\ G ess x)\" sledgehammer [provers = remote_leo2, verbose] by (metis A1b A4 G_def ess_def) (* Necessary existence of an individual is the necessary exemplification of all its essences. *) definition NE :: "\ \ \" where "NE = (\x. \<^bold>\\. \ ess x \<^bold>\ \<^bold>\(\<^bold>\ \))" (* Necessary existence is a positive property *) axiomatization where A5: "\P NE\" (* Necessarily, God exists *) theorem T3: "\\<^bold>\ (\<^bold>\ G)\" sledgehammer [provers = remote_leo2, verbose] by (metis A5 C T2 S5 G_def NE_def) (* God exists *) corollary C2: "\\<^bold>\ G\" sledgehammer [provers = remote_leo2, verbose] by (metis T1 T3 G_def S5) (* The consistency of the entire theory is confirmed by Nitpick. *) lemma True nitpick [satisfy, user_axioms, expect = genuine] oops (* G\"odel's God is flawless: (s)he does not have non-positive properties. *) theorem Flawlessness: "\\<^bold>\\. \<^bold>\x. (G x \<^bold>\ (\<^bold>\(P \) \<^bold>\ \<^bold>\(\ x)))\" sledgehammer [provers = remote_leo2, verbose] by (metis A1b G_def) (* There is only one God: any two God-like beings are equal. *) theorem Monotheism: "\\<^bold>\x.\<^bold>\y. (G x \<^bold>\ (G y \<^bold>\ (x \<^bold>=\<^sup>L y)))\" sledgehammer [provers = remote_satallax, verbose] by (metis Flawlessness G_def) (* Modal Collapse *) lemma MC: "\\<^bold>\\.(\ \<^bold>\ (\<^bold>\ \))\" sledgehammer [provers = remote_satallax, verbose, timeout = 600] -- {* by (metis T2 T3 ess\_def) *} -- {* by (meson T2 T3 ess_def) *} oops (*<*) end (*>*)