Quantifier rank

Last updated February 12, 2024

This mathematical logic-related article is a stub. You can help Wikipedia by expanding it.

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

$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$ .
$qr(\forall _{x}\varphi )=qr(\varphi )+1$ .

Remarks

We write FO[n] for the set of all first-order formulas φ with $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: $qr([LFP_{\phi }]y)=1+qr(\phi )$

Examples

A sentence of quantifier rank 2:

\forall x\exists yR(x,y)

A formula of quantifier rank 1:

\forall xR(y,x)\wedge \exists xR(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 xRy)\wedge (x\neq z\wedge zRx))

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

\forall x(\exists y(x\neq y\wedge xRy))\wedge \exists z(x\neq z\wedge zRx))

Related Research Articles

In mathematics and computer science, the Entscheidungsproblem is a challenge posed by David Hilbert and Wilhelm Ackermann in 1928. The problem asks for an algorithm that considers, as input, a statement and answers "yes" or "no" according to whether the statement is universally valid, i.e., valid in every structure.

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 quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 is not easy to read today; it uses concepts and formalisms that are no longer used and terminology that is often obscure. The version given below attempts to represent all the steps in the proof and all the important ideas faithfully, while restating the proof in the modern language of mathematical logic. This outline should not be considered a rigorous proof of the theorem.

In mathematical logic, model theory is the study of the relationship between formal theories, and their models. The aspects investigated include the number and size of models of a theory, the relationship of different models to each other, and their interaction with the formal language itself. In particular, model theorists also investigate the sets that can be defined in a model of a theory, and the relationship of such definable sets to each other. As a separate discipline, model theory goes back to Alfred Tarski, who first used the term "Theory of Models" in publication in 1954. Since the 1970s, the subject has been shaped decisively by Saharon Shelah's stability theory.

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 propositional logic, it provides a canonical normal form useful in automated theorem proving.

In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers.

In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories (Rathjen 2005).

Descriptive complexity is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity classes in the polynomial hierarchy, is precisely the class of languages expressible by statements of second-order logic. This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods and providing additional evidence that the main complexity classes are somehow "natural" and not tied to the specific abstract machines used to define them.

The Kripke–Platek set theory with urelements (KPU) is an axiom system for set theory with urelements, based on the traditional (urelement-free) Kripke–Platek set theory. It is considerably weaker than the (relatively) familiar system ZFU. The purpose of allowing urelements is to allow large or high-complexity objects to be included in the theory's transitive models without disrupting the usual well-ordering and recursion-theoretic properties of the constructible universe; KP is so weak that this is hard to do by traditional means.

Finite model theory is a subarea of model theory. Model theory is the branch of logic which deals with the relation between a formal language (syntax) and its interpretations (semantics). Finite model theory is a restriction of model theory to interpretations on finite structures, which have a finite universe.

Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form $and, where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic.$

In logic a branching quantifier, also called a Henkin quantifier, finite partially ordered quantifier or even nonlinear quantifier, is a partial ordering

In model theory and related areas of mathematics, a type is an object that describes how a element or finite collection of elements in a mathematical structure might behave. More precisely, it is a set of first-order formulas in a language L with free variables x₁, x₂,..., x_n that are true of a set of n-tuples of an L-structure $. Depending on the context, types can be complete or partial and they may use a fixed set of constants, A, from the structure . The question of which types represent actual elements of leads to the ideas of saturated models and omitting types .$

The Herbrandization of a logical formula is a construction that is dual to the Skolemization of a formula. Thoralf Skolem had considered the Skolemizations of formulas in prenex form as part of his proof of the Löwenheim–Skolem theorem. Herbrand worked with this dual notion of Herbrandization, generalized to apply to non-prenex formulas as well, in order to prove Herbrand's theorem.

In axiomatic set theory, the axiom schema of predicative separation, or of restricted, or Δ₀ separation, is a schema of axioms which is a restriction of the usual axiom schema of separation in Zermelo–Fraenkel set theory. This name Δ₀ stems from the Lévy hierarchy, in analogy with the arithmetic hierarchy.

In set theory and mathematical logic, the Lévy hierarchy, introduced by Azriel Lévy in 1965, is a hierarchy of formulas in the formal language of the Zermelo–Fraenkel set theory, which is typically called just the language of set theory. This is analogous to the arithmetical hierarchy, which provides a similar classification for sentences of the language of arithmetic.

In mathematical logic the theory of pure equality is a first-order theory. It has a signature consisting of only the equality relation symbol, and includes no non-logical axioms at all.

Dependence logic is a logical formalism, created by Jouko Väänänen, which adds dependence atoms to the language of first-order logic. A dependence atom is an expression of the form $, where are terms, and corresponds to the statement that the value of is functionally dependent on the values of .$

In mathematical logic, the spectrum of a sentence is the set of natural numbers occurring as the size of a finite model in which a given sentence is true. By a result in descriptive complexity, a set of natural numbers is a spectrum if and only if it can be recognized in non-deterministic exponential time.

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 languages, in particular to Datalog.

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

Quantifier Rank Spectrum of L-infinity-omega BA Thesis, 2000

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.