Prove the undecidability of a formula
One possible way to see this is to provide a model of "truth values" such that intuitionistic logical proofs translate to statements which are true in that model, but $A \to \lnot \lnot A$ is not true in this model.
One such model is to take truth values to be open subsets of $\mathbb{R}$, with $\top := \mathbb{R}$, $\bot := \emptyset$, $U \wedge V := U \cap V$, $U \vee V := U \cup V$, $\lnot U := \operatorname{int}(U^c)$, $U \rightarrow V := \operatorname{int}(U^c \cup V)$. Then it is possible to prove by structural induction on the proof that whenever $p_1, \ldots, p_n \vdash q$ in natural deduction without reductio ad absurdum ($ND - RAA$), then for any assignment $\mathfrak{U}$ of open subsets of $\mathbb{R}$ to atomic variables, we have $p_1(\mathfrak{U}) \cap \cdots \cap p_n(\mathfrak{U}) \subseteq q(\mathfrak{U})$. On the other hand, if you choose an assignment where an atomic variable $A$ gets mapped to $\mathbb{R} \setminus \{ 0 \}$, then $\lnot A \mapsto \emptyset$, $\lnot \lnot A \mapsto \mathbb{R}$, $(\lnot \lnot A \rightarrow A) \mapsto \mathbb{R} \setminus \{ 0 \}$. Since $\mathbb{R} \not\subseteq \mathbb{R} \setminus \{ 0 \}$, this implies that $\not\vdash (\lnot \lnot A \rightarrow A)$ in $ND - RAA$.
You can look up the theory of Heyting algebras for more on this interpretation of intuitionstic logic. Another example of a Heyting algebra which is not a Boolean algebra is the lattice $\{ 0, \frac{1}{2}, 1 \}$ with an appropriate choice of $\rightarrow$ operation; this example has the advantage that it doesn't depend heavily on set-theoretic or topological constructions as the other one, but I personally find it less intuitive to work with. Other examples that are easy to prove using this formulation: $\not\vdash (A \vee \lnot A)$, and $\not\vdash (\lnot(A \wedge B) \rightarrow \lnot A \vee \lnot B)$.
Another completely different approach is through the theory of sequent calculus. Essentially, the idea here is that any proof in $ND - RAA$ can be "simplified" to a "normal form" in which there isn't any redundancy or "cleverness" left in the proof. Here "cleverness" mostly refers to the use of the cut rule: \begin{align*} \Gamma & \vdash P \\ P, \Gamma & \vdash Q \\ \hline \Gamma & \vdash Q \end{align*} where $P$ is a cleverly chosen intermediate step that clarifies the proof. So, in the end, you get a proof with severely restricted possibilities, and from these restrictions you can conclude that certain things can't be proved at all.
Moreover, there are variants of the sequent calculus which lend themselves to a totally automated proof search, which give the result that there is a mechanical decision procedure which decides for each formulas $p_1, \ldots, p_n, q$ whether or not $p_1, \ldots, p_n \vdash q$ in $ND - RAA$.
Another interesting application is that it makes it easy to prove: if $p \vee q$ is a tautology in $ND - RAA$, then either $p$ or $q$ is a tautology in $ND - RAA$. Which is a surprising result at first, given that $A \vee \lnot A$ is a tautology in $ND + RAA$ whereas obviously neither $A$ nor $\lnot A$ is a tautology in $ND + RAA$.
In intuitionistic and classical logic there is a standard way to show that a formula $A$ is unprovable or undecidable (i.e. both $A$ and $\lnot A$ are unprovable), it is based on the completeness theorem.
Completeness theorem says that a formula $A$ is provable (in intuitionistic natural deduction or equivalent system) if and only if $A$ is valid in all the structures (in intutionistic logic these structures are intuitionistic Kripke models).
So:
- To prove that $A$ is unprovable in intuitionistic logic, it is sufficient to show that $A$ is not valid in some Kripke model (this entails that $A$ is not provable in intutionistic natural deduction by the completeness theorem).
- To prove that $A$ is undecidable in intuitionistic logic, it is sufficient to apply point 1. to both $A$ and $\lnot A$; i.e. to show that $A$ is not valid in some Kripke model (this entails that $A$ is not provable in intutionistic natural deduction by the completeness theorem), and $\lnot A$ is not valid in some Kripke model (this entails that $\lnot A$ is not provable in intutionistic natural deduction by the completeness theorem).
As correctly remarked by Henning Makholm in his comment, if a formula $B$ is provable in classical logic, then $\lnot B$ is unprovable in intuitionistic logic (since all intuitionistically provable formulas are classically provable). Therefore, a classically provable formula $B$ is intuitionistically undecidable (take for instance $A \lor \lnot A$, or $\lnot\lnot A \to A$) if and only if $B$ is intuitionistically unprovable.
Let us show that $A \lor \lnot A$ and $\lnot \lnot A \to A$ are unprovable (and then undecidable, since they are classically provable) in intuitionistic logic using the completeness theorem. Assume $A$ is a propositional variable. Consider the following Kripke model for propositional logic: $\mathcal{K} = (\{0,1\},\leq, \Vdash)$ where $\leq$ is the (total) order relation over $\{0,1\}$ defined by \begin{align} 0 \leq 0 && 0 \leq 1 && 1 \leq 1, \end{align} and $\Vdash$ is a binary relation from $\{0,1\}$ to the set of propositional variables such that $0 \not\Vdash A$ and $1 \Vdash A$. According to the definition of intuitionistic Kripke model for propositional logic, it is easy to check that $0 \not\Vdash A \lor \lnot A$ and $0 \not \Vdash \lnot\lnot A \to A$, which means that neither $A \lor \lnot A$ nor $\lnot\lnot A \to A$ are valid in $\mathcal{K}$. Thus, both $A \lor \lnot A$ and $\lnot \lnot A \to A$ are unprovable (and hence undecidable) in intuitionistic logic.
There is also a completeness theorem for classical logic: in the formulation given above, replace intutionistic natural deduction with classical natural deduction (or equivalent system), and Kripke models with truth tables (in the propositional case). Therefore, also in classical logic the completeness theorem (for classical logic) can be used to show that a formula is unprovable or undecidable.