{
  "id": "2012.07185",
  "version": "v2",
  "published": "2020-12-13T23:48:20.000Z",
  "updated": "2025-05-13T11:52:34.000Z",
  "title": "Ordinal definability in $L[\\mathbb{E}]$",
  "authors": [
    "Farmer Schlutzenberg"
  ],
  "comment": "48 pages. Added hypotheses to Thms 1.4 and 1.6, to bridge minor gaps in their former \"proofs\". Appeal to [6, Thm 0.2] (in paper's references) for Thm 4.2 clarified. Last part of proof of Thm 4.7 clarified. Added Lem 8.14 and strengthened Lem 8.13, to establish what was claimed to be an \"immediate consequence\" of STH in previous version. Other minor corrections and improvements in exposition",
  "categories": [
    "math.LO"
  ],
  "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.",
  "revisions": [
    {
      "version": "v2",
      "updated": "2025-05-13T11:52:34.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03E45",
      "03E55"
    ],
    "keywords": [
      "ordinal definability",
      "tame mouse modelling zfc",
      "minimal mice model",
      "fine structural hypothesis",
      "initial segment"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 48,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}