Is the Invariant Subspace Problem arithmetic?

It seems to me also that the assertion is naturally expressed by a $\Pi^1_2$ assertion in second-order number theory, as Emil had indicated. Let me explain how one can see this.

The basic issue here is that the natural expression of the statement in the language of set theory makes direct reference to uncountable objects, such as the space and the operator and the closed subspace, and therefore cannot be said to be purely arithmetic nor even projective.

But the point is that, nevertheless, one can use the separability hypothesis to find a natural translation of the statement that brings it into the realm of second-order number theory, the context of much of reverse mathematics, and in this way reduce the complexity to $\Pi^1_2$.

In order to do this, one must translate the basic concepts of separable Hilbert space theory to second-order number theory and develop a bit of analysis in that context. In particular, the only objects available in this context are countable, and so one must represent the space, the operator and the subspaces ultimately as countable objects. For example, one can represent the space by providing detailed information about the countable dense set, such as the metric distances on that set and the linear operations; and one represents operators by how they act on that dense subset, and closed subspaces by their projections of that set, and so on. Everything is ultimately represented by a countable amount of information in this context.

Avigad and Simic have written a beautiful account precisely undertaking this project:

• Jeremy Avigad and Ksenija Simic, Fundamental notions of analysis in subsystems of second-order arithmetic, Ann. Pure Appl. Logic 139 (2006), no. 1-3, 138--184.

If you look there (chapter 9), you will find how they represent the whole space, and they develop the basic theory of real analysis in second-order number theory. Since they are interested in the reverse mathematical aspect of the situation, you will see that they pay attention to precisely which axioms of second-order number theory one needs to develop the basic facts one wants when working with separable Hilbert spaces. Closed subspaces are treated in chapter 11.

Now, putting all this together, one looks at your statement, which asserts:

• For every separable Hilbert space and every bounded linear operator on it, there is a nontrivial closed invariant subspace.

So we have universal quantifiers, followed by an existential quantifier, and each of these quantifiers is quantifying over the space of countable objects available in second-order number theory. The properties of being (the code of) a separable Hilbert space or an unbounded operator on such a space are themselves arithmetic, and the encoding of these concepts into second-order number theory is arranged with that in mind. Thus, altogether the complexity is $\forall\exists$ in second-order number theory, or in other words, $\Pi^1_2$ in the projective hierarchy, which is of course a few steps beyond arithmetic.

This is of course, an upper bound, since it is conceivable that one could find a clever equivalent formulation with reduced complexity.

And while this doesn't make the assertion arithmetic, nevertheless the $\Pi^1_2$ level of complexity means that the assertion will be invariant by forcing, on account of the Shoenfield absoluteness theorem.

I played with this a few years ago at http://terrytao.wordpress.com/2010/06/29/finitary-consequences-of-the-invariant-subspace-problem/ ; in the language of the analytical hierarchy, I was trying to lower the complexity of the invariant subspace problem from $\Pi^1_2$ to $\Pi^1_1$. I didn't quite succeed, because I couldn't quantify universally over all second-order objects, but one can instead reformulate the problem as a universal quantification of an arithmetic sentence over all "barriers" (a class of finite sets of natural numbers that "block" all infinite sequences, see Is there a name for a family of finite sequences that block all infinite sequences? ). Unfortunately, barriers (or more precisely, the property of not being a barrier, which is the relevant predicate when reducing to prenex normal form) are defined by a $\Sigma^1_1$ sentence, so this does not reduce the analytic complexity of the invariant subspace problem; but one can at least express this problem as an infinite conjunction of arithmetic sentences, one for each barrier. (One has of course has to add the predicate of membership in the given barrier to the arithmetic language.)

(There is also a universal quantification over growth functions in my formulation, which is another second order object, but this does not significantly increase the complexity, being a simpler object than the barrier.)

Henry Towsner (private communication) has achieved similar such "finitisations" for any $\Pi^1_2$ sentence.