Theory GoedelProof_P2

(*<*)
theory GoedelProof_P2
imports IHOML
begin
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 3,  atoms e = a b c d, timeout=60]
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. (❙∃⇧Ey. 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 ≡  ❙□(❙∀⇧Ez. 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 "(❙□(❙∀⇧Ez. 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 ❙→ ❙□(❙∀⇧Ez. G z ❙→ Z z)) w" by force
    hence "∀x. G x w ⟶ ((λy. Q) x ❙→ ❙□(❙∀⇧Ez. G z ❙→ (λy. Q) z)) w" by force
    hence "∀x. G x w ⟶ (Q ❙→ ❙□(❙∀⇧Ez. G z ❙→ Q)) w" by simp
    hence 1: "(∃x. G x w) ⟶ ((Q ❙→ ❙□(❙∀⇧Ez. G z ❙→ Q)) w)" by (rule useful)
    have "∃x. G x w" using GodExistenceIsValid by auto
    from 1 this have "(Q ❙→ ❙□(❙∀⇧Ez. G z ❙→ Q)) w" by (rule mp)
    hence "(Q ❙→ ❙□((❙∃⇧Ez. G z) ❙→ Q)) w" using useful by blast
    hence "(Q ❙→ (❙□(❙∃⇧Ez. 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
(*>*)