Recall that W. Ackermann verified what in modern terms we call the bi-interpretability of and , where the latter is (first-order) Peano arithmetic, and the former is finite set theory, the result of replacing in the axiom of infinity with its negation (and with foundation formulated as the schema of -induction). The reference is
I have written about this before. Briefly, one exhibits (definable) translations between the collection of hereditarily finite sets and and verifies that the translation extends to a definable translation of the relations, functions and constants of the language of each structure in a way that verifies that holds in the translation of and verifies that holds in the translation of . Recall that consists of those sets whose transitive closure is finite, that is, is finite, and all its elements are finite, and all the elements of its elements are finite, and so on. Using foundation, one easily verifies that , that is, it is the collection of sets resulting from iterating the power-set operation (any finite number of times) starting from the empty set.
In the direction relevant here, one defines a map by
One easily verifies, using induction on the set-theoretic rank of the sets involved, that this recursive definition makes sense and is injective (and, indeed, bijective).
Of course this argument uses foundation. In the D’Agostino-Policriti-Omodeo-Tomescu paper they consider instead the theory resulting from replacing foundation with the anti-foundation axiom, and proceed to describe a suitable replacement for that injects (codes) into the real numbers. They do quite a bit more in the paper but, for the coding itself, I highly recommend the nice review by Randall Holmes in MathSciNet, linked to above.
The anti-foundation axiom became known thanks to the work of Peter Aczel, and it is his formulation that I recall below, although it was originally introduced in work of Forti and Honsell from 1983, where they call it . Aczel’s presentation appears in the excellent book
MR0940014 (89j:03039)
Peter Aczel. Non-well-founded sets. With a foreword by Jon Barwise.
CSLI Lecture Notes, 14. Stanford University, Center for the Study of Language and Information, Stanford, CA, 1988. xx+137 pp.
ISBN: 0-937073-22-9.
Given a binary relation , its field is the union of its domain and codomain. A decoration of is a function satisfying
for all . When is and the sets in question are well-founded, the only decoration is the identity. Similarly, any well-founded relation admits a unique decoration. Define as the statement that any binary (whether well-founded or not) admits a unique decoration.
In with foundation replaced with one can prove the existence of many non-well-founded sets. One of the appealing aspects of is that the resulting univere is actually quite structured: Other anti-foundation axioms allow the existence of infinitely many Quine atoms, sets such that , for instance. Under , there is exactly one such , usually called . The axiom is sometimes described as saying that it provides solutions to many “equations” among sets. For instance, consider the system of equations and . Under the system has as its unique solution. Note that assuming , is in , as are many other non-well-founded sets.
Here is the open question from the D’Agostino-Policriti-Omodeo-Tomescu paper: Work in set theory with instead of foundation. Is there a unique, injective, function satisfying
for all ?
Note that there is a unique such on the well-founded hereditarily finite sets, and it is in fact injective. In general, existence, uniqueness and injectivity of appear to be open. The claim that there is such a function is a statement about solutions of certain equations on the reals, and the claim that is unique requires moreover uniqueness of such solutions. The expectation is that is transcendental for all non-well-founded hereditarily finite but, even assuming this, the injectivity of seems to require additional work.
For example, consider . The function must satisfy
and, indeed is the unique solution of the equation .
I would be curious to hear of any progress regarding this problem.
It seems to me that it would still be countable. So in fact this map should probably be into some countable subfield of the reals, and perhaps knowing a bit more as to what this subfield should be, and how well this map plays with the algebraic structure could help zero in on the possible proof of the injectivity of $h$.
Hi Asaf. Yes, it is still countable. (Randall’s review includes a quick sketch of why this is so, but it is easy to see in any case.) I agree one should understand the structure of the subfield better if any progress is to be made.
Clearly one has to understand finite accessible pointed graphs, too. One naive thought that came to mind whilst on the bus was to prove this by induction on the size of the transitive closure, or maybe it’s possible to argue directly for transitive sets, then prove by induction on “how many steps needed to get the transitive closure”.
Neither approaches seemed particularly viable, at least after some rudimentary consideration. I’m only listing them here in case someone wants to pick up these ideas. In that case, I’d be very interesting to hear if they work out.
A kind of library 
What is the cardinality of
under 
?
It seems to me that it would still be countable. So in fact this map should probably be into some countable subfield of the reals, and perhaps knowing a bit more as to what this subfield should be, and how well this map plays with the algebraic structure could help zero in on the possible proof of the injectivity of $h$.
Hi Asaf. Yes, it is still countable. (Randall’s review includes a quick sketch of why this is so, but it is easy to see in any case.) I agree one should understand the structure of the subfield better if any progress is to be made.
Clearly one has to understand finite accessible pointed graphs, too. One naive thought that came to mind whilst on the bus was to prove this by induction on the size of the transitive closure, or maybe it’s possible to argue directly for transitive sets, then prove by induction on “how many steps needed to get the transitive closure”.
Neither approaches seemed particularly viable, at least after some rudimentary consideration. I’m only listing them here in case someone wants to pick up these ideas. In that case, I’d be very interesting to hear if they work out.