pith. sign in

arxiv: 2012.07185 · v2 · submitted 2020-12-13 · 🧮 math.LO

Ordinal definability in L[mathbb{E}]

Farmer Schlutzenberg This is my paper

Pith reviewed 2026-05-24 14:29 UTC · model grok-4.3

classification 🧮 math.LO
keywords tame miceextender sequencesordinal definabilityHODinner modelspremiceset theorymice
0
0 comments X

The pith

Tame mice satisfy that their universe equals the sets ordinal definable from some real number.

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

The paper proves several definability facts inside tame mice that model ZFC. It shows such a mouse M satisfies that every set in M is ordinal definable from some real x inside M. It further shows that the extender sequence of M above its first uncountable cardinal is definable over M without any parameters at all. These facts together imply that the whole universe of M arises as the ordinal definable sets of M from its initial segment of height equal to its first uncountable cardinal, and that the HOD of M itself forms the universe of a premouse over a subset of the second uncountable cardinal of M. The mouse also admits no proper inner model obtained by forcing that is strategically sigma-closed.

Core claim

Let M be a tame mouse modelling ZFC. Then M satisfies V equals HOD_x for some real x, the restriction of the extender sequence E^M to indices above omega_1^M is definable without parameters over the universe of M, M has universe HOD^M of X where X equals M restricted to height omega_1^M, and HOD^M is the universe of a premouse over some subset t of omega_2^M. M also has no proper grounds via strategically sigma-closed forcings. Some of these results extend partially to non-tame mice, including that many natural phi-minimal mice model V equals HOD, under an extra fine-structural hypothesis.

What carries the argument

The restriction of the extender sequence E to indices above omega_1^M, shown to be definable without parameters over M and used to establish that M equals HOD^M of its initial segment up to that cardinal.

If this is right

  • M has universe HOD^M of X where X is the initial segment M restricted to height omega_1^M.
  • HOD^M is the universe of a premouse over some subset of omega_2^M.
  • M admits no proper grounds obtained via strategically sigma-closed forcings.
  • Many natural phi-minimal mice model V equals HOD, under the stated fine-structural hypothesis.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The results indicate that the sets appearing in these models have limited definability complexity.
  • It remains open whether the same definability conclusions hold for mice that are not tame.
  • The claims could be checked directly on concrete examples of tame mice that arise in core model constructions.

Load-bearing premise

The central results apply only when the mouse is tame and models ZFC.

What would settle it

A tame mouse M modelling ZFC in which the extender sequence above omega_1^M fails to be definable without parameters over M would show the main definability claim false.

read the original abstract

Let $M$ be a tame mouse modelling ZFC. We show that $M$ satisfies "$V=\mathrm{HOD}_x$ for some real $x$", and that the restriction $\mathbb{E}\upharpoonright[\omega_1^M,\mathrm{OR}^M)$ of the extender sequence $\mathbb{E}^M$ of $M$ to indices above $\omega_1^M$ is definable without parameters over the universe of $M$. We show that $M$ has universe $\mathrm{HOD}^M[X]$, where $X=M|\omega_1^M$ is the initial segment of $M$ of height $\omega_1^M$ (including $\mathbb{E}^M\upharpoonright\omega_1^M$), and that $\mathrm{HOD}^M$ is the universe of a premouse over some $t\subseteq\omega_2^M$. We also show that $M$ has no proper grounds via strategically $\sigma$-closed forcings. We then extend some of these results partially to non-tame mice, including a proof that many natural $\varphi$-minimal mice model "$V=\mathrm{HOD}$", assuming a certain fine structural hypothesis whose proof has almost been given elsewhere.

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.

Referee Report

1 major / 0 minor

Summary. The paper proves that every tame mouse M ⊨ ZFC satisfies V = HOD_x for some real x, that the extender sequence E^M ↾ [ω₁^M, OR^M) is parameter-free definable over M, that M = HOD^M[X] with X = M|ω₁^M, that HOD^M is the universe of a premouse over some t ⊆ ω₂^M, and that M admits no proper strategically σ-closed grounds. It also claims partial extensions of some of these conclusions to non-tame mice, including that many natural φ-minimal mice satisfy V = HOD, but only under an additional fine-structural hypothesis whose proof is described as “almost” completed elsewhere.

Significance. If the tame-case results hold, they supply explicit, parameter-free descriptions of HOD inside mice and rule out certain classes of grounds, which would be a concrete advance in the fine-structure theory of L[E]. The representation M = HOD^M[X] and the definability of the tail of E are particularly useful for further work on ordinal definability and core-model theory.

major comments (1)
  1. [Abstract] Abstract, final paragraph: the partial extension to non-tame mice (including the claim that many natural φ-minimal mice model V = HOD) rests on a fine-structural hypothesis whose complete proof is not supplied in the manuscript. Because this hypothesis is load-bearing for every claim that goes beyond the tame case, the manuscript should either incorporate the missing argument or supply a precise, citable reference to its completed form.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and constructive comment. We address the single major point below.

