Seeking help to understand a simple Kripke model I'm reading A Brief Introduction to the Intuitionistic
Propositional Calculus, at page 7, there is a simple Kripke model represented by a graph, I interpret it as:


*

*$W = \{w_1, w_2\}$

*$w_1 \ge w_2$

*$w_2 \models \alpha$


In this simple Kripke model, the author states that
$\lnot \lnot \alpha \Rightarrow \alpha$ (double negation elimination) fails at $w_1$, which I don't follow.
I attempted to prove by contradiction, but failed:
To show $w_1 \models \lnot \lnot \alpha \Rightarrow \alpha$, we want:
$\forall v \in W, v \ge w_1, \text{if } v \models \lnot \lnot \alpha, \text{ then } v \models \alpha$
The only instance that satisfies $\forall v \in W, v \ge w_1$ is $w_1$ itself,
but since $w_2 \le w_1$ and $w_2 \models \alpha$, we know by definition of Kripke model that $w_1 \models \alpha$. So the conclusion $
v \models \alpha$ always holds.
I don't think this conclusion is right, so I look into the precondition $v \models \lnot \lnot \alpha$, of which the only instance is $w_1 \models \lnot \lnot \alpha$. This holds if and only if $\forall v \ge u, v \not\models \lnot \alpha$.
I got stuck here because I can't find a rule to apply on $v \not\models \alpha$ from page 6.
So far I can only show the law of the excluded middle fails at $w_1$ (not sure if it is correct though) but have no idea about this double negation elimination nor Peirce's law. Since in page 4 it says that triple negation reduction is an intuitionistic tautology, I want to test if $\lnot \lnot \lnot \alpha \Rightarrow \lnot \alpha$ fails, but failed to do so due to a similar reason.
Is there something I missed or am I doing something totally wrong?
 A: I will use the verb "forces" to refer to $\models$, and I will say $v $ "extends" $w$ if $v \geq w$. 
It is not the case that $w_1 \models \alpha$. The only way for a world to satisfy a propositional variable is for the variable to be true in that world, and they have set it up so that neither $\alpha$ nor $\lnot \alpha$ is true in $w_1$. 
At the same time, we do have that $w_1 \models \lnot \lnot \alpha$. This is because there exists an extension of $w_1$ (namely, $w_2$) that does not force $\lnot \alpha$. We have that $w_2 \not \models \lnot \alpha$ because there is an extension of $w_2$ (namely, $w_2$ itself) that does force $\alpha$.  Note that, in general, a node $x$ forces $\lnot \phi$ if and only if no extension of $x$ (including $x$ itself) forces $\phi$. 
Therefore, combining the previous paragraphs, $w_1 \not \models \lnot\lnot \alpha \to \alpha$. 
One difficulty for many people the first time they run into the definition of the forcing relation $\models$ is in how it deals with negation:


*

*$w$ forces $\lnot \phi$ if and only if no extension of $w$ forces $\phi$. 

*$w$ does not force $\lnot \psi$ if and only if some extension forces $\psi$

*$w$ forces $\lnot \lnot \theta$ if and only if no extension $v$ forces $\lnot \theta$, if and only if, for every extension $v$ of $w$ there is an extension $v'$ of $v$ that forces $\theta$.  We usually abbreviate this as: $w$ forces $\lnot \lnot \theta$ if and only if the set of worlds that force $\theta$ is dense above $w$.
It is also worth knowing that the forcing relation is often written $\Vdash$ instead of $\models$. 
A: Showing that Peirce's law fails isn't too hard here (and you don't have to reference the law of the excluded middle).
Suppose that Peirce's law held in intuitionistic logic.  In Polish notation this is CCCpqpp.  Note that C Cpq C Cqr Cpr, and CpCNpq are both provable in intuionistic logic (don't believe me... prove them for yourself!), and that {CCpqCCqrCpr, CpCNpq, CCNppp} is an axiom set for classical logic under detachment and uniform substitution.  Now in CCCpqpp substitute q with "0", which I'm using here to mean "falsum".  We then have CCCp0ppp.  Since Np is defined as Cp0, we have that from any unary truth function of Cp0 we can infer any unary truth function of Np.  Thus replacing Cp0 in CCCp0pp with Np we obtain CCNppp.  So, if Peirce's law held in intuitionistic proposition logic, then intuitionistic propositional logic would end up as having the same theorems as classical propositional logic.  But, those theorems are different, and thus Peirce's law fails in intuitionstic propositional logic. 
