Theory GoedelProof_P1

(*<*)
theory GoedelProof_P1
imports IHOML
begin
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 3,  atoms e = a b c d]
sledgehammer_params[verbose=true]
(*>*)  

section ‹G\"odel's Argument, Formally›

text‹ 
 "G\"odel's particular version of the argument is a direct descendent of that of Leibniz, which in turn derives
  from one of Descartes. These arguments all have a two-part structure: prove God's existence is necessary,
  if possible; and prove God's existence is possible." \<^cite>‹"Fitting"›, p. 138. › 

subsection ‹Part I - God's Existence is Possible›

text‹  We separate G\"odel's Argument as presented in Fitting's textbook (ch. 11) in two parts. For the first one, while Leibniz provides
  some kind of proof for the compatibility of all perfections, G\"odel goes on to prove an analogous result:
 \emph{(T1) Every positive property is possibly instantiated}, which together with \emph{(T2) God is a positive property}
  directly implies the conclusion. In order to prove \emph{T1}, G\"odel assumes \emph{A2: Any property entailed by a positive property is positive}. ›
text‹  We are currently contemplating a follow-up analysis of the philosophical implications of these axioms,
 which encompasses some criticism of the notion of \emph{property entailment} used by G\"odel throughout the argument. ›
  
subsubsection ‹General Definitions›
               
abbreviation existencePredicate::"↑⟨𝟬⟩" (‹E!›) 
  where "E! x  ≡ λw. (❙∃⇧Ey. y❙≈x) w" ― ‹existence predicate in object language›
    
lemma "E! x w ⟷ existsAt x w" 
  by simp ― ‹safety check: @{text "E!"} correctly matches its meta-logical counterpart›

consts positiveProperty::"↑⟨↑⟨𝟬⟩⟩" (‹𝒫›) ― ‹positiveness/perfection›
  
text‹  Definitions of God (later shown to be equivalent under axiom \emph{A1b}):  ›    
abbreviation God::"↑⟨𝟬⟩" (‹G›) where "G ≡ (λx. ❙∀Y. 𝒫 Y ❙→ Y x)"
abbreviation God_star::"↑⟨𝟬⟩" (‹G*›) where "G* ≡ (λx. ❙∀Y. 𝒫 Y ❙↔ Y x)"
  
text‹  Definitions needed to formalise \emph{A3}:  ›
abbreviation appliesToPositiveProps::"↑⟨↑⟨↑⟨𝟬⟩⟩⟩" (‹pos›) where
  "pos Z ≡  ❙∀X. Z X ❙→ 𝒫 X"  
abbreviation intersectionOf::"↑⟨↑⟨𝟬⟩,↑⟨↑⟨𝟬⟩⟩⟩" (‹intersec›) where
  "intersec X Z ≡  ❙□(❙∀x.(X x ❙↔ (❙∀Y. (Z Y) ❙→ (Y x))))" ― ‹quantifier is possibilist›  
abbreviation Entailment::"↑⟨↑⟨𝟬⟩,↑⟨𝟬⟩⟩" (infix ‹⇛› 60) where
  "X ⇛ Y ≡  ❙□(❙∀⇧Ez. X z ❙→ Y z)"
text‹ \bigbreak ›
  
subsubsection ‹Axioms›
    
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›
  A3: "⌊❙∀Z X. (pos Z ❙∧ intersec X Z) ❙→ 𝒫 X⌋" ― ‹axiom 11.10›

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 "⌊D⌋" using A1a A3 by metis

subsubsection ‹Theorems›
    
lemma "⌊❙∃X. 𝒫 X⌋" using A1b by auto
lemma "⌊❙∃X. 𝒫 X ❙∧  ❙◇❙∃⇧E X⌋" using A1a A1b A2 by metis
    
text‹  Being self-identical is a positive property:  ›
lemma "⌊(❙∃X. 𝒫 X ❙∧  ❙◇❙∃⇧E X) ❙→ 𝒫 (λx w. x = x)⌋" using A2 by fastforce
    
text‹  Proposition 11.6  ›
lemma "⌊(❙∃X. 𝒫 X) ❙→ 𝒫 (λx w. x = x)⌋" using A2 by fastforce
    
