# Understanding a compactness proof for modal logics which uses a standard translation

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.

• 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. Jun 8, 2017 at 9:17

• 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? Jun 2, 2017 at 13:55
• 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. Jun 2, 2017 at 14:05
• 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. Jun 2, 2017 at 18:32
• 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? Jun 2, 2017 at 18:37
• Alternatively: Prove that from $ML$-unsatisfiability (no $ML$-model exists), it follows $FOL$-unsatisfiability (no $FOL$-model exists). Jun 2, 2017 at 18:44