Quantifier rank

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 }${\displaystyle \varphi } be a first-order formula. The quantifier rank of ${\displaystyle \varphi }${\displaystyle \varphi }, written ${\displaystyle \operatorname {qr} (\varphi )}${\displaystyle \operatorname {qr} (\varphi )}, is defined as:

• ${\displaystyle \operatorname {qr} (\varphi )=0}${\displaystyle \operatorname {qr} (\varphi )=0}, if ${\displaystyle \varphi }${\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} (\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} (\lnot \varphi )=\operatorname {qr} (\varphi )}.
• ${\displaystyle \operatorname {qr} (\exists _{x}\varphi )=\operatorname {qr} (\varphi )+1}${\displaystyle \operatorname {qr} (\exists _{x}\varphi )=\operatorname {qr} (\varphi )+1}.
• ${\displaystyle \operatorname {qr} (\forall _{x}\varphi )=\operatorname {qr} (\varphi )+1}${\displaystyle \operatorname {qr} (\forall _{x}\varphi )=\operatorname {qr} (\varphi )+1}.

Remarks

• We write ${\displaystyle \operatorname {FO} [n]}${\displaystyle \operatorname {FO} [n]} for the set of all first-order formulas ${\displaystyle \varphi }${\displaystyle \varphi } with ${\displaystyle \operatorname {qr} (\varphi )\leq n}${\displaystyle \operatorname {qr} (\varphi )\leq n}.
• Relational ${\displaystyle \operatorname {FO} [n]}${\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 }${\displaystyle \varphi } is exactly the number of quantifiers appearing in ${\displaystyle \varphi }${\displaystyle \varphi }.

For fixed-point logic, with a least fixed-point operator ${\displaystyle \operatorname {LFP} }${\displaystyle \operatorname {LFP} }: ${\displaystyle \operatorname {qr} ([\operatorname {LFP} _{\phi }]y)=1+\operatorname {qr} (\phi )}${\displaystyle \operatorname {qr} ([\operatorname {LFP} _{\phi }]y)=1+\operatorname {qr} (\phi )}.

• A sentence of quantifier rank 2:

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

• A formula of quantifier rank 1:

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

• A formula of quantifier rank 0:

${\displaystyle R(x,y)\wedge x\neq y}${\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))}${\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))}${\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

• Finite model theory
• Model theory
• Predicate logic
• Quantifier (logic)

• Articles with short description
• Short description matches Wikidata
• Articles lacking in-text citations from September 2025
• All articles lacking in-text citations