set theory - Behavior of externally-infinite elements in ultrapowers of $langle HF,epsilonrangle$

As I pointed out in the comments, $(HF,{in})$ is biinterpretable with $mathbb{N}$, which means that the corresponding ultrapowers are biinterpretable too. So you will find all you need in the vast literature on nonstandard arithmetic.

A nice interpretation of $(HF,{in})$ in $mathbb{N}$ is given by defining $m in n$ if the $m$-th binary digit of $n$ is $1$. For example, here are the first few coded sets:

• $0$ codes $varnothing$


• $1 = 2^0$ codes ${varnothing}$


• $2 = 2^1$ codes ${{varnothing}}$


• $3 = 2^0 + 2^1$ codes ${varnothing,{varnothing}}$

You can similarly interpret the ultrapower $HF^omega/mathcal{U}$ in the ultrapower $mathbb{N}^{omega}/mathcal{U}$. If $bar{m},bar{n} in mathbb{N}^omega$, the $bar{m}$-th binary digit of $bar{n}$ is first interpreted term-by-term giving a sequence $bar{b} in {0,1}^omega$ where each $b_i$ is the $m_i$-th binary digit of $n_i$. In $mathbb{N}^omega/mathcal{U}$, $bar{b}$ is evaluated as either $0$ or $1$, depending on which value occurs $mathcal{U}$-often. This value tells you whether $bar{m} in bar{n}$ according to the above interpretation.

Of course, you can simply compute things directly. Given sequences $bar{x},bar{y} in HF^omega$, we have $bar{x} in bar{y}$ in the ultrapower $HF^omega/mathcal{U}$ if and only if ${i : x_i in y_i } in mathcal{U}$. This gives exactly the same structure as interpreting sets in $mathbb{N}^omega/mathcal{U}$ as described above.

---

It just occurred to me that you may be looking for a more set-theoretic description of the nonstandard elements of $HF^omega/mathcal{U}$.

The wellfounded part of $HF^omega/mathcal{U}$ is precisely $HF$ and no more. A sequence $bar{x} in HF^omega$ will represent a wellfounded set in $HF^omega/mathcal{U}$ if and only if it has bounded rank mod $mathcal{U}$, i.e. ${i : mathrm{rk}(x_i) < n} in mathcal{U}$ for some $n < omega$, in which case it will be constant mod $mathcal{U}$ since there are only finitely many sets of rank less than $n$. If this is not the case, then $langlemathrm{rk}(x_i)rangle$ evaluates to a nonstandard ordinal $N$ in $HF^omega/mathcal{U}$. This means that in $HF^omega/mathcal{U}$, we can (externally) find an infinite descending ${in}$-chain starting with the evaluation of $bar{x}$. So it is impossible to describe the evaluation of $bar{x}$ as a real set.

Without peering into the depths of the nonstandard ${in}$ relation, there is not much to elements of $HF^{omega}/mathcal{U}$. Every element of $HF^omega/mathcal{U}$ has a bijection with a (possibly nonstandard) ordinal, so it looks exactly like an internal initial segment of the nonstandard ordinals.