\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*{ZFC}

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

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

[[!include foundations - contents]]

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

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{history}{History}\dotfill \pageref*{history} \linebreak
\noindent\hyperlink{axioms}{Axioms}\dotfill \pageref*{axioms} \linebreak
\noindent\hyperlink{variations}{Variations}\dotfill \pageref*{variations} \linebreak
\noindent\hyperlink{constructive_versions}{Constructive versions}\dotfill \pageref*{constructive_versions} \linebreak
\noindent\hyperlink{class_theories}{Class theories}\dotfill \pageref*{class_theories} \linebreak
\noindent\hyperlink{large_cardinals}{Large cardinals}\dotfill \pageref*{large_cardinals} \linebreak
\noindent\hyperlink{miscellaneous_variations}{Miscellaneous variations}\dotfill \pageref*{miscellaneous_variations} \linebreak
\noindent\hyperlink{relation_to_structural_set_theories}{Relation to structural set theories}\dotfill \pageref*{relation_to_structural_set_theories} \linebreak
\noindent\hyperlink{related_entries}{Related entries}\dotfill \pageref*{related_entries} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

The most commonly accepted standard [[foundation of mathematics]] today is a [[material set theory]] commonly known as \emph{Zermelo--Fraenkel set theory with the [[axiom of choice]]} or $ZFC$ for short. There are many variations on that theory (including [[constructive mathematics|constructive]] and [[class]]-based versions, which are also discussed here).

