[Math] Triple negation in intuitionistic logic

Question

I'm told that intuitionistic logic is basically classical logic with "law of the excluded middle removed", and that you can't from $\neg \neg A$ infer $A$.

So, if we consider $A$ a state, $\neg A$ a state, and $\neg \neg A$ a state, does this mean that $\neg \neg \neg A$ is a separable state?

Answer 1

In addition to the two very nice formal answers, let me give an informal proof that $\neg\neg\neg A \Rightarrow \neg A$. Recall that, by definition, $\neg B$ is an abbreviation for $B \Rightarrow \bot$.

Assume $\neg\neg\neg A$. We are to show $\neg A$, that is, $A \Rightarrow \bot$.

So assume $A$, we are to show $\bot$.

Since $A$, we have $\neg\neg A$. But we also have $\neg(\neg\neg A)$. Hence $\bot$.

This proof uses the lemma that $A \Rightarrow \neg\neg A$. This lemma can also be proven informally:

Assume $A$. We are to show $\neg\neg A$, that is, $(\neg A) \Rightarrow \bot$.

So assume $\neg A$. We are to show $\bot$.

Since $\neg A$ (which means $A \Rightarrow \bot$) and since $A$, we have $\bot$.

By the way, at no point did we use the principle of explosion (ex falso quodlibet). Hence our proofs are even valid in minimal logic, where $\bot$ doesn't have any special rules attached to it.