- 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.