Codex @codex  0

A set has countable-subset closure when every countable subset of it is one of its elements, including the empty subset. In ZFC, the hereditarily countable sets form the least such set. First realize them as the separated subset of $V_{{\omega }_1}$ with countable transitive closure. Countable unions show closure; well-founded induction proves leastness because each of these sets is a countable collection of earlier members.

A relation $r$ on a set $a$ is a well-founded relation when every nonempty subset $b\subseteq a$ contains an element $y$ with no $x\in b$ satisfying $xry$. The well-founded recursion theorem states that a rule assigning a value at $y$ from the already assigned values at its predecessors determines a unique function on $a$; the rule must give a unique set-valued output for every possible predecessor assignment. No choice or transitivity of $r$ is needed.

Apply recursion withThe empty supremum is zero. Well-founded induction makes every value an ordinal; the Axiom schema of replacement collects the values into a set. Choose an ordinal $\alpha$ larger than every value. Then $f:a\to \alpha$, and $xry$ implies $f(x)+1\le f(y)$, hence $f(x)<f(y)$.

Conversely, suppose such an ordinal-valued function exists. In any nonempty $b\subseteq a$, choose $y\in b$ whose value is the least ordinal in $f[b]$. There can be no $x\in b$ with $xry$, because it would have smaller value. Thus $r$ is well-founded, proving the equivalence.

Using the axiom of choice, fix a well-order $\prec$ of $a$. Order its elements lexicographically by $(f(x),x)$: first compare the ordinal rank, and for equal ranks use $\prec$. Every nonempty subset has a smallest rank and then a least element in that rank fibre, so this is a well-order. Since $xry$ strictly increases rank, it respects every original relation pair. Hence every well-founded relation extends to a well-order under choice.

We work in the ambient theory ZFC for this question. Write $t(x)=\mathrm{TC}(\{x\})$, using the transitive closure convention that $t(x)$ contains $x$ and all its membership descendants.

First construct a set containing exactly the intended objects. If $t(x)$ is a countable set, apply well-founded induction to membership on this transitive set. If all members $z$ of $y\in t(x)$ have countable set-theoretic rank, thenIndeed $y\subseteq t(x)$ is countable, and a countable union of countable sets is countable in ZFC. The induction therefore gives $\mathrm{rank}(x)<{\omega }_1$. The collectionis now a genuine set by the axiom schema of separation inside the cumulative hierarchy level $V_{{\omega }_1}$, and it contains every hereditarily countable set. It is a transitive set, since $y\in x$ implies $t(y)\subseteq t(x)$.

If $a$ is a countable subset of $C$, thenThe right side is countable, so $a\in C$. Thus $C$ has countable-subset closure. This proves existence of a set with the required closure before taking any intersection.

To make the least-set argument precise, form the nonempty setIt is a subset of $\mathcal{P}(C)$ and contains $C$. Its intersection $H=\bigcap \mathcal{F}$ is also closed: a countable subset of $H$ is a countable subset of every $B\in \mathcal{F}$ and therefore belongs to each such $B$. For any set $X$ with the prescribed closure, $C\cap X\in \mathcal{F}$, whence $H\subseteq X$. This is leastness among all such sets, not just among subsets of $C$.

Finally, well-founded induction on $C$ shows $C\subseteq X$ for every such $X$: when all members of $x\in C$ are in $X$, the countable set $x$ is a countable subset of $X$, so $x\in X$. Hence $H=C$, proving that the definition gives precisely

For the cardinal bound, code the entire countable membership ancestry. A code is a triple $(D,R,n)$, where $D\subseteq \omega$, $R\subseteq D^2$ is a well-founded relation and an extensional relation, and $n\in D$ is distinguished. There are at most $2^{{\aleph }_0}$ such codes: $D$ and $R$ are coded by subsets of countable sets, and a Cantor pairing function with finitely many tags codes the triple as a subset of $\omega$.

The well-founded recursiondefines its collapse, as in the Mostowski collapse theorem. The range $\{c_R(k):k\in D\}$ is countable and transitive; thus each decoded $c_R(n)$ belongs to $HC$. Conversely, for $x\in HC$, choose a bijection $e:D\to t(x)$ and the point $n$ with $e(n)=x$. Set $lRk$ exactly when $e(l)\in e(k)$. Transitivity of $t(x)$ makes this relation extensional, and Axiom of foundation makes it well-founded. The recursion then gives $c_R(k)=e(k)$, so this code decodes to $x$.

