This is something that seems to come up every time any foundational issue arises, be it here or elsewhere (including with my colleagues who really ought to know better), and I just kind of need to rant.
Being a constructivist minded mathematician, LEM has never sat well with me but I’ve learned to “live with it” since the rest of you take classical logic as a given. And that’s fine, except there is a consistent mistake being made that bugs me to end.
To wit: if you take your base theory ZFC (feel free to replace ZFC with whatever theory T from here on and literally everything I say will hold word-for-word exactly) and work in classical first-order logic then yes you can rather easily prove that for any proposition P in the langauge of your theory that “P or (not P)” holds but this *does not* mean that somehow P holds or P does not hold. That’s not even the classical meaning.
What you’re actually doing is proving that in any model M of ZFC, either M |= P or M |= (not P). And that in and of itself is fine ofc, but when you jump from there to treating the or as an “exclusive or” then you’ve actually made the unwarranted (or at least unstated) assumption that there is some particular model you are working in. Which, at best, means your ground theory *isn’t* ZFC so much as it’s (at least) ZFC+Con(ZFC). Which again is fine in principle, but it becomes totally illegitmate when you then mistakenly go on to conclude that somehow what holds in your unspecified and unspecifiable canonical model of ZFC holds in all models.
Anyway, /rant. I’m not even clear that anyone who still lurks here knows enough to comment on this but I needed to get it off my chest so to speak.