Theory QML
theory QML
imports Relations
begin
nitpick_params[user_axioms=true, show_all, expect=genuine, format = 3, atoms e = a b c d]
section ‹Embedding of Quantified Modal Logic›
text‹\noindent{As is well known, the Isabelle proof assistant \<^cite>‹"Isabelle"› does not natively support modal logics, so
we have used a technique known as \emph{shallow semantic embedding}, which allows us
to take advantage of the expressive power of higher-order logic in order to embed the semantics
of an object language. We draw on previous work on the embedding of multimodal logics in HOL \<^cite>‹"J23"›,
which has successfully been applied to the analysis and verification of ontological arguments
(e.g. \<^cite>‹C55 and J32 and J35›).}›
subsection ‹Type Declarations›
typedecl e
typedecl w
type_synonym wo = "w⇒bool"
subsection ‹Logical Constants as Truth-Sets›
text‹\noindent{Using the technique of \emph{shallow semantic embedding} each operator gets defined as a function
on world-dependent formulas or \emph{truth sets}.}›
abbreviation mand::"wo⇒wo⇒wo" (infixr "❙∧"51)
where "φ❙∧ψ ≡ λw. (φ w)∧(ψ w)"
abbreviation mor::"wo⇒wo⇒wo" (infixr "❙∨"50)
where "φ❙∨ψ ≡ λw. (φ w)∨(ψ w)"
abbreviation mimp::"wo⇒wo⇒wo" (infixr "❙→"49)
where "φ❙→ψ ≡ λw. (φ w)⟶(ψ w)"
abbreviation mequ::"wo⇒wo⇒wo" (infix "❙↔"48)
where "φ❙↔ψ ≡ λw. (φ w)⟷(ψ w)"
abbreviation mnot::"wo⇒wo" ("❙¬_"[52]53)
where "❙¬φ ≡ λw. ¬(φ w)"
abbreviation xor:: "bool⇒bool⇒bool" (infix"⊕"50) where "φ⊕ψ ≡ (φ∨ψ) ∧ ¬(φ∧ψ)"
abbreviation mxor::"wo⇒wo⇒wo" (infix"❙⊕"50) where "φ❙⊕ψ ≡ λw. (φ w)⊕(ψ w)"
text‹\noindent{We embed a modal logic \emph{K} by defining the box and diamond operators using restricted quantification
over the set of `accessible' worlds (using an \emph{accessibility} relation \emph{R} as a guard).}›
consts R::"w⇒w⇒bool" (infix "r"70)
abbreviation mbox :: "wo⇒wo" ("❙□_"[52]53)
where "❙□φ ≡ λw.∀v. (w r v)⟶(φ v)"
abbreviation mdia :: "wo⇒wo" ("❙◇_"[52]53)
where "❙◇φ ≡ λw.∃v. (w r v)∧(φ v)"
subsection ‹Quantification›
text‹\noindent{Quantifiers are defined analogously.}›
abbreviation mforall::"('t⇒wo)⇒wo" ("❙∀")
where "❙∀Φ ≡ λw.∀x. (Φ x w)"
abbreviation mexists::"('t⇒wo)⇒wo" ("❙∃")
where "❙∃Φ ≡ λw.∃x. (Φ x w)"
abbreviation mforallB :: "('t⇒wo)⇒wo" (binder "❙∀"[8]9)
where "❙∀x. (φ x) ≡ ❙∀φ"
abbreviation mexistsB :: "('t⇒wo)⇒wo" (binder "❙∃"[8]9)
where "❙∃x. (φ x) ≡ ❙∃φ"
subsection ‹Equality›
text‹\noindent{Two different definitions of equality are given. The first one is an extension of standard
equality for use in world-dependent formulas. The second is the well-known Leibniz equality.}›
abbreviation meq:: "'t⇒'t⇒wo" (infix "❙≈"60)
where "x ❙≈ y ≡ λw. x = y"
abbreviation meqL:: "e⇒e⇒wo" (infix "❙≈⇧L"52)
where "x ❙≈⇧L y ≡ λw. ∀φ. (φ x w)⟶(φ y w)"
subsection ‹Validity›
text‹\noindent{Validity is defined as truth in \emph{all} worlds and represented by wrapping the formula
in special brackets (‹⌊-⌋›).}›
abbreviation valid::"wo⇒bool" ("⌊_⌋") where "⌊ψ⌋ ≡ ∀w.(ψ w)"
subsection ‹Verifying the Embedding›
text‹\noindent{The above definitions introduce modal logic \emph{K} with quantification,
as evidenced by the following tests.}›
lemma K: "⌊(❙□(φ ❙→ ψ)) ❙→ (❙□φ ❙→ ❙□ψ)⌋" by simp
lemma NEC: "⌊φ⌋ ⟹ ⌊❙□φ⌋" by simp
text‹\noindent{Local consequence implies global consequence (not the other way round).}›
lemma localImpGlobalCons: "⌊φ ❙→ ξ⌋ ⟹ ⌊φ⌋ ⟶ ⌊ξ⌋" by simp
lemma "⌊φ⌋ ⟶ ⌊ξ⌋ ⟹ ⌊φ ❙→ ξ⌋" nitpick oops
text‹\noindent{(Converse-)Barcan formulas are validated in this embedding.}›
lemma "⌊(❙∀x.❙□(φ x)) ❙→ ❙□(❙∀x.(φ x))⌋" by simp
lemma "⌊❙□(❙∀x.(φ x)) ❙→ (❙∀x.❙□(φ x))⌋" by simp
text‹\noindent{‹β›-redex is valid.}›
lemma "⌊(λα. φ α) (τ::w⇒e) ❙↔ (φ τ)⌋" by simp
lemma "⌊(λα. φ α) (τ::e) ❙↔ (φ τ)⌋" by simp
lemma "⌊(λα. ❙□φ α) (τ::w⇒e) ❙↔ (❙□φ τ)⌋" by simp
lemma "⌊(λα. ❙□φ α) (τ::e) ❙↔ (❙□φ τ)⌋" by simp
text‹\noindent{Modal collapse is countersatisfiable, as shown by Nitpick \<^cite>‹"Nitpick"›.}›
lemma "⌊φ ❙→ ❙□φ⌋" nitpick oops
subsection ‹Axiomatization of Further Logics›
text‹\noindent{The best-known normal logics (\emph{K4, K5, KB, K45, KB5, D, D4, D5, ...}) can be obtained by
combinations of the following axioms.}›
abbreviation T where "T ≡ ❙∀φ. ❙□φ ❙→ φ"
abbreviation B where "B ≡ ❙∀φ. φ ❙→ ❙□❙◇φ"
abbreviation D where "D ≡ ❙∀φ. ❙□φ ❙→ ❙◇φ"
abbreviation IV where "IV ≡ ❙∀φ. ❙□φ ❙→ ❙□❙□φ"
abbreviation V where "V ≡ ❙∀φ. ❙◇φ ❙→ ❙□❙◇φ"
text‹\noindent{Instead of postulating combinations of the above axioms we make use of
the well-known \emph{Sahlqvist correspondence}, which links axioms to constraints on a model's accessibility
relation (cf. \<^cite>‹"J23"› for further details).
We show that reflexivity, symmetry, seriality, transitivity and euclideanness imply
axioms \emph{T, B, D, IV, V} respectively.\footnote{Implication can also be proven in the reverse direction
(which is not needed for our purposes).
Using these definitions, we can derive axioms for the most common modal logics (see also \<^cite>‹"C47"›).
Thereby we are free to use either the semantic constraints or the related \emph{Sahlqvist} axioms. Here we provide
both versions. In what follows we use the semantic constraints for improved performance.}}›
lemma "reflexive R ⟹ ⌊T⌋" by blast
lemma "symmetric R ⟹ ⌊B⌋" by blast
lemma "serial R ⟹ ⌊D⌋" by blast
lemma "transitive R ⟹ ⌊IV⌋" by blast
lemma "euclidean R ⟹ ⌊V⌋" by blast
lemma "preorder R ⟹ ⌊T⌋ ∧ ⌊IV⌋" by blast
lemma "equivalence R ⟹ ⌊T⌋ ∧ ⌊V⌋" by blast
end