(* Christoph Benzmüller, February 2016 *)
theory QML
imports Main
begin
section {* Preliminaris *}
text {*
We present a semantic embedding of quantified modal logic (QML) in classical higher-order logic (HOL).
Quantifiers are provided for Boolean, first-, second- and
higher-order variables (for all types).
The theoretical background of the work presented here has been discussed in \cite{J23}.
This file is intended for reuse by further AFP articles on QML.
We begin by introducing type $i$ for the set of possible worlds and type $\mu$ for the set
of individuals. Formulae in quantified modal logic (QML) are functions from the set of possible worlds
to Booleans. For convenience, their type is written as $\sigma$. *}
typedecl i -- "type for possible worlds"
typedecl \ -- "type for individuals"
type_synonym \ = "(i\bool)"
section {* Embedding of Base Logic \emph{K} *}
text {* In Kripke semantics, a modal formula is interpreted over an arbitrary accessibility relation, a
binary relation between possible worlds. *}
consts r :: "i\i\bool" (infixr "r" 70) -- "accessibility relation r"
text {*
The set of classical connectives and quantifiers is \emph{lifted} to the modal level by passing an
additional parameter $w$, representing the current world, to the connectives'
subformulae or binders' scope. This parameter is only used actively in the definition of both
modalities $\{\Box, \diamond\}$, where it is applied to the accessibility relation $r$.
Modal connectives are typeset in bold font.\footnote{In Isabelle/jEdit, bold characters can be
entered by typing \texttt{\textbackslash bol} before entering the actual character.} Abbreviations
are used in place of definitions to avoid explicit mention of the embeddings' definitions when
invoking automated tools via \emph{Sledgehammer}. *}
abbreviation mtrue :: "\" ("\<^bold>\")
where "\<^bold>\ \ \w. True"
abbreviation mfalse :: "\" ("\<^bold>\")
where "\<^bold>\ \ \w. False"
abbreviation mnot :: "\\\" ("\<^bold>\_"[52]53)
where "\<^bold>\\ \ \w. \\(w)"
abbreviation mnegpred :: "(\\\)\(\\\)" ("\<^sup>\_"[52]53)
where "\<^sup>\\ \ \x.\w. \\(x)(w)"
abbreviation mand :: "\\\\\" (infixr"\<^bold>\"51)
where "\\<^bold>\\ \ \w. \(w)\\(w)"
abbreviation mor :: "\\\\\" (infixr"\<^bold>\"50)
where "\\<^bold>\\ \ \w. \(w)\\(w)"
abbreviation mimp :: "\\\\\" (infixr"\<^bold>\"49)
where "\\<^bold>\\ \ \w. \(w)\\(w)"
abbreviation mequ :: "\\\\\" (infixr"\<^bold>\"48)
where "\\<^bold>\\ \ \w. \(w)\\(w)"
abbreviation mforall :: "('a\\)\\" ("\<^bold>\")
where "\<^bold>\\ \ \w.\x. \(x)(w)"
abbreviation mforallB :: "('a\\)\\" (binder"\<^bold>\"[8]9)
where "\<^bold>\x. \(x) \ \<^bold>\\"
abbreviation mexists :: "('a\\)\\" ("\<^bold>\")
where "\<^bold>\\ \ \w.\x. \(x)(w)"
abbreviation mexistsB :: "('a\\)\\" (binder"\<^bold>\"[8]9)
where "\<^bold>\x. \(x) \ \<^bold>\\"
abbreviation meq :: "\\\\\" (infixr"\<^bold>="52) -- "Equality"
where "x\<^bold>=y \ \w. x = y"
abbreviation meqL :: "\\\\\" (infixr"\<^bold>=\<^sup>L"52) -- "Leibniz Equality"
where "x\<^bold>=\<^sup>Ly \ \<^bold>\\. \(x)\<^bold>\\(y)"
abbreviation mbox :: "\\\" ("\<^bold>\_"[52]53)
where "\<^bold>\\ \ \w.\v. w r v \ \(v)"
abbreviation mdia :: "\\\" ("\<^bold>\_"[52]53)
where "\<^bold>\\ \ \w.\v. w r v \ \(v)"
text {* Finally, a formula is valid if and only if it is satisfied in all worlds. *}
abbreviation valid :: "\\bool" ("\_\"[8]109)
where "\p\ \ \w. p w"
section {* Axiomatizations of Further Systems *}
text {* Different modal logics can be axiomatized through adding a choice of the following definitions
as axioms: *}
(*
using the \emph{Sahlqvist correspondence}.
The best known logics \emph{K4, K5, KB, K45, KB5, D, D4, D5, D45, ...} are obtained through
the addition of combinations of the following axioms: *}
*)
abbreviation M
where "M \ \<^bold>\\. \<^bold>\\ \<^bold>\ \"
abbreviation B
where "B \ \<^bold>\\. \ \<^bold>\ \<^bold>\\<^bold>\\"
abbreviation D
where "D \ \<^bold>\\. \<^bold>\\ \<^bold>\ \<^bold>\\"
abbreviation IV
where "IV \ \<^bold>\\. \<^bold>\\ \<^bold>\ \<^bold>\\<^bold>\\"
abbreviation V
where "V \ \<^bold>\\. \<^bold>\\ \<^bold>\ \<^bold>\\<^bold>\\"
text {* Because the embedding is of a semantic nature, it is more efficient to instead make use of
the well-known \emph{Sahlqvist correspondence}, which links these axioms to constraints on a
model's accessibility relation: axioms $M, B, D, IV, V$ impose reflexivity, symmetry, seriality,
transitivity and euclideanness respectively. *}
abbreviation reflexive
where "reflexive \ (\x. x r x)"
abbreviation symmetric
where "symmetric \ (\x y. x r y \ y r x)"
abbreviation serial :: "bool"
where "serial \ (\x. \y. x r y)"
abbreviation transitive :: "bool"
where "transitive \ (\x y z. ((x r y) \ (y r z) \ (x r z)))"
abbreviation euclidean :: "bool"
where "euclidean \ (\x y z. ((x r y) \ (x r z) \ (y r z)))"
text {* Using these definitions, we can derive axioms for the most common modal logics. Thereby we
are free to use either the semantic constraints or the related Sahlqvist axioms. Here we provide
both versions. We recommend to use the semantic constraints. *}
abbreviation D_sem :: bool
where "D_sem \ serial"
abbreviation D_ax :: bool
where "D_ax \ \D\"
abbreviation B_sem :: bool
where "B_sem \ symmetric"
abbreviation B_ax :: bool
where "B_ax \ \B\"
abbreviation T_sem :: bool
where "T_sem \ reflexive"
abbreviation T_ax :: bool
where "T_ax \ \M\"
abbreviation S4_sem :: bool
where "S4_sem \