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. 



Is the Invariant Subspace Problem arithmetic?
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?](https://mathoverflow.net/questions/29676/is-there-a-name-for-a-family-of-finite-sequences-that-block-all-infinite-sequenc) ). 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.


