TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedaudited 2026-09-22

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Shelah inner model satisfies ZF and Dependent Choice

Statement

$N = H O D (S)$ is a transitive inner model with the same ordinals and reals as the ambient Shelah extension, satisfies every axiom of ZF, and satisfies the serial-relation form of Dependent Choice.

Facts & Assumptions

Given: The class $N$ of the definition item in the ambient Shelah extension.

[F1]

The Shelah HOD(S) model and its real-ordinal presentation: membership in $N$ is hereditary unique definability in a rank from one countable ordinal sequence and finitely many ordinals; the class is first-order and contains all reals and all ordinals; finite tuples of $S$ -parameters interleave.

[F2]

The Shelah inner model is closed under ambient omega-sequences: every ambient $ω$ -sequence with values in $N$ belongs to $N$ .

[F3]

The Solovay inner model satisfies ZF and every real set has a real–ordinal definition and The Solovay inner model satisfies Dependent Choice: the corresponding ZF and DC clauses are already proved for the Solovay $H O D (S)$ model at exactly this interface.

[F4]

The serial-relation Dependent Choice principle over ZF: DC says that for every nonempty set $A$ and every serial relation $R$ on $A$ , there is a sequence $⟨ a_{n} : n < ω ⟩$ in $A$ with $R (a_{n}, a_{n + 1})$ for all $n$ . The definition expressly distinguishes this from the prescribed-start form.

[F5]

The Axiom of Choice: ambient AC, used only to produce the ambient recursive chain below.

Proof

1.1

$N$ is transitive and contains all ordinals and all reals: the transitive closure of a member of $N$ consists of $O D (S)$ -sets by hereditaryness, and every ordinal and every real is definable in a rank from itself as a parameter, so both lie in $N$ . Since the sheaf of definitions is rank-bounded, $N$ is a transitive class, exactly at the HOD(S) interface of [F3].

F1F3

1.2

Extensionality, Foundation, Pairing, Union and Infinity hold: each axiom's witness is definable in a rank from the same parameters as its inputs, and the definitions close under these operations because a finite tuple of $S$ -parameters interleaves into one.

1.3

Separation: for $A \in N$ and a formula $ψ$ , the set $A \cap ψ^{N}$ is defined in a rank from the definition of $A$ conjoined with $ψ$ and the rank bound of the separating instance, so it lies in $N$ .

1.4

Replacement: if $F$ is a definable function on $A \in N$ with values in $N$ , then the image is defined from the same $S$ -parameter and ordinals as $A$ and $F$ , without selecting a code for each value: one quantifies in a rank over the unique value of $F$ . Hence the image belongs to $N$ .

1.5

Power set: for $A \in N$ , the uniform predicate " $y$ is a subset of $A$ " is ranked and definable from the parameters defining $A$ , so the power set of $A$ as computed in $N$ is a set of $N$ . Together with steps 1.2 through 1.4 this verifies all axioms of ZF in $N$ .

1.6

Dependent Choice: let $A \in N$ be nonempty and let $R \in N$ be serial on $A$ . In the ambient model, AC first selects some $a_{0} \in A$ and then recursively chooses $a_{n + 1} \in A$ with $R (a_{n}, a_{n + 1})$ , which is possible by seriality. The resulting $ω$ -sequence lies in $N$ by [F2]; transitivity and the absoluteness of membership in the set $R$ give $N ⊨ R (a_{n}, a_{n + 1})$ for all $n$ . Thus the starting-point-free serial-relation form of DC stated in [F4] holds in $N$ ; no equivalence with the separately named prescribed-start form is used.

F2F4F5

2.1

$N$ has the same ordinals and reals as the ambient extension, since it contains them all and is transitive.

F1step 1.1

3.1

Steps 1.1 through 1.6 verify the ZF and same-ordinals-and-reals clauses, and step 1.6 verifies DC; this is the Statement.

step 2.1step 1.6∎

Depends on

Used by

Dependency tree · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Robert M. Solovay, A Model of Set-Theory in Which Every Set of Reals Is Lebesgue Measurable (standard reference, not scraped)
Saharon Shelah, Can You Take Solovay's Inaccessible Away? (standard reference, not scraped)