In the book Modal Logics (pp.$\,$84$-$85) of Patrick Blackburn, Maarten de Rijke and Yde Venema (alternatively, here,$\,$p.11$\,$"PROPOSITION $4$"), the authors claim that compactness for their basic modal logic can be proven by reducing it to the compactness theorem of first-order logic as explained in the following. (They did not provide the proof itself but only claim its existence.)

We can translate any formula in basic modal logic ($ML$) to first-order logic ($FOL$) using a standard translation $ST_x:ML\rightarrow FOL$ ($x$ being a first-order variable) with:

  1. $ST_x(p_i)=P_i x$, for every proposition $p\in PROP$
  2. $ST_x(\bot)=x\ne x$
  3. $ST_x(\lnot\psi)=\lnot ST_x(\psi)$
  4. $ST_x(\psi\lor\varphi)=ST_x(\psi)\lor ST_x(\varphi)$
  5. $ST_x(\Box\psi)=\forall y(Rxy\rightarrow ST_y(\psi))$

Now, we can take every modal structure $\mathfrak{M}=(W,R,V)$ as first-order structure, since it provides the set of worlds $W$ as domain together with relations $R^\mathfrak{M}$, and $P_i^\mathfrak{M}:=V(p_i)$.
So we have a theorem:

For all modal structures $\mathfrak{M}$ it is $\mathfrak{M},w\vDash_{ML}\psi$ if and only if $\mathfrak{M}\vDash_{FOL}ST_x(\psi)[x\leftarrow w]$,
where $[x\leftarrow w]$ means that $w$ is assigned to the free FOL-variable $x$.

Now they claim (without proof) that:

we can use this bridge to import results, ideas, and proof techniques from one to the other

by which they include compactness. But in order to show the compactness theorem for $ML$, we have to show as a Lemma that every $ML$-formula $\psi$ is satisfiable if and only if $ST_x(\psi)$ is satisfiable. Clearly, we can show "$\Rightarrow$" by using the $\mathfrak{M}$ that satisfies $\psi$ to construct a satisfying structure for $ST_x(\psi)$ as explained. But how can we prove that if $ST_x(\psi)$ has a model (i.e. a satisfying FOL-structure), then $\psi$ has a model (i.e. a satisfying modal structure)? Or why would we not need to do this?

My idea would be to afterwards set up the compactness proof as follows.
Let $\Gamma\subseteq ML$ be a satisfiable set of basic modal logic formulas. This is by Lemma (TODO) equivalent to $\{ST_x(\psi)|\psi\in\Gamma\}$ being satisfiable, which means by the compactness theorem for first order logic, that every finite subset $\Phi\subseteq\{ST_x(\psi)|\psi\in\Gamma\}$ is satisfiable, which by Lemma (TODO) means that every finite $\Phi\subseteq\Gamma$ is satisfiable.

How can we either show "$\Leftarrow$" of Lemma (TODO), or avoid it being required? Why can't it be that there is some $FOL$-structure which satisfies $ST_x(\psi)$, from which we cannot construct a modal structure $\mathfrak{M}$ to satisfy $\psi$? Since clearly, $FOL$-structures are much more general than modal structures.

  • $\begingroup$ Hint: There is a much better explanation given here, on pages 29,30, including the compactness proof. Unlike in the cited literature of the question, explicitly $\mathcal{M}\mapsto\mathcal{S}_\mathcal{M}$ is a bijection between the class of modal models and first-order models. Unfortunately, ''$\Leftarrow$'' of the Lemma (which is Theorem 2.11 (a)), is still not proven. $\endgroup$
    – xamid
    Jun 8, 2017 at 9:17

1 Answer 1


If I got your question right, Proposition 2.47 of the blue book (or, Proposition 3 of the handbook) establishes equivalence of a modal formula and its translation (in corresponding models). As for compactness, it is perfectly explained in Example 2.48 of the blue book. It goes roughly like this: if we have a set of modal formulae, and every subset of the set is satisfiable (i.e. has a model), then it follows, by Proposition 2.47, that all subsets of the standard translation of the initial set are satisfiable as well. Hence, by compactness theorem, the whole set is satisfiable, and we can translate its formulae back to formulae of modal logic.

  • $\begingroup$ I've read that they claimed this, which is why I asked my question. So when you have shown that from satisfiability of every finite subset $\Phi\subseteq\Gamma$ of $ML$-formulas follows satisfiability of $\{ST_x(\psi)|\psi\in\Gamma\}$, how do you show that this now implies also satisfiability of $\Gamma$? Since it could be that $\{ST_x(\psi)|\psi\in\Gamma\}$ is satisfied only by structures that do not have a corresponding modal structure? $\endgroup$
    – xamid
    Jun 2, 2017 at 13:55
  • $\begingroup$ Sorry, I think I do not understand your question. If for some model $M$ we have that $M \models ST_x(\psi)[w]$ then we have $(M,w) \models \psi$. And this $M$ is the same relational structure. $\endgroup$ Jun 2, 2017 at 14:05
  • $\begingroup$ You are right, your comment is clear. But it was not proven that $M\vDash ST_x(\psi)$ implies $M\vDash\psi$, for all first-order structures $M$.. but only that for modal structures of the form $M=(W,R,V)$, we can construct a first-order structure $M'=(W,R,(P_i)_{p_i\in PROP})$, where $M'\vDash ST_x(\psi)$ it is simply abbreviated $M\vDash ST_x(\psi)$. It masks indeed the fact that no general construction from first-order structures to modal structures exists. $\endgroup$
    – xamid
    Jun 2, 2017 at 18:32
  • $\begingroup$ Question in short: How to prove that from ($FOL$)-satisfiability of $\{ST_x(\psi)|\psi\in\Gamma\}$ follows ($ML$)-satisfiability of $\Gamma$? Or how to prove the compactness theorem for $ML$ without doing this? $\endgroup$
    – xamid
    Jun 2, 2017 at 18:37
  • $\begingroup$ Alternatively: Prove that from $ML$-unsatisfiability (no $ML$-model exists), it follows $FOL$-unsatisfiability (no $FOL$-model exists). $\endgroup$
    – xamid
    Jun 2, 2017 at 18:44

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .