4 ms·

> 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 fr

> 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.

thaumasiotes 3y ago
> 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?
- saithound 3y ago
  "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.
  - thaumasiotes 3y ago
    Thanks! > 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)"
    - Kranar 3y ago
      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.

thaumasiotes 3y ago

> 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?

saithound 3y ago
"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.
- thaumasiotes 3y ago
  Thanks! > 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)"
  - Kranar 3y ago
    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.