Theory FittingProof

(*<*)
theory FittingProof  
imports IHOML
begin
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 4,  atoms e = a b c d, timeout=60]
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. (❙∃⇧Ey. 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 ≡  ❙□(❙∀⇧Ez. ⦇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 ❙→ ❙◇(❙∃⇧Ez. ⦇X z⦈)⌋" 
  using A1a A2 by blast ― ‹this is the one used in the book›
theorem T1b: "⌊❙∀X::↑⟨𝟬⟩. 𝒫 ↓X ❙→ ❙◇(❙∃⇧Ez. 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 ❙→ ❙◇(❙∃⇧Ez. 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 ❙→ ((ℰ ↓⇩1G) x)⌋" using A1b by metis
text‹  Theorem 11.21  ›
theorem God_starIsEssential: "⌊❙∀x. G* x ❙→ ((ℰ ↓⇩1G*) x)⌋" by meson
    
abbreviation necExistencePred:: "↑⟨𝟬⟩" (‹NE›) where
  "NE x  ≡ λw. (❙∀Y.  ℰ Y x ❙→ ❙□(❙∃⇧Ez. ⦇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) ⟶ (❙□(❙∃⇧Ez. ⦇Y z⦈)) w" by simp
    hence "(ℰ (λx. G x w) g w) ⟶ (❙□(❙∃⇧Ez. ⦇(λx. G x w) z⦈)) w" by (rule allE)
    hence 2: "((ℰ ↓⇩1G) g w) ⟶ (❙□(❙∃⇧E G)) w" using A4b by meson
    have  "(❙∀x. G x ❙→ ((ℰ ↓⇩1G) x)) w" using GodIsEssential by (rule allE)
    hence  "(G g ❙→ ((ℰ ↓⇩1G) g)) w" by (rule allE)
    hence  "G g w ⟶ (ℰ ↓⇩1G) g w" by simp
    from this 1 have 3: "(ℰ ↓⇩1G) 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
(*>*)