Theory AndersonProof

(*<*)
theory AndersonProof  
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 ‹Anderson's Alternative›
  
text‹ In this final section, we verify Anderson's emendation of G\"odel's argument, as it is presented in the last
part of the textbook by Fitting (pp. 169-171). ›
  
subsection ‹General Definitions›
 
abbreviation existencePredicate::"↑⟨𝟬⟩" ("E!") 
  where "E! x  ≡ λw. (❙∃⇧^Ey. y❙≈x) w"
  
consts positiveProperty::"↑⟨↑⟨𝟬⟩⟩" ("𝒫")
  
abbreviation God::"↑⟨𝟬⟩" ("G⇧^A") where "G⇧^A ≡ λ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›
  A2: "⌊❙∀X Y. (𝒫 X ❙∧ (X ⇛ Y)) ❙→ 𝒫 Y⌋" and   ― ‹Axiom 11.5›
  T2: "⌊𝒫 G⇧^A⌋"                                 ― ‹Proposition 11.16›
        
lemma True nitpick[satisfy] oops ― ‹model found: axioms are consistent›
    
theorem T1: "⌊❙∀X. 𝒫 X ❙→ ❙◇❙∃⇧^E X⌋" 
  using A1a A2 by blast  ― ‹positive properties are possibly instantiated›  
theorem T3: "⌊❙◇❙∃⇧^E G⇧^A⌋" using T1 T2 by simp  ― ‹God exists possibly›  
    
    
subsection ‹Part II - God's Existence is Necessary if Possible›
        
text‹  ‹𝒫› now satisfies only one of the stability conditions. But since the argument uses an \emph{S5} logic, 
the other stability condition is implied. Therefore ‹𝒫› becomes rigid (see p. 124).  ›
axiomatization where
  A4a: "⌊❙∀X. 𝒫 X ❙→ ❙□(𝒫 X)⌋"      ― ‹axiom 11.11›
      
text‹  We again postulate our \emph{S5} axioms: ›
axiomatization where
 refl: "reflexive aRel" and
 tran: "transitive aRel" and
 symm: "symmetric aRel"
 
lemma True nitpick[satisfy] oops ― ‹model found: so far all axioms consistent›
 
abbreviation rigidPred::"('t⇒io)⇒io" where
 "rigidPred τ ≡ (λβ. ❙□((λz. β ❙≈ z) ❙↓τ)) ❙↓τ"

lemma A4b: "⌊❙∀X. ❙¬(𝒫 X) ❙→ ❙□❙¬(𝒫 X)⌋" 
  using A4a symm by auto ― ‹symmetry is needed (which corresponds to \emph{B} axiom)›
lemma "⌊rigidPred 𝒫⌋" 
  using A4a A4b by blast ― ‹@{text "𝒫"} is therefore rigid in a \emph{B} logic›

text‹  Essence, Anderson Version (Definition 11.34) ›
abbreviation essenceOf::"↑⟨↑⟨𝟬⟩,𝟬⟩" ("ℰ⇧^A") where
  "ℰ⇧^A Y x ≡ (❙∀Z. ❙□(Z x) ❙↔ Y ⇛ Z)"

      
text‹  Necessary Existence, Anderson Version (Definition 11.35)  ›  
abbreviation necessaryExistencePred::"↑⟨𝟬⟩" ("NE⇧^A") 
  where "NE⇧^A x  ≡ (λw. (❙∀Y.  ℰ⇧^A Y x ❙→ ❙□❙∃⇧^E Y) w)"
    
text‹  Theorem 11.36 - If g is God-like, then the property of being God-like is the essence of g. ›

