mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...

, 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 Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premise ...

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 First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...

(FO) Let φ be a FO formula. The quantifier rank of φ, written qr(φ), is defined as *

qr(\varphi) = 0

, if φ is atomic. *

qr(\varphi_1 \land \varphi_2) = qr(\varphi_1 \lor \varphi_2) = max(qr(\varphi_1), qr(\varphi_2))

. *

qr(\lnot \varphi) = qr(\varphi)

. *

qr(\exists_x \varphi) = qr(\varphi) + 1

. Remarks * We write FO for the set of all

first-order In mathematics and other formal sciences, first-order or first order most often means either: * "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of high ...

formulas φ with

qr(\varphi) \le n

. * Relational FO (without function symbols) is always of finite size, i.e. contains a finite number of formulas * Notice that in

Prenex normal form A formula of the predicate calculus is in prenex normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier-free part, called the matrix. Together with the normal forms in prop ...

the Quantifier Rank of φ is exactly the number of quantifiers appearing in φ. Quantifier Rank of a higher order Formula * For

Fixpoint logic In mathematical logic, fixed-point logics are extensions of classical predicate logic that have been introduced to express recursion. Their development has been motivated by descriptive complexity theory and their relationship to database query la ...

, with a least fix point operator LFP:

) = 1 + 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 A formula of the predicate calculus is in prenex normal form (PNF) if it is written as a string of quantifiers and bound variables, called the prefix, followed by a quantifier-free part, called the matrix. Together with the normal forms in prop ...

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

* . * .

External links

Quantifier Rank Spectrum of L-infinity-omega
BA Thesis, 2000 {{Mathematical logic Finite model theory Model theory Predicate logic Quantifier (logic)

Definition

Examples

See also

References

External links