3 ms·

"Given that some of these powerful set theoretic axioms are independent from each other, I'm not sure whether ZFC+CH could have a different idea about BB(8000)

by jerf 4y ago

"Given that some of these powerful set theoretic axioms are independent from each other, I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would." It can not. The TMs can only be affected by things that affect them at a finite level. To put it another way that may be easier to see, for them to have a different idea about a given BB number, there must be two otherwise identical machines facing their decision about what state to transfer into, but the one armed with the CH must choose one state and one without it must choose another. (There must always be some such first state, even if it is the very first transition.) There's nowhere to encode that inside a TM state transition table. That is the "outside" mechanics of a TM, which are fully defined by the problem itself. The "inner" mechanics of a TM, where we talk about what the machine is "really doing", may have such effects, but that's a bit more mundane. And not even necessarily relevant; while you may have two machines, one with ZFC+CH and one with ZFC without CH, they're both going to be hammered by a machine doing "something" that definitely isn't just running a clearly-defined axiomatic system over propositions, but something "mixed up" beyond all human understanding. What can affect the BB number is oracles. This is also in some sense "why" oracles are defined as essentially function calls that TMs can make with a sort of equivalent of a system call operation that user space code can use to invoke a kernel's functionality... you can easily encode that into a single finite state transfer. BB relative to an external oracle can be (and is) different than conventional BB. However, while the numbers are larger... much, much, much (etc.) larger... I think in some sense it's also less mathematically interesting and returns to just being "yet another large number generator"; BB is interesting precisely as the boundary between computability and non-computability, and BB+oracle is just straight-up uncomputable. But that's not that interesting, really; there's an infinite number of already-uncomputable functions anyhow.

hakuseki 4y ago
It seems to me that the two formal systems can disagree about BB(n) for some n without disagreeing about the state of any given Turing machine at any specific time step. For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt. If all machines other than M can be either run to completion or proven not to halt, then the value of BB(n) would be provable in ZFC+notCH but undecidable in ZFC+CH.
- karatinversion 4y ago
  > For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt. Just to add, this can only happen for a Turing machine M that does not actually halt. If you take a system which cannot prove that M does not halt, you can consistently add a new axiom that M halts - but the number of steps to halt, and thus BB(n), will be a non-standard number.
- IngoBlechschmid 4y ago
  > For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt. In general, this can happen, but not with this particular choice of example: If ZFC+CH proves that some machine halts, then so does ZFC (and, in fact, so do ZF and IZF). This is because a given Turing machine halting is a mere number-theoretic statement, such statements "are absolute between V and L" and CH holds in L.
Kranar 4y ago
I disagree but am open to being corrected. It's possible that for a TM named X there is a proof that it halts in ZFC+CH and there is a proof that it does not halt in ZFC+notCH. This would mean that X does not actually halt but that ZFC+CH contains a non-standard model of the integers [1] where BB(n) = some non-standard integer. [1] https://en.wikipedia.org/wiki/Non-standard_model_of_arithmetic https://en.wikipedia.org/wiki/Non-standard_model_of_arithmet...
- jerf 4y ago
  That might affect your proving power but it won't affect the Turing Machine itself. That Turing Machine either will or will not halt after the given number of steps, regardless of whether or not you "hand it" the CH or not. To change the result of BB requires not a change of how you are approaching the proof but the behavior of the TMs themselves, but the TMs are well-defined. Regardless of the computability of the number, BB(10,000,000) is a particular number, regardless of what proof system you try to approach it with. Amusingly, this opens up the distinct possibility of a wrong proof. You take the CH as an axiom, or, perhaps more likely, some other attractive axiom more relevant to the task at hand, and you "prove" a result with that axiom, but then you never find out that your proof is wrong and in fact the TM's behavior is other than what you proved, because... how are you supposed to run a TM for 10^10^10^10^10^10^10^10^10^10^10^10^10^10^10 steps to check your proof anyhow? (Especially since that number would be the tiniest insignificant baby steps for the BB(7) winner.) Again, if you want to change the BB number, you need to change the Turing Machines themselves, most commonly by adding an oracle to them to result in BB*.
  - Kranar 4y ago
    But that's not what OP said and you're stating something that is very different. OP said the following: "I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would." And the answer to that is yes, it's in principle possible that ZFC+CH contains a proof that a given TM halts after N steps while ZFC+notCH contains a proof that said TM does not halt after N steps. If that were the case and assuming that both are consistent it will be the case that said TM does not in fact halt (period) and that ZFC+notCH uses a model of non-standard arithmetic in its proof. You mention the possibility of a wrong proof, but that is mixing up the notion of proof and truth which are not the same things. The proofs in ZFC+notCH and ZFC+CH are both correct since a proof is nothing more than a syntactic structure that adheres to certain rules. It's that ZFC+notCH is using a model of natural numbers that is not what most people normally consider to be a natural number, it's using a model of natural numbers that admits for the possibility of incredibly large numbers that are larger than any ordinary/standard natural number. In effect ZFC+CH would contain a proof that after some unimaginably large number of steps the Turing machine halts whereas ZFC+notCH does not allow for the existence of numbers that large. So the main concept here is that two formal systems may have different notions of what a natural number is. We humans share some idea of what a natural number is supposed to be and we call those the standard natural numbers but the problem is that there is no formal way to precisely pin down those numbers without also allowing for the possibility of bizarre non-standard natural numbers as well. In this hypothetical case we would conclude that ZFC+notCH comes closer to modelling what we consider the actual natural numbers compared to ZFC+CH, but nevertheless it's impossible for any first order formal system to fully specify the natural numbers and only the natural numbers.

