3 ms·
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 t
by 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.