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