Let $\mathfrak{A} $ be any finite structure. Does its first order theory $ \mathfrak{T} := \mathfrak{TH}(\mathfrak{A}) $ have bounded quantifier rank, in the sense that there is a $ q\in\mathbb{N} $ such that for all $ \varphi\in\mathfrak{T} $ with $ qr(\varphi) > q $ there is a $ \varphi'\in\mathfrak{T} $ with $ qr(\varphi')\leq q $ and $ \varphi'\equiv\varphi $ ?

  • $\begingroup$ Isn't this a question for Mathoverflow rather than CS theory? $\endgroup$ Commented Aug 27, 2017 at 21:10
  • 6
    $\begingroup$ @Andrej, Finite model theory and descriptive complexity are also considered part of TCS. $\endgroup$
    – Kaveh
    Commented Aug 27, 2017 at 21:37
  • 1
    $\begingroup$ Excellent, so it's like Bob Harper said once: math is a special case of computer science. $\endgroup$ Commented Aug 28, 2017 at 6:02
  • $\begingroup$ Computer science is also a special case of math, and they are both also special cases of logic, and vice versa. $\endgroup$
    – fhyve
    Commented Sep 6, 2017 at 1:53

2 Answers 2


The theory of any finite structure is model complete. In fact, it is easy to see that any formula is equivalent to an existential formula with one quantifier per each element of the structure, after which all quantifiers of the original formula can be simulated by conjunctions and disjunctions. In particular, the number of quantifiers (hence quantifier rank) is bounded by the size of the structure.

  • $\begingroup$ Actually, one additional universal quantifier is needed, which allows to express that there are no further elements. In all answers there is one assumption that should be made explicit: the presence o fequality, i.e., that x=y is an allowed atomic formula. $\endgroup$
    – Thomas S
    Commented Aug 30, 2017 at 9:12
  • $\begingroup$ No additional quantifier is needed. Remember we are not trying to axiomatize the theory of the structure, but to find a formula equivalent to a given one modulo the theory. And the presence of equality is universal standard for classical first-order logic. Its absence would need to be stated. $\endgroup$ Commented Aug 30, 2017 at 9:17
  • $\begingroup$ Ah. You are right. "Modulo Theory". Concerning equality: as we are trying to explain easy things to people from outside Logic, it does not hurt to make the framework explicit. One more remark: replacing quantifiers by conjunctions and disjunctions is perfectly good. However, there are alternatives: since a formula with, say, m free variables defines an m-ary relation of A, the new formula can, after guessing all elements and checking which is which (modulo automorphisms), also explicitly "enumerate" all tuples, for which the old formula yields "true". $\endgroup$
    – Thomas S
    Commented Aug 30, 2017 at 10:12

To make what Emil said a bit more concrete: consider the formula expressing existence of k distinct objects. That shows we need unbounded number of quantifiers.

Now you have a formula with q quantifiers and your model has k objects in it you can express the formula by stating that k distinct objects exists and the relation between them can be expressed as a CNF.


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.