algar-lecture-notes.tex

\documentclass[10pt,reqno,a4paper,openany]{amsbook}
\usepackage{etex}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{etoolbox,chngcntr}
\usepackage{amsmath,amsthm,amssymb,array,stmaryrd,color,graphicx,mathtools,multirow,setspace}
\usepackage{soul}\setul{0.3ex}{}
\usepackage{bussproofs}
\usepackage{manfnt}
\usepackage{xspace}
\usepackage{longtable}
\usepackage{booktabs}
\usepackage[protrusion=true,expansion=true]{microtype}
\usepackage[bookmarksdepth=2,pdfencoding=auto]{hyperref}

\graphicspath{{images/}}
\usepackage{libertine}

% Hack to load extpfeil from https://tex.stackexchange.com/a/297109/32372
\expandafter\def\csname opt@stmaryrd.sty\endcsname
{only,shortleftarrow,shortrightarrow}
\usepackage{extpfeil}
\newextarrow{\xbigtoto}{{20}{20}{20}{20}}
   {\bigRelbar\bigRelbar{\bigtwoarrowsleft\rightarrow\rightarrow}}

\usepackage[all]{xy}
\usepackage{tikz}
\usetikzlibrary{calc,shapes.callouts,shapes.arrows,matrix,patterns}
\newcommand{\hcancel}[5]{%
    \tikz[baseline=(tocancel.base)]{
        \node[inner sep=0pt,outer sep=0pt] (tocancel) {#1};
        \draw[red, line width=0.3mm] ($(tocancel.south west)+(#2,#3)$) -- ($(tocancel.north east)+(#4,#5)$);
    }%
}

\usepackage{pifont}
\newcommand{\cmark}{\ding{51}}
\newcommand{\xmark}{\ding{55}}

\usepackage[natbib=true,style=numeric,maxnames=10]{biblatex}
\usepackage[babel]{csquotes}
\bibliography{algar-lecture-notes}

\theoremstyle{definition}
\newtheorem{defn}{Definition}[chapter]
\newtheorem{ex}[defn]{Example}

\theoremstyle{plain}
\newtheorem{prop}[defn]{Proposition}
\newtheorem{cor}[defn]{Corollary}
\newtheorem{lemma}[defn]{Lemma}
\newtheorem{thm}[defn]{Theorem}
\newtheorem{scholium}[defn]{Scholium}

\theoremstyle{remark}
\newtheorem{rem}[defn]{Remark}
\newtheorem{question}[defn]{Question}
\newtheorem{speculation}[defn]{Speculation}
\newtheorem{caveat}[defn]{Caveat}
\newtheorem{conjecture}[defn]{Conjecture}

\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\FF}{\mathbb{F}}
\renewcommand{\AA}{\mathbb{A}}
\newcommand{\A}{\mathcal{A}}
\newcommand{\B}{\mathcal{B}}
\newcommand{\CCC}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\EEE}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\G}{\mathcal{G}}
\let\acuteH\H
\newcommand{\konig}{K\acuteH onig}
\renewcommand{\H}{\mathcal{H}}
\newcommand{\OOO}{\mathcal{O}}
\newcommand{\K}{\mathcal{K}}
\newcommand{\N}{\mathcal{N}}
\newcommand{\M}{\mathcal{M}}
\renewcommand{\L}{\mathcal{L}}
\renewcommand{\P}{\mathcal{P}}
\newcommand{\R}{\mathcal{R}}
\newcommand{\T}{\mathcal{T}}
\newcommand{\I}{\mathcal{I}}
\newcommand{\J}{\mathcal{J}}
\renewcommand{\S}{\mathcal{S}}
\newcommand{\U}{\mathcal{U}}
\newcommand{\V}{\mathcal{V}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\PP}{\mathbb{P}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\CC}{\mathbb{C}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\GG}{\mathbb{G}}
\newcommand{\TT}{\mathbb{T}}
\newcommand{\aaa}{\mathfrak{a}}
\newcommand{\bbb}{\mathfrak{b}}
\newcommand{\ccc}{\mathfrak{c}}
\newcommand{\ppp}{\mathfrak{p}}
\newcommand{\qqq}{\mathfrak{q}}
\newcommand{\mmm}{\mathfrak{m}}
\newcommand{\nnn}{\mathfrak{n}}
\newcommand{\?}{\,{:}\,}
\renewcommand{\_}{\mathpunct{.}\,}

\newenvironment{indentblock}{%
  \list{}{\leftmargin\leftmargin}%
  \item\relax
}{%
  \endlist
}

