There is a tree-like Kripke model in which the set of worlds $\mathfrak{W}$ is ordered as a tree:

(a) there is a smallest world $W_0$

(b) for any $W_i \ne W_0$ there is a unique preceding world $W_k: W_k \prec W_i$.

I don't know how to find a statement that can't be refuted by a Kripke tree model of height less than 2.

And also, how can I show that for any natural number n: there exists a statement that is refutable in Kripke's models and isn't refutable by any model with n worlds?

I got carried away with this tough problem. I didn't find anything related to it on the Internt, so I didn't manage to get to the answer. Can anyone help me to solve it?


2 Answers 2


Consider the formula $\phi=(q\to(p\lor \neg p))\lor( \neg q\to (p\lor \neg p))$ and suppose $K$ is a tree with root $r$ such that $r\nVdash \phi$, then:

(1) there is $w_0\geq r$ s.t. $w_0\Vdash q$ and $w_0\nVdash p\lor \neg p$. Thus there are $v_1,v_2\geq w_0$ s.t. $v_1\nVdash p$, $v_2\Vdash p$.

(2) there is $w_1\geq r$ s.t. $w_1\Vdash \neg q$ and $w_1\nVdash p\lor \neg p$. Thus there are $v_3,v_4\geq w_1$ s.t. $v_3\nVdash p$, $v_4\Vdash p$.

Now, if $v_2=w_0$, then by persistency $v_1\Vdash p$, contradiction. If $w_0=r$, then $w_1\Vdash q$, contradiction. Therefore, $r<w_0<v_2$, showing the height of $K$ is at least 2.

(For the general claim, it could be helpful to have a look at the Rieger-Nishimura lattice. )

  • 1
    $\begingroup$ What's the role of $v_1$ here? My argument from $w_0 \not\Vdash p \lor \lnot p$ would be: therefore, $w_0 \not\Vdash p$ and $w_0 \not\Vdash \lnot p$, and from the latter, it further follows that there exists $v_2 \ge w_0$ such that $v_2 \Vdash p$ (assuming "the base universe is classical", or at least that $K$ is finite and the Kripke model has decidable forcing relation on atoms). $\endgroup$ May 25, 2022 at 18:32
  • $\begingroup$ Yes, you are right that $v_1=w_0$ and $v_3=w_1$. $\endgroup$
    – D.Q.
    May 25, 2022 at 18:42
  • 1
    $\begingroup$ Hmm, following the Rieger-Nishimura lattice idea... I think probably the entry $\lnot\lnot p \lor (\lnot\lnot p \rightarrow p)$ is another example that requires height at least 2. Since if $r$ does not force that, then $r \not\Vdash \lnot\lnot p$; but also there exists $w_0 \ge p$ with $w_0 \Vdash \lnot\lnot p$ and $w_0 \not\Vdash p$. From the first, in particular $w_0 \not\Vdash \lnot p$, so there exists $w_1 \ge w_0$ with $w_1 \Vdash p$. And similar arguments show $r \ne w_0$ and $w_0 \ne w_1$. $\endgroup$ May 25, 2022 at 18:55
  • 1
    $\begingroup$ More generally, if we label the nodes above a certain point $x_n$ and $y_n$ where $x_n$ are the "cross" $\lor$ entries and $y_n$ are the "side" $\rightarrow$ entries, it looks like a similar argument should show that if $x_n$ requires at least depth $m$ to refute, then $x_{n+3}$ requires at least depth $m+1$ to refute. $\endgroup$ May 25, 2022 at 19:12

We consider the Rieger-Nishimura lattice. In order to refer to elements, starting at some level other than the bottom, we will let $x_n$ be the element at the $n$th level at the "cross", and $y_n$ the element at the $n$ level at the "side". In other words, a piece of the lattice would look like:

    x       y
     n+3     n+3
  /    \  /
 y       x
  n+2     n+2
   \  /    \
    x      y
     n+1    n+1
  /   \  /
 y     x
  n     n

In this lattice, note that $x_{n+3} = y_{n+1} \vee y_{n+2} = y_{n+1} \vee (y_{n+1} \rightarrow x_n).$ Now, each element also induces a formula in the atom $p$ preserving the Heyting algebra structure which (past some point) is recursively defined by $x_{n+2}(p) := y_n(p) \lor y_{n+1}(p)$ and $y_{n+2}(p) := y_{n+1}(p) \rightarrow x_n(p)$.

We now claim that if $x_n(p)$ requires a Kripke model of depth at least $m$ to refute, then $x_{n+3}(p) = y_{n+1}(p) \lor (y_{n+1}(p) \rightarrow x_n(p))$ requires a Kripke model of depth at least $m+1$ to refute. To see this, suppose $r$ is the root of a Kripke model refutation of $x_{n+3}(p)$. Then $r \not\Vdash y_{n+1}(p)$ and also $r \not\Vdash y_{n+1}(p) \rightarrow x_n(p)$. From the latter, we see that there exists $w_1 \ge r$ such that $w_1 \Vdash y_{n+1}(p)$ but $w_1 \not\Vdash x_n(p)$. From the hypothesis, the subtree rooted at $w_1$ must have depth at least $m$; and clearly $w_1 \ne r$, implying that the overall tree must have a depth of at least $m+1$.

However, for $n$ sufficiently large, $x_n(p)$ is classically valid, but since the Rieger-Nishimura lattice is a Heyting algebra with $x_n \ne \top$, $x_n(p)$ is not intuitionistically valid; and by the previous paragraph, we see that there is no upper bound on the depth required to refute the formulas $x_n(p)$.

Note that for the specific case of a formula requiring a tree of depth 2 to refute, an argument similar to the one above shows that the entry $\lnot\lnot p \lor (\lnot\lnot p \rightarrow p)$ suffices.

  • $\begingroup$ Or, I suppose if you allowed using an arbitrary number of atoms, then $v_1 \lor (v_1 \rightarrow (v_2 \lor (v_2 \rightarrow \cdots (v_n \lor \lnot v_n) \cdots )))$ would work similarly. It is interesting, though, to have the result that only one atom is really needed. $\endgroup$ May 25, 2022 at 21:35

You must log in to answer this question.

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