Movatterモバイル変換

Existential quantification

From Wikipedia, the free encyclopedia

Mathematical use of "there exists"

"∃ " and "∄ " redirect here. For the letter turned E, seeƎ. For the Japanese katakana ヨ, seeYo (kana). For the Ukrainian nightclub also called ∄ , seeK41 (nightclub).

Existential quantification
Type	Quantifier
Field	Mathematical logic
Statement	$\exists xP(x)$ is true when $P(x)$ is true for at least one value of $x {\displaystyle x}$ .
Symbolic statement	$\exists xP(x)$

Inpredicate logic, anexistential quantification is a type ofquantifier which asserts theexistence of an object with a givenproperty. It is usually denoted by thelogical operator symbol ∃, which, when used together with a predicate variable, is called anexistential quantifier ("∃x" or "∃(x)" or "(∃x)"^[1]), read as "there exists", "there is at least one", or "for some". Existential quantification is distinct fromuniversal quantification ("for all"), which asserts that the property or relation holds forall members of the domain.^[2]^[3] Some sources use the termexistentialization to refer to existential quantification.^[4]

Quantification in general is covered in the article onquantification (logic). The existential quantifier is encoded asU+2203 ∃THERE EXISTS inUnicode, and as\exists inLaTeX and related formula editors.

Basics

[edit]

Consider theformal sentence

For some natural number

n {\displaystyle n}

n\times n=25

This is a single statement using existential quantification. It is roughly analogous to the informal sentence "Either $0\times 0=25$ , or $1\times 1=25$ , or $2\times 2=25$ , or... and so on," but more precise, because it doesn't need us to infer the meaning of the phrase "and so on." (In particular, the sentence explicitly specifies itsdomain of discourse to be the natural numbers, not, for example, thereal numbers.)

This particular example is true, because 5 is a natural number, and when we substitute 5 forn, we produce the true statement $5\times 5=25$ . It does not matter that " $n\times n=25$ " is true only for that single natural number, 5; the existence of a singlesolution is enough to prove this existential quantification to be true.

In contrast, "For someeven number $n {\displaystyle n}$ , $n\times n=25$ " is false, because there are no even solutions. Thedomain of discourse, which specifies the values the variablen is allowed to take, is therefore critical to a statement's trueness or falseness.Logical conjunctions are used to restrict the domain of discourse to fulfill a given predicate. For example, the sentence

For some positive odd number

n {\displaystyle n}

n\times n=25

islogically equivalent to the sentence

For some natural number

n {\displaystyle n}

n {\displaystyle n}

is odd and

n\times n=25

Themathematical proof of an existential statement about "some" object may be achieved either by aconstructive proof, which exhibits an object satisfying the "some" statement, or by anonconstructive proof, which shows that there must be such an object without concretely exhibiting one.

Notation

[edit]

Insymbolic logic, "∃" (a turned letter "E" in asans-serif font, Unicode U+2203) is used to indicate existential quantification. For example, the notation $\exists {n}{\in }\mathbb {N} :n\times n=25$ represents the (true) statement

There exists some

n {\displaystyle n}

in the set ofnatural numbers such that

n\times n=25

The symbol's first usage is thought to be byGiuseppe Peano inFormulario mathematico (1896). Afterwards,Bertrand Russell popularised its use as the existential quantifier. Through his research in set theory, Peano also introduced the symbols $\cap$ and $\cup$ to respectively denote the intersection and union of sets.^[5]

Properties

[edit]

Negation

[edit]

A quantified propositional function is a statement; thus, like statements, quantified functions can be negated. The $\lnot \$ symbol is used to denote negation.

For example, ifP(x) is the predicate "x is greater than 0 and less than 1", then, for a domain of discourseX of all natural numbers, the existential quantification "There exists a natural numberx which is greater than 0 and less than 1" can be symbolically stated as:

\exists {x}{\in }\mathbf {X} \,P(x)

This can be demonstrated to be false. Truthfully, it must be said, "It is not the case that there is a natural numberx that is greater than 0 and less than 1", or, symbolically:

\lnot \ \exists {x}{\in }\mathbf {X} \,P(x)

If there is no element of the domain of discourse for which the statement is true, then it must be false for all of those elements. That is, the negation of

\exists {x}{\in }\mathbf {X} \,P(x)

is logically equivalent to "For any natural numberx,x is not greater than 0 and less than 1", or:

\forall {x}{\in }\mathbf {X} \,\lnot P(x)

Generally, then, the negation of apropositional function's existential quantification is auniversal quantification of that propositional function's negation; symbolically,

\lnot \ \exists {x}{\in }\mathbf {X} \,P(x)\equiv \ \forall {x}{\in }\mathbf {X} \,\lnot P(x)

