| ▲ | Jweb_Guru 3 hours ago | |
I think the constructive position is basically that people's entire issue with lack of excluded middle being absent is just that people like being able to say "P" instead of "~~P" because it sounds better, considering you can prove ~~P for all the classical propositions that use excluded middle. | ||
| ▲ | antonvs 25 minutes ago | parent [-] | |
> people like being able to say "P" instead of "~~P" because it sounds better It depends on how old an intuitionist/constructionist you are. Back in the day, they were interested in logic as a description of correct reasoning. Brouwer saw LEM as a mistake in the foundations. These days, the influence of formalization, including proof theory and model theory, has removed a lot of the teeth from that debate and made it possible to summarize as you have. I studied this in the early 1980s, and my professor was definitely in the "this is a black and white issue" camp, although he came down on the classical side. (Side note, I was once a back seat passenger in a car with my prof and Quine in the front seat, who was visiting at the time. Quine was famously committed to the idea that first order logic is the only kind worthy of the name.) | ||