Provide a Kripke model to prove that $\neg(\neg P\lor \neg Q\lor R)\to (P\land Q \land R)$ is false in intuitionistic logic Could anyone check my working please?

Provide a Kripke model to prove that $\neg(\neg P\lor \neg Q\lor \neg R)\to (P\land Q \land R)$ is false in intuitionistic logic.

Here $k_0$ forces $\neg(\neg P\lor \neg Q\lor \neg R)$: this is equivalent to $\lnot\lnot P\land\lnot Q\land\lnot\lnot R$ by deMoran's law. For $k_0$ to prove $\lnot\lnot P$ either $k_0$ or a higher node must force $P$ - which $k_1$ fufilled. The same goes for $Q$ and $R$.
$k_0$ does not force $P,Q,R$. Therefore the antecedent is forced at $k_0$, but not the consequent - thus this model falsifies this sentence.

 A: The given Kripke model is a valid counterexample to the statement.
However, the analysis is not quite correct.  In particular, you say: "For $k_0$ to prove $\lnot \lnot P$ either $k_0$ or a higher node must force $P$ - which $k_1$ fufilled."  In fact, the correct statement is: $p \Vdash \lnot \lnot P$ if and only if for all $q \ge p$, it is not the case that for all $r \ge q$, $r \not\Vdash P$.  (And if you believe that the underlying universe for the Kripke model satisfies classical logic, or if you're working with a finite Kripke model, then this is equivalent to: $\forall q \ge p, \exists r \ge q, r \Vdash P$.)  Now, in the given model, it is indeed true that $k_0 \Vdash \lnot \lnot P$ -- in either the case $q = k_0$ or the case $q = k_1$, we can use $r = k_1$.
In this case, you could also work directly with the formula as given, instead of going via de Morgan's law.  i.e. by definitions, $k_0 \not\Vdash \lnot P$ since $k_1 \ge k_0$ and $k_1 \Vdash P$; similarly, $k_1 \not\Vdash \lnot P$; and so on for $Q$ and $R$.  Therefore, $k_0 \not\Vdash \lnot P \vee \lnot Q \vee \lnot R$, and similarly $k_1 \not\Vdash \lnot P \vee \lnot Q \vee \lnot R$; so again by definitions, $k_0 \Vdash \lnot(\lnot P \vee \lnot Q \vee \lnot R)$.

To see the difference between the incorrect statement and the correct statement about $p \Vdash \lnot \lnot P$, consider the standard counterexample model to $P \vee \lnot P$ where $k_0 \le k_1, k_0 \le k_2$ with $k_1, k_2$ incomparable, and only $k_1 \Vdash P$.  Then in this model $k_0 \not\Vdash \lnot \lnot P$, despite the fact that $k_1 \ge k_0$ and $k_1 \Vdash P$.  On the other hand, $k_2 \ge k_0$, and there is nothing $\ge k_2$ which forces $P$.
