nLab notation

Idea

A list of basic notation common in mathematics.

Glossary

In logic and dependent type theory

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

Other notation

• $\wedge _A$ The meet operator in the meet-semilattice $A$.

• $\vee _A$ The join operator in the join-semilattice $A$.

• $\uparrow _A$ $(${$\alpha$}$)$ The principal up-set, coinitial/final segment generated by the singleton subset {$\alpha$} in the partial order, or join-semilattice $A$.

• $\uparrow _A (\alpha)$ The up-set, or coinitial/final segment generated by the subset $\alpha$ in the partial order, or join-semilattice $A$.

• {$x|\phi(x;y_i)$} The $\phi$-definable predicate class. For set-variable $x$, and class-variable $A$,

Theorem

$\forall x (x\in A \Leftrightarrow \phi (x)$

• $0$ The first limit-ordinal in the Von Neumann ordinals, i.e. ∅. The initial category. Also refers to the number zero, or the additive identity in a rig or a ring, or the trivial ring itself.

• $0_A$ The bottom element, or the zero of complete partial order, or bound meet-semilattice $A$.

• $1$ The first successor-ordinal in the Von Neumann ordinals, i.e. ∅. The terminal category.

• $1_A$ The top element, or unit of the complete partial order, or bound meet-semilattice $A$.

• $A_i$ The predicate class of i -cells in n-category A.

• $Arr(A), A_1$ The predicate class of morphisms, or 1-cells in category $A$.

• $Fun_A(B,C), Hom_A(B,C)$ The hom-set, or hom-object called the functor category of functors from domain $B$, to codomain $C$ in category $A$.

• $Hom_A(x,y), hom(x,y), A(x,y)$ The hom-set, or hom-object of morphisms from domain $x$, and codomain $y$ in category $A$.

• $Nat _A(f,g)$, $Hom_A(f,g)$ The hom-set or hom-object of natural transformations from domain f, and codomain g in functor category $A$.

• $Ob(A), A_0$ The predicate class of objects, or 0-cells in category $A$.

• ZFC The standard first-order foundational material pure axiomatic set theoretical logic with Axiom of Choice.

Not at all complete.*