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

\hypertarget{the_ultrafilter_theorem}{}\section*{{The ultrafilter theorem}}\label{the_ultrafilter_theorem}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{statement_and_proof}{Statement and proof}\dotfill \pageref*{statement_and_proof} \linebreak
\noindent\hyperlink{strength_and_weakness_as_a_choice_principle}{Strength and weakness as a ``choice principle''}\dotfill \pageref*{strength_and_weakness_as_a_choice_principle} \linebreak
\noindent\hyperlink{other_formulations}{Other formulations}\dotfill \pageref*{other_formulations} \linebreak
\noindent\hyperlink{failures}{Failures}\dotfill \pageref*{failures} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

In [[classical mathematics]], the ultrafilter theorem is a theorem about ultrafilters, proved as a standard application of [[Zorn's lemma]]. In the [[foundations]] of mathematics, however, it is interesting to consider which results are implied by it or equivalent to it (very few imply it without being equivalent, other than those that imply the full axiom of choice itself).

\hypertarget{statement_and_proof}{}\subsection*{{Statement and proof}}\label{statement_and_proof}

\begin{utheorem}
Given a [[set]] $X$, every proper [[filter]] on $X$ may be extended to an [[ultrafilter]] (that is, a maximal proper filter) on $X$.

\end{utheorem}
\begin{proof}
Given a proper filter $F$ on $X$, consider the [[partial order|poset]] of proper filters that refine (contain) $F$, ordered by inclusion (reverse refinement). Of course, $F$ is in this poset. Given a chain $\mathcal{C}$ of proper filters that refine $F$, the [[union]] $F \cup \bigcup \mathcal{C}$ is a proper filter that refines $F$ and is an upper bound of $\mathcal{C}$. By [[Zorn's lemma]], there is a proper filter maximal among those that refines $F$, which is therefore maximal among all proper filters.

\end{proof}
Although this proof uses Zorn's lemma, the statement itself is weaker. In particular, it is weaker than the [[axiom of choice]] (even assuming the principle of [[excluded middle]]).

\hypertarget{strength_and_weakness_as_a_choice_principle}{}\subsection*{{Strength and weakness as a ``choice principle''}}\label{strength_and_weakness_as_a_choice_principle}

Although the ultrafilter theorem is weaker than the axiom of choice, it can be used to prove quite a few results that are traditionally proved using [[Zorn's lemma]] (or some other thing equivalent to the axiom of choice). For example, it can be used to prove

\begin{itemize}%
\item the [[Hahn–Banach theorem]] (which in turn implies existence of Lebesgue non-measurable sets),


\item the [[Banach-Tarski paradox|Banach–Tarski paradox]],


\item the [[prime ideal theorem]] for [[rigs]], [[rings]], and [[Boolean algebras]],


\item that every [[formally real field]] can be [[total order|totally ordered]],


\item existence and uniqueness of [[algebraic closures]] (see [[splitting field]]),


\item existence of non-trivial [[ultraproducts]],


\item the [[compactness theorem]] and completeness theorem for [[first-order logic]] (see below)



\end{itemize}
as a partial list. An enlightening discussion of the things one might expect to be able to prove using the ultrafilter theorem is given \href{http://mathoverflow.net/questions/202458/how-do-i-apply-the-boolean-prime-ideal-theorem}{here at MO}.

However, in other respects, the ultrafilter theorem is very weak as a ``choice principle''. For example, it is too weak to prove the axiom of [[countable choice]] (so for example, it cannot prove that a countable union of countable sets is countable), a fact exhibited in Cohen's first model for the failure of the axiom of choice (where even countable choice fails but the ultrafilter theorem holds). It therefore cannot prove the [[axiom of dependent choice]] either.

It can prove \emph{some} traditional applications of [[dependent choice]]. For example, it can be used to [[linear order|linearly order]] any set. From there it can be used to prove that a countable union of nonempty finite sets is countable, which in turn can be used to establish the weak K\"o{}nig lemma; see \href{/nlab/show/compactness+theorem#totalorder}{here}.

\hypertarget{other_formulations}{}\subsection*{{Other formulations}}\label{other_formulations}

Here are several statements equivalent (internal to an arbitrary [[topos]]) to the ultrafilter theorem.

The first three are, if you work through the definitions, almost direct rephrasings of the theorem above:

\begin{itemize}%
\item Every [[net]] has a universal subnet. (We must define `subnet' and `universal net' properly to make this work, at which point the equivalence is immediate.)


\item The Boolean prime ideal theorem: every proper [[ideal]] in a [[Boolean ring]] is contained in a [[prime ideal]]. (Stronger formulations of the Boolean prime ideal theorem also follow.)


\item The [[Stone representation theorem]]: every [[Boolean algebra]] is a subalgebra of some (classical) [[power set]] $2^X$. (Stronger formulations of the Stone representation theorem also follow.)



\end{itemize}
These basic results in [[logic]] are equivalent to the ultrafilter theorem:

\begin{itemize}%
\item Consistency: if a set $\Sigma$ of formulas in propositional [[classical logic]] is syntactically consistent (proves no contradiction), then it is semantically consistent (has a model). (The converse is immediate; stronger formulations of the consistency theorem, including for predicate logic, also follow.)


\item Compactness: if every finite subset of $\Sigma$ has a model, then so does $\Sigma$. (The converse is immediate; stronger formulations of the compactness theorem, including for predicate logic, also follow.)



\end{itemize}
Various characterisations of [[compact spaces]] are equivalent to the ultrafilter theorem:

\begin{itemize}%
\item Given a set $S$, the space $2^S$ (in the product topology) is compact. (This can be seen as a very weak form of the Tychonoff theorem below.)


\item More generally, if every ultrafilter on a [[convergence space]] $X$ is convergent, then $X$ is compact. (The converse is immediate.)


\item A [[uniform space]] is compact if it is [[complete space|complete]] and [[totally bounded space|totally bounded]] (i.e. it is [[Bishop-compact]]). (The converse is immediate.)



\end{itemize}
These classical results in analysis are equivalent to the ultrafilter theorem in a [[Boolean topos]] with [[natural numbers object]]:

\begin{itemize}%
\item The [[Tychonoff theorem]] for [[Hausdorff spaces]]: any product of compact Hausdorff spaces is compact; equivalently, any product of compact Hausdorff spatial [[locales]] is spatial. (If we drop the Hausdorff condition, then the result is equivalent to the full [[axiom of choice]].)


\item [[Stone–Čech compactification]]: the [[compact Hausdorff spaces]] form a [[reflective subcategory]] of [[Top]]. (The classical result that they form a reflective subcategory of the category $T_{3\frac{1}{2}}$ of completely regular Hausdorff spaces is enough; the classical result that the reflection is a dense embedding on $T_{3\frac{1}{2}}$ also follows.)


\item [[Banach–Alaoglu theorem]]: the closed unit ball of the double dual of a [[Banach space]] is weak* compact. (The result for \emph{separable} spaces does not require the ultrafilter theorem.)



\end{itemize}
\hypertarget{failures}{}\subsection*{{Failures}}\label{failures}

Of course, since the ultrafilter theorem is independent of [[ZF]], there are models in which it fails. More strongly, however, there are apparently models of ZF in which \emph{every ultrafilter (on every set) is principal}. See \href{http://mathoverflow.net/questions/76495/existence-of-non-principal-ultrafilters-on-sets/76499#76499}{this MO answer}.

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

Various equivalences with the ultrafilter theorem are stated and proved (in ) in

\begin{itemize}%
\item Eric Schechter; [[HAF|Handbook of Analysis and its Foundations]].

\end{itemize}
See a summary (in GIF!): \href{http://www.math.vanderbilt.edu/~schectex/ccc/excerpts/equivuf1.gif}{page 1} and \href{http://www.math.vanderbilt.edu/~schectex/ccc/excerpts/equivuf2.gif}{page 2}.

It's possible that I've made some mistakes above in deciding which of these use excluded middle or the existence of a natural numbers object. (I very much doubt that any of them use replacement.)

[[!redirects ultrafilter principle]] [[!redirects ultrafilter theorem]] [[!redirects ultrafilter lemma]]



\end{document}