>>11581223Not this guy, but I'd say there's more reasons not to take it than to take it.
>Name one reason not to take it as an axiom.Properly capturing computational semantics of undecidable problems.
>>11581199E.g. fix a language and consider the enumerable collection of all legal computer programs theirin (e.g. all the ascii strings that compile in C). Let be the predicate denoting whether a given program will halt.
E.g.
P("int main(){return 7;}")
should be true, since that program compiles and, when executed, return 7immediatenly.
And
P("int main(){while(3==3){} return 7;}")
shoudl be false, since that program compiles and when run actually never breaks out of the while loop.
https://en.wikipedia.org/wiki/Halting_problemIt's known since Turing that this predicate can't be turned into an effective procedure (it's ndecidable).
Now, by the LEM, for any program X it's "true" that .
It's dubious - unless you're a hard Platonist - what that latter proposion ought to express, given that by the solution to the Halting problem, we know that there's a for which we can't decide P(a) nor not(P(a))
Not adopting the law of excluded middle doesn't get us into the situation.
>>11581239>proofs by contradiction, which are pretty usefulI suppose that point can be made, but it can also be contested.
It must be stressed that whenever Q is a propositition that's provable in the classical logic with the law of excluded middle, then there's statements Q' that are constructively provable, and which are classically immediatenly equivalent with Q.
https://en.wikipedia.org/wiki/Double-negation_translationSo it's not like adopting LEM enables you to prove more theorems (it just makes the proofs easier, as adding an axiom does.)
While, at the same time...
>Name one reason not to take it as an axiom.There's axioms A, that are inconsistent with LEM, but not with the rest of one's theory, e.g. in Synthetic Differential Geometry.
