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.
Quantifier Rank of a Formula in First-order language (FO)
Let φ be a FO formula. The quantifier rank of φ, written qr(φ), is defined as
q r ( φ ) = 0 , if φ is atomic. q r ( φ 1 ∧ φ 2 ) = q r ( φ 1 ∨ φ 2 ) = m a x ( q r ( φ 1 ) , q r ( φ 2 ) ) . q r ( ¬ φ ) = q r ( φ ) . q r ( ∃ x φ ) = q r ( φ ) + 1 .Remarks
We write FO[n] for the set of all first-order formulas φ with q r ( φ ) ≤ n .Relational FO[n] (without function symbols) is always of finite size, i.e. contains a finite number of formulasNotice 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φ]y) = 1 + qr( φ)...
A sentence of quantifier rank 2: ∀ x ∃ y R ( x , y ) A formula of quantifier rank 1: ∀ x R ( y , x ) ∧ ∃ x R ( x , y ) A formula of quantifier rank 0: R ( x , y ) ∧ x ≠ y A sentence in prenex normal form of quantifier rank 3: ∀ x ∃ y ∃ z ( ( x ≠ y ∧ x R y ) ∧ ( x ≠ z ∧ z R x ) ) A sentence, equivalent to the previous, although of quantifier rank 2: ∀ x ( ∃ y ( x ≠ y ∧ x R y ) ) ∧ ∃ z ( x ≠ z ∧ z R x ) ) 