> The fact BB(745) can't be constructed using ZFC only means that [...]
...so what?
The claim wasn't that BB(745) can't be constructed using ZFC, or that it's not computable.
The claim was that its value is independent of ZFC, that the ZFC axioms do not make any logical implication about the value. This necessarily means that there are multiple possible values; if there were only one value, that value would be logically implied by ZFC regardless of whether it was provable in ZFC.
I should also note that these two observations are not compatible with each other:
> BB(745) is a specific integer, so it's nothing more than a sequence of finite digits
>This necessarily means that there are multiple possible values; if there were only one value, that value would be logically implied by ZFC regardless of whether it was provable in ZFC.
This is a false statement. The fact that BB(745) can't be constructed using ZFC does not mean that it has multiple values. All it means is that there is at least one Turing Machine that never halts but can't be proven to run forever using ZFC, that is it.
BB(745) is one specific integer, there is nothing really special about ZFC in this sense, it's just one axiomatic system that happens to be very useful as the foundation of most of the mathematics that is studied, but one could just as easily work with a different axiomatic system instead.
There are values of BB(n) that have no construction using Peano arithmetic but do have a construction in ZF, and there are values of BB(n) that do not have a construction in ZF but have one in ZFC, and there are values of BB(n) that do not have a construction in ZFC but do have one in ZFC + Inaccessible Cardinal Axiom, so on so forth.
ZFC does not have some kind of authoritative status in the universe of mathematics; it's possible that an alien race is doing mathematics using a far more powerful axiomatic system in which case BB(745) is constructible but BB(7450) is not.
>All finite digit sequences can be constructed.
A construction is a proof that provides a means of calculating a given value [1]. The set of all theorems that can be enumerated in ZFC do not contain a construction for the value of BB(745).
> A construction is a proof that provides a means of calculating a given value [1]. The set of all theorems that can be enumerated in ZFC do not contain a construction for the value of BB(745).
Of course they do. They just don't contain a proof that that value has the relevant properties that define the Busy Beaver sequence.
There's a big difference between constructing the value 107 and proving that that same value satisfies a given set of constraints.
We'll agree to disagree on this point then. My stance is you're using the word construction in a more layman like manner whereas I am using it in the more formal sense. It's not a particularly big deal either way.
The answer to all of these questions is obviously "yes".
Is BB(745) one of those constructible numbers? This is harder to answer, except that you have firmly taken the position that it is. Hence it must be constructible.
> The claim was that its value is independent of ZFC, that the ZFC axioms do not make any logical implication about the value.
This is not what "independent from ZFC" means: e.g. ZFC easily proves that BB(745) is larger than 10000. It even proves that BB(745) is a sum of at most six primes.
Independence here just means that for any fixed (meta-theoretic) numeral n, ZFC cannot prove that BB(745) is exactly n -- unless ZFC is inconsistent, a possibility we can't really rule out.
This implies that ZFC (again, if it's consistent) does not suffice to establish an explicit upper bound BB(745) < n either. But that's very far from ZFC not making _any_ logical implications about the value.
> This is not what "independent from ZFC" means: e.g. ZFC easily proves that BB(745) is larger than 10000. It even proves that BB(745) is a sum of at most six primes.
I would respond to the first example by noting that you're correct, but I am limited to using a finite number of words when I talk, and to the second one by not considering it a contradiction of what I said. (Though I'm making the assumption here that you're applying a theorem that holds for every integer to BB(745).)
> Independence here just means that for any fixed (meta-theoretic) numeral n, ZFC cannot prove that BB(745) is exactly n -- unless ZFC is inconsistent, a possibility we can't really rule out.
My understanding was that the independence of the continuum hypothesis takes the following form:
(1) If ZFC is consistent, then ZFC ∪ {CH} is also consistent.
(2) If ZFC is consistent, then ZFC ∪ {¬CH} is also consistent.
This is quite explicit that independence allows for the selection of (one of) multiple values. It happens to be an exact match to what is given on Wikipedia right now:
> The answer to this problem is independent of ZFC, so that either the continuum hypothesis or its negation can be added as an axiom to ZFC set theory, with the resulting theory being consistent if and only if ZFC is consistent.
You appear to be saying that a proposition that is entailed by ZFC, but not proven by ZFC, is nevertheless independent of ZFC, but I don't think that can be right?
"The proposition CH is independent of ZFC" and "the value of BB(745) is independent of ZFC" are two different statements.
A proposition P is independent of ZFC if it's not possible to prove P and not possible to prove its negation ~P either.
If P(-) is a unary predicate, we say that the value of an integer v with definition P(-) is independent of ZFC if ZFC proves that there is a unique integer v such that P(v), but fails to prove that P(v) implies v=n for any specific (meta-theoretic) numeral n. 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!
Basically, two different (but not unrelated) senses of independent.
> 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.
You can construct the particular natural number that it is, obviously. Constructing BB(745) means providing that number and a proof that it's the right one.
...so what?
The claim wasn't that BB(745) can't be constructed using ZFC, or that it's not computable.
The claim was that its value is independent of ZFC, that the ZFC axioms do not make any logical implication about the value. This necessarily means that there are multiple possible values; if there were only one value, that value would be logically implied by ZFC regardless of whether it was provable in ZFC.
I should also note that these two observations are not compatible with each other:
> BB(745) is a specific integer, so it's nothing more than a sequence of finite digits
> BB(745) can't be constructed using ZFC
All finite digit sequences can be constructed.