Constructivist proofs + LEM = classical math?

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.

• Just a minor comment, Constructive Logic + LEM, as in your title, is a fairly clear thing (i.e. take all the axioms and rules of a given constructive logic and add LEM to them). Classical logic - LEM is much less clear since many presentations of classical logic rely on LEM for the connectives to behave "correctly". That is, merely removing LEM from the list of axioms for a particular presentation of classical logic could produce something much weaker than constructive logic. Apr 11, 2019 at 21:40

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.