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 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φ]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
)
)
