(*<*) theory GoedelProof_P1 imports IHOML begin nitpick_params[user_axioms=true, show_all, expect=genuine, format = 3, atoms e = a b c d] sledgehammer_params[verbose=true] (*>*) section ‹G\"odel's Argument, Formally› text‹ "G\"odel's particular version of the argument is a direct descendent of that of Leibniz, which in turn derives from one of Descartes. These arguments all have a two-part structure: prove God's existence is necessary, if possible; and prove God's existence is possible." \<^cite>‹"Fitting"›, p. 138. › subsection ‹Part I - God's Existence is Possible› text‹ We separate G\"odel's Argument as presented in Fitting's textbook (ch. 11) in two parts. For the first one, while Leibniz provides some kind of proof for the compatibility of all perfections, G\"odel goes on to prove an analogous result: \emph{(T1) Every positive property is possibly instantiated}, which together with \emph{(T2) God is a positive property} directly implies the conclusion. In order to prove \emph{T1}, G\"odel assumes \emph{A2: Any property entailed by a positive property is positive}. › text‹ We are currently contemplating a follow-up analysis of the philosophical implications of these axioms, which encompasses some criticism of the notion of \emph{property entailment} used by G\"odel throughout the argument. › subsubsection ‹General Definitions› abbreviation existencePredicate::"↑⟨𝟬⟩" ("E!") where "E! x ≡ λw. (❙∃⇧^{E}y. y❙≈x) w" ― ‹existence predicate in object language› lemma "E! x w ⟷ existsAt x w" by simp ― ‹safety check: @{text "E!"} correctly matches its meta-logical counterpart› consts positiveProperty::"↑⟨↑⟨𝟬⟩⟩" ("𝒫") ― ‹positiveness/perfection› text‹ Definitions of God (later shown to be equivalent under axiom \emph{A1b}): › abbreviation God::"↑⟨𝟬⟩" ("G") where "G ≡ (λx. ❙∀Y. 𝒫 Y ❙→Y x)" abbreviation God_star::"↑⟨𝟬⟩" ("G*") where "G* ≡ (λx. ❙∀Y. 𝒫 Y ❙↔Y x)" text‹ Definitions needed to formalise \emph{A3}: › abbreviation appliesToPositiveProps::"↑⟨↑⟨↑⟨𝟬⟩⟩⟩" ("pos") where "pos Z ≡ ❙∀X. Z X ❙→𝒫 X" abbreviation intersectionOf::"↑⟨↑⟨𝟬⟩,↑⟨↑⟨𝟬⟩⟩⟩" ("intersec") where "intersec X Z ≡ ❙□(❙∀x.(X x ❙↔(❙∀Y. (Z Y) ❙→(Y x))))" ― ‹quantifier is possibilist› abbreviation Entailment::"↑⟨↑⟨𝟬⟩,↑⟨𝟬⟩⟩" (infix "⇛" 60) where "X ⇛ Y ≡ ❙□(❙∀⇧^{E}z. X z ❙→Y z)" text‹ \bigbreak › subsubsection ‹Axioms› axiomatization where A1a:"⌊❙∀X. 𝒫 (❙⇁X) ❙→❙¬(𝒫 X) ⌋" and ― ‹axiom 11.3A› A1b:"⌊❙∀X. ❙¬(𝒫 X) ❙→𝒫 (❙⇁X)⌋" and ― ‹axiom 11.3B› A2: "⌊❙∀X Y. (𝒫 X ❙∧(X ⇛ Y)) ❙→𝒫 Y⌋" and ― ‹axiom 11.5› A3: "⌊❙∀Z X. (pos Z ❙∧intersec X Z) ❙→𝒫 X⌋" ― ‹axiom 11.10› lemma True nitpick[satisfy] oops ― ‹model found: axioms are consistent› lemma "⌊D⌋" using A1a A1b A2 by blast ― ‹axioms already imply \emph{D} axiom› lemma "⌊D⌋" using A1a A3 by metis subsubsection ‹Theorems› lemma "⌊❙∃X. 𝒫 X⌋" using A1b by auto lemma "⌊❙∃X. 𝒫 X ❙∧❙◇❙∃⇧^{E}X⌋" using A1a A1b A2 by metis text‹ Being self-identical is a positive property: › lemma "⌊(❙∃X. 𝒫 X ❙∧❙◇❙∃⇧^{E}X) ❙→𝒫 (λx w. x = x)⌋" using A2 by fastforce text‹ Proposition 11.6 › lemma "⌊(❙∃X. 𝒫 X) ❙→𝒫 (λx w. x = x)⌋" using A2 by fastforce lemma "⌊𝒫 (λx w. x = x)⌋" using A1b A2 by blast lemma "⌊𝒫 (λx w. x = x)⌋" using A3 by metis text‹ Being non-self-identical is a negative property: › lemma "⌊(❙∃X. 𝒫 X ❙∧❙◇❙∃⇧^{E}X) ❙→𝒫 (❙⇁(λx w. ¬x = x))⌋" using A2 by fastforce lemma "⌊(❙∃X. 𝒫 X) ❙→𝒫 (❙⇁(λx w. ¬x = x))⌋" using A2 by fastforce lemma "⌊(❙∃X. 𝒫 X) ❙→𝒫 (❙⇁(λx w. ¬x = x))⌋" using A3 by metis text‹ Proposition 11.7 › lemma "⌊(❙∃X. 𝒫 X) ❙→❙¬𝒫 ((λx w. ¬x = x))⌋" using A1a A2 by blast lemma "⌊❙¬𝒫 (λx w. ¬x = x)⌋" using A1a A2 by blast text‹ Proposition 11.8 (Informal Proposition 1) - Positive properties are possibly instantiated: › theorem T1: "⌊❙∀X. 𝒫 X ❙→❙◇❙∃⇧^{E}X⌋" using A1a A2 by blast text‹ Proposition 11.14 - Both defs (\emph{God/God*}) are equivalent. For improved performance we may prefer to use one or the other: › lemma GodDefsAreEquivalent: "⌊❙∀x. G x ❙↔G* x⌋" using A1b by force text‹ Proposition 11.15 - Possibilist existence of \emph{God} directly implies \emph{A1b}: › lemma "⌊❙∃G* ❙→(❙∀X. ❙¬(𝒫 X) ❙→𝒫 (❙⇁X))⌋" by meson text‹ Proposition 11.16 - \emph{A3} implies \emph{P(G)} (local consequence): › lemma A3implT2_local: "⌊(❙∀Z X. (pos Z ❙∧intersec X Z) ❙→𝒫 X) ❙→𝒫 G⌋" proof - { fix w have 1: "pos 𝒫 w" by simp have 2: "intersec G 𝒫 w" by simp { assume "(❙∀Z X. (pos Z ❙∧intersec X Z) ❙→𝒫 X) w" hence "(❙∀X. ((pos 𝒫) ❙∧(intersec X 𝒫)) ❙→𝒫 X) w" by (rule allE) hence "(((pos 𝒫) ❙∧(intersec G 𝒫)) ❙→𝒫 G) w" by (rule allE) hence 3: "((pos 𝒫 ❙∧intersec G 𝒫) w) ⟶ 𝒫 G w" by simp hence 4: "((pos 𝒫) ❙∧(intersec G 𝒫)) w" using 1 2 by simp from 3 4 have "𝒫 G w" by (rule mp) } hence "(❙∀Z X. (pos Z ❙∧intersec X Z) ❙→𝒫 X) w ⟶ 𝒫 G w" by (rule impI) } thus ?thesis by (rule allI) qed text‹ \emph{A3} implies ‹P(G)› (as global consequence): › lemma A3implT2_global: "⌊❙∀Z X. (pos Z ❙∧intersec X Z) ❙→𝒫 X⌋ ⟶ ⌊𝒫 G⌋" using A3implT2_local by (rule localImpGlobalCons) text‹ Being Godlike is a positive property. Note that this theorem can be axiomatized directly, as noted by Dana Scott (see \<^cite>‹"Fitting"›, p. 152). We will do so for the second part. › theorem T2: "⌊𝒫 G⌋" using A3implT2_global A3 by simp text‹ Theorem 11.17 (Informal Proposition 3) - Possibly God exists: › theorem T3: "⌊❙◇❙∃⇧^{E}G⌋" using T1 T2 by simp (*<*) end (*>*)