The technique of forcing in set theory is customarily thought of as a method for constructing outer as opposed to inner models of set theory. A set theorist typically has a model of set theory V and constructs a larger model V[G], the forcing extension, by adjoining a V-generic filter G over some partial order P in V. A switch in perspective, however, allows us to view forcing as a method of describing inner models as well. The idea is simply to search inwardly for how the model V itself might have arisen by forcing. Given a set theoretic universe V, we consider the classes W over which V can be realized as a forcing extension V=W[G] by some W-generic filter G subset P in W. This change in viewpoint is the basis for a collection of questions constituting the topic we refer to as set-theoretic geology. In this talk, I will present some of the most interesting initial results in the topic, along with an abundance of open questions, many of which concern fundamental issues.

A ground model of the universe V is a class W such that 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 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. Our main initial result is that every model of ZFC is the mantle and generic mantle of another model of ZFC. We prove this theorem while also controlling the HOD of the final model, as well as the generic HOD, the intersection of the HODs of all forcing extensions. Iteratively taking the mantle penetrates down through the inner mantles to what we call the outer core, what remains when all outer layers of forcing have been stripped away. Many fundamental questions remain open.

This is joint work with Gunter Fuchs (Muenster) and Jonas Reitz (NY City Tech).