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
q
r
(
φ φ -->
)
=
0
{\displaystyle qr(\varphi )=0}
q
r
(
φ φ -->
1
∧ ∧ -->
φ φ -->
2
)
=
q
r
(
φ φ -->
1
∨ ∨ -->
φ φ -->
2
)
=
m
a
x
(
q
r
(
φ φ -->
1
)
,
q
r
(
φ φ -->
2
)
)
{\displaystyle qr(\varphi _{1}\land \varphi _{2})=qr(\varphi _{1}\lor \varphi _{2})=max(qr(\varphi _{1}),qr(\varphi _{2}))}
q
r
(
¬ ¬ -->
φ φ -->
)
=
q
r
(
φ φ -->
)
{\displaystyle qr(\lnot \varphi )=qr(\varphi )}
q
r
(
∃ ∃ -->
x
φ φ -->
)
=
q
r
(
φ φ -->
)
+
1
{\displaystyle qr(\exists _{x}\varphi )=qr(\varphi )+1}
q
r
(
∀ ∀ -->
x
φ φ -->
)
=
q
r
(
φ φ -->
)
+
1
{\displaystyle qr(\forall _{x}\varphi )=qr(\varphi )+1}
Remarks
We write FO[n] for the set of all first-order formulas φ with
q
r
(
φ φ -->
)
≤ ≤ -->
n
{\displaystyle qr(\varphi )\leq 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:
q
r
(
[
L
F
P
ϕ ϕ -->
]
y
)
=
1
+
q
r
(
ϕ ϕ -->
)
{\displaystyle qr([LFP_{\phi }]y)=1+qr(\phi )}
Examples
A sentence of quantifier rank 2:
∀ ∀ -->
x
∃ ∃ -->
y
R
(
x
,
y
)
{\displaystyle \forall x\exists yR(x,y)}
A formula of quantifier rank 1:
∀ ∀ -->
x
R
(
y
,
x
)
∧ ∧ -->
∃ ∃ -->
x
R
(
x
,
y
)
{\displaystyle \forall xR(y,x)\wedge \exists xR(x,y)}
A formula of quantifier rank 0:
R
(
x
,
y
)
∧ ∧ -->
x
≠ ≠ -->
y
{\displaystyle R(x,y)\wedge x\neq y}
∀ ∀ -->
x
∃ ∃ -->
y
∃ ∃ -->
z
(
(
x
≠ ≠ -->
y
∧ ∧ -->
x
R
y
)
∧ ∧ -->
(
x
≠ ≠ -->
z
∧ ∧ -->
z
R
x
)
)
{\displaystyle \forall x\exists y\exists z((x\neq y\wedge xRy)\wedge (x\neq z\wedge zRx))}
A sentence, equivalent to the previous, although of quantifier rank 2:
∀ ∀ -->
x
(
∃ ∃ -->
y
(
x
≠ ≠ -->
y
∧ ∧ -->
x
R
y
)
)
∧ ∧ -->
∃ ∃ -->
z
(
x
≠ ≠ -->
z
∧ ∧ -->
z
R
x
)
)
{\displaystyle \forall x(\exists y(x\neq y\wedge xRy))\wedge \exists z(x\neq z\wedge zRx))}
See also
References
Ebbinghaus, Heinz-Dieter ; Flum, Jörg (1995), Finite Model Theory , Springer , ISBN 978-3-540-60149-4 Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid ; Maarten, Marx; Spencer, Joel ; Vardi, Moshe Y. ; Venema, Yde; Weinstein, Scott (2007), Finite model theory and its applications , Texts in Theoretical Computer Science. An EATCS Series, Berlin: Springer-Verlag , p. 133, ISBN 978-3-540-00428-8 Zbl 1133.03001
External links
![{\displaystyle qr([LFP_{\phi }]y)=1+qr(\phi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ca704216eaec1ecea0b1fb32f8fac28984890ad0)
