Quantifier rank

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 φ {\displaystyle \varphi } be a first-order formula. The quantifier rank of φ {\displaystyle \varphi } , written qr ⁡ ( φ ) {\displaystyle \operatorname {qr} (\varphi )} , is defined as:

qr ⁡ ( φ ) = 0 {\displaystyle \operatorname {qr} (\varphi )=0} , if φ {\displaystyle \varphi } is atomic.

qr ⁡ ( φ 1 ∧ φ 2 ) = qr ⁡ ( φ 1 ∨ φ 2 ) = max ( qr ⁡ ( φ 1 ) , qr ⁡ ( φ 2 ) ) {\displaystyle \operatorname {qr} (\varphi _{1}\land \varphi _{2})=\operatorname {qr} (\varphi _{1}\lor \varphi _{2})=\max(\operatorname {qr} (\varphi _{1}),\operatorname {qr} (\varphi _{2}))} .

qr ⁡ ( ¬ φ ) = qr ⁡ ( φ ) {\displaystyle \operatorname {qr} (\lnot \varphi )=\operatorname {qr} (\varphi )} .

qr ⁡ ( ∃ x φ ) = qr ⁡ ( φ ) + 1 {\displaystyle \operatorname {qr} (\exists _{x}\varphi )=\operatorname {qr} (\varphi )+1} .

qr ⁡ ( ∀ x φ ) = qr ⁡ ( φ ) + 1 {\displaystyle \operatorname {qr} (\forall _{x}\varphi )=\operatorname {qr} (\varphi )+1} . Remarks

We write FO ⁡ [ n ] {\displaystyle \operatorname {FO} [n]} for the set of all first-order formulas φ {\displaystyle \varphi } with qr ⁡ ( φ ) ≤ n {\displaystyle \operatorname {qr} (\varphi )\leq n} . Relational FO ⁡ [ n ] {\displaystyle \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 φ {\displaystyle \varphi } is exactly the number of quantifiers appearing in φ {\displaystyle \varphi } .

In higher-order logic For fixed-point logic, with a least fixed-point operator LFP {\displaystyle \operatorname {LFP} } : qr ⁡ ( [ LFP ϕ ] y ) = 1 + qr ⁡ ( ϕ ) {\displaystyle \operatorname {qr} ([\operatorname {LFP} _{\phi }]y)=1+\operatorname {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}

A sentence in prenex normal form of quantifier rank 3:

∀ 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))}

Tags