I shall describe recent work focussed on general relations of
the set-theoretic universe to its forcing extensions and grounds. A set
theoretical assertion is forceable (or possible) if it holds in some
forcing extension, and necessary if it holds in all forcing extensions.

These concepts are fundamentally modal in nature, and it is natural to
inquire which modal assertions are valid for this forcing interpretation.
What is the modal logic of forcing? The answer, established in joint work
with B. Loewe, is that if ZFC is consistent, then the ZFC-provably valid
principles of forcing are exactly those in the modal theory known as S4.2.

The ideas admit a duality, looking downward to ground models rather than
upward to forcing extensions, and in this case we have established the same
S4.2 theory of validities, provided that ground models are downward
directed. The Downward Directedness hypothesis is the principal open
question of set-theoretic geology, introduced by myself, Fuchs and Reitz,
and one of our initial results is that every model of ZFC is the
Mantle---the intersection of all grounds---of another model of ZFC. Some of
this analysis engages pleasantly with various philosophical views on the
nature of mathematical existence.