Quantifier rank

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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.

Prerequisits: Formula, Quantifier.

Definition[edit]

Quantifier Rank of a Formula in First-Order language (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[n] for the set of all first-order formulas φ with qr(\varphi) \le 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 Fix Point Logic, with a least fix point operator LFP:
qr([LFPφ]y) = 1 + qr( φ)

...

Examples[edit]

  • 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 formula in prenex normal form of quantifier rank 3:
\forall x\exists y\exists z ((\lnot x = y) \land x R y )  \land ( (\lnot x = z) \land z R x )
  • A formula, equivalent to the latter, although of quantifier rank 2:
\forall x ( \exists y ((\lnot x = y) \land x R y ) ) \land ( \exists z ((\lnot x = z) \land z R x ) )

External links[edit]

See also[edit]

References[edit]