[proofplan]
Prove the stronger assertion by structural induction on the formation of strictly negative formulas, allowing free variables as parameters. The base cases are $\bot$ and atomic equations. The inductive steps show that stability is preserved by conjunction, by implication into an already stable formula, and by universal quantification.
[/proofplan]
[step:Handle the base formulas]
The formula $\bot$ is stable in intuitionistic logic: from $h:\neg\neg\bot$, apply $h$ to the identity map $\bot\to\bot$ to obtain $\bot$.
If the formula is an atomic equation $s=t$, stability is exactly the standing hypothesis on $T$. Thus $T$ proves $\neg\neg(s=t)\to s=t$ for every atomic equation.
[/step]
[step:Show that conjunction preserves stability]
Suppose $N_1$ and $N_2$ are strictly negative and stable, and assume
\begin{align*}
h:\neg\neg(N_1\land N_2).
\end{align*}
To prove $N_1$, it is enough by the induction hypothesis for $N_1$ to prove $\neg\neg N_1$. If $r:N_1\to\bot$, then $r$ turns any proof of $N_1\land N_2$ into $\bot$ by projecting the first component, contradicting $h$. Hence $\neg\neg N_1$, so $N_1$. The same argument using the second projection gives $N_2$. Therefore $N_1\land N_2$ follows.
[/step]
[step:Show that implication into a stable formula preserves stability]
Let $A$ be any formula and let $N$ be strictly negative and stable. Assume
\begin{align*}
h:\neg\neg(A\to N).
\end{align*}
We prove $A\to N$. Let $a:A$ be given. By the induction hypothesis for $N$, it suffices to prove $\neg\neg N$. If $r:N\to\bot$, then any $f:A\to N$ gives $r(f(a)):\bot$, so $r$ and $a$ define a refutation of $A\to N$. This contradicts $h$. Hence $\neg\neg N$, and stability of $N$ gives $N$. Since $a$ was arbitrary, $A\to N$ holds.
[/step]
[step:Show that universal quantification preserves stability]
Let $N(x)$ be strictly negative and stable uniformly in the parameter $x$, and assume
\begin{align*}
h:\neg\neg\forall x\,N(x).
\end{align*}
To prove $\forall x\,N(x)$, fix an arbitrary element $a$. By the induction hypothesis applied to $N(a)$, it is enough to show $\neg\neg N(a)$. If $r:N(a)\to\bot$, then any proof of $\forall x\,N(x)$ gives $N(a)$ by specialization, and hence gives $\bot$ by $r$. Thus $r$ refutes $\forall x\,N(x)$, contradicting $h$. Therefore $\neg\neg N(a)$, and stability gives $N(a)$. Since $a$ was arbitrary, $\forall x\,N(x)$ follows.
[/step]
[step:Conclude by induction]
The base cases and closure steps match exactly the inductive definition of strictly negative formulas. Structural induction therefore proves that every strictly negative formula is stable over $T$. In particular, for each strictly negative $N$,
\begin{align*}
T\vdash \neg\neg N\to N.
\end{align*}
[/step]
[step:Summarize the induction]
The proof has checked the base formulas and each constructor in the grammar. Because strictly negative formulas are exactly the formulas generated by those constructors, the structural induction covers every strictly negative formula.
[guided]
The proof has checked the base formulas and each constructor in the grammar. Because strictly negative formulas are exactly the formulas generated by those constructors, the structural induction covers every strictly negative formula.
[/guided]
[/step]
