Quantifier Rank of a Formula in First-order language (FO)

Let φ be a FO formula. The quantifier rank of φ, written qr(φ), is defined as

• ${\displaystyle qr(\varphi )=0}$ , if φ is atomic.
• ${\displaystyle qr(\varphi _{1}\land \varphi _{2})=qr(\varphi _{1}\lor \varphi _{2})=max(qr(\varphi _{1}),qr(\varphi _{2}))}$ .
• ${\displaystyle qr(\lnot \varphi )=qr(\varphi )}$ .
• ${\displaystyle qr(\exists _{x}\varphi )=qr(\varphi )+1}$ .
• ${\displaystyle qr(\forall _{x}\varphi )=qr(\varphi )+1}$ .

Remarks

• We write FO[n] for the set of all first-order formulas φ with ${\displaystyle qr(\varphi )\leq n}$ .
• Relational FO[n] (without function symbols) is always of finite size, i.e. contains a finite number of formulas
• Notice that in Prenex normal form the Quantifier Rank of φ is exactly the number of quantifiers appearing in φ.

Quantifier Rank of a higher order Formula

• For Fixpoint logic, with a least fix point operator LFP: ${\displaystyle qr([LFP_{\phi }]y)=1+qr(\phi )}$ 

• A sentence of quantifier rank 2:

${\displaystyle \forall x\exists yR(x,y)}$ 

• A formula of quantifier rank 1:

${\displaystyle \forall xR(y,x)\wedge \exists xR(x,y)}$ 

• A formula of quantifier rank 0:

${\displaystyle R(x,y)\wedge x\neq y}$ 

• A sentence in prenex normal form of quantifier rank 3:

${\displaystyle \forall x\exists y\exists z((x\neq y\wedge xRy)\wedge (x\neq z\wedge zRx))}$ 

• A sentence, equivalent to the previous, although of quantifier rank 2:

${\displaystyle \forall x(\exists y(x\neq y\wedge xRy))\wedge \exists z(x\neq z\wedge zRx))}$ 

• Prenex normal form
• Ehrenfeucht–Fraïssé_game
• Quantifier

• Ebbinghaus, Heinz-Dieter; Flum, Jörg (1995), Finite Model Theory, Springer, ISBN 978-3-540-60149-4.
• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel; Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007), Finite model theory and its applications, Texts in Theoretical Computer Science. An EATCS Series, Berlin: Springer-Verlag, p. 133, ISBN 978-3-540-00428-8, Zbl 1133.03001.

• Quantifier Rank Spectrum of L-infinity-omega BA Thesis, 2000