In this chapter we outline some common terminology, notation and facts about syntactic and semantic logical concepts that are used, mutatis mutandis, in all chapters in the part.

We assume that the reader has basic background on propositional and first-order classical logic. Some general references are listed in the bibliographic notes.

Preliminaries on Modal Logic

Modal Logical Languages and Connectives

Throughout the book we assume that the generic notion of modal logic subsumes the one of temporal logic. That applies, in particular, to modal languages, operators, formulae, etc. For instance, whenever we say ‘modal formulae’, that also refers, in particular, to temporal formulae, unless otherwise specified.

Modal languages. Hereafter we assume an arbitrarily fixed multimodal language L with an alphabet containing a possibly infinite set of atomic propositions PROP, a sufficient set of propositional connectives from which all others are definable – typically something like conjunction and negation – plus an abstract family of (usually, unary or binary) modal operators O.We call the pair (O, PROP) the signature of the language. For instance, given the set of actions Act, we will use the set of modal operators O = ﹛EXa, AXa | a ∈ Act﹜. The modal μ-calculus introduced in Chapter 8 follows a slightly different syntax for modal operators, see Section 8.1.1.

Logical connectives. Throughout this book we will use standard notation for the propositional logical connectives, as follows.

1. • _ for truth;

2. • ⊥ for falsum;

3. • ￢ for negation;

4. • ∧ for conjunction;

5. • ∨ for disjunction;

6. • →for implication (a.k.a., conditional);

7. • ↔for bi-implication (a.k.a., bi-conditional). Often this is also called ‘equivalence’.We will reserve the use of this word for relations of equivalence, e.g. between formulae.