0
$\begingroup$

I read that the formula $\neg \neg A \supset A$ is not intuitionistically valid. Why is that? If someone can explain me I would be glad.

$\endgroup$
1
$\begingroup$

Remember that : $\lnot \lnot A \supset A$ is : $((A \supset \bot) \supset \bot) \supset A$.

According to the BHK-interpretation, a proof of $A \supset \bot$ is a procedure $\gamma_0$ that transform a proof of $A$ into a proof of $\bot$.

A proof of $(A \supset \bot) \supset \bot$ is a procedure $\gamma_1$ that, when "applied" to $\gamma_0$, extract a proof of $\bot$.

Thus, a proof of $((A \supset \bot) \supset \bot)$ must be a procedure $\gamma_2$ that, when "applied" to $\gamma_1$, extract a proof of $A$.

But then, having extracted it, we can use it with $\gamma_0$ to get a proof of $\bot$, and this is impossible : the calculus must be sound, i.e. $\bot$ (the absurdity) has no proof.

$\endgroup$

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.