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

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