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

Question

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.

Answer 1

Note: This is not really answering the question, this is just some comments posted as an answer. :)

Note that in VO, one is defining sets over the set of natural numbers (similar to sets defined in recursion theory) where as in descriptive complexity setting (SO, $\exists$-SO, SO-Horn) we are talking about finite structures. An SO formula in the former setting will give not $PH$ but the whole analytical hierarchy as Arthur Milchior has written in his answer. IMHO, a better comparison would be with bounded arithmetic theories. I don't think you can get below c.e. sets unless you bound all quantifiers to finite domains, to get $P$ or $NP$ the size of domains should be very small.

is the presence of one unbounded quantifier enough to capture c.e. sets?

The problem is you probably want the language to be without extra symbols like equality, addition, multiplication (right?), if we had them then by MRDP theorem, Diophantine formulas (first-order existential quantifiers in front of an equality of two polynomials) would capture c.e. sets. If we are not allowing these symbols in the language, the problem is more complicated, one can use higher order quantifiers to define them, but that would increase the quantifier complexity. So if I want to give a short answer to your question about a single quantifier, I don't know.

If we can express $AC^0$ relations in the language, then a single unbounded existential quantifier would suffice for capturing c.e. sets, the reason is $AC^0$ can check that a string $c$ is the computation of a TM $e$ on input $x$. First-order formulas bounded by polynomials in presence of equality, addition, and multiplication capture PH, so if we have them in the language the answer is positive, but as I said you are probably looking for a language without these symbols.

Some additional comments:

Assume that we have a restriction of VO which can express at least $AC^0$. Then a single unbounded existential quantifier of number type in front of those restricted formulas will give the whole c.e. sets.

Answer 2

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

Answer 3

To answer to your comment, I guess I should make another answer, speaking only on Krom and Horn (May be I should ask a question about those to CSTheory)

I suggest that you read section 5.3 page 34 of my paper about the problem I met on Horn and Krom in High Order logic. You will meet the same problem in Variable Order (which is clearly a superset of High Order).

I don't know if you did pay attention to it, but SO(krom) is equal to P when the first order is universal; indeed you can express NP-complete problem if you add existantial first order variable. (I don't remember the example I had before, I can try to search it if you want it)

I don't know what this syntactical resctriction would become for high order or variable order logic... my point is just that you should also think of a good way to restrain quantifiers, because restraining the quantifier-free part alone is not usefull (at least for Krom formulae)