text‹ As shown before, this theorem's proof could be completely automatized for G\"odel's and Fitting's variants.
For Anderson's version however, we had to provide Isabelle with some help based on the corresponding natural-language proof 
given by Anderson (see \<^cite>‹"anderson90:_some_emend_of_goedel_ontol_proof"› Theorem 2*, p. 296) ›
(*Anderson's Proof: Suppose that g is God-like* and necessarily has a property Q. Then
by definition (of "God-like*"), that property is positive. But necessarily, if
Q is positive, then if anything is God-like*, then it has Q -again by the
definition of "God-like* ," together with the fact that if something has a
property necessarily, then it has the property. But if a property is positive,
then it is necessarily positive (Axiom 4). Hence, if Q is positive, then it is
entailed by being God-like* (by modal logic-as in the original Theorem 2).
But Q is positive and hence is entailed by being God-like*. Thus we have
proved that if an entity is God-like* and has a property essentially, then that
property is entailed by the property of being God-like*.
Suppose a property Q is entailed by the property of being God-like*. Then
Q is positive by Axioms 2 and 3* and therefore, since g is God-like*, g has
Q necessarily (by the definition of "God-like*"). Hence, if something is
God-like*, it has a property essentially if and only if that property is entailed
by being God-like-i.e., God-likeness* is an essence* of that thing.
Q.E.D.*)
theorem GodIsEssential: "⌊❙∀x. G⇧^A x ❙→ (ℰ⇧^A G⇧^A x)⌋"
proof -
{
  fix w
  {
    fix g
    {
      assume "G⇧^A g w"
      hence 1: "∀Y. (𝒫 Y w) ⟷ (❙□(Y g)) w" by simp
      {
        fix Q
        from 1 have 2: "(𝒫 Q w) ⟷ (❙□(Q g)) w" by (rule allE)
        have  "(❙□(Q g)) w ⟷ (G⇧^A ⇛ Q) w" ― ‹we need to prove @{text "→"} and @{text "←"}›
        proof
            assume "(❙□(Q g)) w" ― ‹suppose g is God-like and necessarily has Q›
            hence 3: "(𝒫 Q w)" using 2 by simp ― ‹then Q is positive›
            
            {
              fix u
              have "(𝒫 Q u) ⟶ (∀x. G⇧^A x u ⟶ (❙□(Q x)) u)" 
                by auto ― ‹using the definition of God-like›
              have "(𝒫 Q u) ⟶ (∀x. G⇧^A x u ⟶ ((Q x)) u)" 
                using refl by auto ― ‹and using @{text "□(φ x) ⟶ φ x"}›
            }    
            hence "∀z. (𝒫 Q z) ⟶ (∀x. G⇧^A x z ⟶ Q x z)" by (rule allI)
            hence "⌊𝒫 Q ❙→ (❙∀x. G⇧^A x ❙→ Q x)⌋"
              by auto ― ‹if Q is positive, then whatever is God-like has Q›
            hence "⌊❙□(𝒫 Q ❙→ (❙∀x. G⇧^A x ❙→ Q x))⌋" by (rule NEC) 
            
            hence "⌊(❙□(𝒫 Q)) ❙→ ❙□(❙∀x. G⇧^A x ❙→ Q x)⌋" using K by auto
            hence "⌊(❙□(𝒫 Q)) ❙→ G⇧^A ⇛ Q⌋" by simp
            hence "((❙□(𝒫 Q)) ❙→ G⇧^A ⇛ Q) w" by (rule allE)
            hence 4: "(❙□(𝒫 Q)) w ⟶ (G⇧^A ⇛ Q) w" by simp (*if a property is necessarily positive, then it is entailed by being God-like*)
            have "⌊❙∀X. 𝒫 X ❙→ ❙□(𝒫 X)⌋" by (rule A4a) ― ‹using axiom 4›
            hence "(❙∀X. 𝒫 X ❙→ (❙□(𝒫 X))) w" by (rule allE)
            hence "𝒫 Q w ⟶ (❙□(𝒫 Q)) w" by (rule allE)
            hence "𝒫 Q w ⟶ (G⇧^A ⇛ Q) w" using 4 by simp (*if Q is positive, then it is entailed by being God-like*)
            thus "(G⇧^A ⇛ Q) w" using 3 by (rule mp) ― ‹@{text "→"} direction›
         next
           assume 5: "(G⇧^A ⇛ Q) w" ― ‹suppose Q is entailed by being God-like›
           have "⌊❙∀X Y. (𝒫 X ❙∧ (X ⇛ Y)) ❙→ 𝒫 Y⌋" by (rule A2)
           hence "(❙∀X Y. (𝒫 X ❙∧ (X ⇛ Y)) ❙→ 𝒫 Y) w" by (rule allE)
           hence "∀X Y. (𝒫 X w ∧ (X ⇛ Y) w) ⟶ 𝒫 Y w" by simp
           hence "∀Y. (𝒫 G⇧^A w ∧ (G⇧^A ⇛ Y) w) ⟶ 𝒫 Y w" by (rule allE)
           hence 6: "(𝒫 G⇧^A w ∧ (G⇧^A ⇛ Q) w) ⟶ 𝒫 Q w" by (rule allE)
           have "⌊𝒫 G⇧^A⌋" by (rule T2)
           hence "𝒫 G⇧^A w" by (rule allE)
           hence "𝒫 G⇧^A w ∧ (G⇧^A ⇛ Q) w" using 5 by (rule conjI)
           from 6 this have "𝒫 Q w" by (rule mp) ― ‹Q is positive by A2 and T2›
           thus "(❙□(Q g)) w" using 2 by simp (*@{text "←"} direction *)
         qed    
     } 
     hence  "∀Z. (❙□(Z g)) w ⟷ (G⇧^A ⇛ Z) w" by (rule allI)
     hence "(❙∀Z. ❙□(Z g) ❙↔  G⇧^A ⇛ Z) w" by simp
     hence "ℰ⇧^A G⇧^A g w" by simp
    }
    hence "G⇧^A g w  ⟶ ℰ⇧^A G⇧^A g w " by (rule impI)
  }
  hence "∀x. G⇧^A x w  ⟶ ℰ⇧^A G⇧^A x w "  by (rule allI)
}
 thus ?thesis by (rule allI) 
