{"id":"palomar/PALOMAR-2026-09-19-000005","url":"https://github.com/elliotglazer/definable-saturated/tree/e683bba9e758323b43dd1d6206ed2f6fc9510f06","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-19-000005-v1.json","repo":"https://github.com/elliotglazer/definable-saturated","tags":["math.LO","msc:03C62","msc:03E35","msc:03E40","set-theory","model-theory","lean","consistency"],"score":0,"title":"definable-saturated","trust":"high","domain":"math.LO","source":"palomar","authors":["Elliot Glazer"],"reviews":0,"subject":"math.LO","summary":"A Lean 4 formalization of the relative consistency of ZFC + CH together with the following assertion. There is a countably saturated elementary extension of the natural-number arithmetic structure of cardinality aleph one; all such set-sized presentations are isomorphic; and no such presentation is ordinal definable. The class is defined without parameters. Removing CH from the asserted theory gives a consistent negative answer to MathOverflow question 382009 about definability up to isomorphism versus an ordinal-definable copy. Every notion in the final sentence is internal to the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-19","reactions":{},"formalized":true,"formalizes":[{"title":"Ordinal-definable families in Cohen, random, and collapse extensions, version 21","identifier":"docs/paper/ordinal_definable_families_rewritten_v21.pdf","relationship":"adapts"}]}