[raincole]

> I’m pretty sure you and the other commenter have this mixed up.

We really don't.

> that BB(748) is independent of ZFC

> there are different models that have different values of BB(748)

> ZFC is insufficient to determine the value of BB(748)

These three statements are equivalent.

f(n)=X is independent of ZFC means there are different models of ZFC that have different values of f(n). It's a very trivial theorem[0]. If you don't like it, I can't convince you otherwise.

> that doesn’t actually change anything

Changing the model will not change how any machine works in our physical, mechanical universe. However, it does change the value of BB(748).

I understand your line of thinking: There is only one mechanical universe, which is the one where we exist. We can build Turing machines in this universe. BB(n) depends on Turning machines. Since there is only one single universe, there is only one single value of BB(n).

It's a perfectly fine mental model for most cases. This was exactly how I thought when the first time I heard about BB(n). But it's not the kind of math than Scott Aaronson et al. are doing.

Bar keeps running in our mechanical universe. But it can also halt in some non-standard number of steps. This weird, absurd-sounding proposition works because non-standard numbers simply don't map to anything in mechanical universe. They're purely abstract objects living in ZFC+~Con(ZFC).

[0]: Given f(n)=X is independent of ZFC. Which means f(n)=X and ~(f(n)=X) are both consistent relative to ZFC. Therefore, if there is any model of ZFC, there is a model M1 that entails ZFC+(f(n)=X), and a model M2 that entails ZFC+~(f(n)=X). The value of f(n) cannot be the same in M1 and M2.

[wat10000]

My argument has nothing to do with the universe. My argument is that there is a single definition of the BB function and its definition does not allow for different values in different circumstances.

What is “a model” here? Can I say that there’s a model ZFC’ which is the same as ZFC except that 107 is considered to be equivalent to 200, and therefore BB(4) in ZFC’ is actually 200? Or can I say that ZFC’’ says integers only go up to 100 and therefore BB(4) is 100 in that model? Or is it something more restricted than that?

[raincole]

> Or can I say that ZFC’’ says integers only go up to 100 and therefore BB(4) is 100 in that model?

You'd be defining a new axiomatic system here, not just a model of ZFC. I don't know how we're going to formalize Turning machine in this system, but if we managed to do it, the value of BB(4) is likely to be indeed 100, at least for some models of this new system.

Roughly speaking, a model of ZFC is a set and a binary relationship over the set, whose members all satisfy every axiom of ZFC. Obviously this super simplified definition does a crazy amount of handwaving.

But we don't need to accept or understand the idea of model. What we need to accept is this simple idea:

An axiomatic system can be consistent, but wrong.

For example, if ZFC is consistent, then T = ZFC+~Con(ZFC) would be consistent as well. But this T is wrong, as it believes ZFC is inconsistent.

Similarly, if ZFC is indeed consistent, then T is wrong about which Turing machines halt. Therefore it would have a wrong value of BB(748) (and many other BB(n)).

However, since ZFC can't prove its own consistency, it can't prove that value is wrong. That's why there are different values of BB(748). Those values are not necessarily equally correct, it's just that ZFC isn't strong enough to prove which one is wrong.

Models, nonstandard natural numbers, etc... are more or less technical details (so mathematicians can avoid scary terms like 'wrong'.)

[edanm]

> An axiomatic system can be consistent, but wrong.

But then its unsound, isn't it? Isn't our background assumption that ZFC is consistent and sound? It can't prove its own consistency, but we are assuming that under standard models, it is sound.

> For example, if ZFC is consistent, then T = ZFC+~Con(ZFC) would be consistent as well.

It would be consistent if ZFC didn't also prove ZFC+Con(ZFC), but then it would indeed be unsound.

> Similarly, if ZFC is indeed consistent, then T is wrong about which Turing machines halt. Therefore it would have a wrong value of BB(748) (and many other BB(n)).

No, if it's sound, it just doesn't have a proof of the form "BB(748)=K" for any K.

> However, since ZFC can't prove its own consistency, it can't prove that value is wrong. That's why there are different values of BB(748). Those values are not necessarily equally correct, it's just that ZFC isn't strong enough to prove which one is wrong.

No, ZFC is just not strong enough to prove any of these.

[wat10000]

Am I understanding you correctly that there’s is one specific finite integer which equals BB(748), but that some models of ZFC will say it’s a different one, and it’s just not correct?

And since we can find a four-state Turing machine that runs for more than 100 steps before halting, ZFC’’ is just not correct when it says that BB(4) = 100, but we still say that 100 is the value in that model?

[Kranar]

In all models where BB(748) = F and F is actually finite, then F will be the same in all such models. There can't be two models that disagree about the value of F for some actual natural number. It's only in models where BB(748) = Q where Q != F then Q is necessarily not actually finite and hence not an actual natural number.

From within those models Q satisfies all the properties of being a natural number but it's not actually a natural number. Q is some successor of 0, you can add 1 to Q to get another distinct mathematical object, there is some predecessor to Q called P so that P + 1 = Q, etc etc... Q satisfies all the properties within ZFC of being a natural number but it isn't an actual natural number.

Furthermore if ZFC is consistent then it's impossible for any model of ZFC to have BB(4) = 100. ZFC is sufficiently powerful to prove that BB(4) != 100, it is not sufficiently powerful enough to prove that BB(748) = F for some actual natural number F.

[wat10000]

I think this is where I get stuck (or it falls apart). The definition of BB requires it to equal an actual natural number. If you have a model where BB(748) = Q not an actual natural number, then what you have isn’t actually BB, but some other function.

[Kranar]

The issue is that it's impossible to formally and uniquely define the actual natural numbers, and hence it's impossible to require as part of the formal definition of some mathematical object like BB(n) to equal an actual natural number.

Yes, between you and me we know that BB(n) needs to be a natural number, but we have no way to formally and uniquely define what natural numbers are. The best we can do is come up with a formal definition of natural numbers that includes the actual natural numbers but will also include other number systems that contain mathematical objects that are infinitely big and hence are not actual natural numbers. Hence our formal definition of natural numbers will not uniquely define a single set of numbers {0, 1, 2, 3, ...}, there will be other sets of numbers such as {0, 1, 2, 3, ..., Q - 1, Q, Q + 1, ...} for some infinitely large object Q that satisfy the formal definition of natural numbers. Between you and me, we both know Q isn't an actual natural number, but what we don't know is what formal rule we need to add to our formal definition of natural numbers in order to get rid of Q. In fact, it's worse than that; we know that even if we add a rule that gets rid of Q, there will always be some other number system {0, 1, 2, 3, ..., Q* - 1, Q*, Q* + 1, ...} to take its place. No formal definition can ever uniquely define the natural numbers (unless that formal system is inconsistent).

It's also true that a model where BB(748) = Q is not the actual BB, it's some other function. The problem is that this model satisfies all of the rules of ZFC and all of the properties that ZFC says natural numbers must satisfy and hence it satisfies the formal definition of BB even though it isn't the actual BB. Remember it is impossible for the formal definition of BB to include the property that BB(n) = an actual natural number, because there is no formal definition that uniquely singles out what the actual natural numbers are. Since there exists one such model that satisfies all of the rules about BB but isn't actually the real BB then we can't use ZFC to formally prove what the value of BB(748) actually is.

What we can do is add new rules to ZFC get rid of this model, but that will only push the issue down to BB(749) or BB(750) or maybe if pick a really powerful rule we push the issue down to BB(800)... but the point stands that adding new rules only pushes the problem further down the road, it never eliminates the problem entirely.