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
lemma "⌊((λα. ❙◇φ α) ⇃(τ::↑𝟬)) ❙↔ (❙◇φ ⇃τ)⌋" nitpick oops
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
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
lemma "⌊(λX. ❙◇❙∃X) (P::↑⟨⟨𝟬⟩⟩) ❙→ ❙◇((λX. ❙∃X) P)⌋" by simp
lemma "⌊(λX. ❙◇❙∃X) ❙↓(P::↑⟨⟨𝟬⟩⟩) ❙→ ❙◇((λX. ❙∃X) ❙↓P)⌋"
nitpick[card 't=1, card i=2] oops
lemma "⌊(λX. ❙◇❙∃X) (P::↑⟨↑⟨𝟬⟩⟩)❙→ ❙◇((λX. ❙∃X) P)⌋" by simp
lemma "⌊(λX. ❙◇❙∃X) ❙↓(P::↑⟨↑⟨𝟬⟩⟩)❙→ ❙◇((λX. ❙∃X) ❙↓P)⌋"
nitpick[card 't=1, card i=2] oops
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
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
lemma "⌊(λX. ❙◇❙∃X) ❙↓(P::↑⟨⟨𝟬⟩⟩) ❙→ (λX. ❙∃X) ❙↓P⌋" by simp
lemma "⌊(λX. ❙◇❙∃X) (P::↑⟨⟨𝟬⟩⟩) ❙→ (λX. ❙∃X) P⌋"
nitpick[card 't=1, card i=2] oops
lemma "⌊(λX. ❙◇❙∃X) ❙↓(P::↑⟨↑⟨𝟬⟩⟩)❙→ (λX. ❙∃X) ❙↓P⌋" by simp
lemma "⌊(λX. ❙◇❙∃X) (P::↑⟨↑⟨𝟬⟩⟩)❙→ (λX. ❙∃X) P⌋"
nitpick[card 't=1, card i=2] oops
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
text‹ Example 7.17, p. 101: ›
lemma "⌊❙∀Z::↑𝟬. (λx::𝟬. ❙□((λy::𝟬. x ❙≈ y) ⇃Z)) ⇃Z⌋"
nitpick[card 't=2, card i=2] oops
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
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
lemma "⌊((λX. ❙□(X ⇃(p::↑𝟬))) ❙↓(λx. ❙◇(λz. z ❙≈⇧L x) ⇃p))⌋"
by auto
lemma "⌊((λX. ❙□(X (p::↑𝟬))) ❙↓(λx. ❙◇(λz. z ❙≈⇧C x) p))⌋"
by simp
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
lemma "⌊❙∀α. ((λβ. ❙□(α β)) ❙↓(τ::↑⟨𝟬⟩)) ❙↔ ❙□( (λβ. (α β)) ❙↓τ)⌋"
nitpick[card 't=1, card i=2] oops
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
lemma AimpB_p: "⌊deReImplDeDicto_pred (τ::↑⟨𝟬⟩) ❙→ deDictoImplDeRe_pred τ⌋"
by force
text‹ And global consequence follows directly (since local consequence implies global consequence, as shown before): ›
lemma "⌊deReImplDeDicto (τ::↑𝟬)⌋ ⟶ ⌊deDictoImplDeRe τ⌋"
using AimpB by (rule localImpGlobalCons)
lemma "⌊deReImplDeDicto_pred (τ::↑⟨𝟬⟩)⌋ ⟶ ⌊deDictoImplDeRe_pred τ⌋"
using AimpB_p by (rule localImpGlobalCons)
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"
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
lemma "⌊stabilityB (τ::↑⟨𝟬⟩) ❙→ stabilityA τ⌋"
nitpick[card 't=1, card i=2] oops
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