No, the machine halts iff ZFC is inconsistent -- as you correctly stated up top. Somewhere along the way you got this reversed, looks like. There's the problem.
The argument goes the same even though I misspoke here. If the machine {halts, runs forever} then ZFC is consistent. But this is a contradiction; so ZFC must be inconsistent. Tada, I have an inconsistency proof!
That was the implied next step which made me think my logic was clearly incorrect (which, it was).
If you see it halt, ZFC is inconsistent. If you never see it halt, you CAN'T conclude anything.
But we could already do that under Gödel incompleteness, so there's nothing unusual there!
If you write down random proofs on paper and find a correct proof that leads to contradiction, you've proved ZFC inconsistent, without using BB. If you keep trying forever and never find one, you'll never be able to conclude anything at any point, just like with watching the machine run
But if you run it for BB(754) many steps, you will know.
And you can't prove that it'll run forever without seeing it go past BB(754) and still keep going
BB(754) is X if ZFC is consistent, Y otherwise
Since you can't prove that ZFC is consistent (only disprove), you can't know BB(754), which is the thing we were trying to use to determine whether ZFC is consistent in the first place!
The definition doesn't make it obvious, but this is just the same as plain Gödel incompleteness, we can't get any extra info about ZFC even in principle (unless we happen to see it halt, by chance)
It is crucial at this types of results, when you search for a proof.
There are a lot of things true, better make a table of it, instead of a wall of text:
- If you observe the machine halting, ZFC is inconsistent.
- If the machine hasn't halted yet, you don't know if ZFC is consistent or not.
- If ZFC is inconsistent, the machine will eventually halt. (You have an upper bound for this, given a contradiction.)
- If ZFC is consistent, then the machine won't halt ever.
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.
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.
Eh, this doesn’t really matter. That busy beaver number is just an integer, so there is some TM that does exactly as I have described.
Thus, there I have proved that there is a turing machine that halts iff ZFC is consistent.
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.
What we’ve seen is that there plainly exists a Turing machine which halts iff ZFC is consistent.
All of the other window dressing you’ve added hasn’t changed that simple fact.
I agree that finding busy beaver numbers is the issue. I do not agree that the existence of a TM that halts iff ZFC is consistent is hard.
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?