Formulae in such logics are built from constant symbols, variables, relational symbols, classical connectives, the modal connectives
and
,
the quantifiers
and
,
and parentheses, in a usual way.
A term is either a constant symbol or a variable. We call
,
where Ri is a relation symbol of arity n and t1, ..., tn are terms, a classical atom. A formula is called ground if it contains no quantifiers and no variables.
We define the modal depth of a formula
to be the maximal nesting depth of modalities (i.e. the connectives
and
)
in
.
Definitionfixed-domain first-order Kripke model over a signature without functions ,
simply called first-order Kripke model, is a tuple
,
where D is a set called domain,
is a Kripke frame, and m is an interpretation of constant symbols and relation symbols. For a constant symbol ci, m(ci) is an element of D, denoted also by ciM. For a relation symbol Rj of arity n and a world
,
m(w)(Rj) is a n-ary relation on D, denoted also by
RjM,w.
The satisfiability relation is defined in a usual way (see Definition 5.1.3).
Let L be the name of some propositional normal modal logic, e.g. KD. To define what is the first-order modal logic L we define the class of admissible interpretations to be the class of first-order Kripke models
with
being a L-frame.
The definitions of L-satisfiability and L-models, for a first-order normal modal logic L, are straightforward.
If X is a set of formulae and
is a formula then we write
to denote the fact that for any first-order L-model M, if
then
.