Showing changes from revision #4 to #5: Added | Removed | Changed

Contents

In categorical set theories? such as ETCS?, the set theory is usually a theory of sets and functions? in an abstract category, withcategory, with elements? being defined as the global elements?, the morphisms? out of the terminal object? . However, this approach poses a few conceptual and practical issues, namely that in ordinary mathematical practice, elements are not the same as functions out of the terminal object, set, although they are isomorphic to each other, and function evaluation of elements in defined categorical as function composition of functions out of the terminal set theories is are an abuse of notation.

There are other structural set theories?, such as SEAR, which explicitly put in the elements of a set as a primitive of the theory: this is equivalent to saying that the category is an concrete category rather than an abstract category. In such a presentation involving sets and functions, function evaluation? would be an a external primitive version of an the theory, rather than derived from function composition of evaluation global map elements? , and the axiom of function extensionality is likewise defined directly on the elements. The presentation of such a concrete category, categorical making set the theory reads more like a traditional presentation of set theory in terms of sets and elements, rather than category into theory. anevaluational category, and the axiom of function extensionality is defined directly on the elements, rather than the global element morphisms out of the terminal object. The presentation of such a concrete categorical set theory reads more like a traditional presentation of set theory in terms of sets and elements, rather than category theory.

In this presentation, we will be adapting Tom Leinster’s presentation of ETCS to the concrete setting. Some of these axioms might be redundant, but that was true of Tom Leinster’s original presentation.

Basic primitives

Our theory has the following primitives:

• Some things called sets;

• For every set $A$, these things called elements in $A$, with elements $a$ in $A$ written as $a \in A$;

• For every set $A$ and $B$, these things called functions from $A$ to $B$, with functions $f$ from $A$ to $B$ written as $f:A \to B$;

• For every set $A$ and $B$, an operation called function evaluation assigning every element $a \in A$ and function $f:A \to B$ an element $f(a) \in B$;

• For every set $A$, a function $id_A:A \to A$ called the identity function of $A$;

• For every set $A$, $B$, and $C$, an operation called function composition assigning every function $f:A \to B$ and $g:B \to C$ a function $g \circ f:A \to C$;

Equality of elements and functions

For every set $A$ and elements $a \in A$ and $b \in A$, there is a relation $a = b$ called equality of elements, such that

• for every element $a \in A$, $a = a$
• for every element $a \in A$ and $b \in A$, $a = b$ implies that $b = a$
• for every element $a \in A$, $b \in A$, and $c \in A$, $a = b$ and $b = c$ implies that $a = c$.

For every set $A$ and $B$ and functions $f:A \to B$ and $g:A \to B$, there is a relation $f = g$ called equality of functions, such that

• for every function $f:A \to B$, $f = f$
• for every function $f:A \to B$ and $g:A \to B$, $f = g$ implies that $g = f$
• for every function $f:A \to B$, $g:A \to B$, and $h:A \to B$, $f = g$ and $g = h$ implies that $f = h$.

Basic axioms for functions

Axiom of identity functions. For every set $A$ and for every element $a \in A$, $id_A(a) = a$.

Axiom of currying. composition/evaluation equivalence. For every set $A$, $B$, and $C$, and for every element $a \in A$, $(g \circ f)(a) = g(f(a))$.

Axiom of extensionality. For every set $A$ and $B$ and for every function $f:A \to B$ and $g:A \to B$, if $f(x) = g(x)$ for all elements $x \colon A$, then $f = g$.

The associativity and unit laws of function composition follow from the axioms:

• For every set $A$ and $B$, function $f:A \to B$, and element $a \in A$,

  $$(g \circ id_A)(a) = g(id_A(a)) = g(a)$$

  and extensionality implies that $g \circ id_A = g$.

• For every set $A$ and $B$, function $f:A \to B$, and element $a \in A$,

  $$(id_B \circ g)(a) = id_B(g(a)) = g(a)$$

  and extensionality implies that $id_B \circ g = g$.

