Intuitionistic logic contains the rule $\bot \rightarrow \phi$ for every $\phi$. In the formulations I have seen this is a separate axiom, and the logic without this axiom(?) is termed "minimal logic".
Is this rule required for practical proof problems in intuitionism? Is there a good example of a practical proof which goes through in intuitionism which doesn't go through without this axiom, or do all/most important practical results also go through in minimal logic? And can you please illustrate this with a practical example?
Context: We are faced with a decision theory problem in which it might be very useful to have a powerful reasoning logic which can nonetheless notice and filter consequences which are passing through a principle of explosion. So if the important proofs use a rule like $(A \vee B), \neg A \vdash B$ and we can replace that with $(A \vee B), \neg A \vdash \neg \neg B$ to distinguish the proofs going through the 'explosive' reasoning, that would also be useful.
ADDED clarification: I'm not looking for a generic propositional formula which can't be proven, I'm looking for a theorem in topology or computability theory or something which can be proven in intuitionism but not in minimal logic, along with a highlighting of which step requires explosion. Could be a very simple theorem but I'd still want it to be a useful statement in some concrete domain.
Best Answer
In minimal logic you can't prove a formula of the form $\forall x \;\neg A(x) \rightarrow B(x)$, where $B(x)$ doesn't have $\bot$ as a subformula, unless you can already prove $\forall x\;B(x)$. To see this, note that if we can prove $\forall x\;(A(x) \rightarrow \bot) \rightarrow B(x)$ in minimal logic, then we could prove the same formula with $\bot$ replaced by $\top$, ie $\forall x\;(A'(x) \rightarrow \top) \rightarrow B(x)$ (where $A'$ has any instances of $\bot$ in $A$ replaced by $\top$). Since $\forall x \;A'(x) \rightarrow \top$ is provable, we deduce that $\forall x\;B(x)$ is also provable.
To give an explicit example, we can easily prove in intuitionisitic logic that if a natural number $n$ is not prime, then there are $a, b$ such that $1 < a, b < n$ and $n = ab$. But this won't work in minimal logic.
I think the key part of the proof that works for intuitionistic logic but not minimal logic is the following principle. On the basis of this principle it shouldn't be surprising that the above example holds in intuitionistic logic. If $\phi$ is a quantifier free formula, then we can prove $$ \neg(\forall x < y \;\neg\phi(x)) \rightarrow \exists x < y\; \phi(x) $$ (This is a bounded version of the classical principle $\neg \forall x \neg \phi \rightarrow \exists x \phi$).
We prove this by induction on $y$. Note that if we have ex falso, then the case $y = 0$ is easy. Suppose now that we have shown this for $y$ and want to show it for $y + 1$. Suppose further $\neg(\forall x < y + 1\; \neg \phi(x))$. Since $\phi(x)$ is quantifier free, we know that either $\phi(y)$ or $\neg \phi(y)$ holds (by another inductive argument). Suppose that $\phi(y)$ holds. Then we can trivially show $\exists x < y + 1\;\phi(x)$. Now suppose that $\neg \phi(y)$ holds. Note that we can't have $\forall x < y\; \neg \phi(x)$ because this would imply $\forall x < y + 1 \; \neg \phi(x)$ (because for every $x < y + 1$ either $x = y$ or $x < y$ by yet another inductive argument!). Hence $\neg (\forall x < y \; \neg\phi(x))$ holds and so by the inductive hypothesis we can show $\exists x < y\; \phi(x)$, and deduce $\exists x < y + 1\;\phi(x)$.
So ex falso was explicitly used for the case $y = 0$. I suspect that it is also important for the inductive argument that for every $x < y + 1$ either $x = y$ or $x < y$ that I didn't show.