Theory IHOML_Examples

(*<*)
theory IHOML_Examples
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 ‹Textbook Examples›
  
text‹  In this section we provide further evidence that our embedded logic works as intended by proving the examples discussed in the book.
 In many cases, we consider further theorems which we derived from the original ones. We were able to confirm that all results
 (proofs or counterexamples) agree with Fitting's claims. ›
  
subsection ‹Modal Logic - Syntax and Semantics (Chapter 7)›

text‹ Reminder: We call a term \emph{relativized} if it is of the form ‹↓α›
(i.e. an intensional term preceded by the \emph{extension-of} operator), otherwise it is \emph{non-relativized}.
Relativized terms are non-rigid and non-relativized terms are rigid. ›
  
subsubsection ‹Considerations Regarding ‹βη›-redex  (p. 94)›

text‹  ‹βη›-redex is valid for non-relativized (intensional or extensional) terms:  ›
lemma "⌊((λα. φ α)  (τ::↑𝟬)) ❙↔ (φ  τ)⌋" by simp
lemma "⌊((λα. φ α)  (τ::𝟬)) ❙↔ (φ  τ)⌋" by simp
lemma "⌊((λα. ❙□φ α) (τ::↑𝟬)) ❙↔ (❙□φ τ)⌋" by simp
lemma "⌊((λα. ❙□φ α) (τ::𝟬)) ❙↔ (❙□φ τ)⌋" by simp    
text‹  ‹βη›-redex is valid for relativized terms as long as no modal operators occur inside the predicate abstract:  ›
lemma "⌊((λα. φ α) ⇃(τ::↑𝟬)) ❙↔ (φ ⇃τ)⌋" by simp
text‹  ‹βη›-redex is non-valid for relativized terms when modal operators are present:  ›
lemma "⌊((λα. ❙□φ α) ⇃(τ::↑𝟬)) ❙↔ (❙□φ ⇃τ)⌋" nitpick oops   ― ‹countersatisfiable›
lemma "⌊((λα. ❙◇φ α) ⇃(τ::↑𝟬)) ❙↔ (❙◇φ ⇃τ)⌋" nitpick oops   ― ‹countersatisfiable›
    
