[dullcrisp]

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.

[l33t7332273]

It is not circular. Such a Turing machine clearly exists.

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.

[GolDDranks]

You "clearly" is not so clear.

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?

[GolDDranks]

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.

[l33t7332273]

I agree that the problem is identifying the machine, not its existence.

[dullcrisp]

Oh dear.

[l33t7332273]

Excuse me?

[dullcrisp]

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.

[l33t7332273]

I’m saying that it doesn’t matter if you know if ZFC is consistent; I have proven there exists a TM that halts iff it is.