\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*{foundation of mathematics}

\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{categories}{Category theory and foundations}\dotfill \pageref*{categories} \linebreak
\noindent\hyperlink{MFCT}{Mathematical foundations of category theory}\dotfill \pageref*{MFCT} \linebreak
\noindent\hyperlink{Identity}{The concept of \emph{identity}}\dotfill \pageref*{Identity} \linebreak
\noindent\hyperlink{CFM}{Categorial foundations of mathematics}\dotfill \pageref*{CFM} \linebreak
\noindent\hyperlink{CFCT}{Categorial foundations of category theory}\dotfill \pageref*{CFCT} \linebreak
\noindent\hyperlink{Other}{Other topics}\dotfill \pageref*{Other} \linebreak
\noindent\hyperlink{Concrete}{Effect of foundations on concrete problems}\dotfill \pageref*{Concrete} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

In the context of \emph{foundations of mathematics} or \emph{[[mathematical logic]]} one studies formal systems -- [[theories]] -- that allow us to formalize much if not all of [[mathematics]] (and hence, by extension, at least aspects of mathematical fields such as fundamental [[physics]]).

There are two different attitudes to what a desirable or interesting foundation should achieve:

\begin{enumerate}%
\item In \textbf{proof-theoretic foundations} the emphasis is on seeing which formal systems, however convoluted they may be conceptually, allow us to formalize and prove which [[theorems]].

The archetypical such system is [[ZFC]] [[set theory]]. Other formal systems of interest here are [[elementary function arithmetic]] and [[second order arithmetic]], because they are [[proof theory|proof-theoretically]] weak, and still can derive ``almost all of undergraduate mathematics'' (\hyperlink{Harrington}{Harrington}).


\item In \textbf{[[practical foundations]]} (following a term introduced in (\hyperlink{Taylor}{Taylor})) the emphasis is on conceptually natural formalizations that \emph{concentrate the essence of practice and in turn use the result to guide practice} (\hyperlink{Lawvere}{Lawvere}), as in (\hyperlink{EilenbergSteenrod}{Eilenberg-Steenrod}, \hyperlink{Harper}{Harper}).

Formal systems of interest here are [[ETCS]] or flavors of [[type theory]], which allow natural expressions for central concepts in mathematics (notably via their [[categorical semantics]] and the conceptual strength of [[category theory]]).



\end{enumerate}
\hypertarget{categories}{}\subsection*{{Category theory and foundations}}\label{categories}

There are two big questions about [[category theory]] and the logical foundations of mathematics:

\begin{enumerate}%
\item What foundations are adequate to formulate category theory?
\item How can category theory provide a foundation for mathematics?

\end{enumerate}
These questions also apply to [[higher category theory]], which also involves the relation between them. (2-categories as a foundation for categories, for example.)

For a philosophical treatment of category theoretic foundations see [[foundations and philosophy]].

\hypertarget{MFCT}{}\subsubsection*{{Mathematical foundations of category theory}}\label{MFCT}

The problem with mathematical foundations of category theory is that in category theory we frequently speak of [[large category|large categories]], which it is tricky to deal with rigorously in the usual sort of [[set theory|set theories]].

