Coquand and Schwichtenberg’s lectures at the MAP summer school made it clear that for (higher-order) number theory, constructive logic is actually an extension of classical logic, rather than a restriction. This applies to all concrete mathematics and, more generally, to any theory with decidable atomic formulas. This is the result of Gentzen’s double negation translation. There are actually many double negation translations that can be used to interpret classical logic inside constructive logic. I used a different double negation translation when proving the consistency of PA with Coq. However, Gentzen’s translation is the most direct.
The proof that Gentzen’s translation interprets classical logic uses the following fact that I didn’t know. For any formula φ in (higher-order) number theory that uses only the connectives ∀, ⇒, ¬, and ∧, the statement (¬¬φ ⇒ φ) is constructively valid (actually, this applies to a somewhat wider class of formulas called Harrop formulas). In other words, proof by contradiction is allowed for this set of formulas. Furthermore, this is a sufficient set of formulas for doing classical reasoning. One can define a classical existential connective as ¬∀x.¬P x, and a classical disjunction as ¬(¬A ∧ ¬B).
This is Gentzen’s interpretation of classical number theory. Disjunctions and existential quantifiers are translated into formulas using negation, conjunction, and universal quantification. So one can see that classical reasoning is just reasoning inside the existential and disjunction free fragment of constructive logic. From the other side of the fence, one can view constructive logic as an extension of classical logic by the constructive existential and disjunction operators.