[Aeium]

Yes, this is clearly true. Pardon the hasty first reading and deleted comment please.

It doesn't address what I am claiming though.

The busy beaver is not defined entirely by halting vs not-halting.

Looping beavers are excluded as well.

The middle ground I am claiming is that there is a middle ground between non-halting and provably non-halting.

I'm claiming there could be a non-halting Beaver that is impossible to prove, which would mean there is no answer for the BB function.

[rdlw]

> The busy beaver is not defined entirely by halting vs not-halting.

> Looping beavers are excluded as well.

Looping beavers do not halt.

> there is a middle ground between non-halting and provably non-halting

Yes, there are turing machines that encode mathematical theorems which are independent of ZFC, meaning they cannot be proven to halt or not to halt. The state-of-the-art is BB(748), which is known to be independent [0].

There are also much smaller known turing machines which encode classically difficult math problems, like the Goldbach conjecture [1]. This means that the value of BB(27) cannot be proven until the Goldbach conjecture is proven or disproven, as until that is done, we will always have something like "BB(27) is N unless the Goldbach conjecture is false".

However, our inability to prove these things does not change the fact that they have specific values. To stick with the BB(27) example, say that it seems we've narrowed it down to some huge number A, or a number dependent on the first number for which Goldbach does not hold. Call that second number B. We may be unable to find the value of B (doing so would disprove Goldbach), but it is still a specific number. There still exists a concrete value for BB(27)--it's A if Goldbach is true, and it's B is Goldbach is false.

[0] https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-unde...

[1] https://gist.github.com/anonymous/a64213f391339236c2fe31f874... This 27-state machine halts when it finds a counterexample to the Goldbach conjecture.

[immibis]

Busy beavers are the machines in some size class which run the longest, then halt. They may be alternatively defined as the ones which produce the most output, then halt. Machines which obviously loop are excluded, and so are machines that non-obviously loop - for example ones that loop until they prove the Riemann hypothesis are excluded if the Riemann hypothesis is false and the proof system is consistent.