Persistency on formulas in Kripke models

Question

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.

Answer 1

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' \nVdash A \to B$.

This means :

$w' \Vdash A$ and $u \nVdash 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 \nVdash 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$.