by jerf 4y ago

hakuseki 4y ago

It seems to me that the two formal systems can disagree about BB(n) for some n without disagreeing about the state of any given Turing machine at any specific time step. For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt. If all machines other than M can be either run to completion or proven not to halt, then the value of BB(n) would be provable in ZFC+notCH but undecidable in ZFC+CH.

karatinversion 4y ago
> For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt. Just to add, this can only happen for a Turing machine M that does not actually halt. If you take a system which cannot prove that M does not halt, you can consistently add a new axiom that M halts - but the number of steps to halt, and thus BB(n), will be a non-standard number.
IngoBlechschmid 4y ago
> For example, ZFC+CH might non-constructively predict that some machine M halts, while ZFC+notCH might predict that M does not halt. In general, this can happen, but not with this particular choice of example: If ZFC+CH proves that some machine halts, then so does ZFC (and, in fact, so do ZF and IZF). This is because a given Turing machine halting is a mere number-theoretic statement, such statements "are absolute between V and L" and CH holds in L.

Kranar 4y ago

I disagree but am open to being corrected. It's possible that for a TM named X there is a proof that it halts in ZFC+CH and there is a proof that it does not halt in ZFC+notCH. This would mean that X does not actually halt but that ZFC+CH contains a non-standard model of the integers [1] where BB(n) = some non-standard integer. [1] https://en.wikipedia.org/wiki/Non-standard_model_of_arithmetic https://en.wikipedia.org/wiki/Non-standard_model_of_arithmet...

jerf 4y ago
That might affect your proving power but it won't affect the Turing Machine itself. That Turing Machine either will or will not halt after the given number of steps, regardless of whether or not you "hand it" the CH or not. To change the result of BB requires not a change of how you are approaching the proof but the behavior of the TMs themselves, but the TMs are well-defined. Regardless of the computability of the number, BB(10,000,000) is a particular number, regardless of what proof system you try to approach it with. Amusingly, this opens up the distinct possibility of a wrong proof. You take the CH as an axiom, or, perhaps more likely, some other attractive axiom more relevant to the task at hand, and you "prove" a result with that axiom, but then you never find out that your proof is wrong and in fact the TM's behavior is other than what you proved, because... how are you supposed to run a TM for 10^10^10^10^10^10^10^10^10^10^10^10^10^10^10 steps to check your proof anyhow? (Especially since that number would be the tiniest insignificant baby steps for the BB(7) winner.) Again, if you want to change the BB number, you need to change the Turing Machines themselves, most commonly by adding an oracle to them to result in BB*.
- Kranar 4y ago
  But that's not what OP said and you're stating something that is very different. OP said the following: "I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would." And the answer to that is yes, it's in principle possible that ZFC+CH contains a proof that a given TM halts after N steps while ZFC+notCH contains a proof that said TM does not halt after N steps. If that were the case and assuming that both are consistent it will be the case that said TM does not in fact halt (period) and that ZFC+notCH uses a model of non-standard arithmetic in its proof. You mention the possibility of a wrong proof, but that is mixing up the notion of proof and truth which are not the same things. The proofs in ZFC+notCH and ZFC+CH are both correct since a proof is nothing more than a syntactic structure that adheres to certain rules. It's that ZFC+notCH is using a model of natural numbers that is not what most people normally consider to be a natural number, it's using a model of natural numbers that admits for the possibility of incredibly large numbers that are larger than any ordinary/standard natural number. In effect ZFC+CH would contain a proof that after some unimaginably large number of steps the Turing machine halts whereas ZFC+notCH does not allow for the existence of numbers that large. So the main concept here is that two formal systems may have different notions of what a natural number is. We humans share some idea of what a natural number is supposed to be and we call those the standard natural numbers but the problem is that there is no formal way to precisely pin down those numbers without also allowing for the possibility of bizarre non-standard natural numbers as well. In this hypothetical case we would conclude that ZFC+notCH comes closer to modelling what we consider the actual natural numbers compared to ZFC+CH, but nevertheless it's impossible for any first order formal system to fully specify the natural numbers and only the natural numbers.