qed

text‹  Axiom 11.37 (Anderson's version of 11.25) ›
axiomatization where 
 A5: "⌊𝒫 NE⇧^A⌋"
 
lemma True nitpick[satisfy] oops ― ‹model found: so far all axioms consistent›
 
text‹  Theorem 11.38 - Possibilist existence of God implies necessary actualist existence:  › 
theorem GodExistenceImpliesNecExistence: "⌊❙∃ G⇧^A ❙→  ❙□❙∃⇧^E G⇧^A⌋"
proof -
{
  fix w 
  {
    assume "∃x. G⇧^A x w"
    then obtain g where 1: "G⇧^A g w" ..
    hence "NE⇧^A g w" using A5 by blast                  ― ‹axiom 11.25›
    hence "∀Y. (ℰ⇧^A Y g w) ⟶ (❙□❙∃⇧^E Y) w" by simp
    hence 2: "(ℰ⇧^A G⇧^A g w) ⟶ (❙□❙∃⇧^E G⇧^A) w" by (rule allE)
    have  "(❙∀x. G⇧^A x ❙→ (ℰ⇧^A G⇧^A x)) w" using GodIsEssential
      by (rule allE) ― ‹GodIsEssential follows from Axioms 11.11 and 11.3B›
    hence  "(G⇧^A g ❙→ (ℰ⇧^A G⇧^A g)) w" by (rule allE)
    hence  "G⇧^A g w ⟶ ℰ⇧^A G⇧^A g w"  by blast
    from this 1 have 3: "ℰ⇧^A G⇧^A g w" by (rule mp)
    from 2 3 have "(❙□❙∃⇧^E G⇧^A) w" by (rule mp)
  }
  hence "(∃x. G⇧^A x w) ⟶ (❙□❙∃⇧^E G⇧^A) w" by (rule impI)
  hence "((❙∃x. G⇧^A x) ❙→  ❙□❙∃⇧^E G⇧^A) w" by simp
}
 thus ?thesis by (rule allI) 
qed
    
text‹  Some useful rules: ›    
lemma modal_distr: "⌊❙□(φ ❙→ ψ)⌋ ⟹ ⌊(❙◇φ ❙→ ❙◇ψ)⌋" by blast
lemma modal_trans: "(⌊φ ❙→ ψ⌋ ∧ ⌊ψ ❙→ χ⌋) ⟹ ⌊φ ❙→ χ⌋" by simp

text‹  Anderson's version of Theorem 11.27  › 
theorem possExistenceImpliesNecEx: "⌊❙◇❙∃ G⇧^A ❙→ ❙□❙∃⇧^E G⇧^A⌋" ― ‹local consequence›
proof -
  have "⌊❙∃ G⇧^A ❙→ ❙□❙∃⇧^E G⇧^A⌋" using GodExistenceImpliesNecExistence 
    by simp ― ‹follows from Axioms 11.11, 11.25 and 11.3B›
  hence "⌊❙□(❙∃ G⇧^A ❙→ ❙□❙∃⇧^E G⇧^A)⌋" using NEC by simp
  hence 1: "⌊❙◇❙∃ G⇧^A ❙→ ❙◇❙□❙∃⇧^E G⇧^A⌋" by (rule modal_distr)
  have 2: "⌊❙◇❙□❙∃⇧^E G⇧^A ❙→ ❙□❙∃⇧^E G⇧^A⌋" using symm tran by metis
  from 1 2 have "⌊❙◇❙∃ G⇧^A ❙→ ❙◇❙□❙∃⇧^E G⇧^A⌋ ∧ ⌊❙◇❙□❙∃⇧^E G⇧^A ❙→ ❙□❙∃⇧^E G⇧^A⌋" by simp
  thus ?thesis by (rule modal_trans)
qed

lemma T4: "⌊❙◇❙∃ G⇧^A⌋ ⟶ ⌊❙□❙∃⇧^E G⇧^A⌋" using possExistenceImpliesNecEx 
    by (rule localImpGlobalCons) ― ‹global consequence›
  
text‹  Conclusion - Necessary (actualist) existence of God:  ›    
lemma GodNecExists: "⌊❙□❙∃⇧^E G⇧^A⌋" using T3 T4 by metis    
    
subsection ‹Modal Collapse›
  
text‹  Modal collapse is countersatisfiable  ›
lemma "⌊❙∀Φ.(Φ ❙→ (❙□ Φ))⌋" nitpick oops
    
text‹  \pagebreak ›
    
section ‹Conclusion›
text‹  We presented a shallow semantical embedding in Isabelle/HOL for an intensional higher-order modal logic
(a successor of Montague/Gallin intensional logics) as introduced by M. Fitting in his textbook \emph{Types, Tableaus and 
G\"odel's God} \<^cite>‹"Fitting"›. 
We subsequently employed this logic to formalise and verify all results (theorems, examples and exercises) relevant 
to the discussion of G\"odel's ontological argument in the last part of Fitting's book. Three different versions of
the ontological argument have been considered: the first one by G\"odel himself (respectively, Scott), the second 
one by Fitting and the last one by Anderson. ›
  
text‹ By employing an interactive theorem-prover like Isabelle, we were not only able to verify Fitting's results,
but also to guarantee consistency. We could prove even stronger versions
of many of the theorems and find better countermodels (i.e. with smaller cardinality) than the ones presented in the book.
Another interesting aspect was the possibility to explore the implications of alternative formalisations
for definitions and theorems which shed light on interesting philosophical issues concerning entailment,
essentialism and free will, which are currently the subject of some follow-up analysis. ›

text‹ The latest developments in \emph{automated theorem proving} allow us to engage in much more experimentation
during the formalisation and assessment of arguments than ever before. The potential reduction (of several orders of magnitude)
in the time needed for proving or disproving theorems (compared to pen-and-paper proofs), results in almost real-time
feedback about the suitability of our speculations. The practical benefits of computer-supported argumentation go beyond
mere quantitative (easier, faster and more reliable proofs). The advantages are also qualitative, since it fosters a
different approach to argumentation: We can now work iteratively (by `trial-and-error') on an argument
by making gradual adjustments to its definitions, axioms and theorems. This allows us to continuously expose and revise 
the assumptions we indirectly commit ourselves everytime we opt for some particular formalisation.
\pagebreak
 ›
(*<*)
end
(*>*)