text‹  Example 7.13, p. 96: ›
lemma "⌊(λX. ❙◇❙∃X)  (P::↑⟨𝟬⟩) ❙→ ❙◇((λX. ❙∃X)  P)⌋"  by simp    
lemma "⌊(λX. ❙◇❙∃X) ❙↓(P::↑⟨𝟬⟩) ❙→ ❙◇((λX. ❙∃X) ❙↓P)⌋"
  nitpick[card 't=1, card i=2] oops ― ‹nitpick finds same counterexample as book›
text‹  with other types for @{term "P"}:  ›
lemma "⌊(λX. ❙◇❙∃X)  (P::↑⟨↑𝟬⟩) ❙→ ❙◇((λX. ❙∃X)  P)⌋"  by simp    
lemma "⌊(λX. ❙◇❙∃X) ❙↓(P::↑⟨↑𝟬⟩) ❙→ ❙◇((λX. ❙∃X) ❙↓P)⌋" 
  nitpick[card 't=1, card i=2] oops ― ‹countersatisfiable›
lemma "⌊(λX. ❙◇❙∃X)  (P::↑⟨⟨𝟬⟩⟩) ❙→ ❙◇((λX. ❙∃X)  P)⌋"  by simp    
lemma "⌊(λX. ❙◇❙∃X) ❙↓(P::↑⟨⟨𝟬⟩⟩) ❙→ ❙◇((λX. ❙∃X) ❙↓P)⌋" 
  nitpick[card 't=1, card i=2] oops ― ‹countersatisfiable›
lemma "⌊(λX. ❙◇❙∃X)  (P::↑⟨↑⟨𝟬⟩⟩)❙→ ❙◇((λX. ❙∃X)  P)⌋"  by simp    
lemma "⌊(λX. ❙◇❙∃X) ❙↓(P::↑⟨↑⟨𝟬⟩⟩)❙→ ❙◇((λX. ❙∃X) ❙↓P)⌋" 
  nitpick[card 't=1, card i=2] oops ― ‹countersatisfiable›
    
text‹  Example 7.14, p. 98: ›
lemma "⌊(λX. ❙◇❙∃X) ❙↓(P::↑⟨𝟬⟩) ❙→ (λX. ❙∃X) ❙↓P⌋" by simp
lemma "⌊(λX. ❙◇❙∃X)  (P::↑⟨𝟬⟩) ❙→ (λX. ❙∃X)  P⌋" 
  nitpick[card 't=1, card i=2] oops ― ‹countersatisfiable›
text‹  with other types for @{term "P"}:  ›
lemma "⌊(λX. ❙◇❙∃X) ❙↓(P::↑⟨↑𝟬⟩) ❙→ (λX. ❙∃X) ❙↓P⌋" by simp
lemma "⌊(λX. ❙◇❙∃X)  (P::↑⟨↑𝟬⟩) ❙→ (λX. ❙∃X)  P⌋" 
  nitpick[card 't=1, card i=2] oops ― ‹countersatisfiable›
lemma "⌊(λX. ❙◇❙∃X) ❙↓(P::↑⟨⟨𝟬⟩⟩) ❙→ (λX. ❙∃X) ❙↓P⌋" by simp
lemma "⌊(λX. ❙◇❙∃X)  (P::↑⟨⟨𝟬⟩⟩) ❙→ (λX. ❙∃X)  P⌋" 
  nitpick[card 't=1, card i=2] oops ― ‹countersatisfiable›
lemma "⌊(λX. ❙◇❙∃X) ❙↓(P::↑⟨↑⟨𝟬⟩⟩)❙→ (λX. ❙∃X) ❙↓P⌋" by simp
lemma "⌊(λX. ❙◇❙∃X)  (P::↑⟨↑⟨𝟬⟩⟩)❙→ (λX. ❙∃X)  P⌋" 
  nitpick[card 't=1, card i=2] oops ― ‹countersatisfiable›
    
text‹  Example 7.15, p. 99: ›
lemma "⌊❙□(P (c::↑𝟬)) ❙→ (❙∃x::↑𝟬. ❙□(P x))⌋" by auto
text‹  with other types for @{term "P"}:  ›
lemma "⌊❙□(P (c::𝟬)) ❙→ (❙∃x::𝟬. ❙□(P x))⌋" by auto
lemma "⌊❙□(P (c::⟨𝟬⟩)) ❙→ (❙∃x::⟨𝟬⟩. ❙□(P x))⌋" by auto
    
text‹  Example 7.16, p. 100: ›
lemma "⌊❙□(P ⇃(c::↑𝟬)) ❙→ (❙∃x::𝟬. ❙□(P x))⌋" 
  nitpick[card 't=2, card i=2] oops ― ‹counterexample with two worlds found›
    
text‹  Example 7.17, p. 101: ›
lemma "⌊❙∀Z::↑𝟬. (λx::𝟬.  ❙□((λy::𝟬.  x ❙≈ y) ⇃Z)) ⇃Z⌋" 
  nitpick[card 't=2, card i=2] oops ― ‹countersatisfiable›
lemma "⌊❙∀z::𝟬.  (λx::𝟬.  ❙□((λy::𝟬.  x ❙≈ y)  z)) z⌋" by simp
lemma "⌊❙∀Z::↑𝟬. (λX::↑𝟬. ❙□((λY::↑𝟬. X ❙≈ Y)  Z)) Z⌋" by simp
    
subsubsection ‹Exercises (p. 101)›
    
text‹  For Exercises 7.1 and 7.2 see variations on Examples 7.13 and 7.14 above.  ›
text‹  Exercise 7.3:  ›    
lemma "⌊❙◇❙∃(P::↑⟨𝟬⟩) ❙→ (❙∃X::↑𝟬. ❙◇(P ⇃X))⌋" by auto
text‹  Exercise 7.4:  ›  
lemma "⌊❙◇(❙∃x::𝟬. (λY. Y x) ❙↓(P::↑⟨𝟬⟩)) ❙→ (❙∃x. (λY. ❙◇(Y x)) ❙↓P)⌋" 
  nitpick[card 't=1, card i=2] oops ― ‹countersatisfiable›    
    
text‹  For Exercise 7.5 see Example 7.17 above.  ›
text‹ \bigbreak ›    
subsection ‹Miscellaneous Matters (Chapter 9)›

subsubsection ‹Equality Axioms (Subsection 1.1)›
    
text‹  Example 9.1:  ›
lemma "⌊((λX. ❙□(X ⇃(p::↑𝟬))) ❙↓(λx. ❙◇(λz. z ❙≈ x) ⇃p))⌋" 
  by auto ― ‹using normal equality›
lemma "⌊((λX. ❙□(X ⇃(p::↑𝟬))) ❙↓(λx. ❙◇(λz. z ❙≈⇧L x) ⇃p))⌋" 
  by auto ― ‹using Leibniz equality›
lemma "⌊((λX. ❙□(X  (p::↑𝟬))) ❙↓(λx. ❙◇(λz. z ❙≈⇧C x) p))⌋" 
  by simp  ― ‹using equality as defined for individual concepts›

    
subsubsection ‹Extensionality (Subsection 1.2)›
  
text‹  In Fitting's book (p. 118), extensionality is assumed (globally) for extensional terms. While Fitting introduces 
the following extensionality principles as axioms, they are already implicitly valid in Isabelle/HOL:  ›    
lemma EXT: "∀α::⟨𝟬⟩. ∀β::⟨𝟬⟩. (∀γ::𝟬. (α γ ⟷ β γ)) ⟶ (α = β)" by auto
lemma EXT_set: "∀α::⟨⟨𝟬⟩⟩. ∀β::⟨⟨𝟬⟩⟩. (∀γ::⟨𝟬⟩. (α γ ⟷ β γ)) ⟶ (α = β)" 
  by auto
    
subsubsection ‹\emph{De Re} and \emph{De Dicto} (Subsection 2)›

text‹  \emph{De re} is equivalent to \emph{de dicto} for non-relativized (extensional or intensional) terms:  ›
lemma "⌊❙∀α. ((λβ. ❙□(α β)) (τ::𝟬))   ❙↔ ❙□((λβ. (α β)) τ)⌋" by simp
lemma "⌊❙∀α. ((λβ. ❙□(α β)) (τ::↑𝟬))  ❙↔ ❙□((λβ. (α β)) τ)⌋" by simp
lemma "⌊❙∀α. ((λβ. ❙□(α β)) (τ::⟨𝟬⟩))  ❙↔ ❙□((λβ. (α β)) τ)⌋" by simp
lemma "⌊❙∀α. ((λβ. ❙□(α β)) (τ::↑⟨𝟬⟩)) ❙↔ ❙□((λβ. (α β)) τ)⌋" by simp

text‹  \emph{De re} is not equivalent to \emph{de dicto} for relativized terms:  ›    
lemma "⌊❙∀α. ((λβ. ❙□(α β)) ⇃(τ::↑𝟬)) ❙↔ ❙□( (λβ. (α β)) ⇃τ)⌋" 
  nitpick[card 't=2, card i=2] oops ― ‹countersatisfiable›
lemma "⌊❙∀α. ((λβ. ❙□(α β)) ❙↓(τ::↑⟨𝟬⟩)) ❙↔ ❙□( (λβ. (α β)) ❙↓τ)⌋" 
  nitpick[card 't=1, card i=2] oops ― ‹countersatisfiable›
  
text‹  Proposition 9.6 - If we can prove one side of the equivalence, then we can prove the other (p. 120):  ›
abbreviation deDictoImplDeRe::"↑𝟬⇒io" 
  where "deDictoImplDeRe τ ≡ ❙∀α. ❙□((λβ. (α β)) ⇃τ) ❙→ ((λβ. ❙□(α β)) ⇃τ)"
abbreviation deReImplDeDicto::"↑𝟬⇒io" 
  where "deReImplDeDicto τ ≡ ❙∀α. ((λβ. ❙□(α β)) ⇃τ) ❙→ ❙□((λβ. (α β)) ⇃τ)"
abbreviation deReEquDeDicto::"↑𝟬⇒io" 
  where "deReEquDeDicto τ ≡ ❙∀α. ((λβ. ❙□(α β)) ⇃τ) ❙↔ ❙□((λβ. (α β)) ⇃τ)"
text‹ \bigbreak ›
abbreviation deDictoImplDeRe_pred::"('t⇒io)⇒io" 
  where "deDictoImplDeRe_pred τ ≡ ❙∀α. ❙□((λβ. (α β)) ❙↓τ) ❙→ ((λβ. ❙□(α β)) ❙↓τ)"
abbreviation deReImplDeDicto_pred::"('t⇒io)⇒io" 
  where "deReImplDeDicto_pred τ ≡ ❙∀α. ((λβ. ❙□(α β)) ❙↓τ) ❙→ ❙□((λβ. (α β)) ❙↓τ)"
abbreviation deReEquDeDicto_pred::"('t⇒io)⇒io" 
  where "deReEquDeDicto_pred τ ≡ ❙∀α. ((λβ. ❙□(α β)) ❙↓τ) ❙↔ ❙□((λβ. (α β)) ❙↓τ)"

text‹  We can prove local consequence: ›
lemma AimpB: "⌊deReImplDeDicto (τ::↑𝟬) ❙→ deDictoImplDeRe τ⌋"
  by force ― ‹for individuals›
lemma AimpB_p: "⌊deReImplDeDicto_pred (τ::↑⟨𝟬⟩) ❙→ deDictoImplDeRe_pred τ⌋"
  by force ― ‹for predicates›

text‹  And global consequence follows directly (since local consequence implies global consequence, as shown before): ›
lemma "⌊deReImplDeDicto (τ::↑𝟬)⌋ ⟶ ⌊deDictoImplDeRe τ⌋"
  using AimpB by (rule localImpGlobalCons) ― ‹for individuals›
lemma "⌊deReImplDeDicto_pred (τ::↑⟨𝟬⟩)⌋ ⟶ ⌊deDictoImplDeRe_pred τ⌋"
  using AimpB_p by (rule localImpGlobalCons) ― ‹for predicates›
       
    
subsubsection ‹Rigidity (Subsection 3)›
    
text‹  (Local) rigidity for intensional individuals:  ›    
abbreviation rigidIndiv::"↑⟨↑𝟬⟩" where
  "rigidIndiv τ ≡ (λβ. ❙□((λz. β ❙≈ z) ⇃τ)) ⇃τ"
text‹  (Local) rigidity for intensional predicates:  ›    
abbreviation rigidPred::"('t⇒io)⇒io" where
  "rigidPred τ ≡ (λβ. ❙□((λz. β ❙≈ z) ❙↓τ)) ❙↓τ"
  
text‹  Proposition 9.8 - An intensional term is rigid if and only if the \emph{de re/de dicto} distinction vanishes.
Note that we can prove this theorem for local consequence (global consequence follows directly).  ›  
lemma "⌊rigidIndiv (τ::↑𝟬) ❙→ deReEquDeDicto τ⌋" by simp
lemma "⌊deReImplDeDicto (τ::↑𝟬) ❙→ rigidIndiv τ⌋" by auto
lemma "⌊rigidPred (τ::↑⟨𝟬⟩) ❙→ deReEquDeDicto_pred τ⌋" by simp
lemma "⌊deReImplDeDicto_pred (τ::↑⟨𝟬⟩) ❙→ rigidPred τ⌋" by auto
   
subsubsection ‹Stability Conditions (Subsection 4)›
    
axiomatization where
 S5: "equivalence aRel" ― ‹using Sahlqvist correspondence for improved performance›
    
text‹  Definition 9.10 - Stability conditions come in pairs:  ›
abbreviation stabilityA::"('t⇒io)⇒io" where "stabilityA τ ≡ ❙∀α. (τ α) ❙→ ❙□(τ α)"
abbreviation stabilityB::"('t⇒io)⇒io" where "stabilityB τ ≡ ❙∀α. ❙◇(τ α) ❙→ (τ α)"

text‹  Proposition 9.10 - In an \emph{S5} modal logic both stability conditions are equivalent. ›
text‹  The last proposition holds for global consequence: ›  
lemma "⌊stabilityA (τ::↑⟨𝟬⟩)⌋ ⟶ ⌊stabilityB τ⌋" using S5 by blast    
lemma "⌊stabilityB (τ::↑⟨𝟬⟩)⌋ ⟶ ⌊stabilityA τ⌋" using S5 by blast    
text‹  But it does not hold for local consequence: ›      
lemma "⌊stabilityA (τ::↑⟨𝟬⟩) ❙→ stabilityB τ⌋" 
  nitpick[card 't=1, card i=2] oops ― ‹countersatisfiable›
lemma "⌊stabilityB (τ::↑⟨𝟬⟩) ❙→ stabilityA τ⌋" 
  nitpick[card 't=1, card i=2] oops ― ‹countersatisfiable›
    
text‹  Theorem 9.11 - A term is rigid if and only if it satisfies the stability conditions. Note that
 we can prove this theorem for local consequence (global consequence follows directly).  ›
theorem "⌊rigidPred (τ::↑⟨𝟬⟩) ❙↔ (stabilityA τ ❙∧ stabilityB τ)⌋" by meson   
theorem "⌊rigidPred (τ::↑⟨↑𝟬⟩) ❙↔ (stabilityA τ ❙∧ stabilityB τ)⌋" by meson   
theorem "⌊rigidPred (τ::↑⟨↑⟨𝟬⟩⟩) ❙↔ (stabilityA τ ❙∧ stabilityB τ)⌋" by meson   
text‹  \pagebreak ›
(*<*)
end
(*>*)