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
- , if φ is atomic.
- We write FO[n] for the set of all first-order formulas φ with .
- 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 Fix Point 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 formula in prenex normal form of quantifier rank 3:
- A formula, equivalent to the latter, although of quantifier rank 2:
- Quantifier Rank Spectrum of L-infinity-omega BA Thesis, 2000