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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.