I've been researching Constructivism and Godel's Incompleteness theorems as of late. I was hoping to get feedback on this question. In order to do math, we need a set of axioms A and a system of logic L. This pair (A,L) is called "incomplete" if there exist propositions (in the language of A) that are not derivable from A using L. This pair (A,L) is called "inconsistent" if a proposition can be shown to be both true and false. We know that ZFC is incomplete because there exist problems, such as the Continuum Hypothesis, that are independent of ZFC. Because ZFC cannot answer all propositions, it does not necessarily make sense to include the Law of the Excluded Middle when working in ZFC (or even just ZF) because we do not know that a given proposition in question is either true or false. Applying the LEM to a statement that is independent from the axioms will yield invalid math, hence apprehension to using it. (By this reasoning, it would make sense to reject the LEM for any incomplete system.) So, does that last paragraph follow? I favor Platonism myself, but I can certainly sympathize with the above reasoning. It simply seems dangerous to assume that a statement is decidable in ZFC without knowing so for a fact. It seems as if MOST of the time they are, but still, I can sympathize a conservative approach. However, consider the classic proof that there exist a,b irrational such that a^b is rational. When considering .5^.5, do we actually need the LEM? By definition, if a number is not rational then it is irrational, and we have a precise definition for "rational". The number .5^.5 is in one of the two sets, because if it is not rational then we get to define it to be irrational. I have heard it said that constructivists reject this non-constructive proof, but why? It seems as if their reason for rejecting the LEM does not apply here. And therein lies the question... Is the constructivist's reasoning for rejecting the LEM more than just a fear of using it in an incomplete system?