Consider the structure $\langle HF,\epsilon\rangle$ (the hereditarily finite sets with the epsilon-relation). An ultrapower of this structure will have externally-infinite elements -- elements not generated by a finite number of applications of the (definable) singleton+binary-union operations.


Can anybody give me a starting point for literature on the properties of these externally-infinite sets?


Thanks! 



Behavior of externally-infinite elements in ultrapowers of $\langle HF,\epsilon\rangle$
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 $\langle\mathrm{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.


