The Ground Axiom for special statements of set theory

Question

The Ground Axiom (GA), introduced by Hamkins and Reitz, asserts that the universe is not a nontrivial set forcing extension of any inner model, and it is known that GA is consistent relative to ZFC. My question is somehow related to GA.

First a definition:

Definition. Let $\Phi$ be a statement of set theory which is independent of ZFC (or ZFC+large cardinals). Call $\Phi$ forceable, if there is a model $W$ of ZFC and a set of forcing conditions $P$ in $W$ such that $\Phi$ is true in the generic extensions of $W$ by $P$ (we allow the existence of large cardinals in $W$).

Question. 1) Is there a characterization of all forceable sentences $\Phi$ such that the following holds:

If $\Phi$ holds in $V$, then there some inner model $W$ of $V$ in which $\Phi$ fails, and such that $V$ is a set generic extension of $W$.

2) Can you give at least one natural statement $\Phi$ as in (1).

Remark (suggested by Sy Friedman). In the paper "A Large $\Pi^1_2$ Set, Absolute for Set Forcings", Sy Friedman constructs a $\Pi^1_2$ formula $\phi$ which can have many solutions in a cardinal-preserving extension of $L$. $\phi$ also has the property that set-forcing will not add new solutions. So no model in which $\phi$ has more than $\aleph_1$ solutions can be a set-generic extension of a model with only $\aleph_1$ solutions.

Also there are reals $r$ which are minimal over $L$ but which cannot be obtained by set forcing over $L$. Then in $V=L[r]$ the sentence $V=L$ fails, but there is no inner model $W$ of $V$ satisfying $V=L$ such that $V$ is a set forcing extension of $W$.

Answer 1

In your definition, probably you intend that the forcing is nontrivial, since otherwise any consistent $\Phi$ would qualify via trivial forcing. Note also that your forceable terminology conflicts with the terminology used elsewhere, where an assertion $\sigma$ is forceable in a model $V$, if it holds in some set-forcing extension $V[G]$. This is the possibility modal operator $\Diamond\sigma$ of The modal logic of forcing, whose dual $\Box\sigma$ asserts that $\sigma$ is necessary, that is, that $\sigma$ holds in all forcing extensions $V[G]$. Each of these operators is expressible in the first-order language of set theory. That is, $\Phi$ is forceable-in-your-sense if there is some model of set theory in which it is forceable.

Benedikt Löwe and I have also introduced the downward versions of these operators, where we say $\varphi$ is downward possible — let's write it as $\underline\Diamond\varphi$ here — if $\varphi$ holds in some ground model over which the universe was obtained by forcing. Although it is not obvious, the assertion, "there is an inner model $W$ for which $V=W[G]$ is a set-forcing extension and $W\models\varphi$" is first-order expressible in set theory. This kind of observation is the beginning of the subject known as Set-theoretic geology. The dual notion $\underline\Box\varphi$, which asserts that $\varphi$ holds in all ground models, is similarly expressible. The situation of these modal operators in set theory is investigated in our paper Moving up and down in the generic multiverse. In that paper, in order to determine the modal logic, we identify classes of statements, such as the downward switches, which can be turned on and off by going to deeper and deeper grounds, and the downward buttons, which are false in $V$ but true in some ground $W$ and all deeper grounds below $W$. The proofs required us to have large independent families of such buttons and switches, and other types of control statements.

Your statements $\Phi$ are similar to this kind of statement, but go just one step. Specifically, your statements $\Phi$ are precisely the statements for which $\Phi\to\underline\Diamond\neg\Phi$ holds.

I'm not sure what you want in terms of a "classification", but my point is that your property is first-order expressible in the language of set theory, even though it may appear to be second-order because of the quantification over inner models. Set-theoretic geology provides a first-order definable enumeration $W_r$ for $r\in V$ of the collection of all grounds $W_r$ of $V$, and so quantifying over grounds amounts to quantifying over the parameters $r$ used to define them and thus is a first-order quantifier. (You can see an account of the complexity of this definition in my recent paper Superstrong and other large cardinals are never Laver indestructible.)