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'.)
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?
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.
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.
In first order logic it's impossible to uniquely define any property that would also uniquely define the natural numbers.
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.
>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.
How could such a definition give rise to such a set with Q in it?
What you described doesn't rule out {0,1,2... Q-1,Q,Q+1...}, because you only defined how to yield new natural number, but not exclude things that are not yielded that way from N (the set of all natural numbers).
Now, our intuition is to add this missing part into our axioms, right?
So instead:
> 0 is a natural number, and if n is a natural number then so is S(n)
We say:
> For any X⊆N, if 0 ∈ X, and for every n ∈ X, S(n) ∈ X, then X=N.
This is a perfect valid axiom. And it does rule out the nonstandard shit: for a set N' that looks like {0,1,2... Q-1,Q,Q+1...}, we can get X = {0,1,2...}, which is a subset of N'. According to this axiom, if N'=N then X=N', but it clearly doesn't because Q∈X while ~(Q∈N'). Therefore, N' isn't N.
However, this axiom is not included in the commonly accepted Peano Arithmetic! The reason is that this uses second-order logic, and Peano Arithmetic is a first-order theory.
The above axiom effectively defines a predicate, f(X), which accepts a set as input and returns whether the set is N. This is second-order logic.
Peano Arithmetic, being first-order logic, doesn't have such predicate. This is why we can't rule out these nonstandard {0,1,2... Q-1,Q,Q+1...}.
When it comes to ZFC, it's more complicate as in ZFC, 'natural numbers' are ordinals of sets. But ZFC is written in first-order logic as well, and it's known that an axiomatic system written in first-order logic will have nonstandard models. Even if you can rule out {0,1,2... Q-1,Q,Q+1...} by defining PA in ZFC in some unusual way or adding new axioms to ZFC, as long as it's still a first-order theory, it will have 0 (if inconsistent) or multiple (if consistent) models[0].
[0]: https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_...
But the other commenter said:
"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."
Is there some subtlety that allows both of these statements to be true, or is this just a contradiction? Was the other commenter implicitly assuming "unless you involve second-order logic"?
>For any X⊆N, if 0 ∈ X, and for every n ∈ X, S(n) ∈ X, then X=N.
You're right that this is a perfectly valid axiom in SOL, but it's not true that it rules out non-standard "shit". What this axiom does is it forces your theory to have a single model, the categorical model. But this axiom does not in anyway pick out the standard model as the categorical model, it doesn't force the categorical model to be the standard model. It's possible that N = {0, 1, 2, ..., Q - 1, Q, Q + 1, ...} in which case the categorical model ends up being nonstandard. This axiom has no way to force N to be intended standard model.
What it means specifically? ZFC+~(BB(748)=N) allows to extend definition of the Turing machine to a non-standard number of steps?
Can "BB(748) is undefined" be a provable theorem in ZFC+~(BB(748)=N) instead?
While we know that ZFC+~(BB(748)=N) is consistent, we don't know whether \exist Q!=N ZFC+(BB(748)=Q) is consistent.
We can come up with some function BB' that admits that, but it's just a different function.
It seems we can't even define a function with standard domain and non-standard codomain while not using literals for non-standard numbers in its definition.
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.
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?