Your question has a certain affinity with the concept of a *solid bedrock* model, which arises in the theory of set-theoretic geology. Namely, $W$ is *bedrock* for $V$ if $V$ is a forcing extension of $W$ and $W$ satisfies the ground axiom, meaning that it is not a forcing extension of any deeper ground, or in other words, that it is minimal among all the grounds of $V$. The model $W$ is a *solid bedrock* if $W$ is least among all the grounds of $V$.

Although assertions about whether there is a bedrock or whether there are grounds of a certain nature seem at first to be second-order assertions about $V$, because they quantify over the inner models $W$ that might be grounds, in fact these are all first- order expressible in the language of set theory. The reason is that the collection of grounds of $V$ is uniformly definable, in that there is a definable family of classes $W_r$ such that every $W_r$ is a ground of $V$; every ground of $V$ is $W_r$ for some $r$; and the relation $x\in W_r$ is definable in $x$ and $r$. Thus, one may quantify over the collection of grounds by quantifying over the parameter $r$ used in this definition.

In his dissertation, Jonas Reitz proved that there are *bottomless* models $V$, which have no bedrock models; that is, a bottomless model $V$ can be realized as a set-forcing extension $V=W[G]$ of a ground $W$, but one can always go deeper, and realize $W=W_0[G_0]$ as a forcing extension of a still deeper ground, with no bottom.

universal, model of any theory by a syntactic construction. Essentially you generate the Lindenbaum algebra, but of course this can get technically complicated. I've always wondered why set theory is "against" such methods. $\endgroup$ – Andrej Bauer Nov 29 '13 at 7:332more comments