I should finish reading the linked article. But I have a quick initial question. Proofs in ZFC can be enumerated by a machine. In theory, we could devise a mac

I should finish reading the linked article. But I have a quick initial question. Proofs in ZFC can be enumerated by a machine. In theory, we could devise a machine that (1) will certainly eventually halt iff ZFC is inconsistent (proves two contradictory statements), or (2) will never halt iff ZFC is consistent. (Caveats: naturally, if ZFC is consistent, we'll never learn whether we should just keep waiting for the machine to find a contradiction. And our machine will require unbounded storage space.) Can we build a corresponding device that would have different behaviors depending on whether the continuum hypothesis is "true" (whatever that means)? I suppose the computational model would be Turing machine as above.