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

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

CC BY-SA 3.0
2017-08-27T20:52:00.043Z
2017-08-27T20:52:00.043Z
Kaveh
<p>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.</p>

CC BY-SA 3.0
2017-08-30T09:12:07.793Z
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.
Thomas S
CC BY-SA 3.0
2017-08-30T09:17:14.013Z
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.
Emil Jeřábek
CC BY-SA 3.0
2017-08-30T10:12:24.663Z
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".
Thomas S
CC BY-SA 3.0
2017-08-27T16:46:50.267Z
2017-08-27T16:46:50.267Z
Emil Jeřábek
<p>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) &gt; q $ there is a $ \varphi'\in\mathfrak{T} $ with $ qr(\varphi')\leq q $ and $ \varphi'\equiv\varphi $ ?</p>

CC BY-SA 3.0
2017-08-27T21:10:30.267Z
Isn't this a question for Mathoverflow rather than CS theory?
Andrej Bauer
CC BY-SA 3.0
2017-08-27T21:37:51.650Z
@Andrej, Finite model theory and descriptive complexity are also considered part of TCS.
Kaveh
CC BY-SA 3.0
2017-08-28T06:02:56.703Z
Excellent, so it's like Bob Harper said once: math is a special case of computer science.
Andrej Bauer
CC BY-SA 3.0
2017-09-06T01:53:26.557Z
Computer science is also a special case of math, and they are both also special cases of logic, and vice versa.
fhyve
<co.combinatorics><lo.logic><relational-structures>
Does the first order theory of a finite structure have bounded quantifier rank?
D. Rusin
# Does the first order theory of a finite structure have bounded quantifier rank?

(Asked by: username_0 on 2017-08-27)

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 $ ?

**Tags:** co.combinatorics, lo.logic, relational-structures
> **Comments:**
> **username_1**: Isn't this a question for Mathoverflow rather than CS theory?  
> **username_2**: @Andrej, Finite model theory and descriptive complexity are also considered part of TCS.  
> **username_1**: Excellent, so it's like Bob Harper said once: math is a special case of computer science.  
> **username_3**: Computer science is also a special case of math, and they are both also special cases of logic, and vice versa.  

---

## 2 answers

### Answer by username_4 on 2017-08-27. Score: 12 | Accepted answer

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.

> **Comments:**
> **username_5**: 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.  
> **username_4**: 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.  
> **username_5**: 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".  

---

### Answer by username_2 on 2017-08-27. Score: 3

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.


---

