Hacker News Reader

Comment by fnrslvr | Hacker News Reader

As someone whose education straddled the four-pillars pure topics, mathematical foundations, and computer science, I share a bit of a wariness about AC with the constructivists, but I cannot let go of LEM. It's a big part of how I reason, and a number of results that I consider important and illuminating hinge upon it.

My (not entirely informed) sense is that constructive mathematics would have more success if more of an effort was made to pose it as a readily instantiable, tagged embedding within the larger classical mathematical corpus. Less Brouwer-style dogma about LEM being "wrong", more emphasis on streamlining a pathway for results to travel from the mathematical journal literature into software design specs.

View on HN

Note that axioms are usually added, removing is weird. As such i see it mostly the other way around: there is a classical fragment inside constructive logic (this should not contradict what you said tho). In constructive logic, for a proposition `P \in Set` the proposition "P is in the classical fragment" is `dec(P) := P \/ P -> 0` (`0` being the empty type). As such we can define the set of classical propositions: `CL := exists P \in Set, dec(P)`, eg couples of sets together with either an element of it or a function that maps its elements to an inexistent thing (absurdity).

LEM is not wrong, it's just not always true. You must be familiar with the fact that AC is not provable in ZF, as such isn't LEM kinda philosophically wrong for AC? Not forcing LEM to be true is useful to have a better (more generic) understanding of complicated things. In general restricting logics (eg linear logic, constructive logic, etc) is only making them more powerful: we are able to express more propositions and we can internally (or externally as in linear logic with `!`) define the fragment for which the old axioms were valid. Pure languages enable explicit talk about computation, linear languages enable explicit talk about memory. Restriction are about increasing expressivity and most of we time we build them in the way that they retain the same proof-theoretic power.

Didn't you mean "implicit" here instead of "explicit"? Because I have no trouble at all to talk explicitly about memory and computation in full-blown set theory.

>It's a big part of how I reason, and a number of results that I consider important and illuminating hinge upon it.

How many of these results require applying the LEM to undecidable propositions? The LEM works fine in constructive logic for provably-decidable propositions.

It's just that I usually don't care about the decidability of propositions I apply LEM to, so I don't want to have to prove something first I don't care about.

Reply on news.ycombinator.com