Hereditarily countable sets in Antifounded ZF

A set $$x$$ is hereditarily countable when every membership-descendant of $$x$$ (including $$x$$ itself) is countable.

In this paper, Jech proved in ZF that the class of all hereditarily countable sets is a set. (See here and here and here for developments of this result.)

Can this be shown in the variant of ZF that uses Aczel's Antifoundation instead of Foundation?

Another question that I think is equivalent: does ZF prove the existence of a final coalgebra for the countable powerset functor?

• Which antifoundation axiom do you mean, Aczel's? (There are others.) Commented Jul 6 at 22:13
• ZFA is also used for atoms. I learnt "Anti-ZF" from Thomas Forster. Commented Jul 6 at 22:21
• @JoelDavidHamkins Ah yes, ZFC + a proper class of urelements (unlimited atoms :P). Commented Jul 7 at 0:09
• OK, in light of this, I am going back on my previous concession. Since I prefer to call them atoms, not urelements, I shall use henceforth ZFA for set theory with atoms. If you want Aczel's theory, you have to write AFA for the axiom and ZFAFA or something like that for the theory. With apologies to Forster, I find Anti-ZF to be a nonstarter, since it doesn't even reference wellfounded issues and expresses unnecessary negativity toward ZF. Commented Jul 7 at 0:15
• @JoelDavidHamkins I personally would save ZFC + UA for a hypothesis that isn’t just a proper class of inaccessibles! Commented Jul 7 at 13:43

Update. This answer does not answer the question that was asked, since Jech is using what had seemed to me as an idiosyncratic definition of hereditary countable. But upon reflection, I find his definition completely natural in a context without AC. Namely, he defines that a set is hereditary countable when it is countable and every element of the transitive closure is countable. In short, the set itself and every set appearing hereditarily in it is countable. (This is not equivalent, even in ZF as Jech proves, to saying that the transitive closure of the set is countable.)

If a negative answer to the question is possible, I suspect it will arise by finding a model of ZF in which AC fails badly and using it to interpret a model of ZFA where there is proper class of inequivalent accessible pointed graphs such that every node has only countably many children. I have wondered whether Gitik's model, in which every infinite limit ordinal has cofinality $$\omega$$, will be helpful for this.

In ZFA every set is determined by the underlying accessible pointed graph, the $$\in$$ relation on the transitive closure, and the AFA axiom asserts that isomorphic graphs will give rise to the same set.

Thus, the hereditarily countable sets will arise from the countable graphs, which is a set by the argument you mentioned. And so in ZFA the hereditarily countable sets will form a set.

It is interesting to note that, being countable, the underlying graphs of any hereditarily countable set can be realized within the well-founded part of the universe, even if the set that they name is not well-founded. So the hereditarily countable sets in ZFA arise from a functional image of the well-founded hereditarily countable sets, namely, the graph relations on $$\omega$$.

This argument doesn't work at all in the Boffa antifoundation theory, which has a proper class of distinct Quine atoms, all of which are countable. However, even in that theory, there are up to isomorphism only a set of hereditarily countable sets, since they are determined up to isomorphism by the underlying graph relation.

• The pointed graph representing a hereditarily countable set x is given by the transitive closure of {x}, which can't be proved countable. Commented Jul 6 at 22:33
• ? I take it that a set is hereditarily countable means that its transitive closure is countable. And this implies $\text{TC}(\{x\})$ also is countable, since there is only one more point. Commented Jul 6 at 22:36
• Oh this is not what I meant by hereditarily countable. I will have to edit the question. Commented Jul 6 at 22:37
• See the first sentence of Jech's paper. I am using his definition. Commented Jul 6 at 22:38
• Ultimately, this is a non-AC question rather than a anti-foundation question, since my answer works very well in ZFCA. What you need to do for a counterexample, if this is possible, is cook up a very badly behaved model of ZF in which AC fails, and use it interpret a similarly bad model of ZFA. Commented Jul 6 at 22:51