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:

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.

5more comments