= Stability of a formula under double negation
{title2=$\neg\neg A\to A$}
A <first-order formula> $A$ is stable when <intuitionistic first-order logic> proves $\neg\neg A\to A$. Double negations and <logical falsity> are stable. <Logical conjunction> of stable <first-order formulas> is stable; a <logical implication> is stable when its consequent is stable; and <universal quantification> preserves stability. For <logical implication>, from $\neg\neg(A\to B)$ and $A$, assuming $\neg B$ contradicts the first hypothesis, giving $\neg\neg B$ and then $B$. For universality, obtain $\neg\neg A(t)$ from $\neg\neg\forall x\,A(x)$ for arbitrary $t$, then use stability and generalize.
Back to article page
