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.

  • 5
    $\begingroup$ While the abbreviations are famous among the CS community, I'd like to expand them for "the rest of us": PH (Polynomial-time Hierarchy), SO (Second-Order logic), and VO (Variable-Order logic). $\endgroup$ Commented Oct 3, 2010 at 18:59
  • 1
    $\begingroup$ In fact I've never heard of VO before this, so thanks for the clarification. $\endgroup$ Commented Oct 3, 2010 at 19:38
  • $\begingroup$ @Suresh: Yes, I forgot to say that VO is not well-known at all. Anyway, you are most welcome! $\endgroup$ Commented Oct 3, 2010 at 19:52
  • $\begingroup$ There's a nice illustration of various logics and complexity classes here: cs.umass.edu/~immerman/descriptive_complexity.html, though it does not mention VO. $\endgroup$ Commented Oct 3, 2010 at 19:57
  • $\begingroup$ Perhaps I wasn't clear: VO was defined less than a decade ago, and is not well-known. I am interested in it because it is a way to extend first-order logic to make it more powerful, without using fixed-point operators. $\endgroup$ Commented Oct 3, 2010 at 21:18

3 Answers 3


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.


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.

  • $\begingroup$ Thanks for the discussion, I will look at your reformulation. Do you have any suggestions for some ways to restrict the logic so it isn't so powerful -- would something like requiring the unquantified part of the formula to be in CNF with Horn clauses likely to be useful, as it is with classical quantifiers? $\endgroup$ Commented Oct 3, 2010 at 22:14
  • $\begingroup$ To be more precise, I mean a syntactic restriction along the lines of SNP, where the SO quantifiers are applied to a FO formula of specific form (for SNP, with universal FO quantifiers only), and then further restrictions are applied, such as the FO formula inside the FO quantifiers being Horn or Krom. The last paragraph of your Section 5.3 talks about this, but I don't understand your comment that the approach is problematic. $\endgroup$ Commented Oct 4, 2010 at 0:30
  • $\begingroup$ 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) $\endgroup$ Commented Oct 4, 2010 at 0:37

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)

  • 1
    $\begingroup$ Thanks for the insight. This definitely requires further thought! $\endgroup$ Commented Oct 4, 2010 at 11:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.