(*<*) theory GoedelProof_P2 imports IHOML begin nitpick_params[user_axioms=true, show_all, expect=genuine, format = 3, atoms e = a b c d] sledgehammer_params[verbose=true] (*>*) subsection ‹Part II - God's Existence is Necessary if Possible› text‹ We show here that God's necessary existence follows from its possible existence by adding some additional (potentially controversial) assumptions including an \emph{essentialist} premise and the \emph{S5} axioms. Further results like monotheism and the rejection of free will (\emph{modal collapse}) are also proved. › subsubsection ‹General Definitions› abbreviation existencePredicate::"↑⟨𝟬⟩" ("E!") where "E! x ≡ (λw. (❙∃⇧^{E}y. y❙≈x) w)" consts positiveProperty::"↑⟨↑⟨𝟬⟩⟩" ("𝒫") abbreviation God::"↑⟨𝟬⟩" ("G") where "G ≡ (λx. ❙∀Y. 𝒫 Y ❙→ Y x)" abbreviation God_star::"↑⟨𝟬⟩" ("G*") where "G* ≡ (λx. ❙∀Y. 𝒫 Y ❙↔ Y x)" abbreviation Entailment::"↑⟨↑⟨𝟬⟩,↑⟨𝟬⟩⟩" (infix "⇛" 60) where "X ⇛ Y ≡ ❙□(❙∀⇧^{E}z. X z ❙→ Y z)" subsubsection ‹Results from Part I› text‹ Note that the only use G\"odel makes of axiom A3 is to show that being Godlike is a positive property (\emph{T2}). We follow therefore Scott's proposal and take (\emph{T2}) directly as an axiom: › 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› T2: "⌊𝒫 G⌋" ― ‹proposition 11.16› 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 GodDefsAreEquivalent: "⌊❙∀x. G x ❙↔ G* x⌋" using A1b by fastforce theorem T1: "⌊❙∀X. 𝒫 X ❙→ ❙◇❙∃⇧^{E}X⌋" using A1a A2 by blast ― ‹positive properties are possibly instantiated› theorem T3: "⌊❙◇❙∃⇧^{E}G⌋" using T1 T2 by simp ― ‹God exists possibly› subsubsection ‹Axioms› text‹ ‹𝒫› satisfies the so-called stability conditions (see @{cite "Fitting"}, p. 124), which means it designates rigidly (note that this makes for an \emph{essentialist} assumption). › axiomatization where A4a: "⌊❙∀X. 𝒫 X ❙→ ❙□(𝒫 X)⌋" ― ‹axiom 11.11› lemma A4b: "⌊❙∀X. ❙¬(𝒫 X) ❙→ ❙□❙¬(𝒫 X)⌋" using A1a A1b A4a by blast abbreviation rigidPred::"('t⇒io)⇒io" where "rigidPred τ ≡ (λβ. ❙□((λz. β ❙≈ z) ❙↓τ)) ❙↓τ" lemma "⌊rigidPred 𝒫⌋" using A4a A4b by blast ― ‹@{term "𝒫"} is therefore rigid› lemma True nitpick[satisfy] oops ― ‹model found: so far all axioms A1-4 consistent› text‹ \bigbreak › subsubsection ‹Theorems› text‹ Remark: Essence is defined here (and in Fitting's variant) in the version of Scott; G\"odel's original version leads to the inconsistency reported in @{cite C55 and C60} › abbreviation essenceOf::"↑⟨↑⟨𝟬⟩,𝟬⟩" ("ℰ") where "ℰ Y x ≡ (Y x) ❙∧ (❙∀Z. Z x ❙→ Y ⇛ Z)" abbreviation beingIdenticalTo::"𝟬⇒↑⟨𝟬⟩" ("id") where "id x ≡ (λy. y❙≈x)" ― ‹note that \emph{id} is a rigid predicate› text‹ Theorem 11.20 - Informal Proposition 5 › theorem GodIsEssential: "⌊❙∀x. G x ❙→ (ℰ G x)⌋" using A1b A4a by metis text‹ Theorem 11.21 › theorem "⌊❙∀x. G* x ❙→ (ℰ G* x)⌋" using A4a by meson text‹ Theorem 11.22 - Something can have only one essence: › theorem "⌊❙∀X Y z. (ℰ X z ❙∧ ℰ Y z) ❙→ (X ⇛ Y)⌋" by meson text‹ Theorem 11.23 - An essence is a complete characterization of an individual: › theorem EssencesCharacterizeCompletely: "⌊❙∀X y. ℰ X y ❙→ (X ⇛ (id y))⌋" proof (rule ccontr) assume "¬ ⌊❙∀X y. ℰ X y ❙→ (X ⇛ (id y))⌋" hence "∃w. ¬(( ❙∀X y. ℰ X y ❙→ X ⇛ id y) w)" by simp then obtain w where "¬(( ❙∀X y. ℰ X y ❙→ X ⇛ id y) w)" .. hence "(❙∃X y. ℰ X y ❙∧ ❙¬(X ⇛ id y)) w" by simp hence "∃X y. ℰ X y w ∧ (❙¬(X ⇛ id y)) w" by simp then obtain P where "∃y. ℰ P y w ∧ (❙¬(P ⇛ id y)) w" .. then obtain a where 1: "ℰ P a w ∧ (❙¬(P ⇛ id a)) w" .. hence 2: "ℰ P a w" by (rule conjunct1) from 1 have "(❙¬(P ⇛ id a)) w" by (rule conjunct2) hence "∃x. ∃z. w r x ∧ existsAt z x ∧ P z x ∧ ¬(a = z)" by blast then obtain w1 where "∃z. w r w1 ∧ existsAt z w1 ∧ P z w1 ∧ ¬(a = z)" .. then obtain b where 3: "w r w1 ∧ existsAt b w1 ∧ P b w1 ∧ ¬(a = b)" .. hence "w r w1" by simp from 3 have "existsAt b w1" by simp from 3 have "P b w1" by simp from 3 have 4: " ¬(a = b)" by simp from 2 have "P a w" by simp from 2 have "∀Y. Y a w ⟶ ((P ⇛ Y) w)" by auto hence "(❙⇁(id b)) a w ⟶ (P ⇛ (❙⇁(id b))) w" by (rule allE) hence "¬(❙⇁(id b)) a w ∨ ((P ⇛ (❙⇁(id b))) w)" by blast then show False proof assume "¬(❙⇁(id b)) a w" hence "a = b" by simp thus False using 4 by auto next assume "((P ⇛ (❙⇁(id b))) w)" hence "∀x. ∀z. (w r x ∧ existsAt z x ∧ P z x) ⟶ (❙⇁(id b)) z x" by blast hence "∀z. (w r w1 ∧ existsAt z w1 ∧ P z w1) ⟶ (❙⇁(id b)) z w1" by (rule allE) hence "(w r w1 ∧ existsAt b w1 ∧ P b w1) ⟶ (❙⇁(id b)) b w1" by (rule allE) hence "¬(w r w1 ∧ existsAt b w1 ∧ P b w1) ∨ (❙⇁(id b)) b w1" by simp hence "(❙⇁(id b)) b w" using 3 by simp hence "¬(b=b)" by simp thus False by simp qed qed text‹ Definition 11.24 - Necessary Existence (Informal Definition 6): › abbreviation necessaryExistencePred::"↑⟨𝟬⟩" ("NE") where "NE x ≡ (λw. (❙∀Y. ℰ Y x ❙→ ❙□❙∃⇧^{E}Y) w)" text‹ Axiom 11.25 (Informal Axiom 5) › axiomatization where A5: "⌊𝒫 NE⌋" lemma True nitpick[satisfy] oops ― ‹model found: so far all axioms consistent› text‹ Theorem 11.26 (Informal Proposition 7) - Possibilist existence of God implies necessary actualist existence: › theorem GodExistenceImpliesNecExistence: "⌊❙∃ G ❙→ ❙□❙∃⇧^{E}G⌋" proof - { fix w { assume "∃x. G x w" then obtain g where 1: "G g w" .. hence "NE g w" using A5 by auto ― ‹axiom 11.25› hence "∀Y. (ℰ Y g w) ⟶ (❙□❙∃⇧^{E}Y) w" by simp hence 2: "(ℰ G g w) ⟶ (❙□❙∃⇧^{E}G) w" by (rule allE) have "(❙∀x. G x ❙→ (ℰ G x)) w" using GodIsEssential by (rule allE) ― ‹GodIsEssential follows from Axioms 11.11 and 11.3B› hence "(G g ❙→ (ℰ G g)) w" by (rule allE) hence "G g w ⟶ ℰ G g w" by simp from this 1 have 3: "ℰ G g w" by (rule mp) from 2 3 have "(❙□❙∃⇧^{E}G) w" by (rule mp) } hence "(∃x. G x w) ⟶ (❙□❙∃⇧^{E}G) w" by (rule impI) hence "((❙∃x. G x) ❙→ ❙□❙∃⇧^{E}G) w" by simp } thus ?thesis by (rule allI) qed text‹ \emph{Modal collapse} is countersatisfiable (unless we introduce S5 axioms): › lemma "⌊❙∀Φ.(Φ ❙→ (❙□ Φ))⌋" nitpick oops text‹ We postulate semantic frame conditions for some modal logics. Taken together, reflexivity, transitivity and symmetry make for an equivalence relation and therefore an \emph{S5} logic (via \emph{Sahlqvist correspondence}). We prefer to postulate them individually here in order to get more detailed information about their relevance in the proofs presented below. › axiomatization where refl: "reflexive aRel" and tran: "transitive aRel" and symm: "symmetric aRel" lemma True nitpick[satisfy] oops ― ‹model found: axioms still consistent› text‹ Using an \emph{S5} logic, \emph{modal collapse} (‹⌊❙∀Φ.(Φ ❙→ (❙□ Φ))⌋›) is actually valid (see `More Objections' some pages below) › text‹ We prove some useful inference rules: › lemma modal_distr: "⌊❙□(φ ❙→ ψ)⌋ ⟹ ⌊(❙◇φ ❙→ ❙◇ψ)⌋" by blast lemma modal_trans: "(⌊φ ❙→ ψ⌋ ∧ ⌊ψ ❙→ χ⌋) ⟹ ⌊φ ❙→ χ⌋" by simp text‹ Theorem 11.27 - Informal Proposition 8. Note that only symmetry and transitivity for the accessibility relation are used. › theorem possExistenceImpliesNecEx: "⌊❙◇❙∃ G ❙→ ❙□❙∃⇧^{E}G⌋" ― ‹local consequence› proof - have "⌊❙∃ G ❙→ ❙□❙∃⇧^{E}G⌋" using GodExistenceImpliesNecExistence by simp ― ‹follows from Axioms 11.11, 11.25 and 11.3B› hence "⌊❙□(❙∃ G ❙→ ❙□❙∃⇧^{E}G)⌋" using NEC by simp hence 1: "⌊❙◇❙∃ G ❙→ ❙◇❙□❙∃⇧^{E}G⌋" by (rule modal_distr) have 2: "⌊❙◇❙□❙∃⇧^{E}G ❙→ ❙□❙∃⇧^{E}G⌋" using symm tran by metis ― ‹frame conditions› from 1 2 have "⌊❙◇❙∃ G ❙→ ❙◇❙□❙∃⇧^{E}G⌋ ∧ ⌊❙◇❙□❙∃⇧^{E}G ❙→ ❙□❙∃⇧^{E}G⌋" by simp thus ?thesis by (rule modal_trans) qed lemma T4: "⌊❙◇❙∃ G⌋ ⟶ ⌊❙□❙∃⇧^{E}G⌋" using possExistenceImpliesNecEx by (rule localImpGlobalCons) ― ‹global consequence› text‹ Corollary 11.28 - Necessary (actualist) existence of God (for both definitions); reflexivity is still not used: › lemma GodNecExists: "⌊❙□❙∃⇧^{E}G⌋" using T3 T4 by metis lemma God_starNecExists: "⌊❙□❙∃⇧^{E}G*⌋" using GodNecExists GodDefsAreEquivalent by simp subsubsection ‹Monotheism› text‹ Monotheism for non-normal models (with Leibniz equality) follows directly from God having all and only positive properties: › theorem Monotheism_LeibnizEq: "⌊❙∀x. G x ❙→ (❙∀y. G y ❙→ (x ❙≈⇧^{L}y))⌋" using GodDefsAreEquivalent by simp text‹ Monotheism for normal models is trickier. We need to consider some previous results (p. 162): › lemma GodExistenceIsValid: "⌊❙∃⇧^{E}G⌋" using GodNecExists refl by auto ― ‹reflexivity is now required by the solver› text‹ Proposition 11.29: › theorem Monotheism_normalModel: "⌊❙∃x.❙∀y. G y ❙↔ x ❙≈ y⌋" proof - { fix w have "⌊❙∃⇧^{E}G⌋" using GodExistenceIsValid by simp ― ‹follows from corollary 11.28› hence "(❙∃⇧^{E}G) w" by (rule allE) then obtain g where 1: "existsAt g w ∧ G g w" .. hence 2: "ℰ G g w" using GodIsEssential by blast ― ‹follows from ax. 11.11/11.3B› { fix y have "G y w ⟷ (g ❙≈ y) w" proof assume "G y w" hence 3: "ℰ G y w" using GodIsEssential by blast have "(ℰ G y ❙→ (G ⇛ id y)) w" using EssencesCharacterizeCompletely by simp ― ‹follows from theorem 11.23› hence "ℰ G y w ⟶ ((G ⇛ id y) w)" by simp from this 3 have "(G ⇛ id y) w" by (rule mp) hence "(❙□(❙∀⇧^{E}z. G z ❙→ z ❙≈ y)) w" by simp hence "∀x. w r x ⟶ ((∀z. (existsAt z x ∧ G z x) ⟶ z = y))" by auto hence "w r w ⟶ ((∀z. (existsAt z w ∧ G z w) ⟶ z = y))" by (rule allE) hence "∀z. (w r w ∧ existsAt z w ∧ G z w) ⟶ z = y" by auto hence 4: "(w r w ∧ existsAt g w ∧ G g w) ⟶ g = y" by (rule allE) have "w r w" using refl by simp ― ‹using frame reflexivity (Axiom M)› hence "w r w ∧ (existsAt g w ∧ G g w)" using 1 by (rule conjI) from 4 this have "g = y" by (rule mp) thus "(g ❙≈ y) w" by simp next assume "(g ❙≈ y) w" from this 2 have "ℰ G y w" by simp thus "G y w " by (rule conjunct1) qed } hence "∀y. G y w ⟷ (g ❙≈ y) w" by (rule allI) hence "∃x. (∀y. G y w ⟷ (x ❙≈ y) w)" by (rule exI) hence "(❙∃x. (❙∀y. G y ❙↔ (x ❙≈ y))) w" by simp } thus ?thesis by (rule allI) qed text‹ \bigbreak › text‹ Corollary 11.30: › lemma GodImpliesExistence: "⌊❙∀x. G x ❙→ E! x⌋" using GodExistenceIsValid Monotheism_normalModel by metis subsubsection ‹Positive Properties are Necessarily Instantiated› lemma PosPropertiesNecExist: "⌊❙∀Y. 𝒫 Y ❙→ ❙□❙∃⇧^{E}Y⌋" using GodNecExists A4a by meson ― ‹proposition 11.31: follows from corollary 11.28 and axiom A4a› subsubsection ‹More Objections› text‹ Fitting discusses the objection raised by Sobel @{cite "sobel2004logic"}, who argues that G\"odel's axiom system is too strong: it implies that whatever is the case is so necessarily, i.e. the modal system collapses (‹φ ⟶ □φ›). The \emph{modal collapse} has been philosophically interpreted as implying the absence of free will. › text‹ We start by proving an useful FOL lemma: › lemma useful: "(∀x. φ x ⟶ ψ) ⟹ ((∃x. φ x) ⟶ ψ)" by simp text‹ In the context of our S5 axioms, the \emph{modal collapse} becomes valid (pp. 163-4): › lemma ModalCollapse: "⌊❙∀Φ.(Φ ❙→ (❙□ Φ))⌋" proof - { fix w { fix Q have "(❙∀x. G x ❙→ (ℰ G x)) w" using GodIsEssential by (rule allE) ― ‹follows from Axioms 11.11 and 11.3B› hence "∀x. G x w ⟶ ℰ G x w" by simp hence "∀x. G x w ⟶ (❙∀Z. Z x ❙→ ❙□(❙∀⇧^{E}z. G z ❙→ Z z)) w" by force hence "∀x. G x w ⟶ ((λy. Q) x ❙→ ❙□(❙∀⇧^{E}z. G z ❙→ (λy. Q) z)) w" by force hence "∀x. G x w ⟶ (Q ❙→ ❙□(❙∀⇧^{E}z. G z ❙→ Q)) w" by simp hence 1: "(∃x. G x w) ⟶ ((Q ❙→ ❙□(❙∀⇧^{E}z. G z ❙→ Q)) w)" by (rule useful) have "∃x. G x w" using GodExistenceIsValid by auto from 1 this have "(Q ❙→ ❙□(❙∀⇧^{E}z. G z ❙→ Q)) w" by (rule mp) hence "(Q ❙→ ❙□((❙∃⇧^{E}z. G z) ❙→ Q)) w" using useful by blast hence "(Q ❙→ (❙□(❙∃⇧^{E}z. G z) ❙→ ❙□Q)) w" by simp hence "(Q ❙→ ❙□Q) w" using GodNecExists by simp } hence "(❙∀Φ. Φ ❙→ ❙□ Φ) w" by (rule allI) } thus ?thesis by (rule allI) qed text‹ \pagebreak › (*<*) end (*>*)