> This means that no propositions of the form v=n are provable in ZFC. It does not imply that all propositions of the form v=n (v≠n) are independent of ZFC!
Doesn't it mean that there are at least two such propositions, v=n_1 and v=n_2, which are both independent of ZFC?
Assume there is a fixed unique integer i such that i = BB(745).
We know that v=n is unprovable for all n, including i.
We know that v≠i is unprovable because (a) it is a false statement; and (b) we assumed ZFC was consistent.
All that remains to be shown is that there is some other integer j for which v≠j is unprovable. This must be the case: if v≠j were provable for all integers j not equal to i, that would constitute a proof that v=i,† and v=i is unprovable.
So v=i and v=j are both simple truth-valued propositions that are independent of ZFC.
Why are i and j not equally valid choices for the value of v?
† because "ZFC proves that there is a unique integer v such that P(v)"
Sure you are right there would be at least two propositions with different values of n_1 and n_2 that are independent of ZFC. But this does not mean that BB(745) has two values that are actually true, it just means that ZFC is unable to determine which of those two propositions is correct and which one is incorrect.
In fact, from outside of ZFC, it's trivial to see that the correct value would be whichever of the two standard integers is larger, if n_1 is a standard integer and is greater than n_2 then BB(745) would be n_1, otherwise it would be n_2. If there are X such propositions involving standard integers that are independent of ZFC then the actual value of BB(745) would be max(n_1, n_2, ..., n_X).
Of course ZFC can't prove this but that doesn't mean that the real value is unknowable or that the actual value is ambiguous or could take on different values. All it means is that ZFC does not have a sufficiently powerful axiom to prove which of the two values is the true value.
Furthermore because the busy beaver function is co-recursively enumerable, then it follows that any axiomatic system that was able to prove that BB(745) is a different standard integer from max(n_1, n_2, ..., n_X) would be inconsistent, even though ZFC would be unable to prove its inconsistency.
As I said before, ZFC holds no special status or authority on the nature of the busy beaver function so just because ZFC is not powerful enough to discriminate between a set of propositions about what the value of BB(745) is does not mean that BB(745) can actually take on multiple values depending on your interpretation.
I think this is wrong. Because we can run the Turing machines for max(n1, n2) steps. If a machine halts after that many steps, then it rules out the lesser value. If none of them halts after that many steps it rules out the greater value.
So our only uncertainty is between one specific number, and some unspecific bigger number that forever recedes into the distance as we try to approach it.
You propose that the issue is some pesky non-standard numbers that are bigger than any other number. But I'm thinking the issue is rather the for-all symbol.
Like from the outside of the theory we can see that we can prove a certain property for 1, for 2, for 3 etc, in fact we can prove this property for any number. But inside the theory we cannot prove that for-all n the property holds. So there is a divergence between what we want for-all to mean and what it actually ends up meaning?
Or using the there-exists perspective, if there exists an actual object inside a theory that satisfies a property P, then there-exists x such that P(x) will be true. But it can also be true without such an actual object existing.
However, your description is just another way of saying what I'm saying about nonstandard numbers. From outside of the theory you can prove P(1), P(2), P(n) for any N that is an actual natural number, but from inside of the theory you can't do that. Why not? Because from inside of the theory there is a model that is completely consistent with Peano arithmetic but contains some object E that is greater than any standard natural number. The theory can not eliminate the existence of this E and in fact it's possible to construct an E such that P(E) is false.
> In fact, from outside of ZFC, it's trivial to see that the correct value would be whichever of the two standard integers is larger, if n_1 is a standard integer and is greater than n_2 then BB(745) would be n_1, otherwise it would be n_2. If there are X such propositions involving standard integers that are independent of ZFC then the actual value of BB(745) would be max(n_1, n_2, ..., n_X).
This doesn't sound trivial to me. It's easy to see that the largest such value is an upper bound on BB(745), but even that isn't worth much. There could be an infinite number of such values. (In which case your definition of which value was correct would contradict the earlier statement that ZFC proves a unique value of BB(745) exists!)
Also...
> In fact, from outside of ZFC, it's trivial to see that the correct value would be whichever of the two standard integers is larger
What part of your analysis takes place outside of ZFC? This looks to me like you're about to propose that ZFC contains a proof of the value of BB(745), contradicting the stipulation that it doesn't.
-----
In particular, let's say that we have two values, n_1 < n_2, for which BB(745)≠n [either n] cannot be proved.
The definition of the busy beaver sequence tells us that BB(745) is the maximum number of steps a 745-state Turing machine can take without halting, if it's ever going to halt at all.
Describing a 745-state Turing machine which halts after k > n_1 steps would prove BB(745)≠n_1, and therefore cannot be done. But unless we believe that there are Turing machines which ZFC is not able to describe, this would also mean that no such Turing machine exists (since existence would imply description, and description would prove the unprovable). That would make n_1 the "true" value.
But now we have the problem that we just proved v=n_1, which also can't be done.
Did I make a mistake somewhere? Where did we leave ZFC?
>It's easy to see that the largest such value is an upper bound on BB(745), but even that isn't worth much.
Having an upper bound on the value of a BB(N) is all you need to solve BB(N). Why? Because if you have an upper bound called U, then you know that any Turing Machine that runs for more than U steps will run forever. So an upper bound is as good as a solution.
>There could be an infinite number of such values.
No there can't be an infinite number of these because the number of 745 state Turing Machines is finite and each Turing Machine represents one possible value for what BB(N) can be. The number of possible binary Turing Machines with N states is 6 * (N + 1) ^ (3 * N).
As for the rest of your post, I think to address it we should step back from busy beavers and just focus on one specific aspect of it that is easier to reason about.
Let's say there's some Turing Machine H, and whether H halts is independent of ZFC, that is ZFC is unable to prove whether H halts or runs forever. Does this mean that in fact H can both halt and not halt depending on our interpretation? Is it possible that H both halts and does not halt? Can we as humans just decide to choose one axiomatic system where H halts, or we can decide to choose another axiomatic system where H does not halt and both systems are perfectly valid and legitimate?
Of course not. If whether H halts or runs forever is independent of ZFC, then in fact H never halts. It's not a matter of personal choice, or a matter of interpretation, or something we can just arbitrarily choose, H simply runs forever.
We can tell from outside of ZFC that H must run forever, even though from inside of ZFC the proposition is unprovable. That does not mean that ZFC is able to prove that H halts; what it means is that ZFC is unable to precisely define what a natural number is and that from inside of ZFC there are two possible systems of natural numbers:
In one system of natural numbers H runs forever, which is the system of natural numbers that corresponds to the actual truth. This system of natural numbers is what we call the standard model of arithmetic and is the intended interpretation of the natural numbers [1].
In another system of natural numbers, the nonstandard model of arithmetic, H halts after X steps where X is a nonstandard natural number [2]. You can think of a nonstandard natural number as a number that is larger than any standard natural number, for example imagine a whole number with an infinite number of digits. Now we know that a natural number is only supposed to have a finite number of digits, but ZFC is not powerful enough to define natural numbers this way, so it can not eliminate every model of natural numbers that have infinite digits and in one such model H does halt.
In fact, no consistent first order system is powerful enough to define natural numbers in such a way that they only have a finite number of digits, every single first order system will have some model of natural numbers that have an infinite number of digits.
So no, the fact that HALT(H) is independent of ZFC does not mean that we can just decide to pick an axiomatic system where H halts or one where it does not halt and both are valid choices, because in the system where H halts we are no longer working with the actual natural numbers. It's only in the axiomatic system where H never halts that we get to work with the natural numbers.
Given these concepts, you can now apply them to better understand how the busy beaver function can only have one single value. Yes there are propositions of ZFC where BB(745) = n1, and BB(745) = n2, and both of these propositions are independent of ZFC. No, that does not mean that BB(745) can actually be either n1 or n2 and the choice is a matter of preference. Only one axiomatic system represents the actual natural numbers, and the other ones represent the nonstandard natural numbers whose values can be infinitely large and have infinitely many digits.
> This means that no propositions of the form v=n are provable in ZFC. It does not imply that all propositions of the form v=n (v≠n) are independent of ZFC!
Doesn't it mean that there are at least two such propositions, v=n_1 and v=n_2, which are both independent of ZFC?
Assume there is a fixed unique integer i such that i = BB(745).
We know that v=n is unprovable for all n, including i.
We know that v≠i is unprovable because (a) it is a false statement; and (b) we assumed ZFC was consistent.
All that remains to be shown is that there is some other integer j for which v≠j is unprovable. This must be the case: if v≠j were provable for all integers j not equal to i, that would constitute a proof that v=i,† and v=i is unprovable.
So v=i and v=j are both simple truth-valued propositions that are independent of ZFC.
Why are i and j not equally valid choices for the value of v?
† because "ZFC proves that there is a unique integer v such that P(v)"