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$ Aug 27 '17 at 21:10
  • 6
    $\begingroup$ @Andrej, Finite model theory and descriptive complexity are also considered part of TCS. $\endgroup$
    – Kaveh
    Aug 27 '17 at 21:37
  • 1
    $\begingroup$ Excellent, so it's like Bob Harper said once: math is a special case of computer science. $\endgroup$ Aug 28 '17 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
    Sep 6 '17 at 1:53

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
    Aug 30 '17 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$ Aug 30 '17 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
    Aug 30 '17 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, privacy policy and cookie policy

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