quantifier rank

{{Short description|Depth of nesting of quantifiers in a formula}}

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.

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

= In first-order logic =

Let $\varphi$ be a first-order formula. The quantifier rank of $\varphi$ , written $\operatorname{qr}(\varphi)$ , is defined as:

$\operatorname{qr}(\varphi) = 0$ , if $\varphi$ is atomic.
$\operatorname{qr}(\varphi_1 \land \varphi_2) = \operatorname{qr}(\varphi_1 \lor \varphi_2) = \max(\operatorname{qr}(\varphi_1), \operatorname{qr}(\varphi_2))$ .
$\operatorname{qr}(\lnot \varphi) = \operatorname{qr}(\varphi)$ .
$\operatorname{qr}(\exists_x \varphi) = \operatorname{qr}(\varphi) + 1$ .
$\operatorname{qr}(\forall_x \varphi) = \operatorname{qr}(\varphi) + 1$ .

Remarks

We write $\operatorname{FO}[n]$ for the set of all first-order formulas $\varphi$ with $\operatorname{qr}(\varphi) \le n$ .
Relational $\operatorname{FO}[n]$ (without function symbols) is always of finite size, i.e. contains a finite number of formulas.
In prenex normal form, the quantifier rank of $\varphi$ is exactly the number of quantifiers appearing in $\varphi$ .

= In higher-order logic =

For fixed-point logic, with a least fixed-point operator $\operatorname{LFP}$ : $\operatorname{qr}([\operatorname{LFP}_\phi]y) = 1 + \operatorname{qr}( \phi )$ .

Examples

A sentence of quantifier rank 2:

: $\forall x\exists y R(x, y)$

A formula of quantifier rank 1:

: $\forall x R(y, x) \wedge \exists x R(x, y)$

A formula of quantifier rank 0:

: $R(x, y) \wedge x \neq y$

A sentence in prenex normal form of quantifier rank 3:

: $\forall x \exists y \exists z ((x \neq y \wedge x R y) \wedge (x \neq z \wedge z R x))$

A sentence, equivalent to the previous, although of quantifier rank 2:

: $\forall x (\exists y (x \neq y \wedge x R y)) \wedge \exists z (x \neq z \wedge z R x ))$

References

{{Citation

| last1=Ebbinghaus

| first1=Heinz-Dieter

| authorlink1=Heinz-Dieter Ebbinghaus

| last2=Flum

| first2=Jörg

| title=Finite Model Theory

| publisher=Springer

| isbn=978-3-540-60149-4

| year=1995

}}.

{{citation | last1=Grädel | first1=Erich | last2=Kolaitis | first2=Phokion G. | last3=Libkin | first3=Leonid | author3-link=Leonid Libkin | last4=Maarten | first4=Marx | last5=Spencer | first5=Joel | author5-link=Joel Spencer | last6=Vardi | first6=Moshe Y. | author6-link=Moshe Y. Vardi | last7=Venema | first7=Yde | last8=Weinstein | first8=Scott | title=Finite model theory and its applications | zbl=1133.03001 | series=Texts in Theoretical Computer Science. An EATCS Series | location=Berlin | publisher=Springer-Verlag | isbn=978-3-540-00428-8 | year=2007 | page=133 }}.

External links

[https://web.archive.org/web/20100704135152/http://www.math.upenn.edu/%7Enate/papers/thesis/thesis.pdf Quantifier Rank Spectrum of L-infinity-omega] BA Thesis, 2000

Category:Finite model theory

Category:Model theory

Category:Predicate logic

Category:Quantifier (logic)