\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{set theory}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations}

[[!include foundations - contents]]

\hypertarget{mathematics}{}\paragraph*{{Mathematics}}\label{mathematics}

[[!include mathematicscontents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{nave_vs_axiomatic_set_theory}{Na\"i{}ve vs axiomatic set theory}\dotfill \pageref*{nave_vs_axiomatic_set_theory} \linebreak
\noindent\hyperlink{foundational_vs_definitional_set_theory}{Foundational vs definitional set theory}\dotfill \pageref*{foundational_vs_definitional_set_theory} \linebreak
\noindent\hyperlink{MaterialSetTheory}{Material vs structural set theory}\dotfill \pageref*{MaterialSetTheory} \linebreak
\noindent\hyperlink{category_theory_on_set_theory}{Category theory on set theory}\dotfill \pageref*{category_theory_on_set_theory} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{literature}{Literature}\dotfill \pageref*{literature} \linebreak
\noindent\hyperlink{general}{General}\dotfill \pageref*{general} \linebreak
\noindent\hyperlink{ReferencesInHomotopyTypeTheory}{In homotopy type theory}\dotfill \pageref*{ReferencesInHomotopyTypeTheory} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

A \textbf{set theory} is a theory of [[sets]].

\hypertarget{nave_vs_axiomatic_set_theory}{}\subsection*{{Na\"i{}ve vs axiomatic set theory}}\label{nave_vs_axiomatic_set_theory}

\textbf{Na\"i{}ve set theory} is the basic algebra of the [[subsets]] of any given set $U$, together with a few levels of [[power sets]], say up to $\mathcal{P}\mathcal{P}\mathcal{P}U$ and possibly no further. Often students see this first for the set of [[real numbers]] as $U$ (although in fact one could start with the set of [[natural numbers]] and go one level further for an equivalent theory). One could also use [[function sets]] instead of power sets as the basic set-forming operation (especially for a [[predicative mathematics|weakly predicative]] theory in [[constructive mathematics]]).

Once you start thinking very much about the nature of sets in general (rather than merely \emph{using} na\"i{}ve set theory), it quickly becomes clear that one must be careful about how one can and cannot form sets. [[Georg Cantor]] is credited with being the first to think about sets this deeply; although he did not propose a system of general rules for valid set-making operations, he recognised that some sets were `inconsistent'. An \textbf{axiomatic set theory} is a set theory which carefully states the rules (or `[[axioms]]') which sets are assumed to obey.

[[Gottlob Frege]] has perhaps the first axiomatic set theory, but it was found (by [[Bertrand Russell]]) to be logically trivial; see [[Russell's paradox]]. [[Ernst Zermelo]] is credited with the first consistent axiomatic set theory.

\hypertarget{foundational_vs_definitional_set_theory}{}\subsection*{{Foundational vs definitional set theory}}\label{foundational_vs_definitional_set_theory}

There are two ways to go about doing axiomatic set theory. The more ambitious is to develop a \textbf{foundational set theory}: set theory as [[foundations]] for all of mathematics. This is what Frege proposed (although he failed through inconsistency) and which Zermelo achieved.

A variation of Zermelo's system (developed by Fraenkel and Skolem and called Zermelo--Fraenkel set theory or [[ZFC]]) is the orthodox foundations today, although it needs to be supplemented by [[Grothendieck universes]] (or something along those lines) to handle modern [[category theory]], and set theorists often consider further strengthenings of it through [[large cardinal]] [[axioms]] (of which the existence of Grothendieck universes is an example, just the tip of the iceberg).

It is also possible to make a \textbf{definitional set theory}, in which one defines sets in terms of some more primitive concept. For example, [[Bill Lawvere]] proposed a foundation [[ETCC]] based on [[Cat|the category of categories]]; then a set may be defined as a [[discrete category]]. This is also the case in [[homotopy type theory]], where sets are defined as those [[types]] which are [[h-sets]].

In [[constructive mathematics]], a foundation based on [[type theory]] is popular, with types interpreted as \emph{[[preset|presets]]} (sets without [[equality]]); then a set may be defined as a preset equipped with an [[equivalence relation]] (the term [[setoid]] is also used for such a gadget). In [[computer science]], a foundation based on the [[lambda-calculus]] is sometimes seen; in these terms, the concept of \emph{[[list]]} is more natural than set, with the difference being that sets have a coarser notion of equality.

\hypertarget{MaterialSetTheory}{}\subsection*{{Material vs structural set theory}}\label{MaterialSetTheory}

On the $n$Lab we like to distinguish between two types of set theory, especially in foundations:

\begin{itemize}%
\item In a \textbf{[[material set theory]]} (also called a \emph{membership-based set theory}), the elements of a set exist independently of that set. As such, it makes sense to take two completely unrelated sets and ask if two of their members are [[equal]], and sometimes the answer will be Yes. Frequently in material set theory one takes everything to be a [[pure set]], so that elements of sets are themselves sets. Therefore, any two sets may be meaningfully compared to ask if they are equal or if one is a member of the other.


\item A \textbf{[[structural set theory]]}, on the other hand, looks more like [[type theory]]. Here, the elements of a set have no existence or structure apart from their identity as elements of that set. In particular, they are not themselves sets, and cannot be elements of any \emph{other} set, at least not without invoking some explicit [[type casting|type-casting]] operator (which here could simply be a [[function]] from one set to the other). Similarly, elements of different sets cannot be compared to each other (without type-casting them to become elements of the same set).



\end{itemize}
Among category theorists, it's popular to state the axioms of a structural set theory by specifying elementary properties of [[Set|the category of sets]]; the orthodoxy here (to the extent that there is one) is probably [[Bill Lawvere]]'s [[ETCS]], which suffices for most everyday uses but must be supplemented to handle some esoteric parts of modern mathematics. Another structural set theory, which is stronger than ETCS and less closely tied to category theory, is [[SEAR]].

In contrast, [[ZFC]] is an example of a material set theory. From a model of either kind of set theory we can construct a model of the other, so the two are, broadly speaking, equivalent; for example, SEARC (SEAR with the [[axiom of choice]]) is equivalent in this way to ZFC, while ETCS is equivalent to a weak (`bounded') variation of ZFC. A more precise statement is that the two kinds of theories form categories related by the [[material-structural adjunction]].

\hypertarget{category_theory_on_set_theory}{}\subsection*{{Category theory on set theory}}\label{category_theory_on_set_theory}

Category theory can provide a common [[model theory]] to compare various set theories. Although only structural set theories like ETCS treat the elementary properties of the category $Set$ of sets as fundamental, one can ask for any set theory what properties $Set$ satisfies and compare them in those terms. At the very least, $Set$ should be a [[pretopos]].

There is also [[algebraic set theory]], in which a material set theory is interpreted in the [[internal logic]] of some [[ambient category]], often called a ``category of classes''. See also [[stack semantics]].

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[foundational axiom]]


\item [[type theory]]


\item [[constructive set theory]]


\item [[algebraic set theory]]


\item [[descriptive set theory]]


\item [[set-theoretic multiverse]]



\end{itemize}
\hypertarget{literature}{}\subsection*{{Literature}}\label{literature}

\hypertarget{general}{}\subsubsection*{{General}}\label{general}

\begin{itemize}%
\item [[Kenneth Kunen]], \emph{Set theory,an introduction to independence proofs}, North-Holland.


\item [[William Lawvere]], [[Robert Rosebrugh]], \emph{[[Sets for Mathematics]]} , Cambridge UP 2003. (\href{http://books.google.de/books?id=h3_7aZz9ZMoC&pg=PP1&dq=sets+for+mathematics}{web})



\end{itemize}
\hypertarget{ReferencesInHomotopyTypeTheory}{}\subsubsection*{{In homotopy type theory}}\label{ReferencesInHomotopyTypeTheory}

Formalization of set theory in [[homotopy type theory]] (via [[h-sets]]) is discussed in

\begin{itemize}%
\item [[Egbert Rijke]], [[Bas Spitters]], \emph{Sets in homotopy type theory} (\href{http://arxiv.org/abs/1305.3835}{arXiv:1305.3835})


\item [[Univalent Foundations Project]], section 3 of \emph{[[Homotopy Type Theory -- Univalent Foundations of Mathematics]]}


\item J\'e{}r\'e{}my Ledent, \emph{Modeling set theory in homotopy type theory} (2014) (\href{http://perso.ens-lyon.fr/jeremy.ledent/internship_report.pdf}{pdf})



\end{itemize}
See also at [[homotopy type theory FAQ]] \emph{\href{homotopy+type+theory+FAQ#WhatIsHoTTForSetTheorists}{What is HoTT? -- For set theorists}}.

[[!redirects set theory]] [[!redirects set theories]]



\end{document}