Are there statments which do not have a constructive proof?

Question

I understand that a lot of statements are just non-nonconstructive in nature (like negative statements), and I understand that a lot of statements are not provable without the axiom of choice. Without those two categories - are their any statements which cannot be proven without the law of the excluded middle? If they exist, what is an example of such a statement?

Answer 1

In classical logic, you can trivially proof the low of the excluded middle (it is an axiom). However, in intuitionistic (no law of excluded middle) predicate logic, you can only proof this for certain types of formulas, e.g. quantifier-free ones. So yes, there should be statements which do not have a constructive proof.

Example: $\vdash \forall x P(x) \lor \exists x \neg P(x)$ follows in one step in a classical system, whereas in a constructive system you would have to choose one side of the disjunction and prove this, which is impossible for this arbitrary predicate $P$ without any further information.

You can, however, prove the (e.g. Kuroda) double negation translation $\varphi'$ for any classically provable formula $\varphi$. In the above example, $\vdash \neg\neg(\forall x \neg\neg P(x) \lor \exists x \neg P(x))$ would be also intuitionistically provable. This formula is of course classically equivalent to the previous one, but a different (weaker) formula in intuitionistic logic.