Hacker News new | ask | show | jobs
by eli_gottlieb 4073 days ago
>Still, for a subset of statements and properties it is possible to construct a law of excluded middle, but it has to be a constructive proof. The whole idea of Constructive Mathematics is that you have to show a proof for both, the statement and it's negation to hold their respective truth values. The impossibility to proof the first statement, that of all statements the negation is implied, is surely tautologic, assuming it would hold true for most of all statements, just not a class the opening one is part of. This class is an empty element.

It's actually a lot simpler than that. Proofs in constructive logic have computational content, so the actual counterexample to the Law of the Excluded Middle is the Halting Problem. To state the Law of the Excluded Middle constructively is to say, "I possess a Turing machine which can answer yes-or-no to any given proposition in finite time", which is a trivially false statement (particularly where concerning sufficiently large infinities).