Accompanying ZFC, especially taking into account the [[axiom of foundation]], is a picture (or `ontology') of material sets forming a [[cumulative hierarchy]] organized by an [[ordinal number|ordinal]]-valued rank function. This picture (sometimes referred to as the `iterative conception') considers sets as generated by starting at bottom with the [[empty set]] and building to higher ranks by applying a [[power set]] operation to get to a next successor ordinal rank, and taking [[unions]] to get to limit ordinal ranks. This iterative conception finds alternative expression in [[algebraic set theory]].

\hypertarget{history}{}\subsection*{{History}}\label{history}

The first version was developed by [[Ernst Zermelo]] in 1908; in 1922, [[Abraham Fraenkel]] and [[Thoralf Skolem]] independently proposed a precise [[first order logic|first-order]] version with the [[axiom of replacement]]; von Neumann added the [[axiom of foundation]] in 1925. All of these versions included the [[axiom of choice]], but this was considered controversial for some time; one has merely $ZF$ if it is taken out.

$ZFC$ is similar to the [[class]] theories [[NBG]] (due to [[John von Neumann]], [[Paul Bernays]], and [[Kurt Gödel]]) and [[Morse–Kelley set theory|MK]] (due to [[Anthony Morse]] and [[John Kelley]]). The former is a conservative, finitely axiomatisable extension of $ZFC$, while the latter is stronger and cannot be finitely axiomatised (although a conservative extension involving meta-classes could be).

Contemporary set theorists often accept additional [[large cardinal]] [[axioms]], which can greatly increase the strength of $ZFC$, far beyond even $MK$. Other additional axioms which are sometimes added are the [[axiom of determinacy]] (or various weaker versions of it) or the [[axiom of constructibility]]. There are also weaker variants of $ZFC$, especially for [[constructive mathematics|constructive]] and [[predicative mathematics|predicative]] mathematics. Then there are alternatives on a different basis, notably [[New Foundations|NFU]] (a very [[predicative mathematics|impredicative]] [[material set theory]] with a set of all sets) and [[ETCS]] (a [[structural set theory]]).

(The source for this history, especially the dates, is mostly \href{http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory}{the English Wikipedia}.)

\hypertarget{axioms}{}\subsection*{{Axioms}}\label{axioms}

$ZFC$ is a [[material set theory]], based on a global binary \textbf{membership} [[predicate]] $\in$. Everything in standard $ZFC$ is a [[pure set]], which we will call simply a set; but there are also variations with [[urelements]] and [[classes]]. Urelements may be distinguished from sets and classes since they have no elements (although the [[empty set]] also has no elements); sets are usually those classes that are themselves elements (members) of sets. Urelements are also called \emph{atoms}, and $ZF$ with atoms included is sometimes called [[ZFA]] or $ZFU$.

\begin{enumerate}%
\item [[axiom of extensionality|Extensionality]]: If two sets have the same members, then they are \textbf{[[equality|equal]]} and themselves members of the same sets. See [[axiom of extensionality]] for variations, such as whether this is taken as a definition or an axiomatisation of equality of sets, and how the condition might be strengthened if (10) is left out.


\item [[axiom of the null set|Null Set]]: There is an \textbf{[[empty set]]}: a set $\empty$ with no elements. By (1), it follows that this set is unique; by even the weakest version of (5), it is enough to state the existence of some set. (Analogous remarks apply to axioms (3), (4), (6), (7), and (8), except when (5) is omitted and (4) and (6) are needed to derive it.)


\item [[axiom of pairing|Pairing]]: If $a$ and $b$ are sets, then there is a set $\{a,b\}$, the \textbf{[[unordered pairing]]} of $a$ and $b$, whose elements are precisely those sets equal to $a$ or $b$. Between them, (2) and (3) form a nullary/binary pair; the unary version follows from (3), since $\{a\} = \{a,a\}$ by (1). The higher finitary versions rely also on (4) (with $\{a,b,c\} = \{a\} \cup \{b,c\}$, etc), so they should probably be stated explicitly as an [[axiom scheme]] if (4) is omitted (but nobody seems to do that).


\item [[axiom of union|Union]]: If $\mathcal{C}$ is a set, then there is a set $\bigcup \mathcal{C}$, the \textbf{[[union]]} of $\mathcal{C}$, whose elements are precisely the elements of the elements of $\mathcal{C}$. It is normal to write $A \cup B$ for $\bigcup \{A,B\}$, etc, $A \cup B \cup C$ for $\bigcup \{A,B,C\}$, etc. Note that $\bigcup \{A\} = A$ and $\bigcup \empty = \empty$ (using (1) to prove these results), so no special notation is needed for these.


\item [[axiom of separation|Separation/Specification/Comprehension]]: Given any [[predicate]] $\phi[x]$ in the language of set theory with the chosen [[free variable]] shown, if $U$ is a set, then there is a set $\{x \in U \;|\; \phi[x]\}$, the \textbf{[[subset]]} of $U$ given by $\phi$, whose elements are precisely those elements $x$ of $U$ such that $\phi[x]$ holds. There are many variations, from Bounded Separation to Full Comprehension, which we should probably describe at [[axiom of separation]]; the version listed here is Full Separation. This is an [[axiom scheme]], but it can be made a single axiom in $NBG$ (but not completely in $MK$). Note that (5) follows from (4) and (6) using [[classical logic]], so it is often left out, but it must be included in intuitionistic variations, variations where (6) is omitted or weakened (or where (4) is omitted or weakened, in principle, although that never happens in practice), and variations where (5) itself is strengthened.


\item [[axiom of replacement|Replacement/Collection]]: Given a [[predicate]] $\psi[x,Y]$ with the chosen [[free variables]] shown, if $U$ is a set and if for every $x$ in $U$ there is a unique $Y$ such that $\psi[x,Y]$ holds, then there is set $\{\iota\,Y.\;\psi[x,Y] \;|\; x \in U\}$, the \textbf{[[image]]} of $U$ under $\psi$, whose elements are precisely those sets $Y$ such that there is an element $x$ of $U$ such that $\psi[x,Y]$ holds; if $\Psi[x]$ is a defined term, then we write $\{\Psi[x] \;|\; x \in U\}$ for $\{\iota\,Y.\; Y = \Psi[x] \;|\; x \in U\}$. Again there are many variations, from Weak Replacement to Strong Collection, which we should probably describe at [[axiom of replacement]]; the one described here is Replacement. This is also an [[axiom scheme]], but it can be made into a single axiom in both $NBG$ and $MK$. One could combine this with (5) to produce $\{\iota\,Y.\;\psi[x,Y] \;|\; x \in U \;|\; \phi[x]\}$, but nobody seems to do this.


\item [[axiom of power sets|Power Sets]]: If $U$ is a set, then there is a set $\mathcal{P}U$, the \textbf{[[power set]]} of $U$, whose elements are precisely the [[subsets]] of $U$, that is the sets $A$ whose elements are all elements of $U$. When using [[intuitionistic logic]], it is possible to accept only a weak version of this, such as [[subset collection|Subset Collection]] or (even weaker) [[function sets|Exponentiation]]. But in classical logic, Power Sets follows from Exponentiation and the weakest form of (5).


\item [[axiom of infinity|Infinity]]: There is a set $\omega$ of \textbf{[[ordinal number|finite ordinals]]} as pure sets. Normally one states that $\empty \in \omega$ and $a \cup \{a\} \in \omega$ whenever $a \in \omega$, although variations are possible. Using any but the weakest version of (6), it is enough to state that there is a set satisfying [[Peano arithmetic|Peano's axioms]] of [[natural numbers]], or even any [[Dedekind-infinite set]]. It seems to be uncommon to incorporate (2) into (8), but in principle (8) implies (2).


\item [[axiom of choice|Choice]]: If $\mathcal{C}$ is a set, each of whose elements has an element, then there is a set with exactly one element from each element of $\mathcal{C}$. Note that this set is \emph{not} unique, nor can we construct a canonical version which is, so we do not give it any name or notation. This version is the simplest to state in the language of $ZFC$; see [[axiom of choice]] for further discussion and weak versions. It is possible to incorporate (9) into (5) or (6), but this seems to be rare.


\item [[axiom of foundation|Foundation/Regularity/Induction]]: Given a formula $\phi$ with a chosen [[free variable]] $X$, if $\phi$ holds whenever $\phi[a/X]$ holds for every $a \in X$, then $\phi$ holds absolutely. For variations (including the axiom of anti-foundation), see [[axiom of foundation]]. This [[axiom scheme]] can be made into a single axiom even in $ZFC$ itself (although not in versions with intuitionistic logic; in that case it can be made a single axiom only in a class theory).



\end{enumerate}
\hypertarget{variations}{}\subsection*{{Variations}}\label{variations}

Zermelo's original version consists of axioms (1--5) and (7--9), in a somewhat imprecise form (which affects the interpretation of 5) of [[higher-order logic|higher-order]] [[classical logic]].

The modern $ZF$ consists of (1--8) and (10), using [[first-order logic|first-order]] [[classical logic]], the strongest form of (6) (that is, Strong Collection, although the standard Replacement is sufficient with [[classical logic]]), and the strongest form of (5) possible using only sets and not classes (Full Separation). Since Full Separation follows from Replacement with [[classical logic]], it is often omitted from the list of axioms.

$ZFC$ adds (9) and is thus the strongest version without classes or additional axioms. The version originally formulated by Fraenkel and Skolem did not include (10), although the three founders all eventually accepted it.

It is common to take \textbf{Zermelo set theory} ($\mathrm{Z}$) to be $ZF$ without (6), although Zermelo never accepted the first-order formulation; note that the weakest form (Weak Replacement) of (6) follows from (7) and (5), so it holds even in $\mathrm{Z}$.

Another variant is \textbf{bounded Zermelo set theory} ($BZ$), which is like $\mathrm{Z}$ but with only Bounded Separation; this is of interest to category theorists because $BZC$ is equivalent to [[ETCS]].

\hypertarget{constructive_versions}{}\subsubsection*{{Constructive versions}}\label{constructive_versions}

See also [[constructive set theory]].

The most well-known foundations for [[constructive mathematics]] through material set theory are [[Peter Aczel]]'s \textbf{constructive Zermelo--Fraenkel set theory} ($CZF$) and [[John Myhill]]'s \textbf{intuitionistic Zermelo--Fraenkel set theory} ($IZF$).

$CZF$ uses axioms (1--8) and (10), usually weak forms, in [[intuitionistic logic]]; specifically, it uses Bounded Separation for (5), Strong Collection for (6), and an intermediate (Subset Collection) form of (7). $IZF$ is simliar, but it uses Full Separation for (5) and the full strength of (7); Myhill's original version uses only Replacement for (6), but Collection (equivalent to Strong Collection using Full Separation) is standard now.

Note that adding (9) to $IZF$ implies [[excluded middle]] and so makes $ZFC$. However, some authors like to include a weak form of (9), such as [[dependent choice]] or [[COSHEP]].

[[Mike Shulman]]'s survey of material and structural set theories (\hyperlink{Shulman2018}{Shulman 2018}) takes $CPZ^{\circlearrowleft-}$ as the most basic form; it consists of (1--4) and the weakest versions (Bounded Separation and Weak Replacement) of (5\&6) in intuitionistic logic. Adding (10) gives $CPZ^{-}$, adding (8) gives $CPZ^{\circlearrowleft}$, and adding both gives $CPZ$, \textbf{constructive pre-Zermelo set theory}. Shulman gives systematic notation for other versions, which includes those (constructive and classical) listed above.

Myhill has another version, \textbf{constructive set theory} ($CST$); this consists of (1--4), Bounded Separation for (5), Replacement for (6), the weakest (Exponentiation) form of (7), (8), and a weak version (Dependent Choice) of (9). It also uses a variation of the language, with [[urelements]] for natural numbers; note that the existence of $\omega$ still follows using (6). This classifies $CST$ as $\mathrm{C}{\Pi}ZF^{\circlearrowleft} + DC$ in Shulman's system if one ignores the use of urelements and strengthens Replacement to Strong Collection.

\hypertarget{class_theories}{}\subsubsection*{{Class theories}}\label{class_theories}

\textbf{[[Morse--Kelley class theory]]} ($MK$) features both [[sets]] and [[proper classes]]. This allows it to strengthen (5) to Full Comprehension, since $\phi$ can include [[quantification]] over classes; the same holds in (6) and (10), although this does not add any additional strength.

\textbf{Von Neumann--Bernays--G\"o{}del class theory} ($NBG$) uses the same language as $MK$, but it still uses only Full Separation for (5). This makes it conservative over $ZFC$ and also allows for a finite axiomatisation; we replace the formulas in (5) and (6) with classes, and add some special cases of (5) for subclasses, one for each logical connective. (It is provable that plain $ZF$, if consistent, cannot be finitely axiomatized in its own first-order language; $NBG$ escapes this conclusion by extending the language with the notion of classes.)

One can also rework all of the weak versions of set theory above into a class theory like $NBG$, which is conservative over the original set theory. One can also use a class theory like $MK$, although this destroys any attempt to use a weak version of (5).

\hypertarget{large_cardinals}{}\subsubsection*{{Large cardinals}}\label{large_cardinals}

One often adds axioms for [[large cardinals]] to $ZFC$. Even (8) can be seen as a large cardinal axiom, stating that $\aleph_0$ exists. These additional axioms are most commonly studied in the context of a material set theory, but they work just as well in a structural set theory.

Note that adding an [[inaccessible cardinal]] (commonly considered the smallest sort of large cardinal) to $ZFC$ is already stronger than $MK$: given an inaccessible cardinal $\kappa$, one can interpret the sets and classes in $MK$ as the sets in $V_\kappa$ and $V_{\kappa+1}$, respectively. Of course, one can add a large cardinal to $MK$ to get something even stronger.

It is often convenient to assume that one always has more large cardinals when necessary. You cannot say this in an absolute sense, but you can adopt the axiom that every set belongs to some [[Grothendieck universe]]. Adding this axiom to $ZFC$ makes \textbf{Tarski--Grothendieck set theory} ($TG$). This is not the last word, however; you can make it stronger by adding classes in the style of $MK$, or even adding a cardinal which is inaccessible from $TG$. In fact, we have barely begun the large cardinals known to modern set theory!

\hypertarget{miscellaneous_variations}{}\subsubsection*{{Miscellaneous variations}}\label{miscellaneous_variations}

The [[axiom of constructibility]], usually notated ``$V = L$'', is a very strong axiom that can be added to $ZF$; it asserts that all sets belong to the [[constructible universe]] $L$, which can be ``constructed'' in a definable way through a transfinite procedure. This notion of ``constructible'' should not be confused with [[constructive mathematics]]; for instance, $V = L$ implies the [[axiom of choice]] and thus also [[excluded middle]] even with intuitionistic logic. $V = L$ also implies the [[generalized continuum hypothesis]] ($GCH$), which is how G\"o{}del originally proved that $GCH$ was consistent with $ZFC$. However, it is incompatible with the sufficiently large cardinals: the existence of a [[measurable cardinal]] implies that $V \neq L$. Most contemporary set theorists do not regard $V = L$ as potentially ``true.''

The [[axiom of determinacy]] ($AD$) is another axiom that can be added to $ZF$; it asserts that a certain class of infinite [[game]]s is determined (one player or the other has a winning strategy). $AD$ is inconsistent with the full axiom of choice, although it is consistent with dependent choice. A weaker form of $AD$ called ``projective determinacy'' is consistent with $AC$ and is equiconsistent with certain large cardinal assertions.

The $GCH$ itself, or its negation, could also be regarded as an additional axiom that can be added to $ZF$. Many set theorists would prefer to find a more ``natural'' axiom, such as a large cardinal axiom, which implies either $GCH$ or its negation. The equiconsistency of projective determinacy with a large cardinal assertion can be regarded as a step in this direction.

\hypertarget{relation_to_structural_set_theories}{}\subsubsection*{{Relation to structural set theories}}\label{relation_to_structural_set_theories}

The structural set theory \textbf{[[ETCS]]} is equivalent to $BZC$ in that the [[category of sets]] in that theory satisfies $ETCS$ while the well-founded [[pure sets]] in $ETCS$ satisfy $BZC$. This uses (1--4), Bounded Separation for (5), and (7--10), with Weak Replacement following from (5) and (7).

[[Mike Shulman]]'s \textbf{[[SEAR|SEARC]]} is equivalent to $ZFC$ in the same way. $SEAR$, which lacks the axiom of choice, is equivalent to $ZF^{\circlearrowleft}$, which is $ZF$ without (10), in a weaker sense of equivalence.

\hyperlink{Shulman2018}{Shulman 2018} is an extensive survey of variations of $ZFC$ and variations of $ETCS$ (mostly weak ones), showing how these correspond.

\hypertarget{related_entries}{}\subsection*{{Related entries}}\label{related_entries}

\begin{itemize}%
\item [[material set theory]]


\item [[algebraic set theory]]


\item [[cumulative hierarchy]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

Zermelo's axiomatisation grew out of his reflections on his proofs of the well-ordering theorem (1904/08) and was published in

\begin{itemize}%
\item [[Ernst Zermelo]], \emph{Untersuchungen \"u{}ber die Grundlagen der Mengenlehre I} , Math. Ann. \textbf{65} (1908) pp.261-81. (\href{http://gdz.sub.uni-goettingen.de/dms/load/img/?PPN=GDZPPN002262002}{gdz})

\end{itemize}
English versions of the early key texts on set theory by Zermelo, Fraenkel, Skolem, von Neumann et al. can be found in

\begin{itemize}%
\item J. van Heijenoort, \emph{From Frege to G\"o{}del - A Sourcebook in Mathematical Logic 1879-1931} , Harvard UP 1967.

\end{itemize}
There are many texts which discuss ZFC and the [[cumulative hierarchy]] from a traditional (material) set-theoretic perspective. A good example is

\begin{itemize}%
\item Kenneth Kunen, \emph{Set Theory: An Introduction to Independence Proofs}, Studies in Logic and the Foundations of Mathematics Vol. 102 (2006), Elsevier.

\end{itemize}
A classification of axioms of variants of $ZFC$, with an eye towards corresponding [[structural set theories]], is

\begin{itemize}%
\item [[Michael Shulman]] (2018). Comparing material and structural set theories. \href{https://arxiv.org/abs/1808.05204}{arXiv:1808.05204}.

\end{itemize}
[[!redirects ZF]] [[!redirects ZFC]]

[[!redirects Zermelo-Fraenkel set theory]] [[!redirects Zermelo–Fraenkel set theory]] [[!redirects Zermelo--Fraenkel set theory]] [[!redirects Zermelo-Fraenkel]] [[!redirects Zermelo–Fraenkel]] [[!redirects Zermelo--Fraenkel]]

[[!redirects Zermelo set theory]]

[[!redirects CPZ]]

[[!redirects Tarski-Grothendieck set theory]] [[!redirects Tarski–Grothendieck set theory]] [[!redirects Tarski--Grothendieck set theory]] [[!redirects Tarski-Grothendieck]] [[!redirects Tarski–Grothendieck]] [[!redirects Tarski--Grothendieck]]



\end{document}