5 ms·

There is no paradox and yes, BB(745) is a specific integer, so it's nothing more than a sequence of finite digits. The fact BB(745) can't be constructed using

by Kranar 3y ago

There is no paradox and yes, BB(745) is a specific integer, so it's nothing more than a sequence of finite digits. The fact BB(745) can't be constructed using ZFC only means that there is at least one Turing machine among the set of all 745 state Turing machines that runs forever, but can't be proven to run forever using the axioms of ZFC. You'd need a more powerful axiomatic system to prove that this Turing machine actually runs forever. This does not imply any kind of paradox or any kind of issue whatsoever in fact. It just means that ZFC is not powerful enough to prove that certain 745 state Turing Machines run forever.

thaumasiotes 3y ago
> 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 > BB(745) can't be constructed using ZFC All finite digit sequences can be constructed.
- Kranar 3y ago
  >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). [1] https://en.wikipedia.org/wiki/Constructive_proof https://en.wikipedia.org/wiki/Constructive_proof
  - thaumasiotes 3y ago
    > 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.
    - Kranar 3y ago
      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.
      - thaumasiotes 3y ago
        Think of it this way: Is it possible to construct the value 2? Is it possible to construct 3? Is it possible to construct 4? [...] 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.
- saithound 3y ago
  > 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.
- nyssos 3y ago
  > All finite digit sequences can be constructed. 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.

by Kranar 3y ago

thaumasiotes 3y ago

> 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 > BB(745) can't be constructed using ZFC All finite digit sequences can be constructed.

Kranar 3y ago
>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). [1] https://en.wikipedia.org/wiki/Constructive_proof https://en.wikipedia.org/wiki/Constructive_proof
- thaumasiotes 3y ago
  > 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.
  - Kranar 3y ago
    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.
    - thaumasiotes 3y ago
      Think of it this way: Is it possible to construct the value 2? Is it possible to construct 3? Is it possible to construct 4? [...] 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.
saithound 3y ago
> 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.
nyssos 3y ago
> All finite digit sequences can be constructed. 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.