\newcommand{\defeq}{\vcentcolon=}
\newcommand{\defequiv}{\vcentcolon\equiv}
\newcommand{\seq}[1]{\mathrel{\vdash\!\!\!_{#1}}}

\definecolor{gray}{rgb}{0.7,0.7,0.7}

\title{The curious world of constructive mathematics}
\author{Ingo Blechschmidt \vspace*{-2em}}
%\email{iblech@speicherleck.de}

\makeatletter
\counterwithout{section}{chapter}
\counterwithout{footnote}{chapter}
\counterwithout{table}{chapter}
\counterwithout{figure}{chapter}
\patchcmd{\@thm}{\let\thm@indent\indent}{\let\thm@indent\noindent}{}{}
\patchcmd{\@thm}{\thm@headfont{\scshape}}{\thm@headfont{\bfseries}}{}{}
\patchcmd{\@makechapterhead}{\chaptername}{Lecture}{}{}
\patchcmd{\@chapter}{\chaptername}{Part}{}{}
\patchcmd{\@schapter}{\chaptername}{Part}{}{}
\addto\captionsenglish{\renewcommand\chaptername{Lecture}}
\def\l@section{\@tocline{1}{0pt}{1pc}{}{}} % \bfseries}}
\def\l@chapter{\@tocline{-1}{12pt}{0pt}{}{\bfseries}}
\renewcommand\thechapter{\Roman{chapter}}
\newcommand{\nocontentsline}[3]{}
\newcommand{\tocless}[1]{\let\addcontentsline=\nocontentsline}
\normalparindent=12pt
\parindent=\normalparindent
\renewenvironment{proof}[1][\proofname]{\par
  \pushQED{\qed}%
  \normalfont \topsep6\p@\@plus6\p@\relax
  \trivlist
  \item[\hskip\labelsep
        \itshape
    #1\@addpunct{.}]\ignorespaces
}{%
  \popQED\endtrivlist\@endpefalse
}
\let\@afterindenttrue\@afterindentfalse
\def\subsection{\@startsection{subsection}{2}%
  {0pt}{.5\linespacing\@plus.7\linespacing}{-.5em}%
  {\normalfont\bfseries}}
\makeatother

\newenvironment{intro}{\begin{quote}}{\end{quote}\bigskip\noindent}

\newtheorem{exercise}{Exercise}[chapter]
\renewcommand{\theenumi}{\alph{enumi}}

\urlstyle{sf}

\newcommand{\cl}{\mathrm{cl}}
\newcommand{\notnot}{\emph{not~not}\xspace}
\newcommand{\Sh}{\mathrm{Sh}}
\newcommand{\Set}{\mathrm{Set}}

\begin{document}

\begin{abstract}
Constructive mathematics is a flavor of mathematics in which we use the
axiom of choice and the technique of proof by contradiction only in
certain special cases. The square root of two is constructively still
irrational, but there might be vector spaces without a basis.

As a result, proofs are more informative (for instance regarding
bounds), finer distinctions can be made (for instance between positive
existence and mere impossibility of non-existence) and results apply
more generally: Every constructive result also has a geometric
interpretation, where it applies to continuous families, and an
algorithmic interpretation, yielding computational witnesses such as
procedures for computing the objects whose existence has been shown.

Relinquishing the axiom of choice and the principle of excluded middle also
allows us to explore axioms and notions which are incompatible with
these classical laws, such as mathematical settings in which all
functions are continuous or in which the intuitive idea of a ``generic
ring'' can be put on a firm basis.
\end{abstract}

{
\renewcommand{\newpage}{\ }
\renewcommand{\vfill}{\ }
\renewcommand{\vfil}{\ }
\enlargethispage{7em}
{\vspace*{-6em}\centering\includegraphics[width=0.3\textwidth]{phantoms}\par}
\maketitle
}

\setcounter{tocdepth}{1}
{
\renewcommand{\newpage}{\ }
\tableofcontents
}
\thispagestyle{empty}


\chapter{A first glimpse of constructive mathematics}

\begin{intro}
\it
This lecture provides a first glimpse of constructive mathematics with a
focus on applications of constructive mathematics and on providing
intuition for quickly discerning which techniques and results hold
constructively.

This account is an update and translation of~\cite[Section~1]{blechschmidt:pizzaseminar}
and references
include~\cite{bauer:five-stages-video,bauer:five-stages-article,avigad:constructive,sep:intuitionistic-logic,dummett:basis,melikhov:intuitionistic-logic,streicher:constructive}
or more
specifically~\cite{mines-richman-ruitenburg:constructive-algebra,lombardi-quitte:constructive-algebra}
for constructive algebra and~\cite{bishop-bridges:bible} for constructive
analysis.
\end{intro}

\begin{prop}There are irrational numbers~$x$ and~$y$ such that~$x^y$ is
rational.
\end{prop}
\begin{proof}[First proof] The number~$\sqrt{2}^{\sqrt{2}}$ is rational or
irrational. In the first case, set~$x \defeq \sqrt{2}$, $y \defeq \sqrt{2}$.
In the second case, set~$x \defeq \sqrt{2}^{\sqrt{2}}$, $y \defeq \sqrt{2}$.
\end{proof}
\begin{proof}[Second proof] Set~$x \defeq \sqrt{2}$ and~$y \defeq \log_{\sqrt{2}} 3$.
Then~$x^y = 3$ is rational. The verification that~$y$ is irrational is even
easier than that of~$\sqrt{2}$.\footnote{Let~$y = a/b$ with~$a, b \in \ZZ$
and~$b \neq 0$. Since~$y > 0$, we may assume~$a, b \in \NN$. Then~$3 =
(\sqrt{2})^{a/b}$, hence~$3^{2b} = 2^a$. This is in contradiction to the
uniqueness of the prime factor decomposition, since the factor~$3$ occurs on
the left but not on the right.}
\end{proof}

The first proof is \emph{unconstructive}: It does not actually give us an
example for a pair~$(x,y)$ as desired. In contrast, the second proof is
constructive -- the existential claim is verified by an explicit construction
of a suitable example.

Of the many axioms and inference rules of classical logic, exactly one is
responsible for enabling unconstructive arguments, namely the \emph{principle
of excluded middle}:
\[ \varphi \ \vee\ \neg\varphi. \]
The first proof above used this principle in its very first step. In
constructive mathematics, we abstain from this principle; we build
constructive mathematics on \emph{intuitionistic logic}, which contains neither
this principle nor the (equivalent) \emph{principle of double negation
elimination} stating~$\neg\neg\varphi \Rightarrow \varphi$, and insofar as we
layer a set theory on top of our logical foundation, we abstain from the axiom
of choice (which in presence of other common set-theoretical axioms implies the
principle of excluded middle, see Exercise~\ref{ex:diaconescu}) and from Zorn's lemma. As a
consequence, we cannot generally reason by contradiction in constructive
mathematics, and to demonstrate the existence of an object
it is not enough that its nonexistence would entail a contradiction.

Importantly, in constructive mathematicics we do \emph{not} claim that the principle of
excluded middle is false. \marginpar{\dbend}
Indeed, intuitionistic logic is downwardly compatible
with classical logic (every intuitionistic proof is a fortiori also a classical
proof), and some special instances of the principle of excluded middle and with
it some special instances of proof by contradiction are
intuitionistically verifiable (an example is given in
Proposition~\ref{prop:discreteness}). Instead, in constructive mathematics we
merely do not use the principle of excluded middle.

Also, deducing from a statement of the form~``$\exists x \in X\_ \varphi(x)$''
that there actually is an element~$x \in X$ such that~$\varphi(x)$, and then
using this particular element in the rest of an argument, is intuitionistically a
valid logical inference, just as it is in classical logic. The axiom of choice
is unrelated to this kind of proof step, even though they are sometimes
mistaken.


\section{Proof by contradiction vs. proof of a negation}

A rumor about constructive mathematics states that constructively, the term
``contradiction'' would be generally forbidden. This rumor is false. In fact, we need
to distinguish between two distinct figures of proof which are often conflated
in classical informal mathematics:

\begin{enumerate}
\item[1.] ``Assume~$\neg\varphi$. Then $\ldots$, a contradiction.
Hence~$\neg\varphi$ was false and thus~$\varphi$ holds.''
\item[2.] ``Assume~$\psi$. Then $\ldots$, a contradiction. Hence~$\neg\psi$.''
\end{enumerate}

Arguments of the first form are proper proofs by contradiction and hence not
generally accepted in constructive mathematics. What they establish is
only~$\neg(\neg\varphi)$, the impossibility of~$\neg\varphi$; constructively,
this is weaker than a positive affirmation of~$\varphi$. Though there are
situations in which~$\neg\neg\varphi$ implies~$\varphi$, generally it does not
and hence intuitionistically arguments of the first form fail to
estabilish~$\varphi$.

In contrast, arguments of the second kind are fine from an intuitionistic point
of view: They do not constitute proper proofs by contradiction, but instead are proofs of negated
statements. That such proofs are valid follows directly from the definition of
negation as a certain
implication (which, incidentally, texts on classical logic often also adopt):
\[ \neg\psi \defequiv (\psi \Rightarrow \bot), \]
where~``$\bot$'', pronounced ``bottom'', is \emph{absurdity}, a canonical false
statement. (Informally, absurdity is also written as~``$\lightning$'' or~``$1 = 0$''.)
Hence, to establish~$\neg\psi$, we may give a proof of~$\bot$ under
the assumption~$\psi$, just as we may give a proof of~$\beta$ under the
assumption~$\alpha$ if we want to prove~$\alpha \Rightarrow \beta$.

The two proofs below of the following fact from number theory demonstrate the
difference:
\begin{prop}\label{prop:sqrt2}The number~$\sqrt{2}$ is not rational.\end{prop}
\begin{proof}[Proof (only valid classically)]
Assume that the claim is false, that is, that the number~$\sqrt{2}$ is
\emph{not not} rational. Then~$\sqrt{2}$ is rational. Hence there are
integers~$a$ and~$b$ with~$\sqrt{2} = a / b$. Thus~$2b^2 = a^2$. This identity
contradicts the uniqueness of the prime factor decomposition, since the
factor~$2$ occurs an odd number of times on the left but an even number of
times on the right.
\end{proof}
\begin{proof}[Proof (also valid intuitionistically)]
Assume that the number~$\sqrt{2}$ is rational. Then there are integers~$a$
and~$b$, \ldots, a contradiction.
[The requisite theorem on the uniqueness of the prime factor decomposition admits an
intuitionistic proof.]
\end{proof}

Constructively stronger than the statement that~$\sqrt{2}$ is merely
\emph{not rational} is the statement that for every rational number~$x$
the distance~$|\sqrt{2} - x|$ is positive. This stronger claim admits an
intuitionistic proof as well (Exercise~\ref{ex:sqrt2}).


\section{Constructive meaning of mathematical statements}

By our training in classical mathematics, abstaining from the principle of
excluded middle can feel peculiar, perhaps even outrageous: Isn't it obvious
that every mathematical statement is true or false?

This sense of bewilderment is resolved by observing that \emph{even though
constructive mathematicians use the same logical symbols, they have a slightly
different meaning in mind.} When a constructive mathematician argues for some
statement~$\varphi$, they mean that they have an \emph{explicit witness}
for~$\varphi$. This shift in meaning from the classical interpretation is
elaborated by the \emph{Brouwer--Heyting--Kolmogorov interpretation} sketched
below. It is informal and philosophical in nature and not without
issues~\cite{artemov:bhk,sanz-piecha:critical-bhk,dalen:bhk}, but still a useful guide to
the constructive meaning of mathematical statements.


\subsection{The Brouwer--Heyting--Kolmogorov interpretation}

The notion of witnesses is compositional in nature and starts out with the notion of witnesses for \emph{atomic
statements}, those not built from substatements using the logical
connectives~$\wedge,\vee,\Rightarrow$ or the quantifiers~$\forall,\exists$. For
instance, in formal number theory, the atomic statements are of the form
``$s = t$'',
where~$s$ and~$t$ are terms for natural numbers; statements of this form are so
simple that we can check them directly so that witnesses don't need to supply
particular additional information. We hence decree that true atomic statements
have trivial witnesses and that false atomic statements have no witnesses at
all.

Table~\ref{table:bhk} explains how compound statements should be witnessed. For
instance, a witness of a statement of the form
\[ \forall n \? \NN\_ \bigl(\varphi(n) \Rightarrow \psi(n)\bigr) \]
is a rule explaining how, for every natural number~$n : \NN$, witnesses
for~$\varphi(n)$ give rise to witnesses for~$\psi(n)$.

\begin{table}
  \centering
  \small
  \renewcommand{\arraystretch}{1.3}
  \begin{tabular}{@{}rp{4.3cm}p{5.3cm}@{}}
    \toprule
    & {classical logic} & {intuitionistic logic}
    \\\midrule
    statement $\varphi$ & The statement $\varphi$ holds. & We have a witness for $\varphi$. \\
    $\bot$ & A contradiction holds. & We have a witness for a contradiction. \\
    $\varphi \wedge \psi$ & $\varphi$ and $\psi$ hold. & We have a witness for~$\varphi$ and for~$\psi$. \\
    $\varphi \vee \psi$ & $\varphi$ or $\psi$ hold. & We have a witness for~$\varphi$ or for~$\psi$. \\
    $\varphi \Rightarrow \psi$ & If~$\varphi$ holds, then so does~$\psi$. &
    We can (uniformly) construct witnesses for~$\psi$ from witnesses
    for~$\varphi$. \\
    $\neg\varphi$ &
      $\varphi$ does not hold. &
      There is no witness for~$\varphi$. \\
    $\forall x\?X\_ \varphi(x)$ & For all $x \? X$ it holds that~$\varphi(x).$ &
      We can (uniformly) construct, for all~$x \? X$, witnesses for~$\varphi(x)$. \\
    $\exists x\?X\_ \varphi(x)$ & \raggedright There is at least one~$x \? X$
    such that~$\varphi(x)$ holds. & {\raggedright
      We have a~$x \? X$ together with a witness for~$\varphi(x)$.} \\
    \bottomrule
  \end{tabular}
  \caption{\label{table:bhk}Informal recursive definition of the notion of witnesses.}
\end{table}

\begin{ex}
According to the Brouwer--Heyting--Kolmogorov interpretation, the principle of
excluded middle states that we can construct, for every~$\varphi$,
either a witness for~$\varphi$ or a witness for~$\neg\varphi$. This claim is
obviously false.
\end{ex}

\begin{ex}
The BHK interpretation of a doubly negated statement~$\neg\neg\varphi$ is that
there is no witness for~$\neg\varphi$. This state of affairs does not entail
that we actually have a witness for~$\varphi$; in a sense, the
statement~$\varphi$ is only ``potentially true''.
\end{ex}

\begin{ex}\label{ex:key}
Assuming that we cannot find our apartment key, but know that it has to be
somewhere (because we used it last night to unlock the door), constructively we
can only defend the doubly negated statement
\[ \neg\neg (\exists x\_ \text{the key is at position~$x$}). \]
\end{ex}

\begin{ex}
We are running errands and are remembering that we need to fetch certain
ingredients. Unfortunately we don't recall any of them right now. Then we can
constructively defend the statement that the set of ingredients to fetch is not
empty, not however the stronger statement that this set is inhabited.
\end{ex}

\begin{ex}[\cite{sigfpe:katemoss,bbc:katemoss}]
A video surfaced depicting Kate Moss taking drugs, more precisely either drugs
of some type~A or drugs of some type~B. However from the video it wasn't clear
which type of drug it actually was. Hence there was no evidence for either type
of consumption; Kate Moss wasn't prosecuted.
\end{ex}

\begin{rem}The reference of an unspecified ``we'' in table~\ref{table:bhk}
renders our account of the BHK interpretation not only informal, but is also
somewhat misleading. As in classical mathematics, judgments of intuitionistic
logic do not actually depend on you, me or other mathematicians. It's perfectly
possible that statements which haven't yet been constructively verified admit
(as yet unknown) witnesses. More details can be found
in~\cite[pp.~42]{kohlenbach:applprooftheory} and
in~\cite{artemov:bhk,sanz-piecha:critical-bhk,dalen:bhk}. The
Brouwer--Heyting--Kolmogorov interpretation is made more formal and precise by
\emph{realizability theory}~\cite{bauer:realizability,oosten:realizability}.
\end{rem}


\subsection{The computability interpretation}

A second interpretation of mathematical statements suited for constructive
mathematics is given by the following motto: In a certain sense, \emph{we
accept a mathematical statement in constructive mathematics if and only if
there is a computer program witnessing it in finite time.} For instance, that
the statement
\[ \forall n \? \NN\_ \exists p \? \NN\_ p \geq n \wedge \text{$p$ is prime} \]
is valid in constructive mathematics corresponds to the fact that there is a
computer program which reads a number~$n$ as input and then, after some
computation, produces a prime number~$p \geq n$ as output (together with a
witness that~$p$ is in fact greater or equal than~$n$ and that~$p$ is prime).

For the motto to be correct, the notion of ``witnessed by a computer program''
has to be interpreted in sufficiently generous manner, not least because
uncountable and uncomputable structures have their place in constructive
mathematics just as in classical mathematics. A more formal rendition is
provided by the celebrated \emph{Curry--Howard correspondence} and
\emph{propositions as (some) types}.

\begin{rem}Constructive mathematics is emphatically not the same as computable
mathematics; in particular, there are statements which do admit a witness by a
computer program but which are rejected in (most schools of) constructive
mathematics (see Exercise~\ref{ex:markov}). The apparent tension with the motto
presented above is resolved in its more formal treatment. In any case, the two
subjects are closely related and their connection provides useful
intuition.\end{rem}


\subsection{The geometric interpretation}

A third interpretation of mathematical statements suited for constructive
mathematics, and of a substantially different kind than the BHK and the
computability interpretation, is provided by geometry. In a certain sense,
\emph{we accept a mathematical statement in constructive mathematics if and
only if it holds locally in continuous families}.

For instance, while it is a fact of classical mathematics that every complex
number has a square root, a fundamental observation in complex analysis is that
such roots cannot be picked in a locally continuous manner. Hence the standard
formulation of the fundamental theorem of algebra fails in constructive
mathematics.\footnote{More precisely, the fundamental theorem of algebra fails
for the complex numbers built from pairs of Dedekind reals. Constructively, the
reals built using Dedekind cuts are not the same as the reals built using
Cauchy sequences; in fact, the latter are a subset of the former and serve a
different purpose. Such a bifurcation of classically equivalent notions is
typical of constructive mathematics. The fundamental theorem of algebra is
correct for the flavor of complex numbers built from Cauchy
reals~\cite{ruitenburg:roots}, and also for the algebraic
numbers~\cite[Section~VII.4]{mines-richman-ruitenburg:constructive-algebra}
[XXX insert better references] and for complex polynomials (of either flavor)
which are separable. Furthermore, the fundamental theorem of algebra holds in
an approximate sense and in a multiset sense~\cite{richman:fta}, and the
standard version only requires mild choice
principles~\cite{bridges-richman-schuster:wcc}.} This example will be discussed
in more detail in Section~\ref{sect:fta}.

The geometric interpretation not only gives transparent explanations to the
logical subtleties of constructive mathematics, but is in a more precise form
also the workhorse of many modern applications of constructive mathematics to
mathematics in general. We will hence dedicate ample of space to the geometric
interpretation by devoting Lecture~\ref{lect:toposes} to it, and will discuss
some of its more advanced applications in Lecture~\ref{lect:generic}.


\section{Finer distinctions supported by constructive mathematics}

By relinquishing the blanket principle of excluded middle, constructive
mathematics allows us to make finer distinctions -- distinctions which are
hidden in classical mathematics, but carry algorithmic and geometric
significance. We have already seen one instance of this increased
expressiveness in Example~\ref{ex:key}: In classical mathematics, we are
trained to cancel double negations as soon as they arise, but constructively
there is a substantial difference between actually having a mathematical object
and merely knowing that its nonexistence is impossible.


\subsection{Decidability of equality}

A further examples pertains to the basic notion of equality. In classical
mathematics, any given elements~$a,b$ of a set~$X$ are either equal or not --
trivially so, by the principle of excluded middle. Constructively, the
situation is more nuanced.

Firstly, in a positive direction, we do have the following result.

\begin{prop}\label{prop:discreteness}
For every pair of natural numbers~$a$ and~$b$, either~$a = b$ or~$a \neq b$.\end{prop}

\begin{proof}[Proof (constructive)]
We spell out only the case~$b = 0$, that is, we only spell out a proof that
every natural number~$a$ is either zero or not. To this end, we do a induction
on~$a$.

The base step~$a = 0$ is trivial, since if~$a = 0$ then also~$a = 0 \vee a \neq
0$ (we can always weaken statements by adding additional disjuncts).

In the inductive step~$a \to a + 1$, we have~$a + 1 \neq 0$ by one of the basic
axioms of arithmetic (for a complete list, see
Exercise~\ref{ex:stability-axioms}) and hence in particular~$a+1 = 0 \vee
a+1\neq0$ by weakening. (This proof is one of the rare instances of a correct
induction proof where the inductive step does not refer to the induction
hypothesis.)
\end{proof}

As from any constructive proof, a computer program witnessing the asserted fact
can be extracted. It will (roughly) have type $\mathsf{Nat} \times \mathsf{Nat}
\to \mathsf{Bool}$, computing~$\mathsf{true}$ or~$\mathsf{false}$ depending on
whether its two inputs agree or are distinct. Because the presented proof proceeded
by induction, the resulting program will proceed by recursion.

Sets like the set of natural numbers for which equality is decidable have a
special name in constructive mathematics, hinting at a connection with topology:
\begin{defn}A set~$X$ is \emph{discrete} if and only if for every
elements~$a,b \in X$, either~$a = b$ or~$a \neq b$.\end{defn}
In classical mathematics, all sets are discrete. Constructively, discreteness
is a nontrivial property, and although~$\NN$ is discrete and with it also~$\ZZ$
and~$\QQ$, there are many important sets which constructively cannot be shown
to be discrete:

\begin{prop}Already in the case~$X = \{\star\}$ it holds that if the
powerset~$P(X)$ is discrete, then the principle of excluded middle
holds.\end{prop}

\begin{proof}Let~$\varphi$ be a statement and consider the element~$K_\varphi
\defeq \{ x \in X \,|\, \varphi \} \in P(X)$. If~$K_\varphi = X$,
then~$\varphi$; and if~$K_\varphi \neq X$, then~$\neg\varphi$.\end{proof}

\begin{prop}If the set of (any of the usual flavors of the) reals is discrete,
then the principle of omniscience holds (XXX this has not been
introduced).\end{prop}

The failure of the discreteness of the set of real numbers can be explained in
computational terms as follows. In computable mathematics, a real numbers is
represented by a program computing better and better rational approximations.
Given two such programs, we can simulate or execute them to obtain
approximations to a desired precision, hoping to distinguish the two
represented real numbers. However, in case that the two numbers actually agree,
in finite time we will never verify this fact: Computably, we cannot rule out
the possibility that a difference between the two numbers will only be detected
in the as yet unexplored range of rational approximations.\footnote{This
argument can be formalized using Turing machines and realizability theory;
see~\cite[Section~4.2.1]{blechschmidt:filmat} for a review. The analysis
dramatically changes (see~\cite[Section~4.2.2]{blechschmidt:filmat}) if we
instead refer to the infinite-time Turing machines of Hamkins and
Lewis~\cite{hamkins-lewis:ittm} which can carry out an infinite amount of
computation before halting. A philosophically intriguing (and, by necessity,
informal) account referring to machines in the real world as opposed to
idealized Turing machines has been put forward by Andrej
Bauer~\cite{bauer:int-mathematics}.}

Lest an impression that only topologically simple domains can be shown to be
discrete in constructive mathematics emerges, here is a more sophisticated
example of a discrete set.

\begin{prop}The set~$\overline{\QQ}$ of algebraic numbers is
discrete.\end{prop}

\begin{proof}See~\cite[Section~XXX]{mines-richman-ruitenburg:constructive-algebra}.\end{proof}


\subsection{Minima of sets of natural numbers}

As an approximate rule of thumb, in the author's personal experience, every
result of classical mathematics which has received constructive scrutiny turned
out to either
\begin{enumerate}
\item be manifestly and unsurprisingly unconstructive, or
\item admit a constructive reformulation.
\end{enumerate}
Of course, the jury is still out on the many results not yet studied from a
constructive point of view.

The results ``every vector space has a basis'' and ``there exist
nonmeasurable subsets of the reals'' are of the first kind. Such results often
provide great abstract insight to the mathematical landscape -- it is
comforting to know that there cannot be vector spaces so bizarre that they
don't have a basis or that the notion of measurable subsets is not trivial.
On the other hand,
such results also tend to not influence concrete situations too much: How could
an infinite basis for which there is no hope that we ever learn any actual
description of inform our computations? (Better uncover topological structure
and look for a Schauder basis!)

Indeed, there are even metatheorems, reported on in
Lecture~\ref{lect:constructive-content}, to the effect that in sufficiently
concrete and logically simple situations, the axiom of choice and the principle
of excluded middle do not allow to prove results which couldn't be proven
without them. And as further evidence, there is Friedman's \emph{grand
conjecture}~\cite{XXX} -- informal but not yet challenged -- that every result
published in the Annals by a mathematician not self-identifying as a set
theorist or logician can be (reformulated to be) provable even in~\textsc{efa},
a foundational system much weaker than~\textsc{zfc},~\textsc{zf} or even Peano
arithmetic.

An example of a result of type~(b) uses the basic observation that every
inhabited set of natural numbers contains a minimal element. This result is not
available in constructive mathematics as stated, but there are two constructive
substitutes.

\begin{defn}A set~$X$ is \emph{inhabited} if and only if there exists an
element of~$X$.\end{defn}

Constructively, the condition that a set~$X$ is inhabited is stronger than~$X$
merely not being empty. The latter is equivalent to the statement that it is
\notnot the case that~$X$ is inhabited.

\begin{prop}If every inhabited set of natural numbers contains a minimal
element, then the principle of excluded middle holds.\end{prop}

To salvage the classical result, we can strengthen its assumption or weaken its
conclusion.

\begin{defn}A subset~$U \subseteq X$ is \emph{detachable} if and only if for
every element~$x \in X$, either~$x \in U$ or~$x \not\in U$.\end{defn}

For instance, the subset of~$\NN$ consisting of the prime numbers is detachable,
while the subset of those numbers~$n$ such that the~$n$-th Turing machine
terminates cannot constructively be shown to be detachable.\footnote{A
computable witness to detachability of this subset would be a \emph{halting
oracle}, but a basic fact of computability theory is that there no such
oracles.}

\begin{prop}\label{prop:minima}\begin{enumerate}
\item Every detachable inhabited subset of~$\NN$ contains a minimum.
\item Every inhabited subst of~$\NN$ does~\notnot contain a minimum.
\end{enumerate}
\end{prop}


\section{Exercises}

\begin{exercise}[Constructive status of classical tautologies]\label{ex:tautologies}
Which of the following classical tautologies can reasonably be expected to
admit constructive proofs?
\begin{enumerate}
\item $\neg(\alpha \vee \beta) \ \Longrightarrow\ \neg\alpha \wedge \neg\beta$
\item $\neg(\alpha \wedge \beta) \ \Longrightarrow\ \neg\alpha \vee \neg\beta$
\item $(\alpha \Rightarrow \beta) \ \Longrightarrow\ (\neg\alpha \vee \beta)$
\item $(\alpha \vee \beta) \wedge \neg\alpha \ \Longrightarrow\ \beta$
\item $\forall M\?P(X)\_ (\exists x\?X\_ x \in M) \vee M = \emptyset$
(already interesting for~$X = \{\star\}$)
\item $\forall n\?\NN\_ (n = 0 \vee n \neq 0)$
\item $\forall x\?\RR\_ (x = 0 \vee x \neq 0)$
\item $\forall x\?\RR\_ (\neg(\exists y\?\RR\_ xy=1) \Rightarrow x = 0)$
\item $\forall z\?\overline{\QQ}\_ (z = 0 \vee z \neq 0)$
\item $\forall f \? \NN \to \{0,1\}\_ (\neg\neg\exists n \? \NN\_ f(n) = 0)
\Rightarrow (\exists n \? \NN\_ f(n) = 0)$ (Markov's principle)
\item $\forall f \? \NN \to \{0,1\}\_ \exists n \? \NN\_ (f(n) = 1
\Rightarrow (\forall m \? \NN\_ f(m) = 1))$ (Drinker's paradox)
\item $\forall f \? \NN \to \{0,1\}\_ (\exists n \? \NN\_ f(n) = 0) \vee
(\forall n \? \NN\_ f(n) = 1)$
\item $\forall f \? \NN_\infty \to \{0,1\}\_ (\exists n \? \NN_\infty\_ f(n) = 0) \vee
(\forall n \? \NN_\infty\_ f(n) = 1)$

{\noindent\scriptsize\emph{Remark.} The set~$\NN_\infty$ is the \emph{one-point
compactification} of~$\NN$. A sensible definition of it in constructive mathematics
is as the set of decreasing binary sequences~$(x_0,x_1,x_2,\ldots)$. The
naturals embed into~$\NN_\infty$ by mapping~$n$ to the sequence~$1^n 0^\omega =
(1,\ldots,1,0,\ldots,0)$, and an element not in the image of this embedding
is~$\infty \defeq 1^\omega = (1,1,\ldots)$. Assuming the principle of excluded
middle (or already weaker principles), every element of~$\NN_\infty$ is of one
of these two forms. Martín Escardó has worked extensively on unexpected
instances of the principle of omniscience for searchable sets
like~$\NN_\infty$~\cite{escardo:omniscience1,escardo:omniscience2,escardo:omniscience}.\par}
\end{enumerate}
\end{exercise}

\begin{exercise}[Basics on negation]
Recalling that negation is defined as implying absurdity,~$\neg\varphi
\defequiv (\varphi \Rightarrow \bot)$, verify intuitionistically without
recourse to truth tables:
\begin{enumerate}
\item $\varphi \Rightarrow \neg\neg\varphi$
\item $\neg\neg\neg\varphi \Leftrightarrow \neg\varphi$
\item $\neg\neg(\varphi \vee \neg\varphi)$
\item $\neg\neg(\alpha \wedge \beta) \Leftrightarrow (\neg\neg\alpha \wedge
\neg\neg\beta)$
\item $\neg(\alpha \vee \beta) \Longleftrightarrow (\neg\alpha \wedge \neg\beta)$
\item $(\neg\neg\alpha \wedge (\alpha \Rightarrow \neg\neg\beta)) \Longrightarrow
\neg\neg\beta$
\item $(\forall\psi\_ (\psi \vee \neg\psi))
\Longleftrightarrow (\forall\psi\_ ((\neg\neg\psi) \Rightarrow
\psi))$

{\noindent\scriptsize\emph{Hint.}
Don't try to verify that double negation elimination for a specific
statement~$\psi$ implies the principle of excluded middle for that same
statement~$\psi$ -- this cannot be shown. There are subtleties regarding the
quantification over $\psi$ (this is not expressible in pure first-order logic),
however the exercise is still instructive if we gloss over this issue.\par}
\end{enumerate}
\end{exercise}

\begin{exercise}[An epistemic riddle on transcendental numbers]
Verify, using a proof by contradiction, that at least one of the numbers~$e +
\pi$ and~$e - \pi$ is transcendental; and that at least one of the
numbers~$e + \pi$ and~$e \cdot \pi$ is transcendental.

{\noindent\scriptsize\emph{Note.} At time of writing, for none of these numbers
a (constructive or classical) proof of their transcendence is known.\par}
\end{exercise}

\begin{exercise}[A stronger form of the irrationality of~$\sqrt{2}$]
\label{ex:sqrt2}
Mine the proof of Proposition~\ref{prop:sqrt2} to give an intuitionistic proof
that for every rational number~$x$, the distance~$|\sqrt{2}-x|$ is positive.

{\noindent\scriptsize\emph{Note.} Strictly speaking, this exercise presupposes
familiarity with an intuitionistic account of the basics of undergraduate real
analysis. Without it, one cannot really be expected to precisely think about
these matters. One such account (though assuming the axiom of dependent choice)
is~\cite{bishop-bridges:bible}. However, this exercise is insightful even when carried out
slightly informally. Keep in mind that, to show that a real number is positive,
constructively it is not enough to merely verify that it cannot be zero or
negative. A safe way to verify that a real number~$a$ is positive is to exhibit
a rational number~$b$ such that~$a \geq b > 0$.\par}
\end{exercise}

\begin{exercise}[Brouwerian counterexamples]
Show that each of the following statements implies the principle of excluded middle,
hence is not available in constructive mathematics.
\begin{enumerate}
\item Every ideal of~$\ZZ$ is finitely generated.

{\noindent\scriptsize\emph{Hint.} Use that finitely generated ideals of~$\ZZ$
are principal ideals and consider the ideal~$\aaa \defeq \{ x \in \ZZ
\,|\, x = 0 \vee \varphi \}$.\par}

{\noindent\scriptsize\emph{Remark.} The failure of every ideal of~$\ZZ$ to be
finitely generated should not be misconstrued to exclaim that in constructive
mathematics, there suddenly would be ideals of~$\ZZ$ of infinite rank. The
failure is simply because, given an abstract ideal, we cannot pinpoint a finite
system of generators.\par}

\item Over every field, the polynomial~$X^2 + 1$ is either reducible or
irreducible.

{\noindent\scriptsize\emph{Hint.} Consider the field~$K \defeq \{ z \in \QQ(i)
\,|\, z \in \QQ \vee \varphi \}$.\par}

\item Subsets of Kuratowski-finite sets are Kuratowski-finite.

{\noindent\scriptsize\emph{Note.} A set~$X$ is \emph{Kuratowski-finite} if and
only if, for some number~$n \in \NN$, there is a surjective map~$[n] \to X$,
where~$[n] = \{ 0,1,\ldots,n-1 \}$. More briefly, a set~$X$ is
Kuratowski-finite iff its elements can be enumerated: $X = \{x_1,\ldots,x_n \}$.\par}

\item Every subset of the (Cauchy or Dedekind) reals which is inhabited and
bounded from above has a supremum.

{\noindent\scriptsize\emph{Note.} A \emph{supremum} of a set~$M$ of reals is a
number~$s$ such that~$M \leq s$ (that is~$x \leq s$ for all~$x \in M$) and such
that for every number~$s'$ with~$M \leq s'$, $s \leq s'$. In constructive
mathematics, we can make finer distinctions between the classically equivalent
constructions of the real numbers: The reals constructed using Cauchy
sequences inject into the reals constructed using Dedekind cuts which in turn
inject into the MacNeille reals, and each serve a different purpose. The Cauchy
and Dedekind reals cannot constructively be shown to be complete in the sense
of this exercise, while the MacNeille reals can. Conversely, the rationals can
be shown to be dense in the first two kinds of reals but not in the MacNeille
reals~\cite[Section~D4.7]{johnstone:elephant}.\par}
\end{enumerate}
Show that the following statement implies Markov's principle (from
Exercise~\ref{ex:tautologies}):
\begin{enumerate}
\addtocounter{enumi}{4}
\item Every real number which is not zero is invertible.
\end{enumerate}
\noindent
Brouwerian counterexamples abound in constructive mathematics; when developing
a constructive account of a theory, they help to clearly demarcate its limits.
As such additional Brouwerian counterexamples can be found in most texts on
constructive mathematics, such
as~\cite{mines-richman-ruitenburg:constructive-algebra}; a compilation mainly
from constructive analysis can be found
in~\cite{mandelkern:brouwerian-counterexamples}.
\end{exercise}

\begin{exercise}[Markov's principle]\label{ex:markov}
Markov's principle is the statement that
\[ \forall f \? \NN \to \{0,1\}\_ (\neg\neg\exists n \? \NN\_ f(n) = 0)
\Rightarrow (\exists n \? \NN\_ f(n) = 0). \]
It is a simple instance of the classical principle of double-negation
elimination, but not available in (most schools of) constructive mathematics.
\begin{enumerate}
\item Why does Markov's principle imply that programs which do not run forever
actually halt?
\item Explain why Markov's principle is witnessed by a computer program (even
though it does not admit a constructive proof). Which assumption on your
metatheory does your argument require?
\end{enumerate}
\end{exercise}

\begin{exercise}[Minima of sets of natural numbers, part one]\label{ex:minima1}
\begin{enumerate}
\item Give a constructive proof of Proposition~\ref{prop:minima}(b).
\item What does the computational witness extracted from the proof of
Proposition~\ref{prop:minima}(a) look like? Can you devise a different proof
corresponding to a different algorithm?
\end{enumerate}
\end{exercise}

\begin{exercise}[Diaconescu's theorem]
\label{ex:diaconescu}
The axiom of choice can be put as: ``Every surjective map has a
section.'' (A \emph{section}~$s$ to a surjective map~$f$ is a map in the other direction such that~$f \circ s =
\mathrm{id}$.) A theorem of Diaconescu states that
the axiom of choice implies the principle of excluded middle. To this end, let~$\varphi$ be a
statement and consider the subsets
\begin{align*}
  U &= \{ x \in X \,|\, (x = 0) \vee \varphi \} \\
  V &= \{ x \in X \,|\, (x = 1) \vee \varphi \}
\end{align*}
of the discrete set~$X \defeq \{ 0,1 \}$.
\begin{enumerate}
\item Verify that~$U = V$ if and only if~$\varphi$.
\item Using that~$x = y \vee x \neq y$ for all elements~$x,y \in X$, show that
the existence of a section of the surjective map
\[ \begin{array}{@{}rcl@{}}
  X &\longrightarrow& \{U,V\} \\
  0 &\longmapsto& U \\
  1 &\longmapsto& V
\end{array} \]
implies~$\varphi \vee \neg\varphi$.
\end{enumerate}
\end{exercise}

% - What constructive mathematics is about: finer distinctions, algorithmic
%   interpretation, geometric interpretation (including teaser on why we
%   might care)
% - Proof by and proof of a contradiction: powers of irrational numbers,
%   discreteness of N, Q, Qbar, failure of discreteness of R
% - Positive information from negative? de Morgan, minimums of sets of
%   natural numbers
% - Relation to classical mathematics
% - Finite sets and the axiom of choice
% - Axiomatic freedom: all functions continuous, all functions
%   computable, generic prime ideal


\chapter{On the constructive content of classical proofs}
\label{lect:constructive-content}

\begin{intro}
Decades of experience in constructive mathematics show: \emph{Most results
in classical mathematics, even those whose proof rests on
non-constructive principles like the axiom of choice or the principle of
excluded middle, have a hidden constructive core.} With a mix of
experience, seasoned tools and general metatheorems, this constructive
content can be extracted from classical proofs. In this way we obtain
constructive reformulations of classical results, especially
if they are of a sufficiently concrete nature.

For instance, while the existence of maximal ideals in arbitrary rings
is equivalent to the axiom of choice, every first-order consequence of
their existence for linear algebra over rings also holds constructively.

This lecture illustrates the latent constructive nature of classical
proofs with examples and presents two general metatheorems which
elucidate proof mining for constructive content. The author learned this
material mostly from diverse texts and slides of Thierry Coquand; the
reference~\cite{coquand:classical} is a good start.
\end{intro}

\begin{thm}[Dickson's lemma]\label{thm:dickson}
Let~$k \in \NN$. Let~$f : \NN \to \NN^k$ be an arbitrary map. Then there are
indices~$i < j$ such that~$f(i) \leq f(j)$ (componentwise).
\end{thm}

\begin{proof}[Proof (classical)]The case~$k = 0$ is trivial and we omit demonstrations of the cases~$k
\geq 2$, hence let~$k = 1$. In this case, the map~$f$ attains some minimal
value. Set~$i$ to be (one of the) positions where this minimal value is
attained. Set~$j \defeq i+1$. Then, trivially, $f(i) \leq f(j)$.
\end{proof}

\begin{thm}\label{thm:surjective-matrix}
Let~$M$ be a surjective matrix with more rows than columns over a commutative
ring~$A$ with unit. Then~$1 = 0$ in~$A$.
\end{thm}

\begin{proof}[Proof (classical)]Assume not. Then there is a maximal
ideal~$\mmm \subseteq A$. The matrix~$M$ remains surjective when considered over
the quotient ring~$A/\mmm$, and by maximality this quotient ring is a field.
Hence we have a contradiction to basic linear algebra, namely to the basic fact
that matrices over fields are not surjective if they have more rows than
columns.\end{proof}

What is the meaning of these non-effective proofs? Theorem~\ref{thm:dickson}
claims the existence of a finite object with a decidable property (a
pair~$(i,j)$ such that~$f(i) \leq f(j)$), but the given proof employs
transfinite methods and gives no indication how we could compute or otherwise
find this object. Instead, the classical proof asks us to grasp the infinitude
of all values of~$f$ and determine their minimum. The issue is even more
pronounced with Theorem~\ref{thm:surjective-matrix}, since the existence of
maximal ideals in nontrivial rings requires the axiom of
choice~\cite{scott:prime-ideals,hodges:krull,banaschewski:krull,erne:krull,howard-rubin:ac}.
To add one more conundrum: Assume that we have a classical proof, using the principle
of excluded middle and the axiom of choice, that some given Turing machine
terminates. Can we then constructively accept that the machine will halt? Do we
have an upper bound for the number of computational steps the machine carries
out before halting?

Astoundingly, it is almost always the case that from classical proofs useful
constructive content can be extracted. In fact, due to general metatheorems,
in many cases there are even explicit mechanical procedures for extracting this
hidden content, while other cases require more creativity for determining
suitable constructive reformulations. For instance:

\begin{enumerate}
\item \emph{Eliminating the axiom of choice by the~$L$-translation.} Can the
axiom of choice ever help in proving arithmetical statements, those first-order
statements in which all quantifiers range over the natural numbers? Well, it surely
might. But a result of Gödel states that~\textsc{zfc} (Zermelo--Fraenkel set
theory with the axiom of choice) is conservative over~\textsc{zf} (ZF set
theory without it) for such statements -- hence all appeals to this axiom can
be mechanically eliminated from a given proof. This is true even if the proof
transcends the arithmetical realm and includes statements which are not
arithmetical; only the asserted claim is required to be arithmetical. Hence we
are free to use the axiom of choice, tranquil in knowing that we could always
reformulate our proofs without it.\footnote{Zermelo--Fraenkel set theory with
the axiom of choice is the go-to foundation of mathematics often cited as
supporting ``almost all'' of current mathematics, one important exception being
some (definitions and) results in category theory dealing with large
structures~\cite{shulman:set-theory,feferman:set-foundations}. A fundamental
result due to Gödel is that the axiom of choice ``holds in~$L$'', the
\emph{constructible universe}, even if it might not hold in~$V$, the true
universe of all sets. More precisely, if~\textsc{zfc} shows some
statement~$\varphi$, then~\textsc{zf} shows its~$L$-relativized
version~$\varphi^L$, where all quantifiers have been restricted to range
over~$L$ instead of~$V$. The conservation result follows because the natural
numbers ``are absolute between~$V$
and~$L$''~\cite{goedel:ac-gch,schoenfield:predicativity}.}

\item \emph{Eliminating the principle of excluded middle by the double-negation
translation and its variants.} At the price of
slightly modifying the asserted claim, the principle of excluded middle
can always be mechanically eliminated from a given proof. This
elimination procedure is facilitated by the \emph{double-negation translation}
reviewed below. In some cases, a refined translation even allows us to preserve the asserted
claim exactly; this technique is variously known as \emph{Friedman's trick},
\emph{nontrivial exit continuation} or (the baby version of) \emph{Barr's
theorem}. To cite a specific instance of this phenomenon, classical~\textsc{zf}
set theory is conservative over its intuitionistic cousin~\textsc{izf}
for~$\Pi^0_2$-statements (statements of the form~$\forall\ldots\forall\_
\exists\ldots\exists\_ \%$, where all quantifiers in the final~``$\%$''
are bounded).

\item \emph{Embracing generic models.} A useful companion to both of the
aforementioned techniques is to switch from referencing all models of a certain
kind to referencing only the \emph{generic model}. For instance, Krull's lemma
stating that a ring element is already nilpotent if it is contained in all
prime ideals requires the Boolean Prime Ideal Theorem, a slightly weaker
version of the axiom of choice but still ineffective and unconstructive.
However, Krull's lemma is valid in the form that a ring element is nilpotent if
it is contained in the \emph{generic prime ideal}. This particular example has
received lots of attention (see the references
in~\cite{blechschmidt-schuster:constructive-maximal-ideals}) and the general
technique will be the object of the fourth lecture.
\end{enumerate}

Noticeably missing in this list is any technique for eliminating uses of the
\emph{powerset axiom} stating that the collection of all subsets of a given
set is again a set. While this axiom is uncontested by ordinary constructive
mathematics and doesn't receive nearly as much philosophical attention as the
axiom of choice or the principle of excluded middle, it is this axiom which actually
and substantially increases logical strength. While~\textsc{zfc}, \textsc{zf}
and \textsc{izf} are equiconsistent (and in fact verify the same
arithmetical~$\Pi^0_2$-statements), systems without the powerset axiom such as Kripke--Platek
set theory~(\textsc{kp}) or constructive Zermelo--Fraenkel set
theory~(\textsc{czf}) are much weaker. We will not discuss this curious state
of affairs and only note that rejecting the powerset axiom can be
well-motivated and is the basis of \emph{predicative mathematics};
references include~\cite{crosilla:predicativity,aczel-rathjen:cst}.


\section{The double-negation embedding of classical into constructive mathematics}

The premier difference between constructive and classical mathematics is in the
existential quantifier~``$\exists$'' and disjunction~``$\vee$''.
Constructively, to verify an existential statement, it is not enough to verify
the impossibility of nonexistence; and to verify a disjunction~$\alpha \vee
\beta$, it is not enough to verify the impossibility of~$\neg\alpha \wedge
\neg\beta$.

That is not to say, however, that the more informative versions of~``$\exists$''
and~``$\vee$'' of constructive mathematics would be in any senser ``better''
than their classical counterparts: There are many situations in which the
classical semantics is exactly the appropriate one. Should we somehow combine
classical and intuitionistic logic to form a joint logic supporting
both the informative connectives from intuitionistic logic and the ``platonic''
connectives from classical mathematics?

Perhaps surprisingly, it turns out that no such combination is necessary, for
the classical connectives are already definable in intuitionistic logic:
\begin{align*}
  \exists^\cl x \? X\_ \varphi(x)
    &\quad\defequiv\quad \neg\neg (\exists x\?X\_ \varphi(x))
    && \text{(this is eqv. to $\neg(\forall x\?X\_ \neg\varphi(x))$)} \\
  \alpha \vee^\cl \beta
    &\quad\defequiv\quad \neg\neg (\alpha \vee \beta)
    && \text{(this is eqv. to $\neg(\neg\alpha \wedge \neg\beta)$)}
\end{align*}

This observation is the starting point of the \emph{double-negation embedding}
of classical logic into intuitionistic logic. This embedding translates any
statement~$\varphi$ into a related statement~$\varphi^{\neg\neg}$, substituting
all occurences of~``$\exists$'' and~``$\vee$'' by~``$\exists^\cl$''
and~``$\vee^\cl$'' (and prefixing all atomic statements by~``$\neg\neg$'')
as detailed in Table~\ref{table:negneg}. Crucially, while the principle of
excluded middle cannot be verified for~``$\vee$'', the principle of excluded
middle for~``$\vee^\cl$'' is an intuitionistic tautology:

\begin{thm}For every statement~$\varphi$,
$\neg\neg(\varphi \vee \neg\varphi)$.
\end{thm}

\begin{proof}By definition of negation, we are to prove
\[ \underbrace{\bigl((\varphi \vee (\varphi\Rightarrow\bot)) \Longrightarrow
\bot\bigr)}_{\equiv\vcentcolon\, \chi}
\Longrightarrow \bot. \]
So assume~$\chi$; we are to show~$\bot$.

Hypothetically, if~$\varphi$, then in particular~$\varphi \vee
(\varphi\Rightarrow\bot)$ and hence, by~$\chi$, $\bot$. This argument
establishes~$\varphi \Rightarrow \bot$.

Thus in particular we have~$\varphi \vee (\varphi \Rightarrow \bot)$ and hence,
by~$\chi$ again, $\bot$.
\end{proof}

The fundamental properties of the double-negation translation are summarized by
the following theorem.

\begin{thm}\label{thm:negneg}
For every statement~$\varphi$, \ldots
\begin{enumerate}
\item classical logic proves~$\varphi \Leftrightarrow \varphi^{\neg\neg}$,
\item intuitionistic logic proves~$\neg\neg(\varphi^{\neg\neg}) \Rightarrow
\varphi^{\neg\neg}$,
\item (if~$\varphi$ is a geometric formula) intuitionistic logic
proves~$\varphi^{\neg\neg} \Leftrightarrow \neg\neg\varphi$, and
\item classical logic proves~$\varphi$ from some set~$\Gamma$ of assumptions
if and only if intuitionistic logic proves~$\varphi^{\neg\neg}$ from the
set~$\Gamma^{\neg\neg}$ of translated assumptions.
\end{enumerate}
\end{thm}

\begin{proof}Instructive exercise.\end{proof}

The double-negation embedding is not only conceptually pleasing, establishing
that intuitionistic logic can serve as a common home for both classical and
constructive mathematics, but also supplies us with a vast source of
constructive results.

\begin{ex}Classical linear algebra teaches us that every finite system of
generators of a vector space over a residue field\footnote{\label{fn:fields}Constructively, the
notion of a field bifurcates into several nonequivalent notions: A nontrivial
commutative ring with unit is a \ldots
\begin{enumerate}
\item a \emph{geometric field} or \emph{discrete field} iff
every element is zero or
invertible (as in~$\QQ$ or~$\overline{\QQ}$),
\item a \emph{residue field} iff
every element which is not invertible is zero (as in the Cauchy or Dedekind
reals), and
\item a \emph{field of fractions} iff
every element which is not zero is invertible (as in the localization of the
Cauchy or Dedekind reals at the set of non-zeros or in the \emph{generic local
ring} described in Lecture~\ref{lect:generic}).
\end{enumerate}These each have their
uses~\cite{johnstone:rings-fields-and-spectra,mulvey:repr}.}
can be thinned to a generating family in which no vector is redundant, hence to
a basis. By slightly massaging the result obtained by the double-negation
embedding, we obtain the constructive theorem that every finitely generated
vector space over a residue field does \emph{not not} possess a basis.

We will learn in Section~\ref{sect:generic-freeness} that this simple theorem
immediately entails (a basic version of) \emph{Grothendieck's generic freeness
lemma}, a result in algebraic geometry fundamental to the theory of moduli
spaces, if applied after localizing at the ``generic prime filter'' (this
requires passing to a more adapted topos). It is marvelous how large the impact
of this simple theorem from undergraduate linear algebra is, if made to apply
in arbitrary toposes by the double-negation embedding and then specializing to
a particularly well-adapted one.\end{ex}


\section{Barr's theorem}
\newpage

Even though Barr's theorem has wide impact, there are definitive situations in
which, provably so, no useful constructive content can be extracted.
Exercise~\ref{ex:no-constructive-content} gives an example for this situation.


\section{Examples from quadratic form theory}
\newpage

\section{Exercises}

\begin{exercise}[Drinker's paradox]
The Drinker's paradox is the tautology
\[ \forall f \? \NN \to \{0,1\}\_ \exists n \? \NN\_ (f(n) = 1
\Rightarrow (\forall m \? \NN\_ f(m) = 1)) \]
of classical logic. A proof proceeds as follows: By the principle of
excluded middle, either there is a number~$n$ such that~$f(n) = 0$ or not. In
the first case, we can take such a number~$n$ as the desired~$n$. In the second
case, we can take~$n \defeq 0$.
\begin{enumerate}
\item Determine the double-negation translation of the Drinker's paradox.
\item Tell a classical logic fairy tale for Drinker's paradox similar to the
story for Dickson's lemma. The protagonist of the story will change their mind
regarding the correct value of~$n$; what is their first choice?
\item Connect the Drinker's paradox to the issue of minima of sets of natural
numbers.
\end{enumerate}
\end{exercise}

\begin{exercise}[Stability of the axioms]\label{ex:stability-axioms}
Peano arithmetic (\textsc{pa}) is set in the language~$(0,S,+,\cdot)$ and has
the following axioms (where leading universal quantifiers are supressed for
brevity):
\begin{enumerate}
\renewcommand{\theenumi}{\arabic{enumi}}
\item $Sx \neq 0$
\item $Sx = Sy \Rightarrow x = y$
\item $y = 0 \vee (\exists x\_ y = Sx)$
\item $x + 0 = x$
\item $x + Sy = S(x+y)$
\item $x \cdot 0 = 0$
\item $x \cdot Sy = (x \cdot y) + x$
\item $P(0) \wedge (\forall n\_ P(n) \Rightarrow P(Sn)) \Longrightarrow
(\forall n\_ P(n))$ (one axiom for each formula~$P(n)$)
\end{enumerate}
Heyting arithmetic~(\textsc{ha}) has exactly the same axioms, but is based on intuitionistic
logic instead of classical logic.
\begin{enumerate}
\item Show that~\textsc{ha} proves the double-negation translation of each
axiom of~\textsc{pa}.
\item Convince yourself that~\textsc{izf} does not prove the double-negation
translation of the axiom of choice. Hence the double-negation translation
alone is insufficient to extract constructive content from proofs using the
axiom of choice.
\end{enumerate}
\end{exercise}

\begin{exercise}[Details on the double-negation translation]
Complete the verification of the fundamental properties of the double-negation
translation stated as Theorem~\ref{thm:negneg}.
\end{exercise}

\begin{exercise}[Minima of sets of natural numbers, part two]
In Proposition~\ref{prop:minima}(b) we showed that every inhabited set of natural
numbers does \notnot contain a minimal element.
\begin{enumerate}
\item Redo Exercise~\ref{ex:minima1}(a) using the motto that in proofs of
negated statements, we are allowed to use finitely many instances of the
principle of excluded middle.
\item Explain how Proposition~\ref{prop:minima}(b) follows
from the double-negation embedding applied to the classical fact that every
inhabited set of natural numbers directly contains a minimal element.

{\noindent\scriptsize\emph{Hint.} It is not enough to just cite the
double-negation embedding. The resulting constructive theorem has to be
massaged a bit to yield Proposition~\ref{prop:minima}(b).\par}
\item Explain in computational terms how your proof of
Proposition~\ref{prop:minima}(b) runs its course.
\end{enumerate}
\end{exercise}

\begin{exercise}[Grothendieck's generic freeness lemma, part one]
XXX
\end{exercise}

\begin{exercise}[No constructive content]\label{ex:no-constructive-content}
Let~$\textsf{Prf}(p)$ be a formula of arithmetic expressing that~$p$ is a
correct encoding of a~\textsc{pa}-proof of~$\bot$. A consequence of Gödel's
second incompleteness theorem is that there is no~\textsc{pa}-proof of
\[ G \defequiv (\forall p\_ \neg\textsf{Prf}(p)), \]
even though for each number~$p_0$ it is actually the case that (and~\textsc{pa}
can verify that)~$p_0$ does not constitute a correct encoding of
a~\textsc{pa}-proof of~$\bot$.
\begin{enumerate}
\item Give a~\textsc{pa}-proof, using the principle of excluded middle, of the
statement
\[ \exists q\_ (\textsf{Prf}(q) \vee G). \]
\item Show that for no number~$q_0 \in \NN$, the
statement~``$\textsf{Prf}(\underline{q_0})
\vee G$'' admits a \textsc{pa}-proof. In this sense no witness can be
extracted from the classical proof in~(a).
\end{enumerate}
\end{exercise}


\chapter{Toposes and their internal language}
\label{lect:toposes}

\begin{intro}
Just as the easiest and shortest path between two truths of the real domain
often passes through the complex domain, sometimes the easiest and most
conceptual path to a result observes that the claim can also be formulated in
the internal language of an alternate mathematical universe -- an alternate
topos -- where the proof can be simple, direct and make use of the finer
distinctions provided by intuitionistic logic.

As such, toposes are the workhorse of many modern applications of constructive
mathematics to mathematics in general. Toposes originated in algebraic
geometry, where they have been used as generalized spaces (allowing for a
nontrivial category of opens instead of only a partially ordered set of opens),
before category theorists observed that there is also a strong logical aspect
to toposes: Toposes can be pictured as mathematical universes -- universes in
which we can do mathematics much in the same way as in the so-called standard
topos of sets and maps, the single topos in which most mathematicians spend all
their professional life in.

Besides the standard topos, in which mathematics unfolds exactly as known and
classical logic reigns, there is a colorful host of alternate toposes -- some
intimately related and useful to the mathematics of the standard topos, some
less so and important to computability theorists and logicians. In most
alternate toposes, only intuitionistic logic is sound and it is a plain fact of
the matter that the law of excluded middle and the axiom of choice fail.

In the lecture we will focus on precise definitions, examples of toposes, and
logical applications to mathematics in general, laying the groundwork for the
fourth lecture on generic models and carefully elucidating why it is that most
toposes validate only intuitionistic logic. References include
\cite{blechschmidt:filmat,leinster:introduction,streicher:ctcl,moerdijk-maclane:sheaves-logic,goldblatt:topoi,johnstone:elephant}
(and \cite{blechschmidt:phd} for applications in algebraic geometry). These
themes constitute just a tiny part of topos theory. Exposition on Olivia
Caramello's grand topos-theoretic bridge-building program~\cite{caramello:tst},
on applications of toposes to the meta-analysis of
logic~\cite{lambek-scott:hocl} and how topos theory can be used to reconcile
seemingly disparate positions in the philosophy of
mathematics~\cite{lambek:incompatible,couture-lambek:reflections} will take
place in more informal settings than the lecture.
\end{intro}

% \begin{document}

\newpage

\emph{Analysis:}
\begin{enumerate}
\item[\cmark/\xmark] Every continuous function~$f : [-1,1] \to \RR$ with~$f(-1) < 0$
  and~$f(1) > 0$ has a zero.
\item[\xmark/\xmark] Let~$X$ be a topological space and let~$f : X \times [-1,1] \to \RR$
be a continuous function with~$f(\cdot,-1) < 0$ and~$f(\cdot,1) > 0$. Then
there is an open covering~$X = \bigcup_i U_i$ such that for each index~$i$,
there is a continuous zero-picking function~$z : U_i \to [-1,1]$.
\end{enumerate}

\emph{Linear algebra:}
\begin{enumerate}
\item[\cmark/\xmark] Every real symmetric matrix has an eigenvector.
\item[\xmark/\xmark] Let~$X$ be a topological space and let~$A : X \to
M^\text{sym}_n(\RR)$ be a continuous map to the space of symmetric~$(n \times
n)$-matrices. Then there is an open covering~$X = \bigcup_{i \in I} U_i$ such
that or all indices~$i \in I$, there is a continuous map~$v : U_i \to \RR^n$
such that for each~$x \in U_i$, the vector~$v(x)$ is an eigenvector of~$A(x)$.
\end{enumerate}

\emph{Commutative algebra:}
\begin{enumerate}
\item[\cmark/\cmark] Let~$M$ be a finitely generated projective module over a local
ring~$A$. Then~$M$ is finite free.
\item[\cmark/\cmark] Let~$M$ be a finitely generated projective module over an
arbitrary commutative ring~$A$. Then there is a partition~$1 = f_1 + \cdots +
f_n \in A$ of unity such that, for each index~$i$, the localized
module~$M[f_i^{-1}]$ is finite free over~$A[f_i^{-1}]$.
\item[\cmark/\xmark] Let~$M$ be a finitely generated module over a (residue)
field~$k$. Then~$M$ is finite free.
\item[\xmark/\xmark] Let~$M$ be a finitely generated module over an
arbitrary commutative ring~$A$. Then there is a partition~$1 = f_1 + \cdots +
f_n \in A$ of unity such that, for each index~$i$, the localized
module~$M[f_i^{-1}]$ is finite free over~$A[f_i^{-1}]$.
\item[\cmark/\cmark] Let~$M$ be a finitely generated module over a (residue)
field~$k$. Then~$M$ is \notnot finite free.
\item[\cmark/\cmark] Let~$M$ be a finitely generated module over an
arbitrary commutative ring~$A$. If~$f = 0$ is the only element of~$A$ such
that~$M[f^{-1}]$ is finite free over~$A[f^{-1}]$, then~$1 = 0$ in~$A$.
\item[\cmark/\cmark] If~$k$ is a (residue) field, there is no linear
surjection~$k^n \to k^m$ with~$m > n$.
\item[\cmark/\cmark] Let~$A$ be an arbitrary commutative ring. If there exists
a linear surjection~$A^n \to A^m$ with~$m > n$, then~$1 = 0$ in~$A$.
\end{enumerate}

\section{Examples}
\newpage
\ \newpage

\section{Definition}
\newpage
\ \newpage

\section{The Kripke--Joyal semantics of sheaf toposes}
\newpage
\ \newpage

\section{Exercises}

\begin{exercise}[{The sheaf of real functions as a
field~\cite[Exercise~28]{blechschmidt:generalized-spaces}}]
Let~$X$ be a topological space. Let~$\CCC$ be the sheaf of continuous real-valued
functions on~$X$.
\begin{enumerate}
\item Let~$U$ be an open of~$X$. Let~$f \in \CCC(U)$. Show that~$U \models (\exists g\?\CCC\_ fg =_\CCC
1)$ iff there is a function~$g \in \CCC(U)$ such that~$fg = 1$.
\item Show that~$\CCC$ is a \emph{residue field} in that
$X \models \forall f\?\CCC\_
  \bigl(\neg(\exists g\?\CCC\_ fg = 1)\bigr) \Rightarrow f = 0$.
\item Give an example of space~$X$ such that it is not the case that~$\CCC$ is a
field in the stronger sense that
$\Sh(X) \models \forall f\?\CCC\_ (\exists g\?\CCC\_ fg = 1) \vee f = 0$.
\item Let~$X = \CC$ and let~$\OOO$ be the sheaf of holomorphic functions on~$X$,
that is~$\OOO(U) = \{ f : U \to \CC \,|\, \text{$f$ holomorphic} \}$.
Show that, in classical mathematics, the sheaf~$\OOO$ is \emph{discrete} in that
\[ \Sh(\CC) \models \forall f\?\OOO\_ \forall g\?\OOO\_ f = g \vee \neg(f = g).
\]
\end{enumerate}

\end{exercise}
\begin{exercise}[{The geometric interpretation of double
negation~\cite[Exercise~26]{blechschmidt:generalized-spaces}}]
Let~$\varphi$ be a formula over an open~$U$ of a topological space~$X$.
\begin{enumerate}
\item Show that there is a largest open,
denoted~``$\llbracket\varphi\rrbracket$'', such
that~$\llbracket\varphi\rrbracket \models \varphi$.\smallskip

{\noindent\scriptsize\emph{Hint.} Consider the union of all opens~$V$ such that~$V
\models \varphi$.\par}

\item Show that~$X \models \neg\neg\varphi$ iff~$\llbracket\varphi\rrbracket$
is dense.

{\noindent\scriptsize\emph{Note.} A subset~$W \subseteq X$ is \emph{dense} iff
for every open~$T \subseteq X$, if~$W \cap T = \emptyset$ then~$T =
\emptyset$.\par}

\item Give a condition on the topological space~$X$ such that the principle of
excluded middle (or equivalently the principle of double negation elimination)
is valid in~$\Sh(X)$.
\end{enumerate}
\end{exercise}

\begin{exercise}[The fundamental properties of the sheaf semantics]
Complete the proof of Proposition~\ref{prop:sheaf-semantics}, so verify
monotonicity and locality of the sheaf semantics.
\end{exercise}

\begin{exercise}[{Unique local existence is global existence~\cite[Exercise~27]{blechschmidt:generalized-spaces}}]
Let~$F$ be a sheaf on a topological space~$X$. Let~$\varphi$ be a formula over~$X$. Assume
that~$\Sh(X) \models \exists!s\?F\_ \varphi(s)$, that is
\[ \Sh(X) \models \exists s\?F\_ \varphi(s) \quad\text{and}\quad
  \Sh(X) \models \forall s\?F\_ \forall t\?F\_ (\varphi(s) \wedge \varphi(t)
  \Rightarrow s = t). \]
Show that for any open~$U \subseteq X$, there is a unique section~$s \in F(U)$
such that~$U \models \varphi(s)$.

{\noindent\scriptsize\emph{Note.} If you do not know the general definition of
a sheaf, then consider only the specific sheaf~$\CCC$ of continuous real-valued
functions.\par}
\end{exercise}


\chapter{Generic models and their applications}
\label{lect:generic}

\begin{intro}
Commutative algebra progressed when the intuitive but informal notion of
``the generic element of a given field~$k$'' was reified in the form of the
specific element~$X$ of the polyomial ring~$k[X]$. The caveat is, of course,
that the expanded ring~$k[X]$ is no longer a field.

A similar story unfolds one level up. \emph{Topos theory provides us with ``the
generic ring'', the ring we are implicitly picturing when someone utters
the phrase ``Let~$R$ be a ring''.} The generic ring has exactly those
properties (of the large class of ``geometric implications'') which all rings
have. To have the generic ring in our ontology,
we need to broaden our notion of existence---the generic ring is not a
ring in the usual sense of the word, but a ring object in an enlarged
topos, and still close enough to the familiar rings in that all
constructive theorems about rings apply to it.

Bizarrely, the generic ring has the property (not formalizable as a
geometric implication) that it is even a field. Hence, if we are to
prove a geometric implication for all rings, we can just as well assume
the field property.

The lecture introduces the notion of topos-theoretic generic models in
general, focussing on the generic ring, the generic prime ideal and
concrete applications.
\end{intro}

The convergence radius of the Taylor series expansion of~$1/(1-x)$ around the
origin, that is the geometric series
$1 + x + x^2 + \cdots$,
is~$1$. That the convergence radius isn't larger doesn't come too surprising in
view of the fact that the function~$1/(1-x)$ has a non-removable discontinuity
at~$x = 1$. But why is also the convergence radius of the expansion
of~$1/(1+x^2)$,
\[ 1/(1+x^2) = 1 - x^2 + x^4 - x^6 + \cdots, \]
just~$1$? The function~$1/(1+x^2)$ is
perfectly well-defined at~$\pm 1$, infinitely derivable on all of~$\RR$, neatly
decaying for~$x \to \pm\infty$ and doesn't have any singularities.

A rewarding explanation of this phenomenon is nowadays relayed in any course on
complex analysis: The function~$1/(1+x^2)$ does have a singularity at
distance~$1$ from the origin, namely at~$\pm i$ in the complex plane, and the disk
of convergence is and can only be so big that it just touches the nearest singularity.

This episode is one example of many how the ``imaginary unit''---once
an elusive \emph{mathematical phantom}---affects the story of the real numbers even
though it itself is not one of them. Like many mathematical phantoms before it,
the imaginary unit obtruded its effects so convincingly that eventually we
embraced it and broadened our notion of existence~\cite{wraith:phantoms}.

Toposes allow us to bring further entities into being, entities which do not
exist in the standard topos but which nevertheless affect the story of the
standard topos. We will focus on:
\begin{enumerate}
\item The \emph{generic ring} -- which cryptically is also a field
\item The \emph{generic prime filter} of a given ring~$A$ -- which
XXX
\item The \emph{generic surjection}~$\NN \to X$ -- which exists also when~$X$
is uncountable
\end{enumerate}
The complex numbers can be compiled down to pairs of real numbers and hence
exhibit already in their very construction an intimate connection with the real
numbers; in a similar vein, these topos-theoretic generic models can be
compiled away in that proofs employing them can be unrolled, in a mechanical
fashion even, so as to not mention them.


\section{Ring-theoretic prelude: the method of indeterminates}
\label{sect:indeterminates}

The Cayley--Hamilton theorem of linear algebra states that every square matrix
over every commutative ring is a root of its characteristic polynomial. Among
its many proofs, the following one is particularly interesting from a logical
point of view: It is enough to verify the claim for the \emph{ring-theoretic
generic~$(n \times n)$-matrix}~$(A_{ij})_{ij}$ over the polynomial
ring~$\ZZ[A_{ij}\,|\,i,j\in\{1,\ldots,n\}]$, since this matrix can specialize
to every specific matrix over every commutative ring and this kind of specialization
preserves the~$n^2$ polynomial identities expressing that the matrix is a root
of its characteristic polynomial. Now to check this special case, it suffices to
verify it for every choice of complex numbers~$a_{ij} \in \CC$ in place of the
formal indeterminates~$A_{ij}$. For complex matrices, the claim follows from
the observation that the claim is immediate for the diagonalizable complex
matrices and that these are dense in the space of all complex matrices.

This approach is known as the \emph{method of indeterminates} and is amenable
to many situations. For instance, there is the
\emph{ring-theoretic generic~$n$-th root} (over~$\ZZ[X]/(X^n-1)$), the
\emph{ring-theoretic generic nilpotent element of index~$\leq n$}
(over~$\ZZ[X]/(X^n)$), the \emph{ring-theoretic generic power series}
(over~$\ZZ[A_0,A_1,\ldots]$), and many others. The central features of the
method of indeterminates are:
\begin{enumerate}
\renewcommand{\theenumi}{\arabic{enumi}}
\item We extend a certain base ring, often~$\ZZ$, to a larger ring~$R_0$ containing
the \emph{generic instance} of the problem at hand.
\item For every specific instance in every ring~$R$, there is a unique
homomorphism~$R_0 \to R$ mapping the generic instance to that one.
\item Since homomorphisms of rings preserve polynomial identities, every
polynomial identity (and in fact even every property which can be expressed as a
geometric formula in the language of rings) satisfied by the generic instance
passes down to every specific instance. In fact, the generic instance satisfies
exactly those polynomial identities which are provable from the ring axioms.
\item Crucially, the generic instance is applicable to special techniques (for
instance involving complex numbers) and has special properties which themselves
do not pass down to every specific instance, but which are useful in
establishing those that do.
\end{enumerate}

The generic models facilitated by topos theory generalize the ring-theoretic
generic elements. The latter are restricted to those kinds of elements which
can be described by polynomial identities (such as~$X^n - 1$ for~$n$-th roots).
For example, there is no ring-theoretic generic non-nilpotent element
or ring-theoretic generic regular element (a ring element~$x \in A$ is
\emph{regular} if and only if for all~$y \in A$, $xy = 0$ implies~$y = 0$).
The topos-theoretic generic models, in contrast, support arbitrary geometric
implications as defining properties, and are not restricted to mere elements
(or finite or infinite lists of elements): For instance, as elucidated in the
next sections, there is the topos-theoretic \emph{generic ring} or the
topos-theoretic \emph{generic prime filter} of any given ring.

Briefly, for every geometric theory~$\TT$ (set of geometric implications as
axioms) over any signature, there exists a topos-theoretic generic model
of~$\TT$. The analogy with the generic elements of ring theory is as follows:
\begin{enumerate}
\renewcommand{\theenumi}{\arabic{enumi}}
\item We extend the base universe, often the standard topos~$\Set$, to a larger
topos~$\Set[\TT]$ containing the \emph{generic model}~$U_\TT$ of~$\TT$.
\item For every specific~$\TT$-model~$M$ in any topos~$\EEE$, there is a unique
map~$\Set[\TT] \to \EEE$ mapping~$U_\TT$ to~$M$.\footnote{To be more precise,
the category of maps~$\mathrm{Hom}(\Set[\TT],\EEE)$ is equivalent to the
category of~$\TT$-models in~$\EEE$, naturally in~$\EEE$. By ``map'', we mean
what is called the ``inverse image part of geometric morphisms'' in topos
theory.}
\item Since such maps preserve geometric implications, every property
which can be expressed as a geometric implication passes from~$U_\TT$ to every
specific model. In fact, the generic model satisfies exactly those geometric
implications which are provable from the axioms of~$\TT$.
\item Crucially, the generic model is applicable to special techniques and has
special properties which themselves do not pass down to every specific model,
but which are useful in establishing those that do.
\end{enumerate}


\section{A fantastical ring}
\newpage
\ \newpage


\section{The generic prime filter}

A commutative ring~$A$ is often studied by its \emph{stalks}~$A_\ppp$ at prime
filters~$\ppp \subseteq A$, those subsets of~$A$ which validate the conditions
on the right:
\begin{align*}
  \top &\,\,\Longrightarrow\, 0 \in \ppp &
  0 \in \ppp &\,\,\Longrightarrow\, \bot \\
  x \in \ppp \wedge y \in \ppp &\,\,\Longrightarrow\, x + y \in \ppp &
  x + y \in \ppp &\,\,\Longrightarrow\, x \in \ppp \vee y \in \ppp \\
  1 \in \ppp &\,\,\Longrightarrow\, \bot &
  \top &\,\,\Longrightarrow\, 1 \in\ppp \\
  x \in \ppp \vee y \in \ppp &\,\Longleftrightarrow\, xy \in \ppp &
  xy \in \ppp &\,\Longleftrightarrow\, x \in \ppp \wedge y \in \ppp
\end{align*}
The stalk~$A_\ppp$ is then the localization~$A[\ppp^{-1}]$, that is
the ring of formal fractions~$x/s$ with~$x \in A$ and~$s \in \ppp$, where~$x/s
= y/t$ iff there exists an element~$u \in \ppp$ such that~$utx = usy$.
The set~$\ppp$ is multiplicatively closed (and saturated) by the last two
conditions.\footnote{Textbooks on classical commutative algebra usually use
\emph{prime ideals} instead of \emph{prime filters}, those subsets which
validate the dual conditions on the left. In classical commutative algebra, we
can freely pass between these two notions by taking complements, as the
complement of a prime ideal is a prime filter and conversely. Constructivly,
prime filters are more useful, and even classically they are slightly more
convenient to work with.} Similarly, an~$A$-module~$M$ is often studied by its
stalks~$M_\ppp = M[\ppp^{-1}]$.

Stalks are interesting because they allow us to zoom in on ``local''
situations---they tend to be simpler than the original ring or module, while
still being intimately connected to the originals. For instance:
\begin{enumerate}
\item The stalks~$A_\ppp$ are always \emph{local
rings},\label{page:local-rings} rings such that a finite sum is invertible only
if one of its summands also is. (This amounts to~$1 \neq 0$ and that
whenever~$x+y$ is invertible, $x$ is invertible or~$y$ is invertible; see
Exercise~\ref{ex:local-rings}.)
\item Classically, if~$A$ is reduced, the stalks~$A_\ppp$ at
\emph{maximal} prime filters (equivalently minimal prime ideals) are even fields.
\item Classically, an~$A$-module~$M$ is flat if and only if all of its stalks~$M_\ppp$ are.
\end{enumerate}

\section{Explicit construction}
\newpage
\ \newpage

\section{Exercises}

\begin{exercise}[Verifying polynomial identities]

\end{exercise}

\begin{exercise}[Limitations of ring-theoretic generics]
Show that each of the following hypothetical ring-theoretic generics do not
exist:
\begin{enumerate}
\item the generic nilpotent element (of arbitrary index)
\item the generic regular element
\item the generic prime element
\end{enumerate}
That is, show that there is no ring~$R_0$ containing an element~$x_0$ of the
desired kind such that for every such element~$x$ of every ring~$R$, there is a
unique homomorphism~$R_0 \to R$ mapping~$x_0$ to~$x$.
\end{exercise}

\begin{exercise}[Local rings]\label{ex:local-rings}
\begin{enumerate}
\item Using the definition of local ring given on
page~\pageref{page:local-rings}, verify that every geometric field in the sense
of Footnote~\ref{fn:fields} is a local ring; that the (Cauchy or Dedekind)
reals form a local ring; that for each prime number~$p$ the subring of~$\QQ$
consisting of those fractions whose denominator is not divisible by~$p$ is a
local ring; and that~$\ZZ$ and~$\QQ[X]$ are not local rings.

{\noindent\scriptsize\emph{Note.} If~$a < b$ are real numbers, then for every
real number~$x$, $x > a$ or~$x < b$.\par}

\item Show that the stalk~$A_\ppp$ of a commutative ring~$A$ at a prime
filter~$\ppp$ is a local ring. What goes wrong in case that~$\ppp$ is instead a
prime ideal and one considers the localization~$A[(A\setminus\ppp)^{-1}]$?

\item Verify in classical mathematics that a ring is local if and only if it
has exactly one maximal ideal.

{\noindent\scriptsize\emph{Hint.} Use that, in classical mathematics, every
nonunit is contained in some maximal ideal.\par}
\end{enumerate}
\end{exercise}

\begin{exercise}[Abstract existence of bounds from the method of
indeterminates]
\begin{enumerate}
\item Using Krull's lemma in its unconstructive form, verify for every
commutative ring~$A$ that if a polynomial~$f \in A[X]$ is nilpotent in~$A[X]$,
all its coefficients are nilpotent in~$A$.
\item Let~$f \in A[X]$ be a polynomial of degree~$d$ such that~$f^n = 0$.
By the proof in~(a), there exists a number~$m$ such that the~$m$-th power of
each of the coefficients of~$f$ vanishes. However, it is conceivable that~$m$
depends not only on~$d$ and~$n$, but also on the ring~$A$ and the specific
values of the coefficients. Explain how the method of indeterminates reviewed
in Section~\ref{sect:indeterminates} can be used to establish that there exists
some bound on~$m$ depending only on~$d$ and~$n$.
\end{enumerate}
\end{exercise}

\begin{exercise}[Anonymously Noetherian rings]
A commutative ring~$A$ is \emph{anonymously Noetherian} iff for every
ideal~$\aaa \subseteq A$ it is \notnot the case that~$\aaa$ is finitely
generated.
\begin{enumerate}
\item Show that residue fields in the sense of Footnote~\ref{fn:fields} are
anonymously Noetherian.
\item Verify that~$\ZZ$ is anonymously Noetherian.

{\noindent\scriptsize\emph{Note.} Either run a direct proof or use the
anonymous least number principle of Proposition~\ref{prop:minima}(a).\par}
\item Look up a proof of Hilbert's basis theorem, for instance the
proof in~\cite[Theorem~7.5]{atiyah-macdonald:commutative-algebra}, and check
that it can be massaged into a constructive proof of the statement that
polynomial rings over anonymously Noetherian rings are anonymously Noetherian.
\end{enumerate}
\end{exercise}

\begin{exercise}[{Prüfer domains as valuation domains~\cite[Exercise~43]{blechschmidt:generalized-spaces}}]
An \emph{integral domain} is a commutative ring such that~$1 \neq 0$ and such that~$xy = 0$
implies~$x = 0$ or~$y = 0$. A \emph{valuation domain} is an integral domain
such that for any two elements, one divides the other. A \emph{Prüfer domain}
is an integral domain such that every finitely generated ideal~$\aaa$ is locally a
principal ideal (in the sense that there exists a partition~$1 = f_1 + \cdots +
f_n$ such that, for each index~$i$, the ideal~$\aaa[f_i^{-1}]$ is a principal
ideal in~$A[f_i^{-1}]$).
\begin{enumerate}
\item Let~$A$ be a ring. Show that~$A^\sim$ is an integral domain if~$A$ is.
Does the converse hold?
\item Let~$A$ be a valuation domain. Show that any matrix over~$A$ can be put
into diagonal form by elementary row and column operations.
\item Let~$A$ be an integral domain. Show that~$A$ is a Prüfer domain if and
only if~$A^\sim$ is a valuation domain.
\item Let~$A$ be a Prüfer domain. Show that any matrix over~$A$ can locally be
put into diagonal form by elementary row and column operations, by applying the
result of part~(b) to~$A^\sim$.
\end{enumerate}
\end{exercise}

\begin{exercise}[{A basic version of Kaplansky's theorem~\cite[Exercise~44]{blechschmidt:generalized-spaces}}]
\begin{enumerate}
\item Let~$A$ be a local ring. Let~$\aaa \subseteq A$ be a finitely generated
ideal such that~$\aaa^2 = \aaa$. Show that~$\aaa = (0)$ or~$\aaa = (1)$.\smallskip

{\noindent\scriptsize\emph{Hint.} Nakayama's lemma.\par}
\item Let~$A$ be a local ring. Let~$M \in A^{n \times n}$ be an idempotent
matrix. Verify that~$M$ is similar to a diagonal matrix with entries~$0$ and~$1$
by applying part~(a) to the ideals of~$k$-minors of~$M$. Deduce that the
cokernel of~$M$ is finite free.
\item Let~$A$ be an arbitrary ring. Let~$M \in A^{n \times n}$ be an idempotent
matrix. Show that the cokernel of~$M$ is finite locally free, by applying the
result of part~(b) to~$A^\sim$.
\item Verify, without using the law of excluded middle or that~$A$ is
Noetherian, that an~$A$-module~$M$ is finitely generated and projective if and
only if it is finite locally free.\smallskip

{\noindent\scriptsize\emph{Note.} A self-contained solution is given in
Ref.~\cite{blechschmidt:kaplansky}.\par}
\end{enumerate}
\end{exercise}

\printbibliography

\end{document}

1
Add Agda exercises

2
classical logic fairy tale
Add Agda exercises
Mention Dialectica
something with minima (for negneg translation)
Exercises: applications of Barr

3
Definition
Examples
Language: definition, properties, IVT, FTA
Exercises: dense, monotone IVT, ...

4
"A fantastical ring"
The generic prime filter
Explicit construction
Exercises: (lift from Spiel & Spaß)

\[
  \forall x_1,\ldots,x_n\?V\_
    \bigl(\forall x\?V\_ \exists a_1,\ldots,a_n\?K\_ x = \sum_i a_i x_i\bigr)
      \Longrightarrow
        \]

Comment on Zorn's lemma

completion of ℕ

Exercise: ∀∃ ⇒ Eventually

History of "AC ⇒ LEM":
1967 Bishop
1975 Douglas Bridges
1975 Diaconescu
1975 Anna Michaelides Penk
1978 Goodman and Myhill
2021 Andrew Swan, https://ncatlab.org/nlab/show/well-ordering+theorem

Cite: https://www2.mathematik.tu-darmstadt.de/~streicher/CLM/clm.pdf

Cite: https://www.mscsnet.mu.edu/~wim/publica/8802hist_print.pdf

https://www.math.ucla.edu/~joan/publicgothenburghandout.pdf
Peculiar characteristics of intuitionistic logic:
◮ (A → B) → ¬(A & ¬B) is provable, but the converse is not.
◮ ∃x¬A(x) → ¬∀xA(x) is provable, but the converse is not.
◮ ¬¬(A ∨ ¬A) is provable, but ¬¬∀x(A(x) ∨ ¬A(x)) is not.

Cite:
https://www.math.ucla.edu/~joan/newnotes.pdf

Cite:
https://arxiv.org/pdf/2102.01561.pdf

Cite:
https://arxiv.org/pdf/2103.08379.pdf