[Kranar]

In first order logic this is correct, "finite" is not uniquely defined. Usually finite is defined in terms of natural numbers, but since natural numbers are not uniquely defined then it follows that finite is also not uniquely defined. Every model has its own interpretation of what it means to be finite, and in the model {0, 1, 2, ..., Q - 1, Q, Q + 1, ...}, Q is finite relative to that model.

In first order logic it's impossible to uniquely define any property that would also uniquely define the natural numbers.

[wat10000]

From a sibling comment, it seems that using second-order logic resolves this. I'm comfortable saying that if you want to stick to first-order logic then you can say that BB(748) has different values depending on the model in some sense, but that the "real" BB function is defined using what we normally think of as the counting numbers as you'd define with second-order logic, and that's the value that's actually correct.

[Kranar]

No second order logic does not resolve this, it actually makes the situation significantly worse since there is no effective proof system in second order logic. Second order logic is studied for its philosophical properties, as a way to understand the limits of logic and the relationship between syntax and semantics, but it's not used for the study of formal mathematics since it lacks an effective proof system.

What second order logic does let you do is deal with only one single model, called the categorical model. So instead of having a theory that has a whole bunch of different models including the actual natural numbers along with undesirable models that contain infinitely large values... you can force your theory to have one single model, no more "It's true in this model, but it's false in that other nonstandard model that's getting in the way." So yes in a particular theory of second order logic BB(748) has one single value because there is only one single model.

So problem solved right? Not even close... because that one single categorical model being used to represent the natural numbers may not be the actual natural numbers, the intended natural numbers where every number is actually finite. Having one single categorical model does not imply working with the actual model you intended to work with. Depending on your choice of second order theory you may be operating within a theory where the single categorical model is indeed unbeknownst to you {0, 1, 2, 3, ..., Q - 1, Q, Q + 1, ...} and hence BB(748) is equal to Q and you'll have no way of knowing this before hand since you lack an effective proof system.

[wat10000]

That sounds to me like "your model might not be what you want it to be and it might define an infinite value for BB(748)," not "BB(748) has different values depending on the model."

[Kranar]

Ultimately, I am addressing the original point that was made:

>I think the more correct statement is that there are different models of ZFC in which BB(748) are different numbers.

You asked how this was possible and that's the specific question that I am addressing. As I mentioned elsewhere, to fully appreciate this answer requires parsing some very subtle and nuanced details that simply can not be glossed over or dismissed, if you genuinely want to know how it's possible that ZFC can be consistent even though different models give different values of BB(748).

If you want to argue something else, about what model is correct or what model is incorrect, that's a perfectly fine argument to have but it's more in the realm of philosophy than it is in the realm of formal mathematics.

[red75prime]

BB(748) has a single value. It is a finite number of steps (N) of some specific Turing machine. ZFC can't prove neither BB(748)=N, nor ~(BB(748)=N). But BB(748)=N is true and ~(BB(748)=N) is false anyway. The end.