4 ms·

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

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.

lapinot 8y ago
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.
- auggierose 8y ago
  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.
logicchains 8y ago
>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.
- auggierose 8y ago
  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.

lapinot 8y ago

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.

auggierose 8y ago
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.

logicchains 8y ago

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

auggierose 8y ago
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.