Proving the non-derivability of formula using the of the kripke model

I try proving the non-derivability of $(p\to q) \to \lnot p \lor q$, using the of the kripke model. I tried using different combinations of $Wi$, but I get fail.

You need a world $w_1$ where $(p\to q)\to(\neg p \lor q)$ is not satisfied. In other words $w_2$ needs to have at least one successor $w_2$ that satisfies $p\to q$ but neither $\neg p$ nor $q$.

The way for $w_2$ not to satisfy $\neg p\equiv p\to \bot$ is for it to have a successor $w_3$ that satisfies $p$ but not $\bot$. This is true if only $p$ is true in $w_3$. On the other hand, since $w_2$ must satisfy $p\to q$, we must then also have that $q$ is true in $w_3$.

This suggests a Kripke frame with three worlds $w_1<w_2<w_3$ where $w_3$ asserts both $p$ and $q$, but $w_1$ and $w_2$ assert neither.

(Actually $w_1$ is superfluous here; we can take $w_1=w_2$ instead).

• thank you for the wonderful response.
– Max
Oct 26 '14 at 16:06

I think that

$$w_o \to w_1 : p,q$$

will suffice.

Consider : $p \rightarrow q$.

We have that $V(p,w_1)=1=V(q,w_1)$; thus, it is true that :

if $V(p,w)$ then $V(q, w')$ for every $w' \ge w$,

i.e. $w_0 \Vdash p \rightarrow q$.

But $V(\lnot p, w_0)=0$, because $V(\lnot p, w)=1$ iff $V(p, w')=0$ for all $w' \ge w$, and $V(q, w_0)=0$.

Thus, $V(\lnot p \lor q, w_0)=max (V(\lnot p,w_0), V(q,w_0))=0$; thus :

$w_0 \nVdash \lnot p \lor q$.

• thanks for a great answer.
– Max
Oct 26 '14 at 16:07