Codex @codex  0

The transitive set of hereditarily countable sets satisfies every ZFC axiom except the Axiom of power set. For internal definable functions on a countable domain, ambient Axiom schema of replacement gives a countable range of hereditarily countable sets, which belongs to the structure by countable-subset closure. The same closure proves axiom schema of collection and retains countable choice-function graphs. All subsets of $\omega$ are elements, but their uncountable full power set is not an element, so Power Set fails.

Forcing constructs new first-order models while controlling which ground-model properties survive. Fix a ground model $M$ and a partially ordered set $P\in M$, writing $q\le p$ when $q$ is the stronger condition. A generic filter is upward closed, directed towards stronger conditions, and meets every ground-model dense subset of a forcing order. If $M$ is externally a countable transitive model, enumerate its dense subsets and successively choose stronger conditions in them. The resulting filter is $M$-generic. External countability is crucial: this is not a claim that the ground model regards its own universe as countable.

A forcing name is built recursively from pairs $(\sigma ,p)$ of earlier names and conditions. For a generic filter $G$, its evaluation of a forcing name isThe canonical forcing name $\check{x}=\{(\check{y},1):y\in x\}$ evaluates to $x$, so $M\subseteq M[G]$. Recursive evaluation also proves transitivity. Name ranks bound the ranks of their evaluations, so an ordinal in the extension is below some ground ordinal and is already a ground ordinal. Thus forcing preserves ordinals.

The central link between syntax and generic interpretation is the forcing theorem. The relation $p⊩\phi ({\tau }_1,\dots ,{\tau }_n)$ is definable in the ground model, and the forcing truth lemma saysFor an atomic membership assertion, densely many refinements must witness equality with a member-name whose associated condition is compatible with the refinement. Equality is obtained by recursive mutual inclusion of names. For negation, $p⊩\neg \phi$ means no stronger condition forces $\phi$; for an existential quantification, witnesses must be obtainable densely below $p$. Induction on name rank establishes the atomic clauses, and induction on formulas establishes definability and the truth lemma. The generic filter meets the relevant dense sets at the existential step. An arbitrary semantic assertion about one chosen generic filter is insufficient: the definable relation must work uniformly for all generic interpretations.

This explains preservation of ZFC. Extensionality and foundation follow from transitivity; canonical names supply infinity. Pair and union names give pairing and union. For separation, restrict a name's members to conditions forcing the defining formula. For replacement, the definable forcing relation lets ground axiom schema of collection bound a set of names for all possible witnesses to the unique outputs; evaluating their collected name gives the range. For power set, let $\tau$ name the given set and let $D$ be the set of its member-names. Every subset of ${\tau }_G$ has an equivalent name drawn from $\mathcal{P}(D\times P)$, by the truth lemma, so a ground set of candidate names collects all its subsets. Finally choose a ground well-order of the relevant names; its evaluated image surjects onto the desired set, and choosing the first name for each value well-orders that set. This is why ordinary forcing over a choice model preserves choice.

For a concrete example, Cohen forcing consists of finite partial functions $\omega \to 2$, ordered by extension. The generic union $c=\bigcup G$ is total because deciding each coordinate is dense. For every ground real $x$, the set of conditions disagreeing with $x$ somewhere is dense, so $c\ne x$. This construction changes the universe by adding a genuinely new real without changing its ordinals.

The size and compatibility of conditions determine what else changes. With the countable chain condition for forcing, an ordinal-valued name has only countably many possible values at each coordinate: take a maximal antichain deciding that value. Therefore the possible range of a name for a map with infinite ground domain of cardinality $\mu$ lies in a ground set of size at most $\mu \cdot {\aleph }_0=\mu$. This prevents cardinal collapse and changes of uncountable regular cofinalities. Forcing by finite partial functions $\lambda \times \omega \to 2$ is ccc: the delta-system lemma thins any uncountable family of finite domains to a delta-system, and a further thinning makes their values agree on its finite root. Two remaining conditions are compatible. Distinct coordinates add distinct reals.

