Theory GoedelProof_P2

theory GoedelProof_P2
imports IHOML
(*<*)
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. (Ey. yx) 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. yx)"  ― ‹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
(*>*)