(This is a generalization ofDe Morgan's laws to predicate logic.)

A common error is stating "all persons are not married" (i.e., "there exists no person who is married"), when "not all persons are married" (i.e., "there exists a person who is not married") is intended:

\lnot \ \exists {x}{\in }\mathbf {X} \,P(x)\equiv \ \forall {x}{\in }\mathbf {X} \,\lnot P(x)\not \equiv \ \lnot \ \forall {x}{\in }\mathbf {X} \,P(x)\equiv \ \exists {x}{\in }\mathbf {X} \,\lnot P(x)

Negation is also expressible through a statement of "for no", as opposed to "for some":

\nexists {x}{\in }\mathbf {X} \,P(x)\equiv \lnot \ \exists {x}{\in }\mathbf {X} \,P(x)

Unlike the universal quantifier, the existential quantifier distributes over logical disjunctions:

$\exists {x}{\in }\mathbf {X} \,P(x)\lor Q(x)\to \ (\exists {x}{\in }\mathbf {X} \,P(x)\lor \exists {x}{\in }\mathbf {X} \,Q(x))$

Rules of inference

[edit]

Transformation rules
Propositional calculus
Rules of inference (List)
Implication introduction / elimination (modus ponens) Biconditional introduction / elimination Conjunction introduction / elimination Disjunction introduction / elimination Disjunctive / hypothetical syllogism Constructive / destructive dilemma Absorption / modus tollens / modus ponendo tollens Modus non excipiens Negation introduction
Rules of replacement
Associativity Commutativity Distributivity Double negation De Morgan's laws Transposition Material implication Exportation Tautology
Predicate logic
Rules of inference
Universal generalization / instantiation Existential generalization / instantiation
v t e

Arule of inference is a rule justifying a logical step from hypothesis to conclusion. There are several rules of inference which utilize the existential quantifier.

Existential introduction (∃I) concludes that, if the propositional function is known to be true for a particular element of the domain of discourse, then it must be true that there exists an element for which the proposition function is true. Symbolically,

P(a)\to \ \exists {x}{\in }\mathbf {X} \,P(x)

Existential instantiation, when conducted in a Fitch style deduction, proceeds by entering a new sub-derivation while substituting an existentially quantified variable for a subject—which does not appear within any active sub-derivation. If a conclusion can be reached within this sub-derivation in which the substituted subject does not appear, then one can exit that sub-derivation with that conclusion. The reasoning behind existential elimination (∃E) is as follows: If it is given that there exists an element for which the proposition function is true, and if a conclusion can be reached by giving that element an arbitrary name, that conclusion isnecessarily true, as long as it does not contain the name. Symbolically, for an arbitraryc and for a propositionQ in whichc does not appear:

\exists {x}{\in }\mathbf {X} \,P(x)\to \ ((P(c)\to \ Q)\to \ Q)

$P(c)\to \ Q$ must be true for all values ofc over the same domainX; else, the logic does not follow: Ifc is not arbitrary, and is instead a specific element of the domain of discourse, then statingP(c) might unjustifiably give more information about that object.

The empty set

[edit]

The formula $\exists {x}{\in }\varnothing \,P(x)$ is always false, regardless ofP(x). This is because $\varnothing$ denotes theempty set, and nox of any description – let alone anx fulfilling a given predicateP(x) – exist in the empty set. See alsoVacuous truth for more information.

As adjoint

[edit]

Main article:Universal quantification § As adjoint

Incategory theory and the theory ofelementary topoi, the existential quantifier can be understood as theleft adjoint of afunctor betweenpower sets, theinverse image functor of a function between sets; likewise, theuniversal quantifier is theright adjoint.^[6]

Notes

[edit]

^Bergmann, Merrie (2014).The Logic Book. McGraw Hill.ISBN 978-0-07-803841-9.
^"Predicates and Quantifiers".www.csm.ornl.gov. Retrieved2020-09-04.
^"1.2 Quantifiers".www.whitman.edu. Retrieved2020-09-04.
^Allen, Colin; Hand, Michael (2001).Logic Primer. MIT Press.ISBN 0262303965.
^Stephen Webb (2018).Clash of Symbols. Springer Cham. pp. 210–211.doi:10.1007/978-3-319-71350-2.ISBN 978-3-319-71349-6.
^Saunders Mac Lane, Ieke Moerdijk, (1992):Sheaves in Geometry and Logic Springer-VerlagISBN 0-387-97710-4.See p. 58.

References

[edit]

Hinman, P. (2005).Fundamentals of Mathematical Logic. A K Peters.ISBN 1-56881-262-0.

Authority control databases	GND

Commonlogical symbols

∧ or &

¬ or ~

↔ or ≡

universal
quantification

∃

existential
quantification

General

Theorems
(list),
paradoxes

Logics

Traditional	Classical logic Logical truth Tautology Proposition Inference Logical equivalence Consistency Equiconsistency Argument Soundness Validity Syllogism Square of opposition Venn diagram
Propositional	Boolean algebra Boolean functions Logical connectives Propositional calculus Propositional formula Truth tables Many-valued logic 3 finite ∞
Predicate	First-order list Second-order Monadic Higher-order Fixed-point Free Quantifiers Predicate Monadic predicate calculus

Set theory

Set hereditary Class (Ur-)Element Ordinal number Extensionality Forcing Relation equivalence partition Set operations: intersection union complement Cartesian product power set identities
Types ofsets	Countable Uncountable Empty Inhabited Singleton Finite Infinite Transitive Ultrafilter Recursive Fuzzy Universal Universe constructible Grothendieck Von Neumann
Maps, cardinality	Function/Map domain codomain image In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal inaccessible Aleph number Operation binary
Theories	Zermelo–Fraenkel axiom of choice continuum hypothesis General Kripke–Platek Morse–Kelley Naive New Foundations Tarski–Grothendieck Von Neumann–Bernays–Gödel Ackermann Constructive

Formal
systems
(list),
language,
syntax

Example
axiomatic
systems
(list)

Principia Mathematica

Proof theory

Model theory

Computability
theory

Mathematics portal

Retrieved from "https://en.wikipedia.org/w/index.php?title=Existential_quantification&oldid=1304127682"

Categories:

Hidden categories:

[8]ページ先頭