This article includes a list of references, related reading, or external links, but its sources remain unclear because it lacks inline citations. Please help improve this article by introducing more precise citations. (September 2025) (Learn how and when to remove this message)

In mathematical logic, the quantifier rank of a formula is the depth of nesting of its quantifiers. It plays an essential role in model theory.

The quantifier rank is a property of the formula itself (i.e. the expression in a language). Thus two logically equivalent formulae can have different quantifier ranks, when they express the same thing in different ways.

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

• 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

This mathematical logic-related article is a stub. You can help Wikipedia by expanding it.

• v
• t
• e