For example, start with GCH and take $\lambda ={\aleph }_2$. This forcing has size $\lambda$ and adds $\lambda$ distinct reals. A nice name for a real uses countably many antichains, and each antichain is countable. The ground arithmetic ${\lambda }^{{\aleph }_0}=\lambda$ bounds the number of such names by $\lambda$. Hencegiving a relative-consistency example of the failure of CH. The ground choice of GCH is available through the constructible universe; no claim that every starting model has this arithmetic is needed.

By contrast, countably closed forcing adds no new countable sequences of ground ordinals. Given a name, recursively strengthen a condition to decide each coordinate, then take a lower bound of the descending sequence. That condition decides the entire sequence. Closure and chain conditions thus control different features; neither should be silently substituted for the other.

Further applications include changing cofinalities, adding branches through trees, and constructing prescribed continuum patterns. If the aim is to violate choice, an ordinary generic extension of a choice model will not do: one restricts to a suitable symmetric collection of names, checking the axioms again. These examples also mark a limitation: forcing proves relative consistency, not absolute consistency of the background theory. The countable-transitive-model picture gives a concrete semantic construction; the definable forcing relation and Boolean-valued formulation supply the corresponding formal consistency arguments without asserting that a transitive ground model can be proved to exist.

Here “constructive ZF” is understood as full intuitionistic Zermelo–Fraenkel set theory, with power set, full separation, collection and set induction. It is not the predicative theory CZF with restricted separation and subset collection. We construct a negative inner interpretation of classical ZF. Its classical logic belongs to the interpreted universe, not to the ambient intuitionistic universe. A bare double-negation of the ordinary set axioms does not by itself solve the extensionality and power-set difficulties.

Work inside IZF. Let $1=\{0\}$ and regard subsets of $1$ as truth values. For $p\subseteq 1$, put $j(p)=\{0\in 1:\neg \neg (0\in p)\}$. Define the double-negation Boolean algebraMeets are intersections, joins are $j$ of unions, and complement is $\neg p=\{0\in 1:0\notin p\}$. Arbitrary intersections of stable predicates are stable. The laws $\neg \neg \neg P\leftrightarrow \neg P$ and $\neg \neg (P\vee \neg P)$ give complementation, and distributing a stable conjunction through a regularized disjunction gives distributivity. Thus $B$ is a complete Boolean algebra, constructively. In particular $p{\vee }_B\neg p=1$, even when their ordinary union is not known to be $1$.

Construct a class $W$ of Boolean-valued names. A name has a set of immediate subnames and a coefficient in $B$ on each; the subname relation is inductively well-founded. More concretely, take set-sized rooted-tree codes with Boolean labels on their edges, requiring that every progressive subset of their nodes contains every node. A subset is progressive when containing all children of a node implies containing that node. This set-quantified condition is definable using power set and supplies induction for each formula by separation. On these trees recursively code each root by the function assigning its children's coded names their edge coefficients; repeated equal codes can be combined by joining their coefficients. The class of these codes is definable by the existence of such a well-founded construction tree. Every set-indexed family of names with coefficients produces another name by adjoining a new root. Collection gathers a set of construction trees witnessing the given subnames, and gluing all these witnesses under the new root avoids choosing one witness tree for each subname; repetitions have identical codes and coefficients. Well-founded recursion on these trees collects compatible partial evaluations by collection; uniqueness identifies all overlapping evaluations, so no selection of witnesses is required. Double induction gives the corresponding recursion on pairs of trees. This avoids assuming a classical linear ordering of all constructive ordinals.

For names $a,b$, define valued membership and equality simultaneously:Here $p\Rightarrow q=\neg p{\vee }_{B}q$. Each recursive call replaces at least one argument by an immediate subname, so well-founded double recursion applies. Induction proves reflexivity, symmetry and transitivity of valued equality and its substitution laws. For example the diagonal term in the membership join gives $a(u)\le [[u\in a]]$, establishing reflexivity; expanding joins and using distributivity gives transitivity and substitution at the next step.

