It is usual to mention theorems of the kind:


Th. Assume there is a proper class of Woodin cardinals, $\mathbb{P} $ is a partial order and $G \subseteq \mathbb{P}$ is V-generic, then $V \models \phi \iff V[G] \models \phi$ 


where $\phi$ is some set theoretic statement (like "the Strong Omega Conjecture holds"), as some sort of evidence that $\phi$ is a statement less intractable than other statements like CH which are not focing-invariant.


My question is, in wich sense are these statements more tractable? What kind of "empirical evidence" gives support to the hope that they can be decided by large cardinal axioms?



Tractability of forcing-invariant statements under large cardinals
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



> 
> $∃y\in\omega^\omega\forall n\in \omega R(x\upharpoonright n, y\upharpoonright n,a\upharpoonright n)$,
> 
> 
> 


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 



> 
> $\exists y\forall z\exists n$ $R(y\upharpoonright n,z\upharpoonright n,x\upharpoonright n,a\upharpoonright n)$,
> 
> 
> 


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:


1. $p[A]\cap p[B]=\emptyset$ and $p[A]\cup p[B]=\omega^\omega$.
2. Item 1 holds in all generic extensions.


A statement $\phi$ admits such a pair iff, in addition,


1. In any forcing extension, $\phi(x)$ iff $x\in p[A]$.


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:



> 
> $V$ is closed under sharps iff $V$ is $\Sigma^1\_3$-absolute. $(\*)$
> 
> 
> 


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.)


