(*<*) theory FittingProof 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 ‹Fitting's Solution› text‹ In this section we consider Fitting's solution to the objections raised in his discussion of G\"odel's Argument pp. 164-9, especially the problem of \emph{modal collapse}, which has been metaphysically interpreted as implying a rejection of free will. Since we are generally commited to the existence of free will (in a pre-theoretical sense), such a result is philosophically unappealing and rather seen as a problem in the argument's formalisation. › text‹ This part of the book still leaves several details unspecified and the reader is thus compelled to fill in the gaps. As a result, we came across some premises and theorems allowing for different formalisations and therefore leading to disparate implications. Only some of those cases are shown here for illustrative purposes. The options we have chosen here are such that they indeed validate the argument (and we assume that they correspond to Fitting's intention. › subsection ‹General Definitions› text‹ The following is an existence predicate for our object-language. (We have previously shown it is equivalent to its meta-logical counterpart.) › abbreviation existencePredicate::"↑⟨𝟬⟩" ("E!") where "E! x ≡ (λw. (❙∃⇧^{E}y. y❙≈x) w)" text‹ Reminder: The `‹⦇_⦈›' parenthesis are used to convert an extensional object into its `rigid' intensional counterpart (e.g. ‹⦇φ⦈ ≡ λ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⦈)" subsection ‹Part I - God's Existence is Possible› 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 (modified)› 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 text‹ \bigbreak › text‹ \emph{T1} (Positive properties are possibly instantiated) can be formalised in two different ways: › theorem T1a: "⌊❙∀X::⟨𝟬⟩. 𝒫 X ❙→ ❙◇(❙∃⇧^{E}z. ⦇X z⦈)⌋" using A1a A2 by blast ― ‹this is the one used in the book› theorem T1b: "⌊❙∀X::↑⟨𝟬⟩. 𝒫 ↓X ❙→ ❙◇(❙∃⇧^{E}z. X z)⌋" nitpick oops ― ‹this one is also possible but not valid so we won't use it› text‹ Some interesting (non-)equivalences: › lemma "⌊❙□❙∃⇧^{E}(Q::↑⟨𝟬⟩) ❙↔ ❙□(❙∃⇧^{E}❙↓Q)⌋" by simp lemma "⌊❙□❙∃⇧^{E}(Q::↑⟨𝟬⟩) ❙↔ ((λX. ❙□❙∃⇧^{E}X) Q)⌋" by simp lemma "⌊❙□❙∃⇧^{E}(Q::↑⟨𝟬⟩) ❙↔ ((λX. ❙□❙∃⇧^{E}❙↓X) Q)⌋" by simp lemma "⌊❙□❙∃⇧^{E}(Q::↑⟨𝟬⟩) ❙↔ ((λX. ❙□❙∃⇧^{E}X) ❙↓Q)⌋" nitpick oops ― ‹not equivalent!› text‹ \emph{T3} (God exists possibly) can be formalised in two different ways, using a \emph{de re} or a \emph{de dicto} reading. › theorem T3_deRe: "⌊(λX. ❙◇❙∃⇧^{E}X) ❙↓G⌋" using T1a T2 by simp theorem T3_deDicto: "⌊❙◇❙∃⇧^{E}❙↓G⌋" nitpick oops ― ‹countersatisfiable› text‹ From the last two theorems, we think ‹T3_deRe› should be the version originally implied in the book, since ‹T3_deDicto› is not valid (\emph{T1b} were valid but it isn't) › lemma assumes T1b: "⌊❙∀X. 𝒫 ↓X ❙→ ❙◇(❙∃⇧^{E}z. X z)⌋" shows T3_deDicto: "⌊❙◇❙∃⇧^{E}❙↓G⌋" using assms T2 by simp subsection ‹Part II - God's Existence is Necessary if Possible› text‹ In this variant ‹𝒫› also designates rigidly, as shown in the last section. › axiomatization where A4a: "⌊❙∀X. 𝒫 X ❙→ ❙□(𝒫 X)⌋" ― ‹axiom 11.11› lemma A4b: "⌊❙∀X. ❙¬(𝒫 X) ❙→ ❙□❙¬(𝒫 X)⌋" using A1a A1b A4a by blast lemma True nitpick[satisfy] oops ― ‹model found: so far all axioms consistent› abbreviation essenceOf::"↑⟨⟨𝟬⟩,𝟬⟩" ("ℰ") where "ℰ Y x ≡ ⦇Y x⦈ ❙∧ (❙∀Z::⟨𝟬⟩. ⦇Z x⦈ ❙→ Y ⇛ Z)" text‹ Theorem 11.20 - Informal Proposition 5 › theorem GodIsEssential: "⌊❙∀x. G x ❙→ ((ℰ ↓⇩_{1}G) x)⌋" using A1b by metis text‹ Theorem 11.21 › theorem God_starIsEssential: "⌊❙∀x. G* x ❙→ ((ℰ ↓⇩_{1}G*) x)⌋" by meson abbreviation necExistencePred:: "↑⟨𝟬⟩" ("NE") where "NE x ≡ λw. (❙∀Y. ℰ Y x ❙→ ❙□(❙∃⇧^{E}z. ⦇Y z⦈)) w" text‹ \bigbreak › text‹ Informal Axiom 5 › axiomatization where A5: "⌊𝒫 ↓NE⌋" lemma True nitpick[satisfy] oops ― ‹model found: so far all axioms consistent› text‹ Reminder: We use ‹↓G› instead of ‹G› because it is more explicit. See (non-)equivalences above. › lemma "⌊❙∃ G ❙↔ ❙∃ ❙↓G⌋" by simp lemma "⌊❙∃⇧^{E}G ❙↔ ❙∃⇧^{E}❙↓G⌋" by simp lemma "⌊❙□❙∃⇧^{E}G ❙↔ ❙□❙∃⇧^{E}❙↓G⌋" by simp text‹ Theorem 11.26 (Informal Proposition 7) - (possibilist) existence of God implies necessary (actualist) existence. › text‹ There are two different ways of formalising this theorem. Both of them are proven valid: › text‹ First version: › theorem GodExImpliesNecEx_v1: "⌊❙∃ ❙↓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 hence "∀Y. (ℰ Y g w) ⟶ (❙□(❙∃⇧^{E}z. ⦇Y z⦈)) w" by simp hence "(ℰ (λx. G x w) g w) ⟶ (❙□(❙∃⇧^{E}z. ⦇(λx. G x w) z⦈)) w" by (rule allE) hence 2: "((ℰ ↓⇩_{1}G) g w) ⟶ (❙□(❙∃⇧^{E}G)) w" using A4b by meson have "(❙∀x. G x ❙→ ((ℰ ↓⇩_{1}G) x)) w" using GodIsEssential by (rule allE) hence "(G g ❙→ ((ℰ ↓⇩_{1}G) g)) w" by (rule allE) hence "G g w ⟶ (ℰ ↓⇩_{1}G) g w" by simp from this 1 have 3: "(ℰ ↓⇩_{1}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‹ Second version (which can be proven directly by automated tools using the previous version): › theorem GodExImpliesNecEx_v2: "⌊❙∃ ❙↓G ❙→ ((λX. ❙□❙∃⇧^{E}X) ❙↓G)⌋" using A4a GodExImpliesNecEx_v1 by metis text‹ In contrast to G\"odel's argument (as presented by Fitting), the following theorems can be proven in logic \emph{K} (the \emph{S5} axioms are no longer needed): › text‹ Theorem 11.27 - Informal Proposition 8 › theorem possExImpliesNecEx_v1: "⌊❙◇❙∃ ❙↓G ❙→ ❙□❙∃⇧^{E}❙↓G⌋" using GodExImpliesNecEx_v1 T3_deRe by metis theorem possExImpliesNecEx_v2: "⌊(λX. ❙◇❙∃⇧^{E}X) ❙↓G ❙→ ((λX. ❙□❙∃⇧^{E}X) ❙↓G)⌋" using GodExImpliesNecEx_v2 by blast text‹ Corollaries: › lemma T4_v1: "⌊❙◇❙∃ ❙↓G⌋ ⟶ ⌊❙□❙∃⇧^{E}❙↓G⌋" using possExImpliesNecEx_v1 by simp lemma T4_v2: "⌊(λX. ❙◇❙∃⇧^{E}X) ❙↓G⌋ ⟶ ⌊(λX. ❙□❙∃⇧^{E}X) ❙↓G⌋" using possExImpliesNecEx_v2 by simp subsection ‹Conclusion (\emph{De Re} and \emph{De Dicto} Reading)› text‹ Version I - Necessary Existence of God (\emph{de dicto}): › lemma GodNecExists_v1: "⌊❙□❙∃⇧^{E}❙↓G⌋" using GodExImpliesNecEx_v1 T3_deRe by fastforce ― ‹corollary 11.28› lemma God_starNecExists_v1: "⌊❙□❙∃⇧^{E}❙↓G*⌋" using GodNecExists_v1 GodDefsAreEquivalent by simp lemma "⌊❙□(λX. ❙∃⇧^{E}X) ❙↓G*⌋" using God_starNecExists_v1 by simp ― ‹\emph{de dicto} shown here explicitly› text‹ Version II - Necessary Existence of God (\emph{de re}) › lemma GodNecExists_v2: "⌊(λX. ❙□❙∃⇧^{E}X) ❙↓G⌋" using T3_deRe T4_v2 by blast lemma God_starNecExists_v2: "⌊(λX. ❙□❙∃⇧^{E}X) ❙↓G*⌋" using GodNecExists_v2 GodDefsAreEquivalent by simp subsection ‹Modal Collapse› text‹ Modal collapse is countersatisfiable even in \emph{S5}. Note that countermodels with a cardinality of one for the domain of individuals are found by \emph{Nitpick} (the countermodel shown in the book has cardinality of two). › lemma "⌊❙∀Φ.(Φ ❙→ (❙□ Φ))⌋" nitpick[card 't=1, card i=2] oops ― ‹countermodel found in \emph{K}› axiomatization where S5: "equivalence aRel" ― ‹assume \emph{S5} logic› lemma "⌊❙∀Φ.(Φ ❙→ (❙□ Φ))⌋" nitpick[card 't=1, card i=2] oops ― ‹countermodel also found in \emph{S5}› text‹ \pagebreak › (*<*) end (*>*)