Note: "Update" at the end of this question hopefully summarizes/clarifies the original language (original text left in place for context).
Philosophical Preface: For the purposes of this question, I am assuming that the notion of "standard $\mathbb{N}$" is not an illusion. In other words, that there is a unique (up to isomorphism) model of $\mathsf{PA}$ which is standard in an "absolute" sense (namely, the numbers we all learned to count with in elementary school, as laid out in the first section of these notes for example). And it is in relation to this "absolutely standard" $\mathbb{N}$ that we can meaningfully speak of whether the $\omega$ of a given set universe is actually standard (i.e. notwithstanding that every universe "thinks" its $\omega$ is standard, when viewed "from the outside" this $\omega$ may or may not be "actually" standard, depending on whether it's order-isomorphic to our "absolutely standard" $\mathbb{N}$). In what follows, this is what I mean when speaking of "standard $\mathbb{N}$" (hopefully this is all relatively conventional and uncontroversial so far?)
Some Background:
At one time, I used to be under the impression that:
- The first-order Peano axioms have many models (both standard $\mathbb{N}$, and also various systems of non-standard natural numbers).
- But Peano axiomatization with second-order induction and "full" second-order semantics ($\mathsf{PA2}$) has a unique (up to isomorphism) model, namely the standard natural numbers (the above-described "absolutely standard" $\mathbb{N}$).
But it now seems to me that second bullet point is probably not quite correct. Instead (as I understand it) any given "domain of discourse" does indeed have a unique (up to isomorphism) model of $\mathsf{PA2}$, but depending on the assumptions you make about the domain you're working in, its model of $\mathsf{PA2}$ may or may not be standard $\mathbb{N}$. For example, if you assume you are working in a $\mathsf{ZFC}$ universe with non-standard $\omega$ (and successor function defined in the usual way as $S(x) = x \cup \{x\}$), then your unique model of $\mathsf{PA2}$ is the $\omega$ of this universe, which by hypothesis is not order-isomorphic to standard $\mathbb{N}$.
The Actual Question:
If one's goal is some formalism whose only possible model (regardless of any additional assumptions about the "domain of discourse") is (up to isomorphism) the above-described "absolutely standard" $\mathbb{N}$, then (if my above-described understanding is correct) $\mathsf{PA2}$ doesn't fully accomplish this goal.
So, is there any formalism (whether an axiomatization in second-order logic, or something else) which does accomplish this goal?
- If you're assuming $\mathsf{ZFC}$ as your foundation, then augmenting $\mathsf{PA2}$ with an additional stipulation that "the $\omega$ of my $\mathsf{ZFC}$ universe is standard" might seem to be a solution. But that's unhelpfully circular, because how do you formalize the "standardness" of $\omega$? That's exactly the problem you're trying to solve in the first place.
Update — A couple additional points:
-
Viewed from the perspective of set-theoretic ($\mathsf{ZFC}$) multiversism, I think my question can be equivalently recast as follows: If I philosophically accept the multiverse, I nonetheless may wish speak of distinctions between one category of universes versus others, in particular to distinguish universes with "standard $\omega$" from others with "non-standard $\omega$". When attempting to articulate this distinction, I certainly have a fairly concrete but somewhat informal concept in mind of what I mean by "standard $\omega$" (see "Philosophical Preface" above). But can this concept of standardness of $\omega$ be formalized? In other words, is there some formal criterion (whether formulated in second-order logic, or some other way) that effectively distinguishes the universes with standard $\omega$ from the other (non-standard $\omega$) universes?
-
The notion of "standardness" of $\mathbb{N}$ becomes, I suppose, somewhat more formal if we think of it as: $X$ is a "standard" natural number iff it equates to any term in first-order logic in which the last symbol is $\mathbf{0}$ and every other symbol is the successor function symbol $\mathbf{S}$ (hence: $\mathbf{0}$, $\mathbf{S0}$, $\mathbf{SS0}$, etc.). However this falls somewhat short of what I have in mind as really "formalizing" standardness. Specifically, it seems like it's kind of "cheating" by using the grammar rules of the language (first-order logic) to inform the semantic meaning of "standardness" in the theory (arithmetic). But maybe this is the best we can do towards formalizing the notion of "standardness" of $\mathbb{N}$?
Best Answer
If we identify "standard $\mathbb{N}$" with the/a theory of true arithmetic, then of course, by incompleteness, the answer is no: being consistent and negation complete, it cannot be 'effective'
One may initially object that this seems too tied to (a) specific (choice of) formalisms; Boolos, et al (2007), for example, may perhaps give such an impression
But when one remembers that one can do a reasonable amount of set theory inside finite-type arithmetic, and type theory inside higher-order logic, and higher-order logic inside second-order logic (Hintikka, Montague) $-$ plus Church-Turing, of course $-$, then it seems pretty much safe to answer your request
for an 'absolute pinning' or 'absolute description' of "(absolutely) standard $\mathbb{N}$" with "No"