# Triple negation in intuitionistic logic?

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?

## No, $\neg \neg \neg A$ is equivalent to $\neg A$.

Given $\neg\neg\neg A$:

1. $\neg \neg \neg A$ (premise)

2.1. $A$ (assumption)

2.2.1. $\neg A$ (assumption)

2.2.2. $A$ (reiterate 2)

2.2.3. $\bot$ (contradiction 4 3)

2.3. $\neg\neg A$ ($\neg$intro 2.2.1-2.2.3)

2.4. $\neg\neg\neg A$ (reiterate 1)

2.5. $\bot$ (contradiction 2.3 2.4)

3. $\neg A$ ($\neg$intro 2.1-2.5)

Given $\neg A$:

1. $\neg A$ (premise)

2.1. $\neg \neg A$ (assumption)

2.2. $\neg A$ (reiterate 1)

2.3. $\bot$ (contradiction 2.2 2.1)

3. $\neg\neg\neg A$ ($\neg$intro 2.1-2.3)

It is standard to identify $\lnot A$ with $A \to \bot$ in intuitionistic logic. The $\lambda$-term $\lambda f^{(A\to B)\to B}{\cdot} \lambda a^{A}{\cdot} f(\lambda g^{A \to B}{\cdot} g(a))$ corresponds to a proof of $(((A \to B) \to B) \to B) \to (A \to B)$ under the Curry-Howard Correspondence. Instantiating $B$ to $\bot$ gives you a proof that $\lnot\lnot\lnot A \to \lnot A$.

The proof of the converse proposition $(A \to B) \to (((A \to B) \to B) \to B)$ is witnessed by $\lambda f^{A\to B}{\cdot}\lambda g^{(A \to B) \to B}{\cdot}g(f)$

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.