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