Question

ZFCfin (ZFC without the axiom of infinity, plus its negation) is biinterpretable with Peano Arithmetic.

Each countable model of PA has what is known as its "standard system": the collection of sets of standard natural numbers which can be coded in that system. Usually the coding is via prime exponentiation: $n$ is in the set coded by $c$ if the $n^{th}$ standard prime divides $c$. The standard system of the standard model has only finite sets of naturals in it; all models with infinite sets in their standard system are nonstandard models.

Nonstandard models of ZFCfin (those not isomorphic to HF) contain "externally infinite" sets; elements of the model for which the number of elements standing in the model's member-of relation to them is greater than any finite number.

Are these "externally infinite" sets of a nonstandard model of ZFCfin somehow connected to the standard system of a nonstandard model of HF?

I ask because I'm starting to work through the literature on nonstandard models of PA and I'm finding it much easier to think of the nonstandard numbers as externally-infinite sets of ZFCfin. I'm wondering how far astray that intuition is likely to lead me.

Edit: I should add that I'm aware the nonstandard sets of ZFCfin are frequently $\epsilon$-illfounded. I still find them easier to think of than infinite numbers (frankly I always thought it strange to rule out such sets in the first place).

Answer 1

Yes, there is a perfect agreement between the standard system of the nonstandard model of ZFCfin, such as a nonstandard version of HF, and the standard system of its corresponding model of PA. The standard systems are identical.

That is, because of the mutual interpretability, from any model of PA we may form a model of ZFCfin and vice versa, and these two models have the same standard system.

The standard system of a model of PA, ZFC or ZFCfin consists simply of the standard parts of the sets of natural numbers that exist in the model. This notion is quite robust and is used in many arguments, particularly in the theory of models of arithmetic. In particular, it admits a variety of equivalent characterizations.

For example, for a nonstandard model M of ZFCfin, the standard system of M is equivalently characterized by any of the following methods. We may regard the standard natural numbers $\mathbb{N}$ as a subclass of $M$, since each one is definable in $M$.

For a set A of natural numbers,

• A is in Ssy(M) if and only if there is an object $a\in M$ such that $A=a\cap\mathbb{N}$, that is, $A$ consists of the elements of $\mathbb{N}$ that are in $a$ in $M$.

• A is in Ssy(M) if and only if there is an object $a\in M$ such that $A=a\cap\mathbb{N}$ and $M$ satisfies that $a$ consists of (nonstandard) natural numbers only.

• A is in Ssy(M) if and only if there is a formula $\varphi$ and parameters $\vec a\in M$ such that $n\in A\iff M\models\varphi(n,\vec a)$. Thus, $A$ is the trace on $\mathbb{N}$ of the set defined by $\varphi(\cdot,\vec a)$.

• A is in Ssy(M) if and only if $A\in\text{Ssy}(\mathbb{N}^M)$, where $\mathbb{N}^M$ is the natural numbers of $M$, as defined in set theory. This is provably a model of PA in ZFCfin.

• A is in Ssy(M) if and only if the characteristic function of $A$ is the standard part of a pseudo-finite binary sequence in $M$.

So it doesn't really matter which coding system you use; you always arrive at the same standard system. Indeed, the first characterization above is a kind of coding-free version. You've already done the coding, in a sense, by working with ZFCfin instead of PA, and so now you just have (nonstandard) sets themselves, rather than codes for such sets. Thus, to get the standard part of a set $a$, you just take the standard elements of it.

These characterizations also apply to ZFC models as well. The Standard System of a ZFC model can also be characterized as the set of standard parts of all reals of $M$. One imagines that the reals of a nonstandard model $M$ of ZFC stick up like overgrown grass, and one gets the standard part by riding a big lawnmower, cutting them down to the standard part.