Quantifier rank

Let ${\displaystyle \varphi }$ be a first-order formula. The quantifier rank of ${\displaystyle \varphi }$, written ${\displaystyle \operatorname {qr} (\varphi )}$, is defined as:

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

Remarks

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

For fixed-point logic, with a least fixed-point operator ${\displaystyle \operatorname {LFP} }$: ${\displaystyle \operatorname {qr} ([\operatorname {LFP} _{\phi }]y)=1+\operatorname {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))}$

• Ehrenfeucht–Fraïssé game