The hypothesis that $V_\kappa$ is $\Sigma_k$ elementary or
even fully elementary in $V$ is much weaker than you say.
One can see part of this quite easily by observing that for
any inaccessible cardinal $\delta$, then
$V_\delta\models\text{ZFC}$ and there are a club of
ordinals $\alpha$ with $V_\alpha\prec V_\delta$. In
particular, if $\delta$ is Mahlo, then there are a
stationary set of inaccessible cardinals $\kappa$ with
$V_\kappa$ fully elementary in $V_\delta$.
In particular, if we lived inside $V_\delta$, we would
believe that there is a stationary proper class of
inaccessible cardinals $\kappa$ with $V_\kappa$ as fully
elementary in the universe as desired.
It turns out that although we can express
$V_\kappa\prec_{\Sigma_k} V$ as a first-order assertion of
$\kappa$ and $k$, it is not possible to express full
elementary $V_\kappa\prec V$ as a single first-order
assertion of set theory. Instead, we may use a scheme.
Thus, we introduce $\kappa$ as a constant symbol, and
consider the scheme, denoted "$V_\kappa\prec V$ ", asserting
of every formula $\varphi$ that $$\forall x\in V_\kappa\
(\varphi(x) \iff V_\kappa\models\varphi[x]\ ).$$ If we
add the assumption that $\kappa$ is inaccessible, then this
is known as the Levy scheme.
Theorem. The following are equiconsistent over ZFC.
- The Levy scheme. That is, the scheme "$V_\kappa\prec
V$ " plus "$\kappa$ is inaccessible."
- "ORD is Mahlo". That is, the scheme asserting of every
definable (with parameters) proper class club, that it
contains an inaccessible cardinal.
Proof. The first implies that $V_\kappa$ satisfies ORD is
Mahlo, since $\kappa$ will be a limit point and hence an
element of any such club as defined in $V$ using parameters
below $\kappa$. If the second is consistent, then so is the
first by a compactness argument, using the reflection
theorem. QED
Meanwhile, if you drop the inaccessibility requirement,
then you can attain the following, which many set theorists
find surprising.
Theorem. The scheme "$V_\kappa\prec V$ " is
equiconsistent merely with ZFC.
Proof. If ZFC is consistent, then so is every finite
fragment of the scheme $V_\kappa\prec V$, by the reflection
theorem. QED
One can even attain a proper class club
$C\subset\text{ORD}$ of cardinals, with each $\kappa\in C$
satisfying the scheme $V_\kappa\prec V$, without going
beyond ZFC in consistency strength.
Both versions of the axiom $V_\kappa\prec V$ were important
in my paper on the maximality
principle, the
principle asserting that any statement that is forceable in
such a way that it remains true in all further extensions
is already true. It turned out that one can force the
maximality principle only from a model of $V_\kappa\prec V$
(and you need $\kappa$ inaccessible for the boldface
maximality principle).
Foreman's maximality principle (the statement: any non-trivial forcing either adds a new real or collapses some cardinals) implies there are no inaccessible cardinal.
Also the consistency of Magidor's question (tree property at all regular cardinals above $\aleph_1$) implies the non-existence of inaccessible cardinals.
Another example is the following maximality principle introduced
at A new maximality principle and its consequences:
$(MP_*):$ For all uncountable regular cardinals $\kappa, 2^{<\kappa}=\kappa^{+}$
and all trees of height and size $\kappa$ are specialized.
Best Answer
Typically, generic absoluteness is a consequence of a stronger property, that in many cases is really the goal one is after. To explain this stronger property, let me begin by reviewing two important absoluteness results.
1) The first is Mostowski's Absoluteness. Suppose $\phi$ is $\Sigma^1_1(a)$, where $a\in\omega^\omega$. This means that $\phi(x)$ for $x\in\omega^\omega$, asserts
where $R$ is a predicate recursive in $a$. These statements are very absolute: Suppose that $M$ is a well-founded model of a decent fragment of ZF, and that $a,x\in M$. Then $\phi(x)$ holds iff $M\models \phi(x)$.
In particular, whether or not $\phi(x)$ holds cannot be changed by forcing, or by passing to an inner or outer model. Note that $M$ could be countable. In fact, only needs to be an $\omega$-model; well-foundedness is not necessary.
This is how the result is usually stated. What is going on is the following:
Suppose that $T$ is a tree (in the descriptive set theoretic sense) and that $T\in M$. Then $T$ is ill-founded iff $M\models T$ is ill-founded.
In particular, $T$ could be the tree associated to $\phi$. This is the tree of all $(s,t)$ such that $s,t$ are finite sequences of the same length $l$, and $\forall n\le l$ $ R(s\upharpoonright l,t\upharpoonright n,a\upharpoonright n)$. So $T$ is the tree of attempts to verify $\phi$: $\phi(x)$ holds iff (there is a $y$ such that for all $n$, $(x\upharpoonright n,y\upharpoonright n)\in T$) iff the tree $T_x$ is ill-founded. Recall that $T_x$ consists of all $t$ such that, if $l$ is the length of $t$, then $(x\upharpoonright n,t\upharpoonright n)\in T$ for all $n\le l$.
The point is that $T$ is a very simple object. As soon as $T,x$ are present, $T_x$ can be built, and the result of the construction of $T_x$ is the same whether it is performed in $V$ or in $M$. Since well-foundedness is absolute, whether or not $T_x$ is ill-founded is the same whether we check this in $M$ or in $V$. Of course, $T_x$ is ill-founded iff $\phi(x)$ holds.
The moral is that the truth of $\Sigma^1_1$ statements is certified by trees. And I think that this is saying that in a strong sense, $\Sigma^1_1$ statements are very tractable. All we need to check their validity is a very easy to build tree and, once we have it, the tree is our certificate of truth or falsehood, this cannot be altered.
Recall that proofs in first-order logic can be described by means of certain finite trees. If something is provable, the tree is a very robust certificate. This is a natural weakening of that idea.
Of course one could argue that, if a $\Sigma^1_1$ statement is not provable, then in fact it may be very hard to establish its truth value, so tractability is not clear. Sure. But, independently of whether or not one can prove something or other, the certificate establishing this truth value is present from the beginning. One does not need to worry that this truth value may change by changing the model one is investigating.
2) The second, and best known, absoluteness result, is Shoenfield's absoluteness. Suppose $\phi$ is $\Sigma^1_2(a)$. This means that $\phi(x)$ holds iff
where $R$ is recursive in $a$. Let $M$ be any transitive model of a decent fragment of ZFC, and suppose that $\omega_1\subset M$ and $a,x\in M$. Then $\phi(x)$ holds iff $M\models\phi(x)$.
This is again a very strong absoluteness statement. Again, if one manages to show the consistency of $\phi(x)$ by, for example, passing to an inner model or a forcing extension, then in fact one has proved its truth.
Again, one could say that if $\phi$ is not provable, then it is in fact not very tractable at all. But the point is that to investigate $\phi$, one can use any tools whatsoever. One only needs to worry about its consistency, for example, and one can make use of any combinatorial statements that one could add to the universe by forcing.
Just as in the previous case, $\Sigma^1_2$ statements can be certified by trees. The tree associated to $\phi$ is more complicated than in the previous case, and it is now a tree of $\omega\times\omega_1$. (Jech's and Kanamori's books explain carefully its construction.) Again, the tree is very absolute: As soon as we have $a$ and all the countable ordinals at our disposal, the tree can be constructed. (One comparing two models $M\subset V$, we mean all the countable ordinals of $V$, even if $M$'s version of $\omega_1$ is smaller.)
3) Generic absoluteness of a statement $\phi$ is typically a consequence of the existence of absolutely complemented trees associated to $\phi$. In fact, all generic absoluteness results I'm aware of are established by proving that there are such trees ("conditional" generic absoluteness results, such as only for proper forcings, or only in the presence of additional axioms, are somewhat different). This is a direct generalization of the situations above.
To define the key concept, recall that if $A$ is a tree of $\omega\times X$, then the projection $p[A]$ of $A$ is the set of all $x\in\omega^\omega$ such that $\exists f\in X^\omega\forall n\in\omega\,(x\upharpoonright n,f\upharpoonright n)\in A$.
Two (proper class) trees $A$ and $B$ on $\omega\times ORD$ are absolutely complemented iff:
A statement $\phi$ admits such a pair iff, in addition,
The idea is that this is a precise, formal, definable approximation to the intuitive statement one would actually like, namely, that there are such trees describing $\phi$ that have this ``complementary'' behavior in all outer models. First-order logic limits ourselves to considering forcing extensions.
Let me point out that $\Sigma^1_1$ and $\Sigma^1_2$ statements admit absolutely complemented pairs, so the existence of such a pair is a natural (far reaching) generalization of the two cases above.
Once we accept large cardinals, we can show that much larger classes than $\Sigma^1_2$ admit absolutely complemented trees. For example, any projective statement does. Once again, the point is that as soon as we have the large cardinals and real parameters in our universe, we have the trees, and the trees certify in unambiguous forcing-unchangeable terms, whether the statements hold at any given real. It is in this sense that we consider these statements more tractable.
Here is a rough sketch of an example I particularly like, due to Martin-Solovay (for measurables) and Woodin (in its optimal form). For details, see my paper with Ralf Schindler, ``projective well-orderings of the reals,'' Arch. Math. Logic (2006) 45:783–793:
The right hand side means that for any $\Sigma^1_3$ statement $\phi$ (so now we have three alternations of quantifiers) and any two step forcing ${\mathbb P}∗\dot{\mathbb Q}$, for any $G$, ${\mathbb P}$-generic over $V$, any $H$, ${\mathbb Q}$-generic over $V[G]$, and for any real $x$ in $V[G]$, we have $$ V[G]\models\phi(x)\Longleftrightarrow V[G][H]\models\phi(x). $$
The left hand side of $(*)$ is a weakening of "there is a proper class of measurable cardinals", which is how the statement is usually presented.
The proof of the implication from left to right in $(*)$ goes by building a tree of attempts to find a witness to the negation of a $\Sigma^1_2$ statement. The goal is that if such a witness can be added by forcing, then in fact we can find one in the ground model. If there is a forcing adding a witness, there is a countable transitive model where this is the case. Essentially, the tree gives the construction of such a model, bit by bit, and if we have a branch, then we have such a model.
So: If there is a witness added in a forcing extension, the tree will have there a branch. So it is illfounded. By absoluteness of well-foundedness, the tree has a branch in $V$. The sharps are used to ``stretch'' the model so that we can use Shoenfield absoluteness, and conclude that there must be a witness in $V$.
4) Projective absoluteness, a consequence of large cardinals, is established by showing the existence of absolutely complemented trees for any projective statement. The theory of universally Baire sets originates with this concept, and the closely related notion of homogeneously Suslin trees. All of this is also connected to determinacy. Once again, to drive the point home: Generic absoluteness is not the goal. The goal is the existence of the pair of trees. Once we have them, we have a strong certificate of truth or falsehood of a statement. I do not know if one is to accept the search for such trees as a more tractable problem than the original statement whose pair of trees we are now searching for. But it certainly says that consistency of the statement, using large cardinals or any combinatorial tools whatsoever, is enough to have a proof of the statement. This seems much more hopeful and generous an approach than if only proofs in the usual sense are allowed. The existence of these trees for projective statements is what I meant in a comment by ``large cardinals settle second order arithmetic.'' Put yet another way: If you show, for example, that a projective statement is not 'decidable' (in the presence of large cardinals), meaning that it is consistent and so is its negation, then you have either actually showed that certain large cardinals are inconsistent, or you have found a way of changing the truth of arithmetic statements, and both of these options are much more significant events than the proof of whatever the projective statement you were interested in was. More likely than not, the truth value of the statement will be uncovered at some point, and you know there is no ambiguity as of what it would be, since the witnessing trees are already present in the universe.
(In spite of its length, I am not completely happy with this answer, but I would need to get much more technical to expand on the many interesting points that your question raises. Hopefully there is some food for thought here. For nice references to some of the issues I mention here, Woodin's article in the Notices is a good place to start, and Steel's paper on the derived model theorem has much of the details.)