This article includes a list of references, but its sources remain unclear because it has insufficient inline citations .(January 2013) (Learn how and when to remove this template message) |

In mathematics and logic, the term "uniqueness" refers to the property of being the one and only object satisfying a certain condition.^{ [1] }^{ [2] } This sort of quantification is known as **uniqueness quantification** or **unique existential quantification**, and is often denoted with the symbols "∃!"^{ [3] } or "∃_{=1}". For example, the formal statement

- Proving uniqueness
- Reduction to ordinary existential and universal quantification
- Generalizations
- See also
- References
- Bibliography

may be read as "there is exactly one natural number such that ".

The most common technique to prove the unique existence of a certain object is to first prove the existence of the entity with the desired condition, and then to prove that any two such entities (say, * and **) must be equal to each other (i.e. ).*

For example, to show that the equation has exactly one solution, one would first start by establishing that at least one solution exists, namely 3; the proof of this part is simply the verification that the equation below holds:

To establish the uniqueness of the solution, one would then proceed by assuming that there are two solutions, namely * and **, satisfying . That is,*

By transitivity of equality,

Subtracting 2 from both sides then yields

which completes the proof that 3 is the unique solution of .

In general, both existence (there exists *at least* one object) and uniqueness (there exists *at most* one object) must be proven, in order to conclude that there exists exactly one object satisfying a said condition.

An alternative way to prove uniqueness is to prove that there exists an object satisfying the condition, and then to prove that every object satisfying the condition must be equal to .^{ [1] }

Uniqueness quantification can be expressed in terms of the existential and universal quantifiers of predicate logic, by defining the formula to mean

which is logically equivalent to

An equivalent definition that separates the notions of existence and uniqueness into two clauses, at the expense of brevity, is

Another equivalent definition, which has the advantage of brevity, is

The uniqueness quantification can be generalized into counting quantification (or numerical quantification^{ [4] }). This includes both quantification of the form "exactly *k* objects exist such that …" as well as "infinitely many objects exist such that …" and "only finitely many objects exist such that…". The first of these forms is expressible using ordinary quantifiers, but the latter two cannot be expressed in ordinary first-order logic.^{ [5] }

Uniqueness depends on a notion of equality. Loosening this to some coarser equivalence relation yields quantification of uniqueness up to that equivalence (under this framework, regular uniqueness is "uniqueness up to equality"). For example, many concepts in category theory are defined to be unique up to isomorphism.

**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" and *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 the philosophy of mathematics, **constructivism** asserts that it is necessary to find a mathematical object to prove that it exists. In classical mathematics, one can prove the existence of a mathematical object without "finding" that object explicitly, by assuming its non-existence and then deriving a contradiction from that assumption. This proof by contradiction is not constructively valid. The constructive viewpoint involves a verificational interpretation of the existential quantifier, which is at odds with its classical interpretation.

In mathematical logic, the **Peano axioms**, also known as the **Dedekind–Peano axioms** or the **Peano postulates**, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly unchanged in a number of metamathematical investigations, including research into fundamental questions of whether number theory is consistent and complete.

In Boolean logic, a formula is in **conjunctive normal form** (**CNF**) or **clausal normal form** if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is **an AND of ORs**. As a canonical normal form, it is useful in automated theorem proving and circuit theory.

In predicate logic, an **existential quantification** is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". Some sources use the term **existentialization** to refer to existential quantification. It is usually denoted by the logical operator symbol ∃, which, when used together with a predicate variable, is called an **existential quantifier**. Existential quantification is distinct from universal quantification, which asserts that the property or relation holds for *all* members of the domain.

In set theory, **Zermelo–Fraenkel set theory**, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as Russell's paradox. Today, Zermelo–Fraenkel set theory, with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics. Zermelo–Fraenkel set theory with the axiom of choice included is abbreviated **ZFC**, where C stands for "choice", and **ZF** refers to the axioms of Zermelo–Fraenkel set theory with the axiom of choice excluded.

