Satisfaction relation in Intuitionistic Logic

Question

I would like to clarify what concerns me in satisfaction relation in Kripke frames for intuitionistic logic (INT). Firstly, is it a true statement that given a Kripke Model $$M = \langle W, R, \models \rangle$$ for INT Logic, the fact that $$M, w \not\models \phi$$ is logically equivalent to the fact that $$M, w \models \neg \phi$$ ? And secondly, is it like in INT Logic that we consider a world $$w \in W$$ in which neither $$M, w \models \phi$$ nor $$M, w \models \neg \phi$$? I mean the case in which we do not "know" anything about satisfaction of some formula in a possible world. The distinction between the two is following. In the first part I am asking about satisfaction relation property (or lack of this property). In the second part I am ciurious about something related but not exactly the same. Whether it's possible that in a specific Kripke Model neither a formula $\phi$ nor a formula $\neg \phi$ is valuated as logical truth.

Answer 1

Is $w \not \vDash \phi$ logically equivalent to $w \vDash \neg \phi$?

No. $\vDash \neg$ implies $\not \vDash$, but not vice versa.
$w \nvDash \phi$ means that it is not the case that $w \vDash \phi$.
$w \vDash \neg \phi$ means that for all subsequent worlds $w' \geq w$, $w' \not \vDash \phi$. This is a stronger statement.

Can there exist $M, w$ such that $w \not \vDash \phi$ and $w \not \vDash \neg \phi$?

Yes. In fact, this is what leads to the invalidity of the law of the excluded middle ($\phi \lor \neg \phi$) in intuitionistic logic.

Consider the following counter model:

$M = \langle W, \leq, \vDash \rangle$ with
$W = \{w_0, w_1\}$
$\leq = \{\langle w_0, w_0 \rangle, \langle w_0, w_1 \rangle, \langle w_1, w_1 \rangle\}$
$\vDash$ such that $w_0 \nvDash p$ and $w_1 \vDash p$

In this model, $w_0 \not \vDash p$: $p$ does not hold at state $w_0$, so we can not claim it to be true.
However, with $w' = w_1$, there exists a future state $w' \geq w_0$ such that $w' \vDash p$, hence we can not claim either that $p$ is false (since that would require that $p$ is false in all subsequent states), and we have $w_0 \not \vDash \neg p$.
Since neither $w_0 \vDash \phi$ nor $w_0 \vDash \neg \phi$, we also have that $w_0 \not \vDash p \lor \neg p$.
Hence $M$ is a counter model of the intuitionistically invalid statement $p \lor \neg p$: It is possible that neither $p$ nor the negation of $p$ holds at a world (and thus, in a model).