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.
Jeremy Avigad and Ksenija 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.