Quantifier rank

Template:Short description Template:No footnotes 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.

Definition

In first-order logic

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

• $\mathrm{qr}(\phi )=0$, if $\phi$ is atomic.
• $\mathrm{qr}({\phi }_1\wedge {\phi }_2)=\mathrm{qr}({\phi }_1\vee {\phi }_2)=max(\mathrm{qr}({\phi }_1),\mathrm{qr}({\phi }_2))$.
• $\mathrm{qr}(\mathrm{\neg }\phi )=\mathrm{qr}(\phi )$.
• $\mathrm{qr}({\mathrm{\exists }}_x\phi )=\mathrm{qr}(\phi )+1$.
• $\mathrm{qr}({\mathrm{\forall }}_x\phi )=\mathrm{qr}(\phi )+1$.

Remarks

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

In higher-order logic

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

Examples

• A sentence of quantifier rank 2:

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

• A formula of quantifier rank 1:

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

• A formula of quantifier rank 0:

$R(x,y)\wedge x\ne y$

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

$\mathrm{\forall }x\mathrm{\exists }y\mathrm{\exists }z((x\ne y\wedge xRy)\wedge (x\ne z\wedge zRx))$

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

$\mathrm{\forall }x(\mathrm{\exists }y(x\ne y\wedge xRy))\wedge \mathrm{\exists }z(x\ne z\wedge zRx))$

See also

• Ehrenfeucht–Fraïssé game

References

• Template:Citation.
• Template:Citation.

External links

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