Post #1511728
2026-04-20 21:41 UTC
@MartinEscardo i was thinking about this a while ago! one of the coolest things about constructive mathematics is the way in which you come across subtle structure which doesn't show up classically because of LEM having a kind of "flattening" effect, making subtly distinct notions equivalent
Replies (1)
-
@mra@mathstodon.xyz 2026-04-20 21:55
as an example, i had a very interesting discussion on irc the other day about the relationship between total orders and decidable orders. if you define totality in the "obvious" way, as \((x\ y : S) \to x \le y \uplus y \le x\), this turns out to be equivalent to decidability of the order (better still, the proof is surprisingly tricky)! to distinguish the two notions, you need to be sure that totality is valued in propositions, and define it as something like \((x\ y : S) \to \| x\le y \uplus y \le x \|\). it's a neat bit of subtlety which simply disappears classically