I have been reading about constructive logic and I also recently became aware of minimal logic. My understanding of minimal logic is not clear, and I don't get how it is defined, or what suffices as a proof in minimal logic. According to the wiki page for minimal logic, it is constructive logic that further does not accept the principle of explosion. I don't understand how you can "not accept" the principle of explosion, if the the principle can be proven using the using the axioms and definitions of constructive logic. The way the wiki page describes it seems to basically say "minimal logic is the logic where we ignore the fact that this principle was proven".
To help outline my confusion, I attempt to present a proof of the same implication with and without explosion. The first proof is essentially my own wording of the proof given on page 3 in this writing about constructive logic.
A proof $p$ of $A \rightarrow \neg \neg A$ is a way to take any proof $a$ of $A$ and turn it into a proof of $\neg \neg A$. By definition of $\neg \neg A$ this means we need to take any proof $a$ of $A$ and turn it into a proof $q$ of $\neg A \rightarrow \bot$. So let $z$ be any proof of $\neg A$, then by definition $z(a)$ is a proof of $\bot$. So $q$ is the assignment $z \mapsto z(a)$ and then $p$ is the assignment $a \mapsto q$ which is a proof of the claim.
Now, on the other hand, what if we proved this by saying, let $a$ be any proof of $A$ and let $z$ be any proof of $\neg A$. Then $A \wedge \neg A$, thus we have explosion therefore the implication we want to prove is true (because everything is true).
Is the second an example of inference that is not allowed in the minimal case? And the first is an example that is allowed in the minimal case?
I feel like the use of explosion could easily be avoided in the second proof then by simply saying "let $a$ be a proof of $A$, let $z$ be a proof of $\neg A$, but $A$ and $\neg A$ is a contradiction therefore $\bot$?
Best Answer
Yes, $\lnot\lnot A$ means $(A\to \bot)\to \bot,$ so assuming we have $A$ we need to show that if we have $(A\to \bot),$ then we have $\bot,$ but this is just implication elimination. You are correct, no explosion here.
Your reasoning in the case where you try to use explosion is not right (even when explosion is valid). You have outstanding assumptions, so you cannot just declare victory once you hit a contradiction and conclude anything you want. What explosion will allow you to conclude here is that $(A\land \lnot A)\to (A\to\lnot\lnot A)$ (which is not exactly helpful), or more generally $(A\land \lnot A)\to B$ for any $B.$
(Also, explosion is usually considered to be an inference from $\bot,$ rather than from $A\land\lnot A,$ but of course one can easily infer $\bot$ from $A\land \lnot A$, so the inference of $B$ from $A\land \lnot A$ is valid.)
But your final paragraph is a correct argument. In fact $(A\land\lnot A)\to \bot$ is just an uncurried version of $A\to (\lnot A\to \bot)$ i.e. $A\to \lnot\lnot A,$ so they are the same proof.