Persistency on formulas in Kripke models Let $ (W,R,f) $ a Kripke model. I have some trouble proving that the persistency property holds for formulas i.e if $ wRw' $ and $ w \Vdash \phi $ then $ w' \Vdash \phi $ , mainly due to the forcing rule for the implication connective ( $ w\Vdash A\to B $ iff for all $ u\ge w, u\Vdash A $ implies $ u\Vdash B $ ) Any help/hint woud be appreciated.

If we are working in _intuitionistic logic_ , I think we have to assume that the _persistency_ condition must holds for propositional variables :

> if $p$ is a propositional variable, $w \le u$, and $w \Vdash p$, then $u \Vdash p$ see [Kripke semantics : **Semantics of intuitionistic logic** ].

If so, we have to prove it by induction; thus the property for the _conditional_ $A \to B$ must be proved assumed that the property holds for $A$ and $B$.

Now we have to prove it by contradiction; assume that for some $w'$ such that $wRw'$ we have : $w' \
Vdash A \to B$.

This means :

> $w' \Vdash A$ and $u \
Vdash B$, for some $u \ge w'$.

Thus, we have $w' \ge w$ such that $w' \Vdash A$, and so : $u \Vdash A$ for $u \ge w' \ge w$.

But $u \
Vdash B$, contradicting the fact that, if $w \Vdash A \to B$, then :

> for all $u \ge w$, if $u \Vdash A$, then $u \Vdash B$.