Quantifier rank explained

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.

Notice that 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

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

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

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

Remarks

• We write FO[n] for the set of all first-order formulas φ with

qr(\varphi) \le 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:

qr([LFP _{\phi]y)} = 1 + qr( \phi )

Examples

• A sentence of quantifier rank 2:

\forall x\exists y R(x, y)

• A formula of quantifier rank 1:

\forall x R(y, x) \wedge \exists x R(x, y)

• A formula of quantifier rank 0:

R(x, y) \wedge x ≠ y

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

\forall x \exists y \exists z ((x ≠ y \wedge x R y) \wedge (x ≠ z \wedge z R x))

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

\forall x (\exists y (x ≠ y \wedge x R y)) \wedge \exists z (x ≠ z \wedge z R x ))

See also

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

References

• .
• .

External links

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