[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.

[red75prime]

> a model where BB(748) = Q is not the actual BB, it's some other function

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 where ZFC+(BB(748)=Q) is consistent.

Intuitively I see it as: by adding axiom ~(BB(748)=N), we codify that this formal system isn't powerful enough to describe a Turing machine with 748 states (and probably all the machines with number of states greater than 748).

[red75prime]

It seems to be even easier: BB codomain is a set of standard natural numbers regardless of which model of ZFS we are using. Therefore BB(748)=Q is false for every non-standard natural number Q.

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.

That is ~(BB(748)=ActualValueOfBB748) is false even if it can't be proven in ZFC. In a sense, busy beaver creates its own mathematical reality.

[Scarblac]

If we just use the successor function, so 0 is a natural number, and if n is a natural number then so is S(n). That should be enough to count steps of a halting Turing machine.

How could such a definition give rise to such a set with Q in it?

[raincole]

You're right... with a catch.

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_...

[Kranar]

I think your contribution to this discussion has been very thorough but I need to nitpick some details:

>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.

[wat10000]

"This is a perfect valid axiom. And it does rule out the nonstandard shit"

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"?

[wat10000]

Does that mean that “finite” is not well defined? That would be very odd.

[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.