 For (iii), consider, for example, a Kripke model based on a frame in which we have an infinite number of stages \(s_0 \preceq s_1 \preceq \ldots \preceq s_n \preceq \ldots\). We may assume that \(D_{s_{n}} = \{ d_0 , \ldots, d_n \}\) and that a monadic predicate \(P\) is true at \(s_n\) of every \(d_m\) in the domain except for \(d_n\). It turns out that \(\forall x \lnot \lnot Px\) is true at \(s_0\) even though \(\lnot \lnot \forall x Px\) is not true at \(s_0\). Therefore, \(\forall x \lnot \lnot A \rightarrow \lnot \lnot \forall x A\) is not intuitionistically valid either. These and similar examples are discussed in Burgess 2009.