Read further down in the Wikipedia article, and you will see the axioms for first order PA. There is no predicate 'is a number'.
/
Regarding your notion about improper sets relative to PA as personal visualization, I didn't ignore it - you even quoted me remarking on it. I said I don't opine as to what does or does not make sense in your mind. But I said your notion makes no sense to me. And I would add that I think it does muddle discussion. But I didn't say you shouldn't think it.
ZF-infinity means ZF plus the negation of the axiom of infinity by default. — fishfry
Some people use it that way. And I have seen it lead to misunderstandings as casual readers fail to note that, in this context, we need the negation of the axiom of infinity and not just leaving out the axiom of infinity.
it's all the finite sets — fishfry
No, not all the finite sets. Only the hereditarily finite sets.
You just explained to me that HF are all the finite sets in ZF — fishfry
I defined 'HF' to stand for the theory (ZF~Inf)+~Inf.
But now I realize that writers often use 'HF' to stand for a class. So my choice to use 'HF' as the abbreviation was not good. From now on, I won't use it to stand for the theory (ZF~Inf)+~Inf. Instead I'll use:
TF = (ZF~Inf)+~Inf
since N is not a definable symbol in PA, I can't say "N is a proper class" because I have no idea what N is. Is that right? — fishfry
To be more precise, whatever symbol 's' we pick, TF does not support a definition:
s = {x | x is a natural number}
because the theory does not prove that there is a such an object.
your definition [of 'proper class' makes perfect sense. I do wonder why I haven't seen it. — fishfry
In class theory, it is well understood that a proper class is a class that is not a member of any class. All I'm doing is pointing out that we can also say that in set theory and conclude in set theory that there are no proper classes. It might be annoying, because it's not a very useful series of formulations. But it its technically correct, and I find that it sharpens the picture. Especially it goes against a common misconception that we can define a predicate symbol only to stand for a relation (sets are 1-place relations) that has members. No, we can always define an empty predicate. For example:
dfn: Jx <-> (x is odd and x is even)
is allowable, even if rather pointless.
That's not a model of PA. w+2 has no successor. — fishfry
Was a typo of omission; I meant {w, w+1, w+2 ...}
"is a natural number" must be a predicate [...] Therefore I can form the COLLECTION, or "predicate satisfier," or as it's officially called the extension of the predicate, N = {x | x is a natural number}. N is a class and it's not a set. So it's a proper class. — fishfry
Yes, we can have a predicate 'is a natural number' in TF. And upon an interpretation of the language, it has an extension (a subset of the universe for the model) and that extension is a set, not a proper class.