>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.
How many of these results require applying the LEM to undecidable propositions? The LEM works fine in constructive logic for provably-decidable propositions.