I don’t think that’s it. I think it’s easy to take such a machine and make a new one that halts iff ZFC is consistent.
Call the machine that halts iff ZFC is inconsistent A. Now consider the machine which computes the following algorithm:
Run A BB(754) times. If A halts, then run forever, else halt.
If A halts then our machine runs forever, and vice versa. Thus, our machine halts when ZFC is consistent and our machine runs forever when A halts, so ZFC is consistent iff our machine halts.
“Halts” doesn’t seem like a real word after writing that.
How do you make the new machine compute BB(754)? BB is the canonical example of an uncomputable function, precisely because you can decide the halting problem if you can compute it (or any upper bound). Granted, BB may be computed for specific arguments, as OP mentions for 1–4, but the existence of the ZFC-dependent machine is, at least to me, a very good argument that the boundary of what's possible is much lower.
Oh, sure. I was just pointing out that the hardness is in determining the busy beaver number and that it didn’t matter if your algorithm halts iff ZFC is consistent or if it’s an algorithm that halts iff ZFC is inconsistent.
No, if you had an algorithm that (you could prove) halts iff ZFC is consistent, then if that algorithm halts, you’ll have a proof that ZFC is consistent, which isn’t possible. Thus, the existence of such an algorithm would be a contradiction that proves the inconsistency of ZFC.
The problem with your construction is that it relies on knowing the value of BB(754), which is impossible to know so long as ZFC is consistent, since its value is dependent on the consistency of ZFC.
Conversely, if ZFC is inconsistent, then there exists a (finite) proof of this fact, so the opposite case isn’t a problem.
Essentially it’s like saying define X to be the length of the shortest proof of the inconsistency of ZFC, if one exists. If I could prove any upper bound on X, I could prove the consistency of ZFC, which, according to Gödel’s incompleteness theorem, would itself prove the inconsistency of ZFC.
The intuition is that a monkey typing randomly on a typewriter can come up with texts which either are or aren't valid proofs of ZFC or not, and each one which is a valid proof either is a proof of a contradiction or not. To check either of these things is mechanical. If ZFC is inconsistent, eventually the monkey should hit on the inconsistency.
It’s an unknown integer, whose value depends on the consistency of ZFC. Let me show you why this is circular.
I can define another integer N which is 1 if there exists a proof of the inconsistency of ZFC and 0 if there doesn’t (note that BB(754) already encodes this information). Then I can define a program that determines the consistency of ZFC thusly: if N=1, I define the program to immediately return false. If N=0, I define the program to immediately return true. Thus, there exists a program that can determine the consistency of ZFC, it’s one of the two programs I’ve defined.
The fact that there exists a program that returns the consistency of ZFC isn’t in question. The trick is proving that a particular program does so. Or if you like, proving that there exists a program along with a proof that it does so. What you’ve defined is an oracle: it depends on already knowing the answer to what you’re asking so it doesn’t have to compute it.
BB(754) is an uncomputable number. It's independent of ZFC, so an enumeration of all consequences of axioms of ZFC doesn't contain it. How is that supposed TM of yours is supposed to know whether it has run BB(754) steps or not?
Oh, but other slightly bigger TMs exist – lets say in class TM(860) for the sake of an example – that might halt with after a more steps than BB(754). This _sounds_ intuitive. But: how do you prove that? It might be that all TM(860)s either halt within BB(754) steps or then run forever. There indeed might be some that halt in finite steps after BB(754), but that is not guaranteed! You need to prove it. But with what?
Oops, never mind, there exists a simple construction that you can perform to each TM(754) that clearly extends BB(754) a finite amount. Maybe you are corrent that such Turing machine exists. But seems that identifying it isn't possible in ZCF.
I’m saying that all you’ve proven is that if you know a priori whether ZFC is consistent, you can construct a Turing machine that returns this value. If you consider that to be window dressing I don’t know what else I can tell you.
Call the machine that halts iff ZFC is inconsistent A. Now consider the machine which computes the following algorithm:
Run A BB(754) times. If A halts, then run forever, else halt.
If A halts then our machine runs forever, and vice versa. Thus, our machine halts when ZFC is consistent and our machine runs forever when A halts, so ZFC is consistent iff our machine halts.
“Halts” doesn’t seem like a real word after writing that.