• For every set $A$, $B$, $C$, and $D$, function $f:A \to B$, $g:B \to C$, and $h:C \to D$, and element $a \in A$,

  $$(h \circ (g \circ f))(a) = h((g \circ f)(a)) = h(g(f(a)) = (h \circ g)(f(a)) = ((h \circ g) \circ f)(a)$$

  and extensionality implies that $h \circ (g \circ f) = (h \circ g) \circ f$.

Thus, these axioms imply that the collection of sets, functions, and elements form a concrete category that is evaluational and extensional.

Those who are versed in type theory would recognize that the axiom of currying as an instance of currying? a function $f:((B \to C) \times (A \to B)) \to A$ to a function $f^{'}:(B \to C) \to ((A \to B) \to A)$, hence the name of the axiom.

Other axioms

Singletons

Axiom of singletons. There is a set $\mathbb{1}$, called a singleton, with a unique element $* \in \mathbb{1}$, called a point.

Axiom of singletons. Cartesian products. There For is every a set$\mathrm{<span><del\; class="diffmod">\; 𝟙</del><ins\; class="diffmod">\; A</ins></span>}$ \mathbb{1} A , called and asingleton$B$ , with there is a unique set element$*A<span><del\; class="diffmod">\; \in </del><ins\; class="diffmod">\; \times </ins></span>\mathrm{<span><del\; class="diffmod">\; 𝟙</del><ins\; class="diffmod">\; B</ins></span>}$ * A \in \times \mathbb{1} B, called a point Cartesian product of $A$ and $B$, with a function $p_A:A \times B \to A$ called the projection onto $A$ and a function $p_B:A \times B \to B$ called the projection onto $B$, such that given two elements $a \in A$ and $b \in B$ there is a unique element $a, b \in A \times B$ such that $p_A(a, b) = a$ and $p_B(a, b) = b$.

$\mathbb{1}$Axiom of fibers. is For a terminal set, in the sense that for every set$A$ , there and is a unique function$\mathrm{<span><del\; class="diffmod">\; f</del><ins\; class="diffmod">\; B</ins></span>}:A\to 𝟙$ f:A B \to \mathbb{1} . , This element is because$\mathrm{<span><del\; class="diffmod">\; 𝟙</del><ins\; class="diffmod">\; b</ins></span>}\in B$ \mathbb{1} b \in B , only and has function a unique element in it. This implies that for every element$\mathrm{<span><del\; class="diffmod">\; a</del><ins\; class="diffmod">\; f</ins></span>}<span><del\; class="diffmod">\; \in </del><ins\; class="diffmod">\; :</ins></span>A\to B$ a f:A \in \to A B , and there every is function a set$f{f}^{-1}<span><del\; class="diffmod">\; :</del><ins\; class="diffmod">\; (</ins></span>\mathrm{<span><del\; class="diffmod">\; A</del><ins\; class="diffmod">\; b</ins></span>}<span><del\; class="diffmod">\; \to </del><ins\; class="diffmod">\; )</ins></span>𝟙$ f:A f^{-1}(b) \to \mathbb{1} and called the$g:A \to \mathbb{1}$fiber , of$f(a)=*$ f(a) f = * and over$\mathrm{<span><del\; class="diffmod">\; g</del><ins\; class="diffmod">\; b</ins></span>}(a)=*$ g(a) b = * , which with by a extensionality function implies that$\mathrm{<span><del\; class="diffmod">\; f</del><ins\; class="diffmod">\; i</ins></span>}<span><del\; class="diffmod">\; =</del><ins\; class="diffmod">\; :</ins></span>g{f}^{-1}(b)\to A$ f i:f^{-1}(b) = \to g A . , Therefore, such that for every two element functions from$\mathrm{<span><del\; class="diffmod">\; A</del><ins\; class="diffmod">\; a</ins></span>}\in f^{-1}(b)$ A a \in f^{-1}(b) , to$\mathrm{<span><del\; class="diffmod">\; 𝟙</del><ins\; class="diffmod">\; f</ins></span>}(i(a))=b$ \mathbb{1} f(i(a)) = b . are A equal, fiber and of so there is a unique function from$\mathrm{<span><del\; class="diffmod">\; A</del><ins\; class="diffmod">\; f</ins></span>}$ A f to over$\mathrm{<span><del\; class="diffmod">\; 𝟙</del><ins\; class="diffmod">\; b</ins></span>}$ \mathbb{1} b is also called the solution set of the equation $f(x) = b$.

Cartesian products

An injection is a function $f:A \to B$ such that for every element $a \in A$ and $b \in A$, if $f(a) = f(b)$, then $a = b$.

Axiom of Cartesian truth products. values. For There every is a set$\mathrm{<span><del\; class="diffmod">\; A</del><ins\; class="diffmod">\; \Omega </ins></span>}$ A \Omega and called a$B$set of truth values , there with is an a element set$A\perp <span><del\; class="diffmod">\; \times </del><ins\; class="diffmod">\; \in </ins></span>\mathrm{<span><del\; class="diffmod">\; B</del><ins\; class="diffmod">\; \Omega </ins></span>}$ A \bot \times \in B \Omega , called a Cartesian true product of such that for every set$A$ and $B$ , with and a injection function$p_{A}f:A\times B\to \mathrm{<span><del\; class="diffmod">\; A</del><ins\; class="diffmod">\; B</ins></span>}$ p_A:A f:A \times B \to A B , called there the is a unique functionprojection onto $A$$\chi_A:B \to \Omega$ and called a the function$p_B:A \times B \to B$classifying function called of theprojection onto $B$$A$ , such given that two elements$a\in A$ a \in A and is the fiber of$b{\chi }_A\in B$ b \chi_A \in B there over is a unique element$<span><del\; class="diffmod">\; (</del><ins\; class="diffmod">\; \perp </ins></span>a,b)\in A\times B$ (a, \bot b) \in A \times B such that $p_A((a, b)) = a$ and $p_B((a, b)) = b$.

The structure consisting of sets Axiom of function sets.$C$ For every set , $A$$A$ and , and $B$$B$ there is a set , with a pair of functions $B^A$$f:C \to A$ called the and function set$g:C \to B$ with a function is called a $(-)((-)):B^A \times A \to B$span such that for every set between $C$$A$ and function and $f:C \times A \to B$$B$ there is a function . A Cartesian product $g:C \to B^A$$A \times B$ such that for all elements of $c \in C$$A$ and and $a \in A$$B$, with functions $g(c)(a) = f(c, a)$$p_A:A \times B \to A$ and $p_B:A \times B \to B$ is a terminal span between $A$ and $B$, in the sense that for every other span $(C, f:C \to A, g:C \to B)$, there is a unique function $h:C \to A \times B$ such that for all elements $c \in C$, $p_A(h(c)) = f(c)$ and $p_B(h(c)) = g(c)$.

Suppose that there exist two functions Axiom of natural numbers.$h:C \to A \times B$ There exists a set and $\mathbb{N}$$k:C \to A \times B$ called a such that for all elements set of natural numbers$c \in C$ with an element , $0 \in \mathbb{N}$$p_A(h(c)) = f(c)$ and a function and $s:\mathbb{N} \to \mathbb{N}$$p_B(h(c)) = g(c)$ such that for every other set . This is because for every $A$$a \in A$ with an element and $a \in A$$b \in B$ and a function there is a unique element $g:A \to A$$(a, b) \in P$, there is a unique function such that $f:\mathbb{N} \to A$$p_A((a, b)) = a$ such that and $f(0) = a$$p_B((a, b)) = b$ and . This implies that $f(s(a)) = g(f(a))$$h(c) = (f(c), g(c))$ and $k(c) = (f(c), g(c))$, which by extensionality implies that $h = k$. Therefore, every two functions $h$ and $k$ from $C$ to $A \times B$ such that $p_A(h(c)) = f(c)$, $p_B(h(c)) = g(c)$, $p_A(k(c)) = f(c)$, $p_B(k(c)) = g(c)$ are equal, and so there is a unique function $h$ from $C$ to $A \times B$ such that $p_A(h(c)) = f(c)$, $p_B(h(c)) = g(c)$.

Fiber

A surjection is a function $f:A \to B$ such that for every $b \in B$ the fiber of $f$ at $b$ is inhabited. A right inverse of $f$ is a function $g:B \to A$ such that for all elements $a \in A$, $f(g(a)) = a$. A choice set is a set $B$ such that all surjections into $B$ have right inverses.

Axiom of fibers. choice. For Every every set is a choice set.$A$ and $B$, element $b \in B$, and function $f:A \to B$, there is a set $f^{-1}(b)$ called the fiber of $f$ over $b$ with a function $i:f^{-1}(b) \to A$, such that for every element $a \in f^{-1}(b)$, $f(i(a)) = b$. A fiber of $f$ over $b$ is also called the solution set of the equation f(x) = b.

Function sets

These axioms imply that the collection of sets, functions, and elements form a model of ETCS?.

…

Set of truth values

…

Set of natural numbers

…

Choice sets

…

References

• Tom Leinster?, Rethinking set theory, (arxiv:1212.6543)