# Intuitionistic logic, tree-like Kripke model

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?

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, 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. )

• 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). May 25, 2022 at 18:32
• Yes, you are right that $v_1=w_0$ and $v_3=w_1$.
– D.Q.
May 25, 2022 at 18:42
• 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$. May 25, 2022 at 18:55
• 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. 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.

• 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. May 25, 2022 at 21:35