Is Kripke/relational/possible world semantics the special case of the the set semantics or first order logic?

142 Views Asked by At

I am reading https://www.springer.com/gp/book/9783319225562 about expression of modal operators as the predicates in the first order (and possibly higher order) logic. My question is - is the modal logic the special case of first order logic (just some more axioms?) Is the Kripke/relational/possible world semantics the special case of the set semantics for the first order logic?

I have some doubts about this, because modal operator takse the formula/sentence as its arguments, but there is no structure (function or predicate) in the FOL, that could take formula/sentence as the argument, only connectives can act upon predicates/formulas but FOL connectives can not act as unary functions (like modal operators do).

Would be happy for clarification.

1

There are 1 best solutions below

0
On BEST ANSWER

Short version:

Yes, it is.


Incidentally, this old MSE answer of mine is related; it's not an exact duplicate, since there the OP is building off of this initial observation, but it covers some of the same ground. Also, this old mathoverflow answer of mine while not directly related may be of separate interest.

Also, at some point I suspect you'll become unsatisfied with the level of detail available in introductory texts on the subject. For a more advanced text I strongly recommend Chagrov/Zakharyaschev's awesome book - it's what I learned from.


Kripke frames in the propositional modal logic context are indeed a special case of first-order logic in a natural way. This is a bit involved:

We start with the languages. Each propositional language $P=\{p_i:i\in I\}$ has a corresponding first-order language consisting of unary predicates, one for each propositional atom, together with a new binary relation $R$ - namely, $$\Sigma_P=\{R\}\cup\{U_i:i\in I\}.$$

Next, we pass from Kripke frames to first-order structures. Each frame/valuation pair $\mathcal{K}=((K,\rightarrow),\nu)$ for $P$ (that is, $(K,\rightarrow)$ is a directed graph and $\nu$ is a map from $K\times P$ to $\{\top,\perp\}$) has a corresponding $\Sigma_P$-structure $Struc_\mathcal{K}$ whose elements are worlds, whose unary predicates correspond to the sets of worlds where given propositional atoms hold, and whose binary relation corresponds to the accessibility relation. More precisely:

  • The domain of $Struc_\mathcal{K}$ is $K$.

  • The interpretation of $U_i$ in $Struc_\mathcal{K}$ is $\{w\in K: \nu(w, p_i)=\top\}$.

  • The interpretation of $R$ in $Struc_\mathcal{K}$ is $\{(w,x)\in K^2: w\rightarrow x\}$.

Note that every $\Sigma_P$-structure is of the form $Struc_\mathcal{K}$ for some $\mathcal{K}$.

Now we come to the payoff. We have a translation $$\varphi\mapsto\hat{\varphi}$$ from propositional modal sentences in $P$ to first-order formulas with one free variable in $\Sigma_P$ such that for each frame/valuation pair $\mathcal{K}=((K,\rightarrow), \nu)$ and world $w\in K$ we have $$w\models_\mathcal{K}\varphi\quad\iff\quad Struc_\mathcal{K}\models\hat{\varphi}(w).$$

This translation is a bit tedious to write down in full detail, but here's an example which should illustrate how it works: in the language $P=\{p_1,p_2,p_3\}$, taking our modal sentence to be $$\varphi:\quad p_1\vee(\Box (p_2\wedge\neg p_3)\wedge\Diamond p_1)$$ we would have $$\hat{\varphi}(x):\quad [U_1(x)]\vee[\forall y(xRy\implies U_2(y)\wedge \neg U_3(y))\wedge\exists y(xRy\wedge U_1(y))].$$ (I've added some unnecessary parentheses, and used both square and round brackets, for clarity.) Note that at each "stage" in our translation we have a "current world," and the accessibility relation $R$ comes in when we interpret the modalities as quantifiers: if we're "currently at $x$" then "$\Box \psi$" and "$\Diamond\psi$" correspond to "$\forall y(xRy\implies \hat{\psi})$" and "$\exists y(xRy\wedge \hat{\psi})$" respectively.

  • It's worth noting that the above yields a purely syntactic fact: since $K$ is sound and complete for Kripke frames, the above tells us that for all propositional modal $\gamma,\varphi$ we have $$\gamma\vdash_K\varphi\quad\iff\quad \hat{\gamma}\vdash\hat{\varphi}$$ where "$\vdash_K$" is provability in system $K$ and "$\vdash$" is the usual notion of provability in first-order logic. Many properties of frames are appropriately first-order expressible and yield further equivalences: e.g. $$\gamma\vdash_{S_5}\varphi\quad\iff\quad \hat{\gamma}\wedge \theta\vdash\hat{\varphi}$$ where "$\theta$" is the sentence asserting that $R$ is reflexive, transitive, and symmetric.

So in a precise sense we have a correspondence between Kripke semantics and a fragment of first-order logic.

That said, this does not mean that classical first-order logic is "better" than propositional modal logic: there is an important tradeoff between power and tameness, and sometimes - especially in applications, e.g. in computer science - we care a lot about how tame we can make things while still having a bare minimum of expressive power. The study of tame fragments of first-order logic is extremely deep and interesting.


Now let me mention some subtleties of the analysis above.

One immediate question is how large a fragment of first-order logic is given by Kripke semantics via the above translation. Certainly there's a restriction on the language - we only ever get structures in a single binary relation and a bunch of unary relations. However, it turns out that the situation is even worse: there are first-order formulas in such a language which don't come from Kripke frames at all. For example, consider the very boring propositional language $\{p_1\}$. The formula $$\varphi(x):\quad\exists y(x\not=y\wedge U_1(y))$$ is true of an element $w$ in $Struc_\mathcal{K}$ iff in $\mathcal{K}$ there is some world other than $w$ where $p_1$ is true. But this is not modally expressible - intuitively, starting at a world $w$ we can only every survey worlds a bounded distance from $w$. So Kripke semantics gives us a proper sub-fragment of first-order logic even after we make the obvious language restriction. Indeed, there are lots of "tameness" results about modal logic which show that the gap between "modal-induced" $\Sigma_P$-formulas and arbitrary first-order $\Sigma_P$-formulas is extremely vast.

On the other hand, when we broaden our horizons a bit there are some things modal logic can do which first-order logic can't. Consider for example Lob's axiom $$\Box(\Box p\rightarrow p)\rightarrow \Box p.$$ This is validated in a frame $(K,\rightarrow)$ - that is, true at every world under every valuation - iff $(K,\rightarrow)$ is converse well-founded. But this is not a first-order expressible property. Indeed, the complexity of validity in this sense is quite high.

Finally, we might ask about non-Kripkean semantics. Here my lack of experience shows, but to the best of my knowledge nothing really changes: all natural propositional modal logics (as far as I know) are appropriately embeddable in first-order logic.