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.
