What practical proofs work in intuitionistic but not minimal logic?

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.

• The principle of ex falso quodlibet is logically equivalent to modus tollendo ponens in the presence of fairly minimal rules of inference. I suppose that's what you're alluding to in your third paragraph? – Zhen Lin Sep 13 '13 at 19:56

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.

• How would one prove that a number that is not prime is composite? That seems to require some form of Markov's principle, which may or not be present depending which sort of intuitionistic logic we consider. – Carl Mummert Sep 14 '13 at 12:56
• @CarlMummert I'll edit to explain. – aws Sep 14 '13 at 12:56

The disjunctive syllogism $( (A \vee B), \neg A \vdash B )$ is about the most important deduction that is valid in (Heytings) intuitionistic logic but invalid in (Johanssons) minimal logic. Johanssons article (see link on http://en.wikipedia.org/wiki/Minimal_logic ) also mentions the following formulas that are theorems in intuitionistic logic but are NOT theorems in minimal logic.

$( A \land \lnot A) \to B$

$( ( A \land \lnot A) \lor B ) \to B$

$( B \lor B) \to( \lnot \lnot B \to B )$

$( \lnot A \lor B) \to ( A \to B)$

$( A \lor B) \to ( \lnot A \to B )$

$( A \to ( B \lor\lnot C) \to ((A \land C) \to B))$

$\lnot \lnot ( \lnot \lnot A \to A)$

But maybe Johansson only mentions these because they are mentioned in Heyting's article.

I am doubtful if $( A \lor B) , \lnot A \vdash \lnot \lnot B$ is a theorem of minimal logic , have you proven it or just assumed?
[CORRECTION $( A \lor B) , \lnot A \vdash \lnot \lnot B$ is an theorem of minimal logic, because $( A \land \lnot A) \to \lnot \lnot B$ and $B \to \lnot \lnot B$ are both theorems of minimal logic]

In the 1920's there were discussions what the axioms of constructive logic were, it is just that the founder of intuitionism (Brouwer) liked Heyting and just gave him the honour to name his system THE system of intuitionistic logic, Brouwer found logic bloodless, and not really important)

What I think is a more serious problem is that $( A \land \lnot A) \to \lnot B$ is a theorem of minimal logic. so you could conclude that minimal logic still allows a lot of explosion. I think you would be better of by using a paraconstistent or relevant logic. see:

Good luck

• $(A\lor B),(A\to\bot)\vdash(B\to\bot)\to\bot$ is a theorem of minimal logic. Under the Curry-Howard isomorphism it is the type of the lambda term $\lambda c:B\to\bot.( \mathtt{case~}x\mathtt{~of~}a:A\Rightarrow ya \mid b:B \Rightarrow cb)$ with assumptions $x:A\lor B$, $y:A\to\bot$. – Henning Makholm Sep 13 '13 at 21:47
• yes i was just checking it it is indeed an theorem of minimal logic (thanks to the explosion of negatives) – Willemien Sep 13 '13 at 21:51
• I'm looking for a practical theorem, not a general formula. Like something in topology or computability theory. $(A \wedge \neg A) \rightarrow \neg B$ is plausibly fine. – Eliezer Yudkowsky Sep 13 '13 at 22:32
• "In the 1920's there were discussions what the axioms of constructive logic were, it is just that the founder of intuitionism (Brouwer) liked Heyting and just gave him the honour to name his system THE system of intuitionistic logic, Brouwer found logic bloodless, and not really important)" As I understand it Gödel showed there was "no way in hell" that intuitionist logic had a finite-valued semantics, as Heyting's system does. I don't find that result all that surprising in light of the fact that Brouwer was a very poor Kantian, if you've understood Brouwer's antipathy to logic correctly. – Doug Spoonwood Sep 13 '13 at 22:58
• @DougSpoonwood Brouwer was a constructivist mathematician, not a philosopher. and intuitionistic logic IS Heytings logic and is it is not finite valued. there is a difference between Heytings Logic and Heytings Algebra. – Willemien Sep 14 '13 at 0:42