If you’re going to quibble over whether LEM is justifiable in this case, then you need to justify why you’re only concerned about LEM; why not drop ex falso too (Kolmogorov had serious issues with this axiom, and initially considered it to be incompatible with a constructive logic) and work in a paraconsistent logic?
Also, depending on the precise formulation of this proposition, it doesn’t necessarily need LEM.
I care about LEM because I'm not very happy with the computational content of LEM. I know it can be interpreted as "proceed according to $not-A$; if you find a contradiction by building an $A$, wind back the universe and proceed with the resulting proof of $A$", but this feels unsettling to me. Ex-falso has trivial computational content, and we use it all the time: it's `panic!()`.
(I agree that there are formulations which don't require LEM, but it's important to be precise, especially when writing to dismiss a common misconception among people who haven't got the concepts crisply in their minds. "Is this quantity computable?" is very close in spirit to "can I compute the value of this quantity?", and LEM is exactly the kind of axiom which shows the difference.)
> I'm not very happy with the computational content of LEM
> Ex-falso has trivial computational content, and we use it all the time: it's `panic!()`.
I have major issues with the computational content of a bottom type; my interpretation of the BHK semantics would not admit ex falso as constructive.
Of course this all of this really stems from one’s notion of semantic truth: any non-trivial semantic theory of truth can be argued as the “one true logic”, and there’s not much anyone can say otherwise! As I see it, it really comes down to how useful it turns out to be in modelling the particular domain of discourse.
As it happens, I’m more than happy to accept classical logic: I believe the principle of bivalence is how the world works, and as a result I’m forced to admit LEM if I want my proof calculus to be complete.
You are right that pointing out the connection to LEM is important and worthwhile, regardless of formulation.
By the way, an argument for ex-falso which I found very compelling: Take "False" to be syntactic sugar for "0 = 1"; then you can prove by induction that if False then all numbers are equal. That gives you a great deal of quodlibet completely soundly (since by induction on list-length, all lists are then equal to the empty list, and so on).
Is there a variant of "there exists a program that prints BB(8000)" that doesn't rely on some sort of axiom of choice? Maybe the intuitionists have a more useful definition of computibility if it doesn't posit that such strange machines exist.
> Is there a variant of "there exists a program that prints BB(8000)" that doesn't rely on some sort of axiom of choice?
Why does it rely on the axiom of choice? It’s a consequence of the obvious fact that for every integer n, there exists a program that prints n. This doesn’t require choice.
Maybe choice was stronger than I needed. Thinking about it more, I think the problem is that BB isn't even definable (that I can see) without LEM. There's an "either the machine halts or it doesn't" baked in to the computation of the integer.
A lot of stuff in math doesn't work the same way without the law of the excluded middle, but it's always assumed unless it's stated explicitly that we're working under some other logical system.
If you’re going to quibble over whether LEM is justifiable in this case, then you need to justify why you’re only concerned about LEM; why not drop ex falso too (Kolmogorov had serious issues with this axiom, and initially considered it to be incompatible with a constructive logic) and work in a paraconsistent logic?
Also, depending on the precise formulation of this proposition, it doesn’t necessarily need LEM.