What practical proofs work in intuitionistic but not minimal logic?

Solution 1:

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.

Solution 2:

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:

http://en.wikipedia.org/wiki/Paraconsistent_logic
and
http://en.wikipedia.org/wiki/Relevance_logic

Good luck