3 ms·
Quite apart from the proof theoretic advantages others have mentioned, it's sort of a big leap of faith to believe LEM = (for all propositions P, P or not P).
by tel 10y ago
Quite apart from the proof theoretic advantages others have mentioned, it's sort of a big leap of faith to believe LEM = (for all propositions P, P or not P).
For instance, the continuum hypothesis: unproven and still controversial. We can state it in whatever ambient logic, say ZFC, you like, but then it's independent. It therefore flies directly in the face of LEM. We have to work metamathematically to even survive such a blow (as Gödel already began the trend of, ruining Hilbert's Formalist hopes).
As it turns out, we're generally quite fine exploring the consequences of logical systems even when they're flawed. It's still interesting, pays the bills, and is generally helpful. Some things might be shown "false" by some stickler's particulars of what truth means while others need modification to satisfy everyone, but we're still doing the right things "usually".
But it's still a really good question Hilbert posed: what is the ultimate underlying language that we're using to discuss and drive the mechanism of mathematics? For that, you really have to look critically at things like LEM.