I have been reading and thinking about this for a long time and I still don't understand the motivation for denying excluded middle or double negation elimination. And in the video "5 stages of accepting constructive math", many strange claims are made of theorems that are constructively valid but that make no sense. Subsets of finite sets need not be finite? Injection map from the entire reals into N?
So far to my understanding, it seems that fundamentally the motivation for this, are the beliefs that
1) mathematics is "not real" (that a mathematical object exists only insofar as a mind can create a proof of its construction and do not exist in an object platonic sense)
and 2) that (and this seems to be the most important difference) that computation is "more important" than mathematics (sort of like point one, and also ties in to Curry Howard, propositions as types, etc).
I guess I need to just read more, what would be good books on this, in the philosophy and motivation, or if any knowledgeable anon wants to take time to explain that would be much appreciated.
I simply do not understand how you can reject LEM and DNE, and there must be a theorem under constructive/intuitionist logic where these classical axioms are proven, because they are obviously true, and any logic that denies them is obviously necessarily false a priori.