Definitions for Fixed-domain First-order Modal Logics over Signatures without Functions

Formulae in such logics are built from constant symbols, variables, relational symbols, classical connectives, the modal connectives $\Box$ and $\Diamond$, the quantifiers $\forall$ and $\exists$, and parentheses, in a usual way. A term is either a constant symbol or a variable. We call $R_i(t_1, \ldots, t_n)$, where R_i is a relation symbol of arity n and t₁, ..., t_n 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 $\phi$ to be the maximal nesting depth of modalities (i.e. the connectives $\Box$ and $\Diamond$) in $\phi$.

Definitionfixed-domain first-order Kripke model over a signature without functions $\Sigma$, simply called first-order Kripke model, is a tuple $M = \langle D, W, \tau, R, m \rangle$, where D is a set called domain, $\langle W, \tau, R\rangle$ is a Kripke frame, and m is an interpretation of constant symbols and relation symbols. For a constant symbol c_i, m(c_i) is an element of D, denoted also by c_i^M. For a relation symbol R_j of arity n and a world $w \in W$, m(w)(R_j) is a n-ary relation on D, denoted also by R_j^M,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 $M = \langle D, W, \tau, R, m \rangle$ with $\langle W, \tau, R\rangle$ 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 $\phi$ is a formula then we write $X \models_L \phi$ to denote the fact that for any first-order L-model M, if $M \vDash X$ then $M \vDash\phi$.