Set theory inside arithmetics via the Ackermann yoga

This question reminds me of a magical little-known theorem of Jean Pierre Ressayre that shows that every nonstandard model of $PA$ has a model of $ZF$ as a submodel of its Ackermann intepretation, more specifically:

Theorem. [Ressayre] Suppose $(M, +, \cdot)$ is a nonstandard model of $PA$, and $\in_{Ack}$ is the Ackermann epsilon on $M$, i.e., $a\in_{Ack}b$ iff $\mathcal{M}$ satisfies "the $a$-th digit in the binary expansion of $b$ is 1". Then for every consistent recursive extension $T$ of $ZF$ there is a subset $A$ of $M$ such that $(A,\in_{Ack})$ is a model of $T$.

Proof Outline: By Löwenheim-Skolem, it suffices to consider the case when $M$ is countable. Choose a nonstandard integer $k$ in $M$, and consider the submodel $M_k$ of $(M,\in_{Ack})$ consisting of sets of ordinal rank less than $k$ [as computed within $(M,\in_{Ack})$]. "Usual arguments" show that $(M,\in_{Ack})$ has a Tarskian truth-definition for $M_k$, which in turn implies that $(M_k,\in_{Ack})$ is recursively saturated. Since $M_k$ is also countable, $(M_k,\in_{Ack})$ must be resplendent [which means that it has an expansion to every recursive $\Sigma^1_1$ theory that its elementary diagram is consistent with].

Now add a new unary predicate symbol $A$ to the language ${\in}$ of set theory and consider the (recursive) theory $T^A$ consisting of sentences of the form $\phi^A$, where $\phi \in T$, and $\phi^A$ is obtained by relativizing every quantifier of $\phi$ to $A$. It is not hard to show that $T^A$ is consistent with the the elementary diagram of $(M_k,\in_{Ack})$, so by replendence the desired $A$ can be produced.

[I will be glad to add clarifications]

Ressayre's theorem appears in the following paper:

J. P. Ressayre, Introduction aux modèles récursivement saturés, Séminaire Général de Logique 1983–1984 (Paris, 1983–1984), 53–72, Publ. Math. Univ. Paris VII, 27, Univ. Paris VII, Paris, 1986.

You might want to look into the notion of the standard system of a nonstandard model $M$ of PA. Any nonstandard member $x$ of $M$, determines, via your favorite coding, a subset $X$ of $M$ that is finite in the internal sense of $M$ but may be infinite when seen from outside $M$. Intersecting this $X$ with the standard part $\mathbb N$ of $M$, we get some subset of $\mathbb N$, and the family of all the intersections obtainable in this way, as $x$ varies over $M$, is called the standard system of $M$. With this definition, it's a collection of subsets of $\mathbb N$, but it corresponds, via Ackermann coding, to a collection of subsets of the set $HF$ of hereditarily finite sets (the standard model of ZF minus infinity).