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
, if φ is atomic.
.
.
.
Remarks
- 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 Fixpoint logic, with a least fix point operator LFP:
![{\displaystyle qr([LFP_{\phi }]y)=1+qr(\phi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ca704216eaec1ecea0b1fb32f8fac28984890ad0)