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

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)

Answer 2

It is standard to identify $\lnot A$ with $A \to \bot$ in intuitionistic logic. The $\lambda$-term $\lambda f^{((A\to B)\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)$

Answer 3

Triple negation $\neg \neg \neg P $ is a shorthand for $((P \rightarrow \bot) \rightarrow \bot) \rightarrow \bot$. It turns out however that for any pair of propositions $P$ and $Q$, we have that $((P \rightarrow Q) \rightarrow Q) \rightarrow Q$ simplifies to $P \rightarrow Q$, which lets us simplify triple negation to $P \rightarrow \bot$ which is just the definition of $\neg P$.

To prove this, just note that by modus ponens, we have $P \rightarrow ( (P \rightarrow Q) \rightarrow Q)$, for any P, Q. But we note that the RHS of that is equal to the LHS of $((P \rightarrow Q) \rightarrow Q) \rightarrow Q$ , so we can just compose the two implications to get $P \rightarrow Q$. This holds for any logic with modus ponens and transitive implication.