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.