Constructivist proofs + LEM = classical math?

Question

I have been told that constructivist/intuitionist logic is classical logic - LEM.

I see why LEM doesn't hold given the basic philosophy of constructivist mathematics, ehich I understand to be based on the interpretation of $\exists$ as "we can construct" (and a similar interpretation of the other logical symbols).

However, is it also true that if we take LEM as an additional axiom, and "append" it to whatever mathematical theory we are working with, can we then reproduce any classical proof within the constructivist interpretation?

This is not at all obvious to me from the "philosophical" explanation of what constructivist math is about.

Not that there are two questions:

• is any theorem that is provable in classical math also provable in constructivist math + LEM?

• is any classical proof also reproducable as a constrictivist proof with the same logical steps, within the same theory but with LEM appended as an axiom?

I don't know the answer to either but my question is about the latter.

Answer 1

Short answer is yes, once we add LEM we can do the same proofs as we can in classical mathematics. We do not necessarily get the same mathematics, because that also depends on what axioms you take. Constructivists often have different axioms than classical mathematicians (see e.g. this nLab page). Sometimes these axioms contradict LEM. That would mean that once we add LEM to such a universe, we would be able to prove a contradiction in that universe and it would be inconsistent (technically, the answer to your question is then still "yes", because then we can prove anything).

For example, an axiom of the form $$ \neg \forall x (P(x) \vee \neg P(X)) $$ is intuitionistically consistent but classically simply false.

One concrete example of an intuitionistic school where something happens that classically fails, is the school of Brouwer. There one can prove that every function $[0,1] \to \mathbb{R}$ is (uniformly) continuous, clearly this fails in the classical setting.