A new axiom is proposed, the Ground Axiom, asserting that the universe is not a nontrivial set forcing extension of any inner model. The Ground Axiom is first-order expressible, and any model of ZFC has a class forcing extension which satisfies it. The Ground Axiom is independent of many well-known set-theoretic assertions including the Generalized Continuum Hypothesis, the assertion V=HOD that every set is ordinal definable, and the existence of measurable and supercompact cardinals. The related Bedrock Axiom, asserting that the universe is a set forcing extension of a model satisfying the Ground Axiom, is also first-order expressible, and its negation is consistent.
A new axiom is proposed, the Ground Axiom, asserting that the universe is not a nontrivial set-forcing extension of any inner model. The Ground Axiom is first-order expressible, and any model of ZFC has a class-forcing extension which satisfies it. The Ground Axiom is independent of many well-known set-theoretic assertions including the Generalized Continuum Hypothesis, the assertion V=HOD that every set is ordinal definable, and the existence of measurable and supercompact cardinals. The related Bedrock Axiom, asserting that the universe is a set-forcing extension of a model satisfying the Gr…
We study the reverse mathematics of countable analogues of several maximality principles that are equivalent to the axiom of choice in set theory. Among these are the principle asserting that every family of sets has a $\subseteq$-maximal subfamily with the finite intersection property and the principle asserting that if $P$ is a property of finite character then every set has a $\subseteq$-maximal subset of which $P$ holds. We show that these principles and their variations have a wide range of strengths in the context of second-order arithmetic, from being equivalent to $\mathsf{Z}_2$ to bei…
In Reverse Mathematics, the axiom system DNR, asserting the existence of diagonally non-recursive functions, is strictly weaker than WWKL$_0$ (weak weak König's Lemma).
We introduce a variant of Martin's axiom, called the grounded Martin's axiom, which asserts that the universe is a ccc forcing extension in which Martin's axiom holds for posets in the ground model. This principle already implies several of the combinatorial consequences of Martin's axiom. The new axiom is shown to be consistent with the failure of Martin's axiom and a singular continuum. We prove that the grounded Martin's axiom is preserved in a strong way when adding a Cohen real and that adding a random real to a model of Martin's axiom preserves the grounded version (even though it destro…
I explore two separate topics: the concept of jointness for set-theoretic guessing principles, and the notion of grounded forcing axioms. A family of guessing sequences is said to be joint if all of its members can guess any given family of targets independently and simultaneously. I primarily investigate jointness in the case of various kinds of Laver diamonds. In the case of measurable cardinals I show that, while the assertions that there are joint families of Laver diamonds of a given length get strictly stronger with increasing length, they are all equiconsistent. This is contrasted with …
The ground axiom is the assertion that the set-theoretic universe is not obtainable by forcing over any inner model. Although this appears at first to be a second-order assertion, it is actually first-order expressible in the language of set theory. This article is the extended abstract for a talk at the 2005 Workshop in Set Theory at the Mathematisches Forschungsinstitut Oberwolfach.
We study principles of the form: if a name $σ$ is forced to have a certain property $φ$, then there is a ground model filter $g$ such that $σ^g$ satisfies $φ$. We prove a general correspondence connecting these name principles to forcing axioms. Special cases of the main theorem are: Any forcing axiom can be expressed as a name principle. For instance, $\mathsf{PFA}$ is equivalent to a principle for rank $1$ names (equivalently, nice names) for subsets of $ω_1$, and a principle for rank $2$ names for sets of reals. Moreover, $λ$-bounded forcing axioms are equivalent to name principles. Bagaria…
In this paper, following an idea of Christophe Chalons, I propose a new kind of forcing axiom, the Maximality Principle, which asserts that any sentence phi holding in some forcing extension V^P and all subsequent extensions V^P*Q holds already in V. It follows, in fact, that such sentences must also hold in all forcing extensions of V. In modal terms, therefore, the Maximality Principle is expressed by the scheme (diamond box phi) implies (box phi), and is equivalent to the modal theory S5. In this article, I prove that the Maximality Principle is relatively consistent with ZFC. A boldface ve…
In this paper, without the axiom of choice, we show that if a certain downward Löwenheim-Skolem property holds then all grounds are uniformly definable. We also prove that the axiom of choice is forceable if and only if the universe is a small extension of some transitive model of $\mathsf{ZFC}$.
A ground of the universe V is a transitive proper class W subset V, such that W is a model of ZFC and V is obtained by set forcing over W, so that V = W[G] for some W-generic filter G subset P in W . The model V satisfies the ground axiom GA if there are no such W properly contained in V . The model W is a bedrock of V if W is a ground of V and satisfies the ground axiom. The mantle of V is the intersection of all grounds of V . The generic mantle of V is the intersection of all grounds of all set-forcing extensions of V . The generic HOD, written gHOD, is the intersection of all HODs of all s…
We mechanize, in the proof assistant Isabelle, a proof of the axiom-scheme of Separation in generic extensions of models of set theory by using the fundamental theorems of forcing. We also formalize the satisfaction of the axioms of Extensionality, Foundation, Union, and Powerset. The axiom of Infinity is likewise treated, under additional assumptions on the ground model. In order to achieve these goals, we extended Paulson's library on constructibility with renaming of variables for internalized formulas, improved results on definitions by recursion on well-founded relations, and sharpened hy…
Assuming the P-ideal dichotomy, we attempt to isolate those cardinal characteristics of the continuum that are correlated with two well-known consequences of the proper forcing axiom. We find a cardinal invariant $\mathfrak{x}$ such that the statement that $\mathfrak{x} > ω_{1}$ is equivalent to the statement that 1, $ω$, $ω_{1}$, $ω\times ω_{1}$, and ${\left[ω_{1}\right]}^{< ω}$ are the only cofinal types of directed sets of size at most ${\aleph}_{1}$. We investigate the corresponding problem for the partition relation $ω_{1} \rightarrow (ω_{1}, α)^2$ for all $α< ω_{1}$. To this effect, we i…
We consider the foundational relation between arithmetic and set theory. Our goal is to criticize the construction of standard arithmetic models as providing grounds for arithmetic truth (even in a relative sense). Our method is to emphasize the incomplete picture of both theories and treat models as their syntactical counterparts. Insisting on the incomplete picture will allow us to argue in favor of the revisability of the standard model interpretation. We then show that it is hopeless to expect that the relative grounding provided by a standard interpretation can resist being revisable. We …
We present three natural combinatorial properties for class forcing notions, which imply the forcing theorem to hold. We then show that all known sufficent conditions for the forcing theorem (except for the forcing theorem itself), including the three properties presented in this paper, imply yet another regularity property for class forcing notions, namely that proper classes of the ground model cannot become sets in a generic extension, that is they do not have set-sized names in the ground model. We then show that over certain models of Gödel-Bernays set theory without the power set axiom, …
We develop the theory of partial satisfaction relations for structures that may be proper classes and define a satisfaction predicate appropriate to such structures. We indicate the utility of this theory as a framework for the development of the metatheory of first-order predicate logic and set theory, and we use it to prove that for any recursively enumerable extension T of ZF (Zermelo-Fraenkel set theory) there is a finitely axiomatizable extension T' of GB (von Neumann-Bernays-Gödel class theory) that is a conservative extension of T. We also prove a conservative extension result that just…
The forcing method is a powerful tool to prove the consistency of set-theoretic assertions relative to the consistency of the axioms of set theory. Laver's theorem and Bukovský's theorem assert that set-generic extensions of a given ground model constitute a quite reasonable and sufficiently general class of standard models of set-theory. In sections 2 and 3 of this note, we give a proof of Bukovský's theorem in a modern setting (for another proof of this theorem see Bukovský [4]). In section 4 we check that the multiverse of set-generic extensions can be treated as a collection of countable t…
