4
$\begingroup$

It is known that: $ ``\forall x \exists H_x"$, where $H_x$ is defined as the set of all sets hereditarily subnumerous to $x$, is a theorem of $\text{ZF}$. The formal definition of $H_x$ is:

$$H_x=\{y| \forall z \in TC(\{y\}) (\exists f (f:z \to x \wedge f \text{ is injective}))\}$$, where $TC(k)$ stands for the "Transitive closure of($k$)" defined in the standard manner as the minimal transitive superset of $k$.

Question: is $``\forall x \exists H_x"$ a thorem of "$\text{ZF-Regularity + Aczel's anti-foundation axiom}$"?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ It would be very advisable, if you want more people to understand your questions, that you use actually standard terminology, and not things you expect everyone to understand. What is "subnumerous"? What is "hereditarily subnumerous"? Since you're familiar with the notation $H_x$, surely you are familiar with the more formal definition of "the transitive closure of $y$ has a strictly smaller cardinality than $x$". No? Then why invent new terms? We have too many already. $\endgroup$
    – Asaf Karagila ♦
    Commented Jun 29, 2018 at 19:44
  • $\begingroup$ honestly I thought those terminologies are well understood. Anyhow I'll try to edit with some detail. $\endgroup$
    – Zuhair Al-Johar
    Commented Jun 29, 2018 at 19:57

1 Answer 1

Reset to default
8
$\begingroup$

The answer is yes.

The reason is that in AFA, every set is determined by the isomorphism type of the $\in$ relation on its transitive closure. So if a set $y$ hereditarily injects into another set $x$, then the transitive closure of $y$ is determined by a certain graph relation on the nodes coming from the graph of $x$. By suitable applications of the power set axiom and separation, the collection of all such graphs exists as a set, and the sets to which they correspond exists by the replacement axiom. So $H_x$ exists.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .