Is there a natural restriction of VO logic which captures P or NP? The paper


Lauri Hella and José María Turull-Torres,
Computing queries with higher-order logics,
TCS 355 197–214,
2006.
doi: 10.1016/j.tcs.2006.01.009


proposes logic VO, variable-order logic.  This allows quantification over orders over the variables.  VO is quite powerful and can express some non-computable queries.  (As pointed out by Arthur Milchior below, it actually captures the whole of the analytical hierarchy.)  The authors show that the fragment of VO obtained by allowing only bounded universal quantification over the order variables exactly expresses all c.e. queries.  VO allows the order variables to range over the natural numbers, so bounding the order variables is clearly a natural condition to impose.


  Is there a (nice) fragment of VO that captures P or NP?


As an analogy, in classical first-order logic allowing quantification over sets of objects gives a more powerful logic called second-order logic or SO.  SO captures the whole of the polynomial hierarchy; this is usually written as PH = SO.  There are restricted forms of SO capturing important complexity classes: NP = $\exists$SO, P = SO-Horn, and NL = SO-Krom.  These are obtained by imposing restrictions on the syntax of allowed formulas.

So there are straightforward ways to restrict SO to obtain interesting classes.  I would like to know if there are similar straightforward restrictions of VO that are roughly the right level of expressivity for P or NP.  If such restrictions are not known I would be interested in suggestions for likely candidates, or in some arguments why such restrictions are unlikely to exist.

I have checked the (few) papers that cite this one, and checked the obvious phrases on Google and Scholar, but found nothing obviously relevant.  Most of the papers dealing with logics more powerful than first-order don't seem to deal with restrictions to bring down the power into the realm of "reasonable" computations, but seem content to dwell in the c.e. universe of arithmetic and analytic classes.  I'd be happy with a pointer or a non-obvious phrase to search on; this might be well known to someone working in higher-order logics.
For information, VO is in fact really more powerful than what you state; it contains the entire analytical hierarchy (hence, also the entire arithmetical hierarchy). The result is not published, neither submitted to any place, but you can find it on my page, www.milchior.fr/ho.pdf section 7 page 47. 

In it I show how VO lets you express addition and multiplication on order variable; may be some idea in this paper can help you. In particular I gave an equivalent definition (I prove it is equivalent) and I think it is more easy to use. (I wanted to avoid the fact that, in their definition of VO $\forall i \forall X^i\forall j\exists Y^j (X^i=Y^j)$ is false while    $\forall i \forall X^i\forall i\exists Y^i (X^i=Y^i)$ is true; which means that $i$ was changed after $X$ was quantified; hence it is useless to add "$^i$" when one quantifies $X$.

One straightforward restriction would be to forbid to quantify the same variable twice. I am pretty sure that the restriction is the class ELEMENTARY. The idea is that, for every formula $\phi(i)$ with a free order variable $i$, there would be one number $k$ such that forall $i>k$ the value of $\phi(i)$ would not change; hence if we can find this $k$ (which is probably an elementary function of the size of the universe) we can avoid to really check every possible $\phi(i)$ when we want the value of $\forall i \phi(i)$ but restrict it to $\forall i &lt; k \phi(i)$.

Else, you can certainly restrain VO by restraining the maximal order accepted; but then you obtain a "higher order" language (HO), and this is probably not what you want.