# Satisfaction relation in Intuitionistic Logic

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.

• Your two questions seem to be the same one, can you clarify the distinction between the two ? Jan 3, 2020 at 11:07
• $M,w\nvDash \phi$ does not directly mean $M,w\vDash \lnot\phi$: $M,w\vDash \lnot\phi$ if and only if $M,v\nvDash \phi$ for all $v\ge w$; so $\lnot\phi$ holds at $w$ when no node after $w$ does not satisfy $\phi$. Jan 3, 2020 at 11:17

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