[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents SEAF, short for Sets, Elements, And Functions, is a structural set theory with the following properties: * It is equivalent in strength to the material set theory ZF. (It can be augmented by an axiom of choice to produce SEAFC, which is strongly equivalent to ZFC.) * It contains a subtheory called bounded SEAF which (when augmented by choice) is strongly equivalent to ETCS. Conversely, ETCS can be augmented by a replacement axiom to become equivalent to SEAFC. \section{Description of SEAF} \subsection{Types} SEAF is a theory about three kinds of things: sets, elements, and functions. Every element, and every variable that ranges over elements, is always associated to something denoting a set (which might be a constant or a variable); we say it is an element of that set. If xx is an element of $A$ we write $x\in A$; note that this is not an assertion which may be true or false, but a typing declaration. In formal terms, this means that SEAR is a [[dependent type theory|dependently typed]] theory, with a type of sets, a type of elements for each set term, and a type of functions for each pair of set terms. One consequence of this is that whenever we quantify over elements we must always [[quantification|quantify]] over elements of some set; thus we can say “for all elements $x\in A$” but not “for all elements $x$.” Another consequence is that the assertion $x=y$ is only well-formed (a precondition to its being true or false) if $x$ and $y$ are elements of the same set. In a similar manner, every function is always associated to an ordered pair of sets, the first called its **[[source]]** and the second its **[[target]]**. If $f$ is a function from $A$ to $B$ we write $f:A \to B$. As with elements, the assertion $f = g$ is only well-formed if $f$ and $g$ have the same source and the same target. Implicit in the existence of three types of things is that nothing is both a set and an element, etc., so in particular a statement such as $x=A$ is not well-formed if $x$ is an element and $A$ a set. Furthermore, SEAR does not include an equality relation between sets: even if $A$ and $B$ are both sets we do not consider $A=B$ to be well-formed. (Thus SEAR respects the [[principle of equivalence]].) The final piece of data that we have is a notion of **evaluation** of a function $f:A \to B$ at an element $x \in A$, which is written as $f(x)$ and is an element $f(x) \in B$. ### Basic axioms Now we can state the axioms of structural ZFC, beginning with the most basic ones. **Axiom 1 (Axiom of extensionality):** _Given sets $A$ and $B$ and an [[injection]] $m:A \hookrightarrow B$, if for every element $x \in B$ there exists an element $y \in A$ such that $m(y) = x$, then $m$ is a [[bijection]]. **Axiom 2 (Axiom of empty set):** _There exists a set $\emptyset$ which has no elements._ **Axiom 3 (Axiom of Cartesian products):** _For every set $A$ and $B$, there exists a set $A \times B$ with a function $\pi_A:A \times B \to A$ and a function $\pi_B:A \times B \to B$ such that for every element $a \in A$ and $b \in B$ there is a unique element $(a, b) \in A \times B$, such that $\pi_A((a, b)) = a$ and $\pi_B((a, b)) = b$._ **Axiom 4 (Axiom of fibers):** _For every set $A$ and $B$, function $f:A \to B$, and element $b \in B$, there exists a set $f^{*}(b)$ with a unique function $i:f^{*}(b) \to A$, such that for all elements $c \in f^{*}(b)$, $f(i(c)) = b$. **Axiom 5 (Axiom schema of separation):** _For any formula $\phi(x)$ with free variable $x \in B$, there exists a subset $A \subseteq B$ with chosen injection $m:A \hookrightarrow B$ such that for every element $x \in B$, $\phi(x)$ holds if and only if there exists an element $y \in A$ such that $m(y) = x$._ **Axiom 6 (Axiom schema of collection):** _For any set $A$ and formula $\phi(x, X)$ with free variables $x \in A$ and $X$, there exists a set $B$, function $p:B \to A$, set $C$ and function $M:C \to B$ such that for every $b \in B$, $\phi(p(b), M^{*}(b))$, and for every $a \in A$, if there exists a set $X$ with $\phi(a, X)$, then $a \in \mathrm{im}(p)$._ **Axiom 7 (Axiom of power sets):** For every set $A$ there exists a set $\mathcal{P}(A)$ with a set $\in_A$ and an injection $i_{\in_A}:\in_A \hookrightarrow A \times \mathcal{P}(A)$ such that for every set $B$ and $R$ with an injection $i:R \to A \times B$, there exists a unique function $\chi_R:B \to \mathcal{P}(A)$ and a unique function $j:R \to \in_A$ such that for all elements $r \in R$, $(\mathrm{id}_A, \chi_R)(i(r)) = i_{\in_A}(j(r))$ **Axiom 8 (Axiom of natural numbers):** There exists a set $\mathbb{N}$ with an element $0 \in \mathbb{N}$ and an [[injection]] $s:\mathbb{N} \hookrightarrow \mathbb{N}$, such that for all elements $n \in \mathbb{N}$, $s(n) \neq 0$. **Axiom 9 (Axiom of choice):** Every surjection $f:A \to B$ has a right inverse. **Axiom 10 (Axiom of well-founded materialization):** Every set is isomorphic to a well-founded pure set. --- \section{Axiom of ordered pairing} For all sets $x$ and $y$, there exists a set $(x, y)$, such that for all $a \in x$ and $b \in y$, $(a, b) \in (x, y)$, and for all $c \in (x, y)$, there exist $\pi_1(c)$ and $\pi_2(c)$ such that $\pi_1((a, b)) = a$ and $\pi_2((a, b)) = b$. --- Literal basic stuff about high school algebra: * What is a variable? * What are free and bound variables? * What is substitution of terms for variables? \section{Variables} A variable is a symbol $x$ which represents an arbitrary instantiation of a type $T$. Variables are thus types and written as $x:T$. Variables are usually found in the context, as $\Gamma, x:T, \Delta \vdash \mathcal{J}$ for arbitrary judgment $\mathcal{J}$. \section{Free and bound variables} \section{Substitution} \section{Change of bound variables} category: redirected to nlab