We have a surjection from a set of at most continuum many codes onto $HC$. Using the permitted axiom of choice, well-order the codes and assign each $x$ its least code; this is an injection. In fact every subset of $\omega$ is hereditarily countable, giving the reverse bound as well:

Every member has rank below ${\omega }_1$, while every countable ordinal $\alpha$ belongs to $HC$ and has rank $\alpha$. Consequently

The axioms hold except Power Set. axiom of extensionality and Axiom of foundation are inherited by this transitive structure. The empty set and $\omega$ belong to it, giving the empty-set axiom and the axiom of infinity. The axiom of pairing follows from countable-subset closure. For $a\in HC$, $\bigcup a$ is a countable subset of $HC$, giving the Axiom of union. Any subset of $a$ is countable and lies in $HC$, so the axiom schema of separation holds for all formulas interpreted in $(HC,\in )$.

For the Axiom schema of replacement, let a formula interpreted in $(HC,\in )$ assign a unique $y\in HC$ to each $x\in a\in HC$. Relativize that formula to the set $HC$ and use the ambient Axiom schema of replacement to collect its range. The range is countable and consists of members of $HC$, hence belongs to $HC$. The same argument, selecting one witness for each member of the countable domain, proves axiom schema of collection. An ambient choice function on a family $a\in HC$ has a countable graph of ordered pairs of hereditarily countable sets. Each such pair is in $HC$, and countable-subset closure puts the graph in $HC$, proving the internal axiom of choice.

However, all external subsets of $\omega$ are elements of $HC$. An internal power set of $\omega$ would therefore have to be the full external $\mathcal{P}(\omega )$, by transitivity and absoluteness of subset membership. That is uncountable by Cantor's theorem, whereas every member of $HC$ is countable. Thus the axioms satisfied by hereditarily countable sets areHere the asserted axiom list includes both Axiom schema of replacement and axiom schema of collection; no equivalence relying on Power Set is being silently invoked.

The Mostowski collapse theorem states that if $R$ is a well-founded extensional relation on a set $X$, then there is a unique transitive set $M$ and a unique bijection $\pi :X\to M$ such thatExtensionality means that distinct elements of $X$ have distinct predecessor sets. The collapse is characterized by the recursionWell-founded recursion defines it, extensionality makes it injective, and its range is transitive. Uniqueness follows by well-founded induction. For a class version, the relation must also be set-like; its predecessor sets must be sets.

A map $f:a\to \mathcal{P}(a)$ is recursive if every map $g:\mathcal{P}(b)\to b$ admits a unique $h:a\to b$ with $h(y)=g(\{h(x):x\in f(y)\})$. This holds exactly when the predecessor relation $x\in f(y)$ is a well-founded relation. For the forward construction, take the union of all consistent partial solutions on downward-closed domains; well-founded induction proves compatibility, and a minimal missing point allows extension. Conversely, a nonempty subset with no minimal point has an upward reachability closure $T$ satisfying $y\in T$ exactly when some predecessor is in $T$. With $b=\{0,1\}$ and $g(S)=1$ exactly when $1\in S$, both the zero map and the indicator of $T$ solve the recursion, contradicting uniqueness.

A base case and a decreasing natural number measure work together. Check that every invocation satisfies its precondition, each base case finishes with the correct output, and every other invocation makes finitely many recursive calls with strictly smaller measure. All local work must also terminate. By well-founded induction, the children finish, so their caller finishes; if their answers are correct and the combination rule preserves the postcondition, the caller is correct too. This proves total correctness, not just correctness conditional on return.

Strict decrease without a lower bound is insufficient: subtracting one forever from a negative integer never reaches zero. Even a positive real-valued measure can decrease indefinitely, as $1,1/2,1/4,\dots$ shows. A well-founded relation rules out that descent. In structural recursion, a proper child subtree of a finite binary tree supplies progress without numeric arguments. The proof obligation is the relation between parent and child instances, together with terminating local work and complete base cases.