Incorrect comments on Logical Pinpointing

[Incorrect]

I don’t see how you would define Pn(x) in the language of PA.

Let’s say we used something like this:

Pn(x) iff ((0 + n) = x)

Let’s look at the definition of +, a function symbol that our model is allowed to define:

a + 0 = a
a + S(b) = S(a + b)

“x + 0 = x” should work perfectly fine for nonstandard numbers.

So going back to P(x):

“there exists some n such that ((0 + n) = x)”

for a nonstandard number x, does there exist some number n such that ((0+n) = x)? Yup, the nonstandard number x! Set n=x.

Oh, but when you said nth successor you meant n had to be standard? Well, that’s the whole problem isn’t it!

[TorqueDrifter]

But any nonstandard number is not an nth successor of 0 for any n, even nonstandard n (whatever that would mean). So your rephrasing doesn’t mean the same thing, intuitively—P is, intuitively, “x is reachable from 0 using the successor function”.

Couldn’t you say:

• P0: x = 0

• PS0: x = S0

• PSS0: x = SS0

and so on, defining a set of properties (we can construct these inductively, and so there is no Pn for nonstandard n), and say P(x) is “x satisfies one such property”?

[Incorrect]

An infinite number of axioms like in an axiom schema doesn’t really hurt anything, but you can’t have infinitely long single axioms.

∀x((x = 0) ∨ (x = S0) ∨ (x = SS0) ∨ (x = SSS0) ∨ ...)

is not an option. And neither is the axiom set

P0(x) iff x = 0
PS0(x) iff x = S0
PSS0(x) iff x = SS0
...
∀x(P0(x) ∨ PS0(x) ∨ PS0(x) ∨ PS0(x) ∨ ...)

We could instead try the axioms

P(0, x) iff x = 0
P(S0, x) iff x = S0
P(SS0, x) iff x = SS0
...
∀x(∃n(P(n, x)))

but then again we have the problem of n being a nonstandard number.