One common view seems to be to found category theory on a theory of sets and classes; see \href{https://en.wikipedia.org/wiki/Category_%28mathematics%29#Definition}{the English Wikipedia's definition}, for example. But the standard reference, Saunders Mac Lane's \emph{Categories for the Working Mathematician}, assumes the existence of a universe (an inaccessible cardinal) instead. Both of these approaches rely on a distinction between \emph{small} and \emph{large} categories. There is a category of all [[small category|small categories]], but this category is not itself small; there is no category of all categories.

[[Alexander Grothendieck]] used more (although \href{http://permalink.gmane.org/gmane.science.mathematics.categories/6847}{apparently} he did not need to); he used what we now call [[Grothendieck universes]]. He assumed that every set is contained within a universe; that is, for every cardinal number $\kappa$, there is a cardinal inaccessible from $\kappa$. (This is still a rather moderate axiom, compared to some of the large-cardinal axioms studied by set theorists.) Now one has a relative notion of small and large; the category of all $U$-small categories (where $U$ is some universe) is $U$-large but must be $U'$-small for some other universe $U'$, and there exists a category (which is both $U$-large and $U'$-large) of all $U'$-small categories.

If one does not accept the [[axiom of choice]], then there are additional complications in general category theory. In particular, one must distinguish between a universal \emph{property} (for example, having all [[product]]s) and having a universal \emph{structure} realising that property (in the example, a functor taking each pair $(x,y)$ of objects to a specific product cone $x \leftarrow x \times y \rightarrow y$). This difficulty was overcome by Michael Makkai using [[anafunctor]]s, but these have not been widely adopted, even by constructivists.

For a summary of the mathematical foundations of category theory, see Mike Shulman, \emph{Set theory for category theory}, \href{http://arxiv.org/abs/0810.1279}{arXiv:0810.1279}.

\hypertarget{Identity}{}\paragraph*{{The concept of \emph{identity}}}\label{Identity}

One way to think of category theory is as a framework in which the idea is formalized that every kind of [[equality]] is really secretly a choice of [[isomorphism]] or [[equivalence]]. In some sense the notion of identity potentially breaks the [[principle of equivalence]].

[[Michael Makkai]] works on a language, [[FOLDS]] (`first-order logic with dependent sorts'), which is designed to make it impossible to formulate any statements that break the [[principle of equivalence]].

\hypertarget{CFM}{}\subsubsection*{{Categorial foundations of mathematics}}\label{CFM}

[[Bill Lawvere]] proposed to found mathematics on [[ETCC]] (for ` Elementary Theory of the Category of Categories'), a first-order axiomatisation of [[Cat|the category of categories]]. This has not been very successful, but his other proposal, a first-order axiomatisation of [[Set|the category of sets]], works well. These and related approaches to foundations may be called \emph{structural} or \emph{categorial} (or \emph{categorical}, which is more common but clashes with another sense of `categorical' in logic).

Lawvere's system [[ETCS]] (for `the Elementary Theory of the Category of Sets') essentially states that the category of sets is a [[topos]] with certain properties, in particular a [[well-pointed topos]]. This can be stated in elementary (first-order) terms; indeed, the system of axioms for ETCS in 1965 was retrospectively an important step in Lawvere's quest to give a first-order axiomatization for the topos concept that was originally formulated in higher-order terms by the Grothendieck school, resulting in 1970 in the by the now-default notion of \emph{elementary} topos that subsumes the original notion, now called [[Grothendieck topos]], as an important special case.

It is also possible to found mathematics on the [[internal logic|internal language]] of a topos. In this case, the topos need \emph{not} be well-pointed (and indeed, the condition that a topos be well-pointed cannot be stated in its own internal language; or if you prefer, \emph{every} topos is well-pointed \emph{internally}). This is equivalent to a certain formulation of [[type theory]], so it is (in a sense) nothing new, although it leads to new perspectives, as in the next paragraph.

Categories (not just toposes) can serve as models of [[type theory|type theories]], each type theory corresponding to a certain class of categories. Toposes correspond directly to a constructive but impredicative type theory; to make the theory predicative (in the constructivists' sense) you generalise to a [[pretopos]] (maybe [[locally cartesian closed category|locally cartesian closed]]), to make the theory nonconstructive you specialise to a [[Boolean topos]], and so on. More specifically, every category's internal language is a type theory (with many odd constants), and every type theory (of appropriate form) defines a category (its free model); this is an [[adjunction]] between categories and type theories. [[Paul Taylor]]'s book \emph{[[Practical Foundations|Practical Foundations of Mathematics]]} is essentially all about this subject, as is (at a more advanced level) most of the career of [[Michael Makkai]].

[[Jim Lambek]] proposed to use the [[free topos]] as ambient world to do mathematics in. Being syntactically constructed, but universally determined, with higher-order [[intuitionistic type theory]] as [[internal language]] he saw it as a reconciliation of the three classical schools of [[philosophy of mathematics]], namely [[formalism]], [[platonism]], and [[intuitionism]]. His latest views on this variant of categorical foundations can be found in (\hyperlink{LS11}{Lambek-Scott 2011}).

Certain `strong' axioms of [[set theory]] (those involving [[quantification]] over all sets) are difficult to state in category-theoretic (or type-theoretic) terms, but this can be overcome in a theory like ETCS; talk to Mike Shulman. (Ironically, this makes it harder to do foundations with categorial foundations!)

In contrast, many of the optional or controversial axioms of set theory (such as the [[axiom of choice]]) can be stated quite directly in ETCS. These can be examined quite well in a na\"i{}ve set-theoretic language that never need be precise about whether one's foundations are traditional (membership-based), categorial, or whatever.

\hypertarget{CFCT}{}\subsubsection*{{Categorial foundations of category theory}}\label{CFCT}

Relevant topics: [[ETCC]], [[FOLDS]], [[homotopy type theory]]

\hypertarget{Other}{}\subsection*{{Other topics}}\label{Other}

\begin{itemize}%
\item There is also [[algebraic set theory]].

\end{itemize}
A big picture intro to the comparison between set theory, type theory and topos/category theory as approaches to foundations is in

\begin{itemize}%
\item [[Steve Awodey]], \emph{From Sets to Types to Categories to Sets} \href{http://www.andrew.cmu.edu/user/awodey/preprints/stcsFinal.pdf}{pdf}

\end{itemize}
\hypertarget{Concrete}{}\subsection*{{Effect of foundations on concrete problems}}\label{Concrete}

It may seem on first sight that foundational questions in mathematics are remote from ``real mathematics''. This is not quite so. For a list of ``real world'' problems that do depend on foundations see

\begin{itemize}%
\item [[effects of foundations on ``real'' mathematics]]

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

\begin{itemize}%
\item [[synthetic mathematics]]

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

\begin{itemize}%
\item [[Bertrand Russell]], \emph{[[Principia Mathematica]]}, 1910


\item [[William Lawvere]], \emph{Foundations and applications: axiomatization and education}, Bulletin of Symbolic Logic 9 (2003), 213-224 (\href{http://www.math.ucla.edu/~asl/bsl/0902/0902-006.ps}{ps}, \href{http://projecteuclid.org/euclid.bsl/1052669290}{Euclid})


\item L. A. Harrington (ed.), \emph{Harvey Friedman's Research on the Foundations of Mathematics}, Studies in Logic and the Foundations of Mathematics (2012)



\end{itemize}
[[practical foundations|Practical foundations]] in terms of [[type theory]] language are laid out in

\begin{itemize}%
\item [[Paul Taylor]], \emph{[[Practical Foundations of Mathematics]]}, Cambridge University Press (\href{http://www.cs.man.ac.uk/~pt/Practical-Foundations/html/index.html}{web})

\end{itemize}
Under [[computational trinitarianism]] this corresponds to a practical foundation in [[program|programming]], laid out in

\begin{itemize}%
\item [[Robert Harper]], \emph{[[Practical Foundations for Programming Languages]]} (\href{http://www.cs.cmu.edu/~rwh/plbook/book.pdf}{web})

\end{itemize}
A foundation for [[algebraic topology]] in this practical spirit is laid out in

\begin{itemize}%
\item [[Samuel Eilenberg]], [[Norman Steenrod]], \emph{[[Foundations of Algebraic Topology]]}

\end{itemize}
The following contains a careful discussion of [[Gödel's incompleteness theorem]] in the context of categorical foundations using the free topos:

\begin{itemize}%
\item [[Jim Lambek]], [[Phil Scott]], \emph{Reflections on Categorical Foundations of Mathematics} , pp.171-185 in Sommaruga (ed.), \emph{Foundational Theories of Classical and Constructive Mathematics}, Springer New York 2011. (\href{https://www.site.uottawa.ca/~phil/papers/LS11.final.pdf}{draft})

\end{itemize}
A comparative discussion of complexities of different foundations is in

\begin{itemize}%
\item [[Freek Wiedijk]], \emph{Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics} (\href{http://www.cs.ru.nl/~freek/zfc-etc/zfc-etc.pdf}{pdf})

\textbf{Abstract} This paper presents [[Automath]] encodings (which also are valid in LF/P) of various kinds of foundations of mathematics. Then it compares these encodings according to their size, to find out which foundation is the simplest.

The systems analyzed in this way are two kinds of [[set theory]] (ZFC and NF), two systems based on Church's [[higher order logic]] ([[Isabelle]]/Pure and [[HOL]]), three kinds of [[type theory]] (the [[calculus of constructions]], Luo's extended calculus of constructions, and Martin-L\"o{}f predicative type theory) and one [[ETCS|foundation based on category theory]]. The conclusions of this paper are that the simplest system is type theory (the calculus of constructions) but that type theories that know about serious mathematics are not simple at all. Set theory is one of the simpler systems too. Higher order logic is the simplest if one looks at the number of concepts (twenty-five) needed to explain the system. On the other side of the scale, category theory is relatively complex, as is Martin-L\"o{}f's type theory.


\item [[Colin McLarty]], \emph{Set theory for Grothendieck's number theory}, \href{http://www.cwru.edu/artsci/phil/Groth%20found.pdf}{pdf}



\end{itemize}

\vspace{.5em} \hrule \vspace{.5em}
Some old discussions from this page archived \href{http://nforum.mathforge.org/discussion/4172/foundation-of-mathematics/?Focus=33992#Comment_33992}{here}

[[!redirects foundation]] [[!redirects foundations]] [[!redirects Foundation]] [[!redirects Foundations]] [[!redirects foundation of mathematics]] [[!redirects foundations of mathematics]]



\end{document}