By convention, what are the tautologies and the consequence relation of modal logics

logicmodal-logic

When looking at a modal logic as a propositional logic, it seems like there are a few choices for which sentences form the tautologies (A, B, C below) and what the consequence relation should be (D, E below).

I'm not saying that these are all reasonable choices, just that they capture some of the intuition behind being a set of tautologies or being a consequence relation. If we treat the possible world semantics of modal logic as conceptually prior, what are the set of tautologies and the consequence relation normally considered to be?

$$ \text{$\varphi$ is a tautology if and only if it holds at the designated world $0$} \tag{A} $$
$$ \text{$\varphi$ is a tautology if and only if it holds at every world that's accessible from $0$ } \tag{B} $$
$$ \text{$\varphi$ is a tautology if and only if it holds at every world.} \tag{C} $$

$$ \text{$\Gamma \vdash \varphi$ holds if and only if $\varphi$ holds at $0$ whenever $\Gamma$ holds at the topic world} \tag{D} $$

$$ \text{$\Gamma \vdash \varphi$ holds if and only if, for every possible world $w$, at least one $\Gamma$ is false or $\varphi$ is true} \tag{E} $$

Best Answer

We can take validity to be the limiting case of logical consequence from the empty set. So, the question reduces to what logical consequence for modal languages consists in.

That's a non-trivial issue, since we actually have two natural candidates for being consequence relations: local consequence and global consequence. Both notions have different properties. The deeper reason for this difference is that local consequence is basically a first-order notion, while global consequence is a second-order notion. Let me explain.

Assuming the standard definition of frames and models for similarity types, I will restrict myself to consequence for a basic modal language $\mathcal{L}$, where we have exactly one 1-place modal operator $\Diamond$. For $\Phi \subseteq \mathcal{L}, \varphi \in \mathcal{L}$ we can define:

  • If $\mathcal{M} =(W,R ,V)$ is an $\mathcal{L}$-model and $w \in W$, let $\mathcal{M}, w \models \Phi$ iff $\mathcal{M}, w \models \psi$, for all $\psi \in \Phi$. If $\mathcal{F} =(W,R)$ is an $\mathcal{L}$-frame, let $\mathcal{F} \models \Phi$ iff $\mathcal{F} \models \psi$, for all $\psi \in \Phi$
  • $\varphi$ is a local consequence of $\Phi$ ($\Phi \models \varphi$) iff for any $\mathcal{L}$-model $\mathcal{M} = (W, R, V)$ and any $w \in W$ we have: $M, w \models \Phi$ only if $M, w \models \varphi$
  • $\varphi$ is a global consequence of $\Phi$ ($\Phi \models^g \varphi$) iff for every $\mathcal{L}$-frame we have: $\mathcal{F} \models \Phi$ only if $\mathcal{F} \models \phi$.

These notions of consequence have different properties. For instance for local consequence we have a deduction theorem, while this is not the case with the global notion. More importantly, choosing the global notion means to consider modal logic as a means to describe frames, while choosing the local version implies looking at modal logic as a way to talk about models. Modal logic as a frame description tool allows via its associated notion of global validity (global consequence from the empty set) to capture many essentially second-order properties like well-foundedness. This is no accident. As Thomason showed global consequence basically coincides with the consequence relation of monadic second order logic. So, global consequence and global validity are second-order concepts.

In contrast taking modal logic as talking about models means taking a first-order perspective on modal logic. Indeed the van Benthem characterization result tells us that modal logic as a means to describe models is the bisimulation invariant fragment of first-order logic. So, local consequence and local validity are first-order notions.

Of course matters a more complicated than outlined above. For instance I have said nothing on the consequence relation defined via so-called general frames. General frames yield a sort of connection between the local and the global notion. This is in parallel to the case of general models for second-order logic, which provide a first-order perspective on second-order logic. But the rough picture above should indicate the complexities involved in the notion of modal consequence, which have no parallel in classical logic.

Related Question