nLab element

This entry is about the concept in mathematics, specifically in set theory/type theory/category theory. For the concept in chemistry see at chemical element.

Idea

An element of a set is a thing which “belongs to,” or “is an element of,” that set.

The circularity of this definition is unavoidable in foundational set theories in which “set” is an undefined term. In “definitional” set theories, where “set” is defined in terms of something else, elements are likewise defined in terms of the same “something else.”

If sets (or setoids) are regarded as the semantics of some type theory, then an element of a set is the interpretation of a term of some type.

Generalisations

• A term of some type.
• a global element of any object in any category or higher category with a terminal object.
• a generalised element of any object in any category or higher category;
• a morphism in a category, a different sort of element from an object;
• An object in a category;
• in general, $k$-morphisms or $k$-cells in an $\infty$-category;

Related concepts

symbol	in propositional logic	Unicode
$:$	typing relation	U+003A
=	propositional equality relation	U+003D
$\neg$	logical negation operator	U+00AC
$\neg \neg$	double negation	U+00AC&U+00AC
$\nLeftarrow$, $\nleftarrow$	negation of converse implication, or negation of converse conditional	U+21CD, U+219A
$\nLeftrightarrow$, $\nleftrightarrow$	negation of logical equivalence, or negation of biconditional	U+21CE, U+21AE
$\nRightarrow$, $\nrightarrow$	negation of implication, or negation of conditional	U+21CF, U+219B
$\Leftarrow$, $\leftarrow$	converse implication, or converse conditional	U+21D0, U+2190
$\Rightarrow$, $\rightarrow$	implication, or conditional	U+21D2, U+2192
$\Leftrightarrow$, $\leftrightarrow$	logical equivalence, or biconditional	U+21D4, U+2192
$\wedge$	logical conjunctionoperator	U+2227
$\vee$	logical dysjunction operator	U+2228
$\neq$	inequality, or apartness relation	U+2260
$\vdash$	syntactic entailment relation	U+22A2
$\vDash$	semantic entailment relation	U+22A8
$\top$	truth value, or top element	U+22A3
$\bot$	false value, or bottom element	U+22A4
$\veebar$, $\oplus$	logical exclusive dysjunction operator	U+22BB, U+2295
$\bar{\wedge}$	logical non-conjunction operator	U+22BC
$\bar{\vee}$	logical non-dysjunction operator	U+22BD

symbol	in first-order logic	Unicode
$\forall$	universal quantifier	U+2200
$\exists$	existential quantifier	U+2203
$\exists!$	uniqueness quantifier	U+2203&U+0021
$\nexists$	negation of existential quantifier	U+2204

symbol	in set theory	Unicode
×	binary Cartesian product, or binary product	U+00D7
$\varnothing$	empty, or uninhabited set	U+2205
$\in$	membership relation	U+2208
$\notin$	negation of membership relation	U+2209
$\ni$	containment relation	U+220B
$\notni$	negation of containment relation	U+220C
$\prod$	n-ary Cartesian product, or product operator	U+220F
$\coprod$	n-ary disjoint union, or coproduct operator	U+2210
$\cap$	binary intersection operator	U+2229
$\cup$	binary union operator	U+222A
$\subset$	subset of relation	U+2282
$\supset$	superset of relation	U+2283
$\nsubset$	negation of subset relation	U+2284
$\nsupset$	negation of superset relation	U+2285
$\subseteq$	inclusion relation, or subset of, or equal to	U+2286
$\supseteq$	converse of inclusion relation, or superset of, or equal to	U+2287
$\sqcup$	binary disjoint union, or binary coproduct operator	U+2294
$\bigcap$	n-ary intersection operator	U+22C2
$\bigcup$	n-ary union operator	U+22C3

$\;$

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in linear logic$\phantom{-}$
$\phantom{A}$$\top$	$\phantom{A}$additive truth
$\phantom{A}$$\bot$	$\phantom{A}$additive falsehood
$\phantom{A}$$0$	$\phantom{A}$multiplicative falsehood
$\phantom{A}$$1$	$\phantom{A}$multiplicative truth
$\phantom{A}$$\multimap$$\phantom{A}$	$\phantom{A}$linear implication$\phantom{A}$
$\phantom{A}$$\otimes$$\phantom{A}$	$\phantom{A}$multiplicative conjunction$\phantom{A}$
$\phantom{A}$$\oplus$$\phantom{A}$	$\phantom{A}$additive disjunction$\phantom{A}$
$\phantom{A}$$\&$$\phantom{A}$	$\phantom{A}$additive conjunction$\phantom{A}$
$\phantom{A}$$\invamp$$\phantom{A}$	$\phantom{A}$multiplicative disjunction$\phantom{A}$
$\phantom{A}$$\;!$$\phantom{A}$	$\phantom{A}$exponential conjunction$\phantom{A}$
$\phantom{A}$$\;?$$\phantom{A}$	$\phantom{A}$exponential disjunction$\phantom{A}$
$\phantom{A}$$^\bot$$\phantom{A}$	$\phantom{A}$negation$\phantom{A}$

$\;$

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in dependent type theory$\phantom{-}$	$\phantom{-}$propositions as types$\phantom{-}$
$\phantom{A}$$\to$	$\phantom{A}$function type	$\phantom{A}$implication
$\phantom{A}$$\times$	$\phantom{A}$product type	$\phantom{A}$conjunction
$\phantom{A}$$+$	$\phantom{A}$sum type	$\phantom{A}$disjunction
$\phantom{A}$$0$, $\emptyset$	$\phantom{A}$empty type	$\phantom{A}$false
$\phantom{A}$$1$	$\phantom{A}$unit type	$\phantom{A}$true
$\phantom{A}$$=$, $\mathrm{Id}$	$\phantom{A}$identity type	$\phantom{A}$propositional equality
$\phantom{A}$$\simeq$	$\phantom{A}$equivalence of types	$\phantom{A}$logical equivalence
$\phantom{A}$$\sum$, $\Sigma$, $\times$	$\phantom{A}$dependent sum type	$\phantom{A}$existential quantifier
$\phantom{A}$$\prod$, $\Pi$, $\to$	$\phantom{A}$dependent product type	$\phantom{A}$universal quantifier
$\phantom{A}$$\mathrm{isContr}$	$\phantom{A}$is contractible type	$\phantom{A}$unique proof
$\phantom{A}$$\mathrm{isContr}(A + B)$	$\phantom{A}$sum type is contractible type	$\phantom{A}$exclusive disjunction
$\phantom{A}$$\mathrm{isContr}\left(\sum_{x:A} B(x)\right)$	$\phantom{A}$dependent sum type is contractible type	$\phantom{A}$uniqueness quantifier
$\phantom{A}$$\mathrm{ua}$	$\phantom{A}$univalence axiom	$\phantom{A}$propositional extensionality