Intuitionistic logic, tree-like Kripke model

Question

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?

Answer 1

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

Answer 2

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.