Law of excluded middle. Do we need it in proofs?

Question

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.

Answer 1

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.

Answer 2

Sure. There exist natural deduction proofs which have all sorts of irrelevant hypotheses and blow up to thousands, or hundreds of lines long. But, there exist proofs which use the law of the excluded middle which are shorter.

Perhaps better let's consider this formula CCpqCCrqCAprq which can replace the A-elimination rule. We can "commute the antecedents" a few times and obtain CApqCCprCCqrr. Consequently, CCpqCCNpqq is a theorem. Using the law of the excluded middle we can write a proof like this:

hypothesis   1 | Cpq
hypothesis   2 || CNpq
LEM          3 || ApNp
Ao {3, 2, 1} 4 || q
Ci 2-4       5 |  CCNpqq
Ci 1-5       6   CCpqCCNpqq.

But does there exist any natural deduction proof which after introduction the hypophthesis "Cpq" and "CNpq" allows use to deduce "q" in just two more steps? I don't see how such a proof could exist. A proof of CCNpqCCpqq will also take 6 steps here, but without the law of the excluded middle, I don't see how you could find a shorter proof. So, it almost surely holds that the law of the excluded middle can sometimes lead to the shortest proof of a theorem.