lemma "⌊𝒫 (λx w. x = x)⌋" using A1b A2  by blast
lemma "⌊𝒫 (λx w. x = x)⌋" using A3 by metis
                                
text‹  Being non-self-identical is a negative property: ›
lemma "⌊(❙∃X. 𝒫 X  ❙∧ ❙◇❙∃⇧E X) ❙→  𝒫 (❙⇁ (λx w. ¬x = x))⌋" 
  using A2 by fastforce
    
lemma "⌊(❙∃X. 𝒫 X) ❙→  𝒫 (❙⇁ (λx w. ¬x = x))⌋" using A2 by fastforce
lemma "⌊(❙∃X. 𝒫 X) ❙→  𝒫 (❙⇁ (λx w. ¬x = x))⌋" using A3 by metis 

text‹  Proposition 11.7  ›
lemma "⌊(❙∃X. 𝒫 X) ❙→ ❙¬𝒫 ((λx w. ¬x = x))⌋"  using A1a A2 by blast
lemma "⌊❙¬𝒫 (λx w. ¬x = x)⌋"  using A1a A2 by blast
 
text‹  Proposition 11.8 (Informal Proposition 1) - Positive properties are possibly instantiated:  ›
theorem T1: "⌊❙∀X. 𝒫 X ❙→ ❙◇❙∃⇧E X⌋" using A1a A2 by blast
    
text‹  Proposition 11.14 - Both defs (\emph{God/God*}) are equivalent. For improved performance we may prefer to use one or the other:  ›
lemma GodDefsAreEquivalent: "⌊❙∀x. G x ❙↔ G* x⌋" using A1b by force 

text‹  Proposition 11.15 - Possibilist existence of \emph{God} directly implies \emph{A1b}:  ›    
lemma "⌊❙∃ G* ❙→ (❙∀X. ❙¬(𝒫 X) ❙→ 𝒫 (❙⇁X))⌋" by meson

text‹  Proposition 11.16 - \emph{A3} implies \emph{P(G)} (local consequence):   ›   
lemma A3implT2_local: "⌊(❙∀Z X. (pos Z ❙∧ intersec X Z) ❙→ 𝒫 X) ❙→ 𝒫 G⌋"
proof -
  {
  fix w
  have 1: "pos 𝒫 w" by simp
  have 2: "intersec G 𝒫 w" by simp
  {    
    assume "(❙∀Z X. (pos Z ❙∧ intersec X Z) ❙→ 𝒫 X) w"
    hence "(❙∀X. ((pos 𝒫) ❙∧ (intersec X 𝒫)) ❙→ 𝒫 X) w"  by (rule allE)   
    hence "(((pos 𝒫) ❙∧ (intersec G 𝒫)) ❙→ 𝒫 G) w" by (rule allE)
    hence 3: "((pos 𝒫 ❙∧ intersec G 𝒫) w) ⟶ 𝒫 G w" by simp
    hence 4: "((pos 𝒫) ❙∧ (intersec G 𝒫)) w" using 1 2 by simp
    from 3 4 have "𝒫 G w" by (rule mp)
  }
  hence "(❙∀Z X. (pos Z ❙∧ intersec X Z) ❙→ 𝒫 X) w  ⟶ 𝒫 G w" by (rule impI)
  } 
  thus ?thesis by (rule allI)
qed    
    
text‹  \emph{A3} implies ‹P(G)› (as global consequence): ›
lemma A3implT2_global: "⌊❙∀Z X. (pos Z ❙∧ intersec X Z) ❙→ 𝒫 X⌋ ⟶ ⌊𝒫 G⌋" 
  using A3implT2_local by (rule localImpGlobalCons) 
  
text‹  Being Godlike is a positive property. Note that this theorem can be axiomatized directly,
as noted by Dana Scott (see \<^cite>‹"Fitting"›, p. 152). We will do so for the second part. ›
theorem T2: "⌊𝒫 G⌋" using A3implT2_global A3 by simp
  
text‹  Theorem 11.17 (Informal Proposition 3) - Possibly God exists: ›
theorem T3: "⌊❙◇❙∃⇧E G⌋"  using T1 T2 by simp

(*<*)
end
(*>*)