Quite often when I am making a natural deduction proof, and I have no fixed idea on how to continue. I find myself thinking:
"lets start with some form of the law of the excluded middle (LEM) and take it from there."
But recently I more and more realise that most proofs can be done simpler and shorter in other ways, even if you may add forms of LEM as one line theorems into a proof. (like in some Fitch setups)
With LEM you standard get into an $ \lor$ elimination proof, (giving two subproofs) while without LEM, you can do the same with a single $\lnot$ introduction subproof.
This made me wonder are there proofs where introducing some form of LEM does shorten the proof?
(off course this is except proofs of the law of excluded middle itself or a closely related theorems like $\forall x (F(x) \lor \lnot F(x)) $)
My question is about "normal" natural deductions containing just the standard introduction and elimination rules for connectives:
- $ \land $ introduction and elimination
- $ \lor $ introduction and elimination
- $ \to $ introduction and elimination
- $ \equiv $ introduction and elimination
- $ \bot $ introduction and elimination
- $ \lnot$ introduction and
- $ \lnot \lnot $ elimination
So without recourse to de DeMorgan laws and other derrived rules.
Best Answer
First, there are theorems provable in a classical setting that cannot be proved without LEM just because they are not true (in full generality) in certain intuitionistic settings, such as the Extreme Value Theorem; see this recent text. Other than that, relying on LEM often shortens the proof but of course gives a weaker result. For instance, showing that $\sqrt{2}$ is irrational is certainly shorter if one is allowed to use LEM, but a proof without an estimate leaves one with a sawdust taste in one's mouth, according to Bishop.