The ground axiom is consistent with V $\neq $ HOD

Abstract

Abstract. The Ground Axiom asserts that the universe is not a nontrivial set-forcing extension of any inner model. Despite the apparent second-order nature of this assertion, it is first-order expressible in set theory. The previously known models of the Ground Axiom all satisfy strong forms of V = HOD. In this article, we show that the Ground Axiom is relatively consistent with V = HOD. In fact, every model of ZFC has a class-forcing extension that is a model of ZFC + GA + V = HOD. The method accommodates large cardinals: every model of ZFC with a supercompact cardinal, for example, has a classforcing extension with ZFC + GA + V = HOD in which this supercompact cardinal is preserved.The Ground Axiom, introduced by Hamkins and Reitz [10,9, 4], is the assertion that the universe of set theory is not a nontrivial set-forcing extension of any inner model. That is, the Ground Axiom asserts that if W is an inner model of the universe V and G is W -generic for nontrivial forcing, then W [G] = V . This is true, for example, in the constructible universe L, in the modelof a measurable cardinal, in most instances of the core model K and in many other canonical models of set theory. Surprisingly, however, the Ground Axiom does not hold in all the canonical inner models, for Schindler has observed that the minimal model M 1 of one Woodin cardinal is a forcing extension of one of its iterates (see also Theorem 5 below). Precursors to the Ground Axiom include work in [1], where set-genericity over an inner model is considered in the case L [x] for x a real.Despite the prima facie second order nature of the Ground Axiom assertion-it quantifies, after all, over all inner models of the universe-the Ground Axiom is actually first-order expressible in the language of set theory. This was proved by Reitz [10,9] and is implicit, independently, in the appendix of Woodin's article [11]. These arguments rely, respectively, on recent work of Laver [5], using methods of Hamkins [3], and independent work of Woodin [11], showing that any model of set theory W is first-order definable as a class in all its set-forcing extensions W [G],