The Axiom of Determinacy Implies Dependent Choices in Mice

Sandra M\"uller

arxiv: 1907.02755 · v1 · pith:WM4TCHQLnew · submitted 2019-07-05 · 🧮 math.LO

The Axiom of Determinacy Implies Dependent Choices in Mice

Sandra M\"uller This is my paper

Pith reviewed 2026-05-25 02:05 UTC · model grok-4.3

classification 🧮 math.LO

keywords axiom of determinacydependent choicespremiceinner modelsscalesset theorymicedeterminacy

0 comments

The pith

The axiom of determinacy implies dependent choices in countably iterable passive premice over their reals.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves that if a countably iterable passive premouse M built over its reals satisfies the axiom of determinacy in a background universe obeying ZF plus dependent choice over those reals, then M itself obeys the axiom of dependent choices. The argument extends Kechris's earlier result for L(R) by applying Steel's scales analysis inside these mice. This matters because it shows that, inside such models, the stronger determinacy axiom already guarantees the weaker dependent choice principle without separate assumption. The result applies in particular to the models M_n(A) for n at most omega when A is a countable set of reals equal to the reals of the model.

Core claim

We show that the Axiom of Dependent Choices, DC, holds in countably iterable, passive premice M constructed over their reals which satisfy the Axiom of Determinacy, AD, in a ZF + DC_{R^M} background universe. This generalizes an argument of Kechris for L(R) using Steel's analysis of scales in mice. In particular, we show that for any n ≤ ω and any countable set of reals A so that M_n(A) ∩ R = A and M_n(A) ⊨ AD, we have that M_n(A) ⊨ DC.

What carries the argument

Countably iterable passive premice M constructed over their reals, with the property that AD holds inside M while the background satisfies ZF + DC over R^M, using Steel's scales analysis.

Load-bearing premise

The premice are countably iterable and passive, and the background universe satisfies ZF plus dependent choice over the reals of the mouse.

What would settle it

Construct or exhibit a countably iterable passive premouse M over its reals such that AD holds in M but DC fails in M, while the background universe satisfies ZF + DC over R^M.

read the original abstract

We show that the Axiom of Dependent Choices, $\operatorname{DC}$, holds in countably iterable, passive premice $\mathcal{M}$ construced over their reals which satisfy the Axiom of Determinacy, $\operatorname{AD}$, in a $\operatorname{ZF}+\operatorname{DC}_{\mathbb{R}^{\mathcal{M}}}$ background universe. This generalizes an argument of Kechris for $L(\mathbb{R})$ using Steel's analysis of scales in mice. In particular, we show that for any $n \leq \omega$ and any countable set of reals $A$ so that $M_n(A) \cap \mathbb{R} = A$ and $M_n(A) \vDash \operatorname{AD}$, we have that $M_n(A) \vDash \operatorname{DC}$.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This generalizes Kechris' AD-implies-DC result from L(R) to M_n(A) mice via Steel's scales, and the argument structure appears clean with no obvious circularity.

read the letter

The core new claim is that if a countably iterable passive premouse M built over its reals satisfies AD in a ZF + DC_{R^M} background, then it satisfies DC. In particular this holds for M_n(A) when M_n(A) ∩ R = A and M_n(A) ⊨ AD. That is a direct extension of the L(R) case, and the paper credits the generalization to Steel's scale analysis inside mice rather than inventing new machinery. The hypotheses are stated explicitly, which helps: countable iterability, passivity, and the background DC over the reals of M. No load-bearing circularity is visible in the abstract or the stress-test note. The result stays inside the existing framework of inner model theory and does not claim to remove the background assumptions or handle non-iterable mice. The main limitation is scope: it applies only under those iterability and background conditions, so it does not give a blanket AD → DC theorem in ZF alone. The citation pattern looks standard, resting on Kechris and Steel without self-referential tricks. This is the kind of incremental but technically useful note that inner model theorists will want to see. It deserves a serious referee because the statement is precise, the method is referenced to prior verified work, and the conclusion is falsifiable inside the theory. I would bring it to a reading group if the group already works on mice and determinacy, but not otherwise. I would not cite it in my own papers unless I needed the exact statement for M_n(A).

Referee Report

0 major / 1 minor

Summary. The manuscript proves that DC holds in countably iterable passive premice M constructed over their reals that satisfy AD inside a ZF + DC_{R^M} background universe. The argument generalizes Kechris' result for L(R) by applying Steel's scales analysis in mice. In particular, for any n ≤ ω and countable A with M_n(A) ∩ R = A and M_n(A) |= AD, it follows that M_n(A) |= DC.

Significance. If the derivation holds, the result extends the known implication from AD to DC beyond L(R) to a natural class of mice, strengthening the connection between determinacy and choice principles in inner model theory. The paper explicitly credits and builds on prior work by Kechris and Steel without introducing new unsupported steps.

minor comments (1)

[Abstract] Abstract: 'construced' is a typographical error and should read 'constructed'.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for the positive report recommending acceptance. The referee's summary accurately captures the main result.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper generalizes Kechris' argument for L(R) using Steel's analysis of scales in mice to establish that AD implies DC inside countably iterable passive premice M over their reals in a ZF + DC_{R^M} background. The hypotheses (countable iterability, passivity, M_n(A) ∩ R = A, M_n(A) ⊨ AD) are stated explicitly as inputs, and the argument structure is presented as inheriting from independent prior results on scales without any reduction of the conclusion to a self-definition, fitted parameter, or self-citation chain. The derivation remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The result rests on the standard definitions of premice, countable iterability, and passivity from inner model theory, plus the background assumption of ZF + DC over the reals; these are domain assumptions drawn from prior literature rather than new postulates introduced here. No free parameters or invented entities are visible in the abstract.

axioms (2)

domain assumption Background universe satisfies ZF + DC_{R^M}
Explicitly stated as the setting in which the mice are considered.
domain assumption M is countably iterable and passive
Core restriction on the class of premice for which the claim is proved.

pith-pipeline@v0.9.0 · 5658 in / 1382 out tokens · 26721 ms · 2026-05-25T02:05:21.793184+00:00 · methodology

The Axiom of Determinacy Implies Dependent Choices in Mice

Core claim

What carries the argument

Load-bearing premise

What would settle it

discussion (0)