Triple negation implies double negation elimination?

Question

I have a question about intuitionistic logic regarding the relationship between the triple negation elimination rule, i.e. $\neg\neg\neg A\leftrightarrow \neg A$, and the double negation elimination. We know from Brouwer (1925) that $\neg\neg\neg A\leftrightarrow \neg A$ is true in intuitionistic logic. Let us define $B$ to be $\neg A$. Substitute $B$ and get $\neg\neg B\leftrightarrow B$. So does that mean the double negation elimination rule can still be applied in some cases in intuitionistic logic? Or am I missing something?

Answer 1

does that mean the double negation elimination rule can still be applied in some cases in intuitionistic logic?

Yes, exactly right. Specifically, the double negation elimination rule $\lnot \lnot B \to B$ can be applied whenever $B$ is a negation, that is $B = \lnot A$ for some $A$, for the reasons you describe.

In general, many specific instances of double negation elimination are provable in intuitionistic logic. Another example is where $B$ is equivalent to $\bot$: then we can show that $\lnot \lnot B \to B$. But the statement $\lnot \lnot P \to P$ for a general predicate $P$ is not provable.