In formal logic and related branches of mathematics, a **functional predicate**, or **function symbol**, is a logical symbol that may be applied to an object term to produce another object term. Functional predicates are also sometimes called *mappings*, but that term has other meanings as well. In a model, a function symbol will be modelled by a function.

In mathematics, a **Heyting algebra** is a bounded lattice equipped with a binary operation *a* → *b* of *implication* such that ≤ *b* is equivalent to *c* ≤. From a logical standpoint, *A* → *B* is by this definition the weakest proposition for which modus ponens, the inference rule *A* → *B*, *A* ⊢ *B*, is sound. Like Boolean algebras, Heyting algebras form a variety axiomatizable with finitely many equations. Heyting algebras were introduced by Arend Heyting (1930) to formalize intuitionistic logic.

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**.

In the foundations of mathematics, **von Neumann–Bernays–Gödel set theory** (**NBG**) is an axiomatic set theory that is a conservative extension of Zermelo–Fraenkel-Choice set theory (ZFC). NBG introduces the notion of class, which is a collection of sets defined by a formula whose quantifiers range only over sets. NBG can define classes that are larger than sets, such as the class of all sets and the class of all ordinals. Morse–Kelley set theory (MK) allows classes to be defined by formulas whose quantifiers range over classes. NBG is finitely axiomatizable, while ZFC and MK are not.

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

In the foundations of mathematics, **Morse–Kelley set theory** (**MK**), **Kelley–Morse set theory** (**KM**), **Morse–Tarski set theory** (**MT**), **Quine–Morse set theory** (**QM**) or the **system of Quine and Morse** is a first order axiomatic set theory that is closely related to von Neumann–Bernays–Gödel set theory (NBG). While von Neumann–Bernays–Gödel set theory restricts the bound variables in the schematic formula appearing in the axiom schema of Class Comprehension to range over sets alone, Morse–Kelley set theory allows these bound variables to range over proper classes as well as sets, as first suggested by Quine in 1940 for his system ML.

**Constructive set theory** is an approach to mathematical constructivism following the program of axiomatic set theory, using the usual first-order language of classical set theory. The logic is constructive, but this is not to be confused with a constructive types approach.

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 mathematical logic, a **Lindström quantifier** is a generalized polyadic quantifier. Lindström quantifiers generalize first-order quantifiers, such as the existential quantifier, the universal quantifier, and the counting quantifiers. They were introduced by Per Lindström in 1966. They were later studied for their applications in logic in computer science and database query languages.

**General set theory** (**GST**) is George Boolos's (1998) name for a fragment of the axiomatic set theory Z. GST is sufficient for all mathematics not requiring infinite sets, and is the weakest known set theory whose theorems include the Peano axioms.

In natural languages, a quantifier turns a sentence about something having some property into a sentence about the number (quantity) of things having the property. Examples of quantifiers in English are "all", "some", "many", "few", "most", and "no"; examples of quantified sentences are "all people are mortal", "some people are mortal", and "no people are mortal", they are considered to be true, true, and false, respectively.

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.

- 1 2 "The Definitive Glossary of Higher Mathematical Jargon — Uniqueness".
*Math Vault*. 2019-08-01. Retrieved 2019-12-15. - ↑ Weisstein, Eric W. "Uniqueness Theorem".
*mathworld.wolfram.com*. Retrieved 2019-12-15. - ↑ "2.5 Uniqueness Arguments".
*www.whitman.edu*. Retrieved 2019-12-15. - ↑ Helman, Glen (August 1, 2013). "Numerical quantification" (PDF).
*persweb.wabash.edu*. Retrieved 2019-12-14. - ↑ This is a consequence of the compactness theorem.

- Kleene, Stephen (1952).
*Introduction to Metamathematics*. Ishi Press International. p. 199. - Andrews, Peter B. (2002).
*An introduction to mathematical logic and type theory to truth through proof*(2. ed.). Dordrecht: Kluwer Acad. Publ. p. 233. ISBN 1-4020-0763-9.

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.

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.