Comment by zozbot234

Comment by zozbot234 5 days ago

2 replies

> Look, I think that it is interesting to work with constructive axioms, but I don't think that humans philosophically reject non-constructive results.

I don't think the point of constructivism is to "philosophically reject non-constructive results". You can accept non-constructive results just fine as a constructivist, so long as they're consistently rephrased as negative statements, i.e. logical statements starting with "NOT ...". This is handy in some ways (you now know instantly what statements correspond to "direct" proofs that can be given a computational semantics and even be reused for all sorts of computer sciencey stuff) and not so handy in others (to some extent, it comes with a kind of denial about the inherently "dual" nature of the fragment of your constructive logic that contains all that negatively-phrased stuff). But these are matters of aesthetics and perceived elegance, more than philosophy.

The duality concern is one that some will want to address by moving even further to linear logics (since these are "dual" like classical logic but also allow for constructive statements) but of course that's yet another can of worms in its own right.

btilly 5 days ago

When you talk about the point of constructivism, do you mean currently, or historically?

For me, personally, the point of constructivism is to wind up talking about mathematics in a language that corresponds with what I want words to mean. I personally want mathematical existence to mean something that could be represented in an ideal computer. And existence in classical mathematics means something very different than that.

But historically, the point of constructivism was to try to avoid paradoxes through careful reasoning. At least that is my understanding. You're welcome to read http://thatmarcusfamily.org/philosophy/Course_Websites/Readi... and decide if that is what Brouwer meant.

Unfortunately for this historical motivation, Gödel proved that every classical mathematical proof can be mechanically transformed into a purely constructive proof, possibly of a much more carefully worded statement. With the result that if there is a contradiction within classical mathematics, there is also a contradiction within constructivism.

Luckily it has been so long since our foundations of mathematics fell apart because of someone finding a contradiction, that we no longer worry about it. (Was the set of all sets that do not contain themselves the last such contradiction? I think it might have been.)

  • zozbot234 5 days ago

    You could argue that the early constructivists' notions of "paradoxes" included things such as "statements about the existence of things that we don't know how to explicitly construct, and that may be even impossible to explicitly construct in the general case". Under Gödel's argument, these statements (like other classical statements) become mere negative statements asserting the non-existence of anything that might contradict the aforementioned non-constructive objects. So, they're no longer "paradoxical" in that sense. Stated another way, decidability/computability (perhaps relative to some appropriate oracle, to fully account for the surprising strength of some loosely-"constructive" principles) is not quite the same concern as consistency. Of course, this was all stated in very fuzzy and imprecise terms to begin with (no real notion back then of what "decidable" and "computable" might mean), so there's that.