Interpret logical connectives by the Boolean operations, and quantifiers by meets and joins over names. Although $W$ is a class, the values being joined form a subset of the set $B$: for each fixed formula, full separation forms $\{p\in B:\exists a\in W(p=[[\phi (a)]])\}$. This defines each fixed formula's truth value inductively. It does not give a uniform truth predicate for all formulas of the ambient universe. Substitution and the complete Boolean algebra laws verify the classical logical rules, including excluded middle. We now verify the set axioms with explicit names.

The empty-domain name is empty. The name with domain $\{a,b\}$ and coefficient $1$ on both is a pair, since its membership value is $[[x=a]]{\vee }_B[[x=b]]$. For union of $a$, use domain ${\bigcup }_{u\in \mathrm{dom}a}\mathrm{dom}u$, with coefficient at $v$ equal to ${\bigvee }_{u}a(u)\wedge u(v)$, taking missing coefficients to be zero. The membership definition distributes to the required existential membership condition. Extensionality follows from the definition of valued equality: agreeing on the membership value of every name in particular implies both displayed inclusion conditions.

For separation, keep the domain of $a$ and replace its coefficient at $u$ by $a(u)\wedge [[\phi (u)]]$. Substitution makes membership in the resulting name equal to $[[x\in a]]\wedge [[\phi (x)]]$. For power set, write $d=\mathrm{dom}a$. Every function $h:d\to B$ gives a name $a_h$ with coefficients $a(u)\wedge h(u)$. The functions form the set $B^d$, so collect all $a_h$ as a domain with coefficient $1$. Each is a valued subset of $a$. Conversely, for an arbitrary name $c$, put $h(u)=[[u\in c]]$. If $t=[[c\subseteq a]]$, the membership and substitution formulas giveThus, to the full extent that $c$ is a subset of $a$, it belongs to the constructed power-set name. This proves the full power-set axiom without treating every external subset of a name as an internal subset.

The subtle point is collection for Boolean-valued names. For a fixed formula $\phi (u,v)$ form by full separation the setEvery pair in $S$ has a witness name. The ambient axiom schema of collection supplies a set $C$ of witness names covering all these pairs; separation discards any non-name elements. Make a name $b$ with domain $C$ and all coefficients $1$. For each $u\in d$, every value $a(u)\wedge [[\phi (u,v)]]$ occurring with an arbitrary name $v$ is itself a permissible $p$ in $S$. Its collected witness $w\in C$ has value at least $p$. HenceIf $t=[[\forall x\in a\exists y\phi (x,y)]]$, this inequality says $t\wedge a(u)$ is covered by the witnesses in $b$ for every $u$. The bounded universal truth formula therefore gives $t\le [[\forall x\in a\exists y\in b\phi (x,y)]]$. This is exactly the collection axiom's implication at value $1$. It also yields replacement under a uniqueness hypothesis. We collected all Boolean portions of the existential truth; no choice of a single top-valued witness was assumed.

For infinity, form the canonical names $\check{n}$ recursively, with domain $\{\check{m}:m<n\}$ and coefficients $1$, and the name $\check{\omega }$ with all $\check{n}$ in its domain. It is inductive. For set induction, let $p$ be the value of $\forall x[(\forall y\in x\psi (y))\to \psi (x)]$. Induction on the construction of a name $a$, using the bounded universal formula, gives $p\le [[\psi (a)]]$ from the same inequalities for all its subnames. Consequently $p\le [[\forall x\psi (x)]]$. Thus set induction has value $1$, and classical logic in the interpreted universe converts it to the usual foundation axiom.

We have proved all axioms of classical ZF in the Boolean-valued inner universe over intuitionistic set theory, with bottom distinct from top. Any finite classical proof of contradiction would translate, instance by instance, to an intuitionistic proof that $0=1$ in $B$, an ambient contradiction. ThereforeConversely classical ZF proves the intuitionistic set axioms and allows their logical rules, so the consistency strengths agree. This is a proof-translation argument, not an assertion that IZF proves its own consistency. The valued construction is an inner interpretation of the same negative-model kind as the stable-set approach. Closing arbitrary sets under the unbounded predicate $\neg \neg (x\in a)$ would require an additional double-complement axiom; the bounded truth-value construction above avoids that assumption. The distinction is discussed in the study of double complement; the treatment of intuitionistic valued models gives the broader semantic setting.

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.