read point-by-point responses

  1. Referee: [Abstract] Abstract, final paragraph: the partial extension to non-tame mice (including the claim that many natural φ-minimal mice model V = HOD) rests on a fine-structural hypothesis whose complete proof is not supplied in the manuscript. Because this hypothesis is load-bearing for every claim that goes beyond the tame case, the manuscript should either incorporate the missing argument or supply a precise, citable reference to its completed form.

    Authors: We agree that the fine-structural hypothesis is essential to all claims beyond the tame case and that its status must be presented with greater precision. The manuscript already qualifies these results as partial and conditional, but the phrasing “almost been given elsewhere” is insufficiently specific. We will revise the abstract and the relevant discussion section to state explicitly that the non-tame results are conditional on the hypothesis, to describe the hypothesis in more detail, and to supply the best available reference or preprint identifier once the work is in citable form. If a complete argument becomes available before resubmission we will incorporate a sketch; otherwise the revision will make the conditional character unmistakable. revision: partial

Circularity Check

0 steps flagged

No significant circularity; main results derived from standard tame mouse theory

full rationale

The paper's core claims (V=HOD_x, parameter-free definability of E above ω₁^M, M=HOD^M[X], etc.) are stated for the domain of tame mice modeling ZFC and derived from the established fine-structural theory of such mice. Tameness is an explicit domain restriction rather than a fitted or self-defined parameter. The partial extension to non-tame mice is explicitly conditional on an external fine-structural hypothesis whose proof is referenced as almost complete elsewhere, but this does not load-bear the primary results or create self-referential reduction. No equations, definitions, or predictions reduce by construction to the paper's own inputs, and no self-citation chain is required for the central derivation.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper rests on the background theory of mice, extenders, and fine structure developed in prior literature; tameness is an additional domain restriction.

axioms (2)
  • domain assumption M is a tame mouse modelling ZFC
    All main theorems are stated under this premise (abstract opening sentence).
  • ad hoc to paper Fine structural hypothesis for non-tame extension
    Partial results for non-tame mice assume a hypothesis whose proof is said to be almost complete elsewhere.

pith-pipeline@v0.9.0 · 5742 in / 1452 out tokens · 28867 ms · 2026-05-24T14:29:05.520746+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

15 extracted references · 15 canonical work pages

  1. [1]

    E. Closson. The Solovay Sequence in Derived Models Associated to Mice . PhD thesis, University of California, Berkeley, 2008

    work page 2008

  2. [2]

    Hugh Woodin

    Peter Koellner and W. Hugh Woodin. Large cardinals from determin acy. In Hand- book of set theory. Vols. 1, 2, 3 , pages 1951–2119. Springer, Dordrecht, 2010

    work page 1951

  3. [3]

    Determinacy in L(R)

    Itay Neeman. Determinacy in L(R). In Matthew Foreman and Akihiro Kanamori, editors, Handbook of set theory , volume 3, chapter 22. Springer, first edition, 2010

    work page 2010

  4. [4]

    Problem list

    Ralf Schindler. Problem list. 1st Girona conference on inner model theory. Available at https://ivv5hpp.uni-muenster.de/u/rds/girona_meetin g_2018.html

    work page

  5. [5]

    The self-iterability of L[E]

    Ralf Schindler and John Steel. The self-iterability of L[E]. Journal of Symbolic Logic, 74(3):751–779, 2009

    work page 2009

  6. [6]

    Schlutzenberg and J

    F. Schlutzenberg and J. R. Steel. Comparison of fine structura l mice via coarse iteration. Archive for Mathematical Logic , 53:539–559, 2014

    work page 2014

  7. [7]

    Fine structure from normal iterability

    Farmer Schlutzenberg. Fine structure from normal iterability. arXiv: 2011.10037

    work page arXiv 2011

  8. [8]

    Iterability for (transfinite) stacks

    Farmer Schlutzenberg. Iterability for (transfinite) stacks. T o appear in Journal of Mathematical Logic. arXiv:1811.03880

    work page arXiv

  9. [9]

    Local mantles in L[x]

    Farmer Schlutzenberg. Local mantles in L[x]. In preparation

    work page

  10. [10]

    Ordinal definability in extender models (talk at Logic Colloquium 2016, Leeds, UK)

    Farmer Schlutzenberg. Ordinal definability in extender models (talk at Logic Colloquium 2016, Leeds, UK). Slides available at https://conferences.leeds.ac.uk/lc2016/slides/

    work page 2016

  11. [11]

    A Long Pseudo-Comparison of Premice inL[x]

    Farmer Schlutzenberg. A Long Pseudo-Comparison of Premice inL[x]. Notre Dame Journal of Formal Logic , 59(4):509–604, 2018. 43

    work page 2018

  12. [12]

    The definability of the extender seque nce E from E ↾ ℵ 1 in L[E]

    Farmer Schlutzenberg. The definability of the extender seque nce E from E ↾ ℵ 1 in L[E]. arXiv: 1906.00276, 2019

    work page arXiv 1906

  13. [13]

    A premouse inheriting strong cardinals from V

    Farmer Schlutzenberg. A premouse inheriting strong cardinals from V . Annals of Pure and Applied Logic , 171(9), 2020

    work page 2020

  14. [14]

    Schlutzenberg

    Martin Zeman? Notes on talk HOD L[E] above ω L[E] 3 below a Woodin limit of Woodins , by F. Schlutzenberg. Available at https://www.math.uci.edu/~mzeman/CMI/cmi-2016.html

    work page 2016

  15. [15]

    Iterates of M1

    Yhizheng Zhu. Iterates of M1. Trans. Amer. Math. Soc. , 371:8811–8827, 2019. 44

    work page 2019