Is the Invariant Subspace Problem arithmetic? Invariant Subspace Conjecture: A bounded operator on a separable Hilbert space has a non-trivial closed invariant subspace. 
Can this conjecture be reformulated as an arithmetic statement, that is, $\Pi^0_n$ statement for some n? (I tried to figure it out, but failed.)
EDIT: For what I understand from answers, it appears to be an open problem. As 
Emil Jerabek and others mentioned, the intrinsic complexity of the conjecture (considered 
as a statement in second-order arithmetic) is $\Pi^1_2$. Apparently, no reduction to lesser 
complexity is known. One may speculate about how much of a solution would be a reduction 
to $\Pi^1_1$ or $\Pi^0_n$, but I would rather not. 
Carl Mummert pointed out an interesting possibility: whether the conjecture itself 
is true or not, its interpretation in computable analysis may be false. 
In this case, if I got it right, the only way to reduce its complexity is to disprove it. 
However, this obstacle would disappear if we are allowed to use set 
theory to prove equivalence, because computable analysis doesn't work there.
Thanks to everyone. 
 A: 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. 
A: 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.
