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!
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:
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.
Let me offer a counterpoint to François's informative answer and explain how one also can look upon the nonstandard ∈ relation on pseudo finite sets as very rich indeed.
I claim that every countable model of set theory, including every countable model of full ZFC and every countable model of ZFC + large cardinals or whatever kind of countable model of set theory you may have, exists as a substructure of your ultrapower, the nonstandard finite sets HF' = HFω/U. Thus, even though the model HF' thinks everything is finite, there are substructures of HF' that exhibit full ZFC with large cardinals and whatnot. For example, one can find substructures with CH or with ¬CH and so on.
To see this, suppose that M = { an | n ∈ ω } is a set with a binary relation E satisfying that there are no finite cycles for E in M, a consequence of the Foundation Axiom. Define functions fn:ω to HF so that for each k, the structure ⟨ { an | n ≤ k }, E ⟩ is isomorphic to the structure ⟨ { fn(k) | n ≤ k }, ∈ ⟩. For any finite set and acyclic relation, we can always find HF sets so as to copy that finite structure, so such fn exist. What this means is that the map an mapsto [f]U will be an isomorphism of ⟨ M, E ⟩ to its image in HF'. Thus, ⟨ M, E ⟩ is a substructure of HF', as desired.
(More generally, HF' is exhibiting a kind of universal property for countable acylclic directed graphs, and models of set theory are merely instances of this.)
The argument boils down, I suppose, to a kind of saturation property.
