(*<*) theory AndersonProof imports IHOML begin nitpick_params[user_axioms=true, show_all, expect=genuine, format = 4, atoms e = a b c d] sledgehammer_params[verbose=true] (*>*) section ‹Anderson's Alternative› text‹ In this final section, we verify Anderson's emendation of G\"odel's argument, as it is presented in the last part of the textbook by Fitting (pp. 169-171). › subsection ‹General Definitions› abbreviation existencePredicate::"↑⟨𝟬⟩" ("E!") where "E! x ≡ λw. (❙∃⇧^{E}y. y❙≈x) w" consts positiveProperty::"↑⟨↑⟨𝟬⟩⟩" ("𝒫") abbreviation God::"↑⟨𝟬⟩" ("G⇧^{A}") where "G⇧^{A}≡ λx. ❙∀Y. (𝒫 Y) ❙↔ ❙□(Y x)" abbreviation Entailment::"↑⟨↑⟨𝟬⟩,↑⟨𝟬⟩⟩" (infix "⇛" 60) where "X ⇛ Y ≡ ❙□(❙∀⇧^{E}z. X z ❙→ Y z)" subsection ‹Part I - God's Existence is Possible› axiomatization where A1a:"⌊❙∀X. 𝒫 (❙⇁X) ❙→ ❙¬(𝒫 X) ⌋" and ― ‹Axiom 11.3A› A2: "⌊❙∀X Y. (𝒫 X ❙∧ (X ⇛ Y)) ❙→ 𝒫 Y⌋" and ― ‹Axiom 11.5› T2: "⌊𝒫 G⇧^{A}⌋" ― ‹Proposition 11.16› lemma True nitpick[satisfy] oops ― ‹model found: axioms are consistent› theorem T1: "⌊❙∀X. 𝒫 X ❙→ ❙◇❙∃⇧^{E}X⌋" using A1a A2 by blast ― ‹positive properties are possibly instantiated› theorem T3: "⌊❙◇❙∃⇧^{E}G⇧^{A}⌋" using T1 T2 by simp ― ‹God exists possibly› subsection ‹Part II - God's Existence is Necessary if Possible› text‹ ‹𝒫› now satisfies only one of the stability conditions. But since the argument uses an \emph{S5} logic, the other stability condition is implied. Therefore ‹𝒫› becomes rigid (see p. 124). › axiomatization where A4a: "⌊❙∀X. 𝒫 X ❙→ ❙□(𝒫 X)⌋" ― ‹axiom 11.11› text‹ We again postulate our \emph{S5} axioms: › axiomatization where refl: "reflexive aRel" and tran: "transitive aRel" and symm: "symmetric aRel" lemma True nitpick[satisfy] oops ― ‹model found: so far all axioms consistent› abbreviation rigidPred::"('t⇒io)⇒io" where "rigidPred τ ≡ (λβ. ❙□((λz. β ❙≈ z) ❙↓τ)) ❙↓τ" lemma A4b: "⌊❙∀X. ❙¬(𝒫 X) ❙→ ❙□❙¬(𝒫 X)⌋" using A4a symm by auto ― ‹symmetry is needed (which corresponds to \emph{B} axiom)› lemma "⌊rigidPred 𝒫⌋" using A4a A4b by blast ― ‹@{text "𝒫"} is therefore rigid in a \emph{B} logic› text‹ Essence, Anderson Version (Definition 11.34) › abbreviation essenceOf::"↑⟨↑⟨𝟬⟩,𝟬⟩" ("ℰ⇧^{A}") where "ℰ⇧^{A}Y x ≡ (❙∀Z. ❙□(Z x) ❙↔ Y ⇛ Z)" text‹ Necessary Existence, Anderson Version (Definition 11.35) › abbreviation necessaryExistencePred::"↑⟨𝟬⟩" ("NE⇧^{A}") where "NE⇧^{A}x ≡ (λw. (❙∀Y. ℰ⇧^{A}Y x ❙→ ❙□❙∃⇧^{E}Y) w)" text‹ Theorem 11.36 - If g is God-like, then the property of being God-like is the essence of g. › text‹ As shown before, this theorem's proof could be completely automatized for G\"odel's and Fitting's variants. For Anderson's version however, we had to provide Isabelle with some help based on the corresponding natural-language proof given by Anderson (see @{cite "anderson90:_some_emend_of_goedel_ontol_proof"} Theorem 2*, p. 296) › (*Anderson's Proof: Suppose that g is God-like* and necessarily has a property Q. Then by definition (of "God-like*"), that property is positive. But necessarily, if Q is positive, then if anything is God-like*, then it has Q -again by the definition of "God-like* ," together with the fact that if something has a property necessarily, then it has the property. But if a property is positive, then it is necessarily positive (Axiom 4). Hence, if Q is positive, then it is entailed by being God-like* (by modal logic-as in the original Theorem 2). But Q is positive and hence is entailed by being God-like*. Thus we have proved that if an entity is God-like* and has a property essentially, then that property is entailed by the property of being God-like*. Suppose a property Q is entailed by the property of being God-like*. Then Q is positive by Axioms 2 and 3* and therefore, since g is God-like*, g has Q necessarily (by the definition of "God-like*"). Hence, if something is God-like*, it has a property essentially if and only if that property is entailed by being God-like-i.e., God-likeness* is an essence* of that thing. Q.E.D.*) theorem GodIsEssential: "⌊❙∀x. G⇧^{A}x ❙→ (ℰ⇧^{A}G⇧^{A}x)⌋" proof - { fix w { fix g { assume "G⇧^{A}g w" hence 1: "∀Y. (𝒫 Y w) ⟷ (❙□(Y g)) w" by simp { fix Q from 1 have 2: "(𝒫 Q w) ⟷ (❙□(Q g)) w" by (rule allE) have "(❙□(Q g)) w ⟷ (G⇧^{A}⇛ Q) w" ― ‹we need to prove @{text "→"} and @{text "←"}› proof assume "(❙□(Q g)) w" ― ‹suppose g is God-like and necessarily has Q› hence 3: "(𝒫 Q w)" using 2 by simp ― ‹then Q is positive› { fix u have "(𝒫 Q u) ⟶ (∀x. G⇧^{A}x u ⟶ (❙□(Q x)) u)" by auto ― ‹using the definition of God-like› have "(𝒫 Q u) ⟶ (∀x. G⇧^{A}x u ⟶ ((Q x)) u)" using refl by auto ― ‹and using @{text "□(φ x) ⟶ φ x"}› } hence "∀z. (𝒫 Q z) ⟶ (∀x. G⇧^{A}x z ⟶ Q x z)" by (rule allI) hence "⌊𝒫 Q ❙→ (❙∀x. G⇧^{A}x ❙→ Q x)⌋" by auto ― ‹if Q is positive, then whatever is God-like has Q› hence "⌊❙□(𝒫 Q ❙→ (❙∀x. G⇧^{A}x ❙→ Q x))⌋" by (rule NEC) hence "⌊(❙□(𝒫 Q)) ❙→ ❙□(❙∀x. G⇧^{A}x ❙→ Q x)⌋" using K by auto hence "⌊(❙□(𝒫 Q)) ❙→ G⇧^{A}⇛ Q⌋" by simp hence "((❙□(𝒫 Q)) ❙→ G⇧^{A}⇛ Q) w" by (rule allE) hence 4: "(❙□(𝒫 Q)) w ⟶ (G⇧^{A}⇛ Q) w" by simp (*if a property is necessarily positive, then it is entailed by being God-like*) have "⌊❙∀X. 𝒫 X ❙→ ❙□(𝒫 X)⌋" by (rule A4a) ― ‹using axiom 4› hence "(❙∀X. 𝒫 X ❙→ (❙□(𝒫 X))) w" by (rule allE) hence "𝒫 Q w ⟶ (❙□(𝒫 Q)) w" by (rule allE) hence "𝒫 Q w ⟶ (G⇧^{A}⇛ Q) w" using 4 by simp (*if Q is positive, then it is entailed by being God-like*) thus "(G⇧^{A}⇛ Q) w" using 3 by (rule mp) ― ‹@{text "→"} direction› next assume 5: "(G⇧^{A}⇛ Q) w" ― ‹suppose Q is entailed by being God-like› have "⌊❙∀X Y. (𝒫 X ❙∧ (X ⇛ Y)) ❙→ 𝒫 Y⌋" by (rule A2) hence "(❙∀X Y. (𝒫 X ❙∧ (X ⇛ Y)) ❙→ 𝒫 Y) w" by (rule allE) hence "∀X Y. (𝒫 X w ∧ (X ⇛ Y) w) ⟶ 𝒫 Y w" by simp hence "∀Y. (𝒫 G⇧^{A}w ∧ (G⇧^{A}⇛ Y) w) ⟶ 𝒫 Y w" by (rule allE) hence 6: "(𝒫 G⇧^{A}w ∧ (G⇧^{A}⇛ Q) w) ⟶ 𝒫 Q w" by (rule allE) have "⌊𝒫 G⇧^{A}⌋" by (rule T2) hence "𝒫 G⇧^{A}w" by (rule allE) hence "𝒫 G⇧^{A}w ∧ (G⇧^{A}⇛ Q) w" using 5 by (rule conjI) from 6 this have "𝒫 Q w" by (rule mp) ― ‹Q is positive by A2 and T2› thus "(❙□(Q g)) w" using 2 by simp (*@{text "←"} direction *) qed } hence "∀Z. (❙□(Z g)) w ⟷ (G⇧^{A}⇛ Z) w" by (rule allI) hence "(❙∀Z. ❙□(Z g) ❙↔ G⇧^{A}⇛ Z) w" by simp hence "ℰ⇧^{A}G⇧^{A}g w" by simp } hence "G⇧^{A}g w ⟶ ℰ⇧^{A}G⇧^{A}g w " by (rule impI) } hence "∀x. G⇧^{A}x w ⟶ ℰ⇧^{A}G⇧^{A}x w " by (rule allI) } thus ?thesis by (rule allI) qed text‹ Axiom 11.37 (Anderson's version of 11.25) › axiomatization where A5: "⌊𝒫 NE⇧^{A}⌋" lemma True nitpick[satisfy] oops ― ‹model found: so far all axioms consistent› text‹ Theorem 11.38 - Possibilist existence of God implies necessary actualist existence: › theorem GodExistenceImpliesNecExistence: "⌊❙∃ G⇧^{A}❙→ ❙□❙∃⇧^{E}G⇧^{A}⌋" proof - { fix w { assume "∃x. G⇧^{A}x w" then obtain g where 1: "G⇧^{A}g w" .. hence "NE⇧^{A}g w" using A5 by blast ― ‹axiom 11.25› hence "∀Y. (ℰ⇧^{A}Y g w) ⟶ (❙□❙∃⇧^{E}Y) w" by simp hence 2: "(ℰ⇧^{A}G⇧^{A}g w) ⟶ (❙□❙∃⇧^{E}G⇧^{A}) w" by (rule allE) have "(❙∀x. G⇧^{A}x ❙→ (ℰ⇧^{A}G⇧^{A}x)) w" using GodIsEssential by (rule allE) ― ‹GodIsEssential follows from Axioms 11.11 and 11.3B› hence "(G⇧^{A}g ❙→ (ℰ⇧^{A}G⇧^{A}g)) w" by (rule allE) hence "G⇧^{A}g w ⟶ ℰ⇧^{A}G⇧^{A}g w" by blast from this 1 have 3: "ℰ⇧^{A}G⇧^{A}g w" by (rule mp) from 2 3 have "(❙□❙∃⇧^{E}G⇧^{A}) w" by (rule mp) } hence "(∃x. G⇧^{A}x w) ⟶ (❙□❙∃⇧^{E}G⇧^{A}) w" by (rule impI) hence "((❙∃x. G⇧^{A}x) ❙→ ❙□❙∃⇧^{E}G⇧^{A}) w" by simp } thus ?thesis by (rule allI) qed text‹ Some useful rules: › lemma modal_distr: "⌊❙□(φ ❙→ ψ)⌋ ⟹ ⌊(❙◇φ ❙→ ❙◇ψ)⌋" by blast lemma modal_trans: "(⌊φ ❙→ ψ⌋ ∧ ⌊ψ ❙→ χ⌋) ⟹ ⌊φ ❙→ χ⌋" by simp text‹ Anderson's version of Theorem 11.27 › theorem possExistenceImpliesNecEx: "⌊❙◇❙∃ G⇧^{A}❙→ ❙□❙∃⇧^{E}G⇧^{A}⌋" ― ‹local consequence› proof - have "⌊❙∃ G⇧^{A}❙→ ❙□❙∃⇧^{E}G⇧^{A}⌋" using GodExistenceImpliesNecExistence by simp ― ‹follows from Axioms 11.11, 11.25 and 11.3B› hence "⌊❙□(❙∃ G⇧^{A}❙→ ❙□❙∃⇧^{E}G⇧^{A})⌋" using NEC by simp hence 1: "⌊❙◇❙∃ G⇧^{A}❙→ ❙◇❙□❙∃⇧^{E}G⇧^{A}⌋" by (rule modal_distr) have 2: "⌊❙◇❙□❙∃⇧^{E}G⇧^{A}❙→ ❙□❙∃⇧^{E}G⇧^{A}⌋" using symm tran by metis from 1 2 have "⌊❙◇❙∃ G⇧^{A}❙→ ❙◇❙□❙∃⇧^{E}G⇧^{A}⌋ ∧ ⌊❙◇❙□❙∃⇧^{E}G⇧^{A}❙→ ❙□❙∃⇧^{E}G⇧^{A}⌋" by simp thus ?thesis by (rule modal_trans) qed lemma T4: "⌊❙◇❙∃ G⇧^{A}⌋ ⟶ ⌊❙□❙∃⇧^{E}G⇧^{A}⌋" using possExistenceImpliesNecEx by (rule localImpGlobalCons) ― ‹global consequence› text‹ Conclusion - Necessary (actualist) existence of God: › lemma GodNecExists: "⌊❙□❙∃⇧^{E}G⇧^{A}⌋" using T3 T4 by metis subsection ‹Modal Collapse› text‹ Modal collapse is countersatisfiable › lemma "⌊❙∀Φ.(Φ ❙→ (❙□ Φ))⌋" nitpick oops text‹ \pagebreak › section ‹Conclusion› text‹ We presented a shallow semantical embedding in Isabelle/HOL for an intensional higher-order modal logic (a successor of Montague/Gallin intensional logics) as introduced by M. Fitting in his textbook \emph{Types, Tableaus and G\"odel's God} @{cite "Fitting"}. We subsequently employed this logic to formalise and verify all results (theorems, examples and exercises) relevant to the discussion of G\"odel's ontological argument in the last part of Fitting's book. Three different versions of the ontological argument have been considered: the first one by G\"odel himself (respectively, Scott), the second one by Fitting and the last one by Anderson. › text‹ By employing an interactive theorem-prover like Isabelle, we were not only able to verify Fitting's results, but also to guarantee consistency. We could prove even stronger versions of many of the theorems and find better countermodels (i.e. with smaller cardinality) than the ones presented in the book. Another interesting aspect was the possibility to explore the implications of alternative formalisations for definitions and theorems which shed light on interesting philosophical issues concerning entailment, essentialism and free will, which are currently the subject of some follow-up analysis. › text‹ The latest developments in \emph{automated theorem proving} allow us to engage in much more experimentation during the formalisation and assessment of arguments than ever before. The potential reduction (of several orders of magnitude) in the time needed for proving or disproving theorems (compared to pen-and-paper proofs), results in almost real-time feedback about the suitability of our speculations. The practical benefits of computer-supported argumentation go beyond mere quantitative (easier, faster and more reliable proofs). The advantages are also qualitative, since it fosters a different approach to argumentation: We can now work iteratively (by `trial-and-error') on an argument by making gradual adjustments to its definitions, axioms and theorems. This allows us to continuously expose and revise the assumptions we indirectly commit ourselves everytime we opt for some particular formalisation. \pagebreak › (*<*) end (*>*)