[musername]

>Agda’s logic is constructive, which means it’s impossible to prove the statement that all statements are either true or false, . This proposition is called the law of the excluded middle. This makes it impossible to perform, for example, a general proof by contradiction, or other similar “classical” proofs from mathematics. There is a large philosophical debate among mathematicians (those who follow Hilbert, and those who follow Brouwer) as to which is better

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.

I would basically assume this means nonsense statements can be constructed, but they can't be used in constructive proofs. It doesn't imply that there has to be a class of nonsense statements where the opposite still holds value. I'm cautios of the definition for statements like there or in the multiple incarnations of the liars paradox (whats the latin plural). IE. a statement should by definition be provably correct either in positive or negative logic, hi and low to use ee terms, and one should imply the other polarity (edit: just not by using negation, because that's the relation you want to prove, without circular logic). The empty element is like null, but what logic set the true ^ negative or just the true statements have to be defined in I dont know.

Interesting to know that there is a tool for this kinda maths, I was under the impression that the debate tends to inductive methods, but here we have intuitionistic (constructive) logic, I take it.

[tel]

I'm not sure everything you're talking about, but it's relatively easy to reason about constructive logic by abandoning the idea that your logic is one of "truth and falsehood"—which are, by modern, western intuition mutually exclusive options—but instead one concerning evidence.

One might believe that the Collatz conjecture is true or false, but we certainly lack evidence for either case today. This isn't exactly three value logic, but instead something else. A logic which incorporates the notion of time and communication of proof.

[nmrm]

> which incorporates the notion of time and communication of proof.

Certainly constructive logics (typically) incorporate a notion of evidence/proof. But constructive logics don't incorporate notions of time or communication (of proof, or in general).

[tel]

Yeah, to be clear, those notions aren't internalized... they just bring into clarity the need for those processes to happen in the meta level.

[eli_gottlieb]

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

[ScottBurson]

> paradox (whats the latin plural)

I think it's "paradoxa", but I've never seen anyone use that in English. Just go with "paradoxes" :-)