8
$\begingroup$

Consider the propositional modal language in one propositional letter, $p$.

Recall that a pointed Kripke frame is a Kripke frame $(W,R)$ with a designated world $w_0\in W$, and a sentence is valid in a pointed Kripke frame iff it is true at $w_0$ for every interpretation of the propositional letters as subsets of $W$.

I'm wondering if it's possible to find a finite model in which $\Box$ means "valid". More precisely, is it possible to find a finite transitive reflexive pointed Kripke model $(W,R,w_0, [[\cdot]])$ such that

$w_0 \Vdash \Box A$ if and only if $A$ is valid in $(W,R,w_0)$?

Certainly it can be done in an infinite frame. For instance, over the infinite tree that has omega many daughters at any node, you can make each sentence satisfiable in the frame true at one of the daughters of the base node. And this even works with infinitely many propositional letters.

(For context: I got thinking about this question after coming back to this earlier question about logical interpretations of $\Box$.)

$\endgroup$
3
  • $\begingroup$ What does $w \Vdash B$ stand for? I am reading your question as "Can we have a finite Kripke model $(W, R, w_0)$ such that, for all $A$, $w_0 \Vdash \Box A$ iff $w_0 \Vdash A$?" but I don't think that's what you are asking. (If it is, consider the trival model.) $\endgroup$ Commented Jul 31, 2020 at 7:57
  • $\begingroup$ @AndrejBauer Sorry there was a typo in an earlier version of the question (I wrote "frame" instead of "model"). Does it make sense now: $w\Vdash B$ just means $B$ is true at $w$ in the pointed Kripke model $(W,R,w_0,[[.]])$ ? $\endgroup$ Commented Jul 31, 2020 at 8:16
  • $\begingroup$ This is impossible since a reflexive frame has the infinite sequence of related points $wRwRwR….$ for each point $w$. Provability Logic (modal logic GL) corresponds to finite, transitive, irreflexive frames. GL interprets $\Box$ as an encoding of a proof in a language that can formulate its own provability predicate. GL is characterized by $\Box (\Box P \to P) \to \Box P$, which takes reflexivity off the table immediately. $\endgroup$
    – PW_246
    Commented Jun 10, 2023 at 14:31

1 Answer 1

10
$\begingroup$

$\def\R{\mathrel R}$No, this is not possible.

Recall that the depth of a point $x$ in a transitive frame $(W,R)$ is the maximal length $d$ of a strictly increasing chain starting at $x$, i.e., $x_1,\dots,x_d$ such that $x_d=x$ and $x_{i+1}\R x_i$, $x_i\not\R x_{i+1}$.

There are formulas in one variable that are satisfiable only in frames of depth $\ge d$ (cf. Thm. 12.21 in Chagrov&Zakharyaschev, Modal logic). Moreover, it is possible to define them in such a way that when satisfied in a model of depth exactly $d$, they force a particular value for $p$ in all points in the root cluster; we will obtain a contradiction from this. An explicit construction of such formulas follows below.

Consider the formulas $$\begin{align} \theta_1(p)&=\Box p,\\ \theta_{i+1}(p)&=p^{i+1}\land\Diamond\theta_i(p)\land\Box\Bigl(p^{i+1}\lor\bigvee_{j\le i}\theta_j(p)\Bigr), \end{align}$$ where $$p^i=\begin{cases}\phantom{\neg}p&\text{if $i$ is odd,}\\\neg p&\text{otherwise.}\end{cases}$$ We will use the property that these formulas are pairwise contradictory; moreover, the following formulas are valid: $$\theta_j\to\Box\neg\theta_i,\qquad j<i.\tag{$*$}$$ We can prove this by induction on $i$. For $i=1$, there is nothing to prove. Assuming it holds for $i$, we show it for $i+1$ as follows. Let $j\le i$, and assume for contradiction that $x\R y$ are such that $x\models\theta_j$ and $y\models\theta_{i+1}$. If $j<i$, $y\models\Diamond\theta_i$ contradicts the induction hypothesis. If $j=i$, we have $y\models\neg p^i$. This directly contradicts the definiton of $\theta_1$ for $i=1$; otherwise, the definition of $\theta_i$ gives $y\models\bigvee_{j<i}\theta_j$, which together with $y\models\Diamond\theta_i$ contradicts the induction hypothesis again. This finishes the proof of $(*)$.

Now, assume for contradiction that $(W,R,w_0,V)$ is as in the question, and let $d$ be the depth of $w_0$. The formula $\theta_d(p)$ is satisfiable in $(W,R,w_0)$ by the valuation that makes $p$ true in points of odd depth, and false in points of even depth. That is, $\neg\theta_d(p)$ is not valid in the pointed frame $(W,R,w_0)$, thus by assumption, $w_0\not\models\Box\neg\theta_d(p)$, i.e., there is $x_d$ such that $$w_0\R x_d\models\theta_d(p).$$ Unwinding the definition, we find a chain $x_d\R x_{d-1}\R\dots\R x_1$ such that $x_i\models\theta_i(p)$. This implies $x_i\not\R x_{i+1}$, as $\theta_i\to\Box\neg\theta_{i+1}$ is valid by $(*)$. Thus, the chain $x_d,\dots,x_1$ is strictly increasing. Since $w_0$ does not have depth $\ge d+1$, we must have $x_d\R w_0$. This implies $w_0\models p^d\lor\bigvee_{j\le d-1}\theta_j(p)$. Using $(*)$, we cannot have $w_0\models\bigvee_{j\le d-1}\theta_j(p)$ as $w_0\R x_d\models\theta_d(p)$, thus we obtain $$w_0\models p^d.$$

However, since $\neg\theta_d(p)$ is not valid in the frame, $\neg\theta_d(\neg p)$ is not valid there either. Then the same argument as above with $p$ and $\neg p$ swapped gives $$w_0\models\neg p^d.$$ This is a contradiction.

I formulated the argument above for reflexive transitive frames as requested, but it can be easily adapted to arbitrary finite pointed Kripke frames $(W,R,w_0)$: we take for $d$ the depth of $w_0$ under the transitive closure of $R$, and replace all instances of $\Box$ inside the $\theta_i$ formulas by the defined modality $$\Box^{\le n}\phi=\bigwedge_{i=0}^n\underbrace{\Box\dots\Box}_i\phi,$$ where $n=|W|$. Note that $\Box^{\le n}$ is the box modality corresponding to the transitive reflexive closure of $R$.

$\endgroup$
2
  • 1
    $\begingroup$ By the way, the situation for intuitionistic logic is quite different. For example, the intuitionistic version of the required property holds for the unique 5-element rooted submodel of the Rieger–Nishimura ladder, more or less because its underlying frame does not map p-morphically onto the unique 4-element rooted subframe of the RN ladder. $\endgroup$ Commented Jul 31, 2020 at 16:44
  • $\begingroup$ Thank you! Yes, I was able to find the model of the intuitionistic version, which is partly what inspired the question. $\endgroup$ Commented Jul 31, 2020 at 18:31

You must log in to answer this question.

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