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.

  • $\begingroup$ 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. $\endgroup$ Apr 11, 2019 at 21:40

1 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.