[nimih]

> How do we know that BB(n) exists for all n?

What would it mean for BB(n) to "not exist"? Recall that BB(n) is defined in a very concrete way: you take all the Turing machines of size n (which are easily enumerable combinatorial objects), remove ones which do not halt, then take the largest runtime of the ones that are left. Since we can always write down a Turing machine which halts immediately, we know that there's a trivial lower bound for each BB(n), and since the Turing machines are deterministic, we know that any machine that halts must do so in a fixed number of steps. With such a straightforward construction, it's hard to see how such a number could "not exist," at least not without appealing to an ontology somewhat outside of the mainstream (e.g. ultrafinitism).

[kotlin2]

In the proof you just provided, you have a step "remove ones which do not halt". By which process do you do that? By the halting-problem, you can't actually make that selection. This ties back into the fact that BB(n) is not computable for all n. I guess what I'm looking for is a proof that the number exists without violating the halting problem. Intuitively, we feel BB(n) should exist because there are finite turing machines with n states. But I'm not sure how to express that rigorously. Or maybe relying on a solution to the halting problem doesn't matter in terms of a proof.

[alexmolas]

The Halting Problem forbids you to build an algorithm that proves if a generic problem halts or not. This doesn't forbid you to check if a specific algorithm halts or not. For example, you know that the specific program `print("Hello World")` halts. So you can remove the ones that do not halt by inspecting them one by one and developing a specific algorithm for each one that determines if it halts or not.

[kotlin2]

If you could inspect any Turing machine and devise a specific algorithm that determines if it halts, then you yourself would be an algorithm that solves the generic halting problem.

[alexmolas]

no, because you can build an algorithm that fools the algorithm that solves the generic halting problem. I wrote a "proof" of that in my blog [1]

[1]: https://www.amolas.dev/blog/halting-problem/

[kotlin2]

Exactly. So your claim that:

> So you can remove the ones that do not halt by inspecting them one by one and developing a specific algorithm for each one that determines if it halts or not.

Is impossible. You can’t, in general, inspect Turing machines one-by-one to determine if they halt.

[elijaht]

You don’t need to show a process.

Trivially a non-halting program for any n exists. Also trivially there must be some non-halting program with the highest number of steps.

We can’t necessarily find that program, but there is almost by definition some non halting program with the highest number of steps

[puffoflogic]

> Also trivially there must be some non-halting program with the highest number of steps.

That isn't trivial. Whether a given program halts might be independent of ZFC, or of any consistent logical system you might try to use. The question of whether such a program "really" halts is one which might not have an answer. ZFC claims there must be an answer, because LEM, but why should we care what ZFC or first order logic or anything has to say on the matter, if they can't actually tell us whether it halts?

[morelisp]

> By which process do you do that?

It's not a constructive proof, you don't need to give a process.

[kotlin2]

That's true. The part that "feels" weird is that there is no algorithm that could perform the separation into halting / non-halting subsets. Choosing elements from a set based on uncomputable properties almost feels like an extension of the axiom of choice.