Proof and Computation

CHAPTER: GENERALIZED SPACES FOR CONSTRUCTIVE ALGEBRA

I. Blechschmidt]Ingo Blechschmidt

Università di Verona

Department of Computer Science

Strada le Grazie 15

37134 Verona, Italy

The purpose of this contribution is to give a coherent account of a particular
narrative which links locales, geometric theories, sheaf semantics and
constructive commutative algebra. We are hoping to convey a firm grasp of three
(1) Locales are a kind of space in which opens instead of points are
(2) Sheaf semantics allows us to explore mathematical objects from custom-tailored
mathematical universes.
(3) Without loss of generality, any reduced ring is a field.

§.§ Introduction[
Unlike some other texts on locales or sheaves, this text is set in a
constructive (but impredicative) metatheory. We do not use the law of excluded
middle nor any version of the axiom of choice, and we also do not adopt any
nonclassical principles. We freely use powersets, but more for linguistic
convenience than by necessity.
In particular, the central idea presented in
Section <ref>, the reduction technique by which we can pretend that any
given reduced ring is a field, is very robust with respect to the metatheory.
Even though we chose a semantic point of view for its derivation, the final
result is a purely syntactical transformation. As it stands, this text could be
formalized in the kind of type theory which is valid in
toposes [1] or
in izf [2].]

The notion of space is fundamental to large parts of mathematics. This notion
exists in various flavors, ranging from the basic cartesian spaces $\RR^n$ to
the more general metric and topological spaces and also including several more
and slightly exotic flavors such as the diffeological spaces from differential topology.

Common to all of the mentioned flavors of space is that points are their
building blocks: cartesian, metric, topological and diffeological spaces are,
first and foremost, sets of points. Their spatial structure – a metric, a
topology or a diffeology – is additional data to the underlying set:

Definition. A metric space consists of a set $X$ of points
together with a map $d : X \times X \to \RR_{\geq 0}$ satisfying the metric

Definition. A topological space consists of a set $X$ of points
together with a set $\OOO(X) \subseteq P(X)$ of point sets which are deemed
open such that (arbitrary, set-indexed) unions and finite intersections
of open sets are open.

Locales are a further and particularly unique flavor of the notion of space
which turn this classical picture upside down: Locales embrace opens
instead of points as primitive building blocks. With locales, points are a
derived concept. In particular, the opens of a locale are not sets of points;
in fact, they need not be sets of anything in peculiar.

Section <ref> explores the basics of the theory of locales, with a
focus on examples and issues for constructive mathematics. Accessible
introductions to the theory include
Refs. johnstone:art,johnstone:point. The interplay between logic and
geometry is particularly stressed in
Refs. vickers:continuity,vickers:locales-toposes. We recommend
Ref. belanger-marquis:pointless for a historical guide and
Ref. picado-pultr:frames-and-locales for a comprehensive modern
textbook on the subject.

Geometric theories and sheaf models. The most sensible solution to
the task

Determine the continuous complex-valued functions $f$ with $f(z)^2 = z$.

is not the single set

\[ \{ f : \CC \to \CC \,|\, \text{$f$ is continuous and $f(z)^2 = z$ for all~$z \in \CC$} \}. \]

Rather, since the solvability of this functional equation varies with the
domain on which $f$ should be defined (having no global solution defined on all
of $\CC$ but two solutions on small disks not containing the origin), we should
consider the family

\[ (\{ f : U \to \CC \,|\, \text{$f$ is continuous and $f(z)^2 = z$ for all~$z
\in \CC$} \})_{U \in \OOO(\CC)} \]

of sets as the solution (or perhaps, since no solution was actually given, as
an apt description) of the task.

If we are building a prime ideal $\ppp$ step by step, adding elements to it
when the need arises, the most sensible answer to the question

Is $x$ contained in the prime ideal $\ppp$?

is not a single truth value, but a family of truth values, parametrized by the
possible stages of construction of $\ppp$.

Somewhat surprisingly, these two examples can be treated by a single theory,
the theory of sheaves. Sheaves help to organize such families in an
efficient manner and reify them as single coherent entities; the first family
is (part of) a sheaf of sets and the second family is (part of) a
sheaf of truth values. Sheaves will be the subject of
Sections <ref>–<ref>.

Sheaves interact particularly well with geometric theories, which we
review in Section <ref>. Firstly, sheaves allow us to
generalize our notion of a model of a geometric theory. For instance, a
set-based model of the geometric theory of rings is just an ordinary ring; but
now we can also consider sheaves of rings as further models.

Some geometric theories only really unfold in the world of sheaves. For
instance, the geometric theory of surjections $\NN \twoheadrightarrow \RR$
reviewed on page item:theory-of-surjections does not have any
set-based models, but this theory is consistent and it does have nontrivial sheaf
models. For the purposes of constructive algebra, sheaf models of some geometric
theories play a vital role, as we will discuss in Section <ref>.

Secondly, geometric theories allow us to efficiently construct the spaces
(locales) on which we want to study sheaves. This is because a fundamental
feature of geometric theories (in contrast to, say, arbitrary first-order
theories) is that their models naturally organize to form a space, the
space (locale) of models reviewed in Section <ref>.

Applications in constructive algebra.

Commutative algebra abounds with techniques to reduce given situations to
simpler ones, for instance passing to a quotient or passing to a
localization. These techniques facilitate short and elegant proofs, such as the
following. (Section <ref> contains some algebraic

Theorem. Let $M$ be an injective matrix with more columns than rows
over a reduced ring $A$. Then $1 = 0$ in $A$.

Proof. Assume not. Then there is a minimal
prime ideal $\ppp \subseteq A$. Since localization is exact, the matrix $M$ is also injective when
considered as a matrix over the stalk $A_\ppp$. Since $A_\ppp$ is a
field, this is a contradiction to basic linear algebra.

However, these reduction techniques typically require transfinite
methods. The displayed proof appeals to the transfinite four times:

* The proof proceeds by contradiction, hence requires the law of excluded

* The proof then requires a minimal prime ideal. Such an ideal can be
obtained in two steps: First, the Boolean Prime Ideal
Theorem is invoked to obtain some prime ideal. Then
Zorn's lemma fabricates a minimal one.[Standard textbooks prove the statement “any nontrivial
ring has a prime ideal” by using Zorn's lemma, which
in the presence of the law of excluded middle is equivalent to the full axiom
of choice; however, the statement is actually equivalent to the weaker Boolean
Prime Ideal Theorem [9, 10].
The combined statement “any nontrivial ring has a minimal prime ideal” is equivalent to
the full axiom of choice [11].]

* Finally, the proof exploits that the stalks of reduced rings at minimal
prime ideals are fields. This requires two further invocations
of .[By , the intersection of all prime ideals of $A_\ppp$
is its nilradical. Since $A_\ppp$ is reduced, the nilradical is the zero ideal.
Since the prime ideals of $A_\ppp$ are in bijection with those prime ideals
of $A$ which are contained in $\ppp$, the ring $A_\ppp$ has exactly one prime
ideal. By , any noninvertible element of $A_\ppp$ is contained in some
prime ideal, hence in the zero ideal. Thus $A_\ppp$ is a field.]

This state of affairs is not satisfactory. A statement as simple as the
displayed example should admit an explicit calculational proof, presenting a
concrete method for transforming the given conditional equations expressing
injectivity into the equation $1 = 0$ without any appeals to the transfinite.

The completeness theorem for coherent logic <cit.> even
gives an a priori reason why (for a given matrix size) a finitary proof has to
exist. However, since the proof of the completeness theorem itself uses (and indeed is equivalent to it), it does not give any indication how such a
proof could be found. (Still, beautiful constructive proofs are known and
presented, for instance, in a celebrated short note by Fred Richman on nontrivial
uses of trivial rings [13] and in the recent
textbook [14] by Henri Lombardi and
Claude Quitté on constructive commutative algebra.)

The key issue with the usual reduction techniques in commutative algebra is
their dependence on ideal objects such as prime or maximal ideals. In
general, those objects can only be obtained by transfinite methods. However, in
practice many arguments do not actually require completed ideal objects:
Their computational core applies just as well to finite approximations of
these ideal objects.

It is then a challenging task in mathematical logic to devise efficient means to
extract this obscured constructive content in a mostly mechanical manner. We
envision to reinterpret any given classical proof employing ideal objects in a
constructive fashion, realizing ideal objects as convenient fictions.

Locales and sheaf models contribute to this program by providing new reduction
techniques for commutative algebra. These techniques have a similar effect as the
classical reduction techniques, but are powered by purely constructive
underpinnings. In a nutshell, the idea is as follows.

* Instead of replacing a given ring with another (for instance a ring $A$ with
one of its stalks $A_\ppp$ at a minimal prime ideal), we replace a given ring
with a sheaf of rings.

* We then maintain the convenient illusion that we are working with a plain old ring
instead of a sheaf by employing the sheaf semantics.

In some cases, these new techniques go even beyond their classical role models.
For instance, while a module need not be free “on a dense open” if all its
stalks at minimal prime ideals are, a module $M$ is free in that sense if its
mirror image $M^\sim$ is free. This observation is the basis for a
new proof of Grothendieck's generic freeness lemma, reviewed in
Section <ref>, which is shorter and arguably more
perspicuous than the previously known classical proofs.

Where to go from here. The themes which this contribution touches
on are embedded into a larger context, and we invite readers to follow those
interesting tangents.

Regarding spaces, the notion of locales can be modified in several ways.
Firstly, there are sites and closely related
toposes. [15, 16].
Given two opens $U$ and $V$ of a locale, there is only a truth value as to
whether $U$ is contained in $V$; with sites and toposes, there can be a
nontrivial set of ways that $U$ is contained in $V$. In an orthogonal
direction, there is the notion of a formal
topology [17, 18]. These implement the idea of
pointfree topology in predicative settings. In this context also basics of
algebraic geometry have been
developed [19, 20, 21].

Regarding sheaf semantics, Section <ref> only presents
the first-order case, but the theory can be extended to include unbounded
quantification [22], function types and power types
and even a fully-fledged type theory [1]. The
sheaf semantics of appropriate toposes has been used to give synthethic
accounts of several fields, such as differential geometry [23],
domain theory [24] and computability
theory [25].

Regarding constructive algebra, there are by now several
textbooks [26, 14, 27]
on constructive algebra available and there is a vast literature on
the intriguing subject of constructivizing classical commutative algebra.
Starting points include
Refs. coste-lombardi-roy:dynamical-method,coquand-lombardi:logical-approach,rinaldi-schuster-wessel:edde,cederquist-coquand:entrel.

Notes for readers familiar with the themes of this contribution.
We present a self-contained proof of the simple
version of Barr's theorem as Theorem <ref>. For reducing
intuitionistic provability to geometric provability, we employ (what amounts
to) the syntactic site, similar to the refined completeness result
by Thierry Coquand [32] but closer to the standard description
of the syntactic site. For reducing classical provability to intuitionistic
provability, we employ a variant of the double negation translation. We were
not able to track down a reference to this approach in the context of
infinitary logic, but the basic idea has long been known and is summarized, for
instance, in Ref. aczel:russell-prawitz.

In Section <ref>, where we introduce sheaves, we should
probably also introduce sites. They would fit the narrative well and allow for
the construction of generic models of arbitrary geometric theories and not only
propositional ones. They would also allow us to cut down on the required metatheory,
sitting comfortably within predicative environments such as arithmetic
universes [34, 35] or czf.
We do not, however, mainly to not require
prerequisites in category theory.

The technique presented in Section <ref> can be
regarded as a first-order (and, if desired, higher-order) coating of an
underlying geometric theory. We propose to take this coating seriously; in
particular to make good use of surprising nongeometric sequents validated by the
generic model; and, for ease of use by algebraists, to cast it in semantic terms,
even though it is all syntax behind the scenes.[By now it is an established idea in constructive algebra that we should
consider the theory of prime filters instead of the prime filters themselves,
hoping that, for instance, a given mathematical proof of the statement “no
prime filter contains $x$” can also be cast in the
geometric language of the theory, which then yields the nilpotency of $x$
constructively. If the given proof uses only geometric reasoning, this is
immediate; if it uses intuitionistic reasoning, it can be compiled down (for
instance precisely by the technique we use); and if it uses classical reasoning, a
version of Barr's theorem might be applicable. The elusive actual prime filters
of the ring are replaced with the concrete and purely syntactical generic prime

This approach misses that the generic model is interesting on its own and in
particular that it satisfies peculiar nongeometric sequents such as “nonunits
are nilpotent” and “any ideal is finitely generated”. In this sense,
the generic model is better than the actual models it aims to replace, and we
believe that potential applications of this insight should be properly

§ LOCALES

The formal definition of a locale will be given below as
Definition <ref>, but we first review examples and comment on
the relevance of locales to constructive mathematics.

§.§ Spaces without points

A metric or topological space without any points is not very interesting: It is
empty, and up to isomorphism there is only one such space. In contrast, a
locale can be nontrivial even if it does not contain any points. This
phenomenon is an instance of a general guiding principle, namely that relinquishing
points increases flexibility.

The locale of surjections $\NN \twoheadrightarrow \RR$. As is
well-known, there are no surjections from $\NN$ to $\RR$.[More
precisely, it is a theorem of classical mathematics that the reals are
uncountable in the sense of admitting no surjection from the naturals. The
situation is more subtle in constructive mathematics. Firstly, in the absence
of countable choice, the reals bifurcate into several distinct flavors, hence
one needs to state which flavor of the reals one is referring to. Secondly, all
known proofs of the uncountability of the Cauchy and the Dedekind reals assume
either the law of excluded middle or the axiom of countable choice. In the
absence of either of these axioms, only the MacNeille reals are known to be
uncountable [36].] Hence there is no
interesting topological space of those surjections. The set $\{ f : \NN
\twoheadrightarrow \RR \,|\, \text{$f$ is a surjection} \}$ is empty, and there
is not much more to say about this state of affairs. However, there is a
well-defined and nontrivial locale $X$ of those surjections.

The points of $X$ are in canonical one-to-one correspondence with the
surjections $\NN \twoheadrightarrow \RR$, hence $X$ does not have any points.
But this locale does have uncountably many basic opens $U_{nx}$, where $n$
ranges over the naturals and $x$ ranges over the reals. We picture $U_{nx}$ as
the “open of those surjections $f$ for which $f(n) = x$” and we can compute with
these opens, consider functions on $X$ and ponder sublocales of $X$. For instance:

* If $x \neq y$, then the intersection of $U_{nx}$ with $U_{ny}$
is truly empty.

* The union of the $U_{nx}$, where $x$ is a fixed real
number and $n$ ranges over the naturals, is all of $X$. No finite number
of these opens covers $X$, hence $X$ is not compact.

* Assuming $x = y \vee \neg(x = y)$ for any pair of reals, there is, for any real $x$, a well-defined continuous function from $X$ to
(the localic version of) the naturals which, on the level of points, would map
a surjection $f : \NN \to \RR$ to the smallest number $n$ such that $f(n) = x$.

* There is a well-defined continuous function from $X$ to (the localic
version of) the reals which, on the level of points, would map a surjection $f$
to the number $\sum_{n=0}^\infty 2^{-n} \arctan(f(n))$. Unlike the previous
example, this function is not locally constant.

*  The locale $X$ is a sublocale of the
locale $Y$ of arbitrary functions $\NN \to \RR$ (which can also be realized as
a topological space). It can be obtained as the intersection of the uncountably
many sublocales $Y_x$, where $Y_x$ is the sublocale of $Y$ consisting of those
functions which hit the real $x$.

* A certain sublocale of $X$, the locale $X'$ of those functions $\NN \to
\RR$ for which any real has infinitely many preimages, has a fractal nature: It
is covered by the (intersections with $X'$ of the) opens $U_{0x}$, where $x$ ranges over the reals; the pairwise
intersection of these opens is (truly) empty; and they are each isomorphic
to $X'$ – on the level of points, by mapping a surjection $f$ in $U_{0x}$ to
the surjection $(n \mapsto f(n+1))$.

There is nothing special about the real numbers in this example;
in fact, the example works just as well with any set $M$ in place of the reals.
For any set $M$, there is a locale of surjections $\NN \twoheadrightarrow M$,
and this locale is trivial (isomorphic to the empty locale) if and only if $M$
is empty. Locales of these kind are used as an important reduction step in the
extension of Grothendieck's Galois theory by André Joyal and
Myles Tierney <cit.>.

Intersection of dense sublocales. In ordinary topology, the
intersection of dense subspaces need not be dense. A simple example is the
intersection of $\QQ$ with its complement in $\RR$. In contrast, the
intersection of (even an arbitrary set of) dense sublocales is always again
dense – even if the intersection might well have no points.

For instance, the locale-theoretic intersection of (the localic version
of) $\QQ$ with its complement does not have any points and is dense in (the
localic version of) the reals. Intuitively, while these two sublocales do not
have any points in common, there still is nontrivial “localic glue”.

Another example is given by item (<ref>) above:
Each of the sublocales $Y_x$ is dense in $Y$, hence their intersection $X$ is
so as well.

The Banach–Tarski paradox. The Banach–Tarski paradox is the
unintuitive statement that a three-dimensional solid ball in $\RR^3$ of
radius $r$ can be partitioned into five disjoint subsets in such a way that
rearranging those subsets using only Euclidean motions yields two disjoint
solid balls of radius $r$ each. The axiom of choice is required to procure
these subsets, and the Banach–Tarski paradox is not in
contradiction with the basic properties of the Lebesgue measure in $\RR^3$
because these intermediate subsets are not measurable.

The traditional way to avoid the Banach–Tarski paradox is to adopt the
axiom of determinacy instead of the axiom of choice. Just as the axiom
of choice posits that a certain property of the finite domain also holds for the
infinite, the axiom of determinacy is a certain statement whose finitary
analogue is provable in unadorned Zermelo–Fraenkel set theory. It entails that
all subsets of $\RR^n$ are measurable.

The Banach–Tarski paradox can also be avoided by adopting a localic point of
view: While the localic counterparts of the five pieces do not have any points
in common, the locale-theoretic pairwise intersections are still nontrivial [38].
Hence there is no paradox, as one would not expect a rearrangement of
overlapping sublocales to preserve volume.

Random sequences. Cantor space is the space $2^\NN$ of
infinite binary sequences, equipped with the product topology. A subset $U
\subseteq 2^\NN$ is open with respect to this topology if and only if for
every $\alpha \in U$, there is a number $n \in \NN$ such that

\[ \{ \beta \in 2^\NN \,|\, \forall i < n\+ \alpha(i) = \beta(i) \} \subseteq U. \]

The open subsets of $2^\NN$ are precisely those subsets which encode
observable (or semidecidable) properties of binary sequences,
those properties for which a finite record of digits suffices to verify that a
sequence has it (but not necessarily to falsify it). For instance, the sets $V
= \{ \alpha \in 2^\NN \,|\, \alpha(0) = \alpha(1) = 1 \}$ and $W = \{
\alpha \in 2^\NN \,|\, \exists n\in\NN\+ \alpha(n) = 1 \}$ are open and the sets

\begin{align*}
A &\defeq \{ \alpha \in 2^\NN \,|\, \forall n\in\NN\+ \alpha(n) = 0 \} \\
B &\defeq \Bigl\{ \alpha \in 2^\NN \,\Big|\, \lim_{n \to \infty} \frac{1}{n} \sum_{i=0}^{n-1} \alpha(i) = \frac{1}{2} \Bigr\}
\end{align*}

are not. With respect to the standard Lebesgue measure on $2^\NN$, the sets $V$
and $W$ have measure $\frac{1}{4}$ and $1$, respectively.

Unlike a regular sequence such as $(0,0,0,\ldots)$, we intuitively expect that, if the
digits of a random sequence are revealed step by step, we will
eventually verify that it is an element of $W$; and moreover, that it has any
observable property $U$ of Lebesgue measure $1$.

Elevating this expectation to a definition, it seems prudent to declare that a
sequence is random if and only if it is contained in the intersection of
all open subsets $U \subseteq 2^\NN$ with Lebesgue measure $1$. One could then
endeavor to setup a develop a theory of probability on this notion.

However, the resulting theory will be trivial for the plain reason that
according to this definition, there are no random sequences: For any
sequence $\alpha$, the set $\{ \beta \in 2^\NN \,|\, \exists n \in \NN\+
\alpha(n) \neq \beta(n) \}$ is open, has measure $1$ and does not
contain $\alpha$.

Despite this fundamental issue, one can still argue that this approach has
merit [38], and hence it is worthwhile to find a
mathematical foundation which is capable of formalizing it. Topological
spaces are too restrictive, but Alex Simpson observed that locales are
sufficiently flexible: There is a locale of random sequences, defined as
the locale-theoretic intersection of all measure-$1$ opens of $2^\NN$. This
locale is nontrivial despite having no points.

§.§ Constructive concerns

By relinquishing points, locales provide a more flexible notion of space.
Section <ref> substantiates this observation
with several examples of nontrivial locales without any points. Constructive
mathematics gives a further, orthogonal motivation to study locales: There are
situations in which the relevant spaces do have enough points, but only if one
subscribes to the axiom of choice or similar non-constructive principles. In
these situations, the pointfree approach facilitated by locales helps to give
constructive versions of classical results. We will further discuss this theme
in Section <ref>. Examples for this phenomenon include
the following.

Compactness of the unit interval. The unit interval, when realized
as a topological space, can fail to be compact in constructive
mathematics. For instance, it fails in the Russian school because the Kleene
tree provides a computable open covering of $[0,1]$ with no computable finite
subcovering (a self-contained exposition of this phenomenon is contained in
Ref. bauer:kleene-tree).

In contrast, the localic version of the unit interval is always compact. The
proof is by an explicit computation with its basic opens, exploiting the inductive
nature of derivations [40].

Similarly, Tychonoff's theorem that the product of any number of compact
topological spaces is again compact is equivalent to the axiom of choice. Its
localic counterpart, the statement that the product of any number of compact
locales is again compact, can be verified without any nonconstructive
principles [41].

Galois theory. Let $L|k$ be a Galois extension. The
fundamental theorem of (infinite) Galois theory states that there is a bijection between
the intermediate extensions $L|E|k$ and the closed subgroups of the topological
Galois group $\Gal(L|k)$. The bijection maps an intermediate extension $L|E|k$
to the subgroup $\Gal(L|E)$ and its inverse maps a closed subgroup $H \subseteq
\Gal(L|k)$ to the fixed field $L^H$.

Much of the proof of the fundamental theorem of Galois theory is constructive,
but some parts use the law of excluded middle and Zorn's lemma in order to
construct certain extensions of given field homomorphisms.[For
instance, the statement $E \subseteq L^{\Gal(L|E)}$ is trivial. For the converse
inclusion, let $x \in L^{\Gal(L|E)}$. Assume for the sake of contradiction
that $x \not\in E$. Using Zorn's lemma and the law of excluded middle, we find
a homomorphism $\sigma : L \to L$ with $\sigma|_E = \operatorname{id}$
and $\sigma(x) \neq x$. This is a contradiction to $x \in L^{\Gal(L|E)}$.]
As a consequence, the fundamental theorem of Galois theory as stated is not
provable in constructive mathematics.

However, this failure is not for fundamental Galois-theoretic reasons, but because of an
unfortunate choice in the definitions. There is a notion of a localic group [42] (a
locale $G$ equipped with continuous maps $G \times G \xrightarrow{\circ} G$, $G
\xrightarrow{(\cdot)^{-1}} G$, $1 \xrightarrow{e} G$ satisfying the group
axioms), and the topological Galois group has a localic counterpart. The
fundamental theorem can be reformulated to refer to this localic Galois group,
and the proof of this reformulation is entirely constructive [43].

If one is so inclined, then one can obtain the topological version of the
fundamental theorem as a corollary of the localic version; the required
non-constructive principles for this step are neatly packaged up in the study
of the relation of the localic Galois group with the topological one.

Incidentally, the fundamental theorem of Galois theory also
showcases a related general phenomenon, namely that classical mathematics
allows to push back topological concerns for a bit longer,
whereas in constructive mathematics we have to embrace topology
(in a sufficiently pointfree form such as locales) from the beginning.

To be more specific, classically, the basic version of the fundamental theorem
(intermediate extensions correspond to subgroups) only holds for finite Galois
extensions. For infinite Galois extensions, we have to restrict to
closed subgroups. Constructively, the basic version cannot even be shown
for finite extensions; we have to employ spatial language even for those, or
else settle for a discrete version of the fundamental theorem: For finite field
extensions, finite intermediate extensions correspond to finite
subgroups <cit.>.
Classically, intermediate extensions of finite extensions and subgroups of
finite groups are automatically finite, but constructively this can
fail.[For instance, the field extension $\QQ(\sqrt{2})|\QQ$ is finite.
However, if the intermediate extension $E \defeq \{ x \in \QQ(\sqrt{2}) \,|\, x
\in \QQ \vee \varphi \}$ is finite, then $\varphi \vee \neg\varphi$. Using the
sheaf semantics reviewed in Section <ref>, this
intermediate extension can be turned into a topological
counterexample <cit.>.]

Gelfand duality. The celebrated Gelfand correspondence states that
the mapping

\[ X \longmapsto \Hom(X, \CC) = \{ f : X \to \CC \,|\, \text{$f$ is continuous} \} \]

defines a contravariant equivalence between compact Hausdorff spaces and
commutative unital $C^\star$-algebras. In the other direction,
a $C^\star$-algebra $A$ is mapped to its maximal spectrum $\Max(A)$, the
topological space of multiplicative linear functionals $A \to \CC$.

Some parts of the proof require the axiom of choice, (only) for fabricating
appropriate elements of the maximal spectrum. But as with the fundamental
theorem of infinite Galois theory, the Gelfand correspondence has a
constructive core, and a pointfree reformulation unearths this constructive
content: There is a contravariant equivalence between compact completely
regular locales and commutative
unital $C^\star$-algebras [44, 45, 46].

The constructive Gelfand correspondence has been used to construct phase spaces
for quantum-mechanical systems in the Bohr topos approach to quantum
mechanics [47, 48, 49].
Briefly, a quantum mechanical system is described by a $C^\star$-algebra $A$
which is in all interesting cases noncommutative. As such the Gelfand correspondence cannot be
applied to $A$. But there is a mirror image of $A$ as a sheaf model on a
certain locale, the Bohr topos of $A$, which is commutative.
Since the universe of sheaves supports intuitionistic reasoning, as we will
review in Section <ref>, the constructive Gelfand
correspondence can then be applied to this mirror image.

For a time, we only knew that zfc proved that there is a
constructive proof of the localic version of Gelfand duality without directly
knowing such a constructive proof. This situation arose because the first proof
of the localic duality [44] employed Barr's
theorem, to be reviewed on page par:barr.

§.§ The basics of the theory of locales

The starting point of the theory of locales is the following
observation. The set $\OOO(X)$ of open subsets of a topological
space $X$ forms a partially ordered set which has

\[ \begin{array}{@{}ccc@{}}
\text{arbitrary joins (suprema)}
\text{finite meets (infima)}, \\
\bigvee && \wedge
\end{array} \]

and where finite meets distribute over arbitrary joins:

\[ U \wedge \bigvee_i V_i = \bigvee_i (U \wedge V_i). \]

The key idea of locales is to elevate this observation to a definition, in the
process dropping the requirement for the elements of the ordered set to be sets
of points:
A frame is a partially ordered set with (arbitrary,
set-indexed) joins and finite meets such that the distributive law
holds. A frame homomorphism $\alpha : A \to A'$ is a monotone map $A
\to A'$ which preserves arbitrary joins and finite meets.

The least element of a frame (the empty join) is denoted “$\bot$” and the
largest element (the empty meet) “$\top$”. The notion of a frame is
(infinitarily) algebraic. To obtain a geometric notion, we “reverse the
direction of the arrows”:

A locale $X$ is given by a frame $\OOO(X)$, the “frame
of opens of $X$”. A morphism $f : X \to X'$ of locales (or “continuous
map of locales”) is a frame homomorphism $\OOO(X') \to \OOO(X)$.

In place of the open sets of points, locales have arbitrary opens, the
elements of their underlying frame. The opens of locales behave similar to the
open sets in topology in that arbitrary unions and finite intersections make
sense; but unlike before, they need not be sets of points. Occasionally we
abuse notation and denote the largest open of a locale $X$ by “$X$”.

Examples for locales include the following.

* Any topological space $Y$ induces a locale $L(Y)$ by
setting $\OOO(L(Y)) \defeq \OOO(Y)$. A continuous map $f : Y \to Y'$ of topological
spaces induces the frame homomorphism $\OOO(Y') \to \OOO(Y),\,U \mapsto f^{-1}[U]$
in the other direction and hence a morphism $L(Y) \to L(Y')$ of locales in the
same direction.

* The one-point locale $\pt$ is the locale induced
by the one-point topological space $\{\star\}$. Its frame of opens is
the powerset of $\{\star\}$, also known as the set $\Omega$ of truth
values. Its least element is $\bot = \emptyset$ and its largest element
is $\top = \{\star\}$, and potentially not all elements of $\Omega$ are equal
to one of these two.

* The locale of surjections $\NN \twoheadrightarrow \RR$ and the localic
version of the reals of Section <ref> are best
constructed as classifying locales, a notion to be introduced in
Section <ref>.

* The radical ideals of any ring $A$ form a frame and hence give rise to a
locale. We will identify this locale in Theorem <ref> to be the
spectrum of $A$ as studied in algebraic geometry.

Several notions in topology only refer to open sets and not to points. Such
notions have an immediate counterpart in locale theory. For instance, a
locale $X$ is compact iff for any family $(U_i)_{i \in I}$ of opens
of $X$ such that $\top = \bigvee_{i \in I} U_i$, there is a (Kuratowski-)finite
subset $I' \subseteq I$ such that $\top = \bigvee_{i \in I'} U_i$.[A
set $M$ is Kuratowski-finite iff there is a surjection $[n]
\twoheadrightarrow M$, where $[n] = \{1,2,\ldots,n\}$. In constructive
mathematics, we distinguish this notion from the stronger condition for a
set $M$ to be Bishop-finite, which requires that there is a
bijection $[n] \to M$.]
With this definition, a topological space $Y$ is compact iff its induced locale $L(Y)$ is.

Points do not appear in the definition of a locale, but they can be defined as
a derived concept:
A point of a locale $X$ is a locale morphism $\pt \to

This definition is inspired from the situation with topological spaces, where
continuous maps from the one-point space to a topological space $Y$ are in
canonical bijection with the points of $Y$.

The underlying frame homomorphism $\alpha : \OOO(X) \to \Omega$ of a point $x$
of $X$ can be pictured as mapping each open $U$ of $X$ to the truth value to which
extent $x$ belongs to $U$. Mnemonically, we write $x \inplus U$ iff $\alpha(U)
= \top$.

The point $x$ is completely determined by the information to which opens it
belongs, that is by the set $\{ U \in \OOO(X) \,|\, \alpha(U) = \top \}$. This set is a completely
prime filter, that is a subset $\fff \subseteq \OOO(X)$ which is upward-closed,
closed under finite meets and for which $\bigvee_i U_i \in \fff$ implies $U_i
\in \fff$ for some index $i$; and conversely, any such completely prime filter
gives rise to a point of $X$ (Exercise <ref>).

A locale $X$ is spatial if and only if its points
suffice to detect the inclusion relation on the opens of $X$, that is if for any opens $U, V \in \OOO(X)$,
if $x \inplus U \Rightarrow x \inplus V$ for all points $x$ of $X$, then $U
\preceq V$.

An equivalent definition is: A locale $X$ is spatial if and only if its points
suffice to distinguish its opens, that is if for any opens $U, V \in \OOO(X)$, if $x \inplus U
\Leftrightarrow x \inplus V$ for all points $x$ of $X$, then $U = V$.

For instance, any locale induced by a topological space is spatial. The locale
of surjections $\NN \twoheadrightarrow \RR$ is a striking example of a locale which fails to be
spatial. The localic real line is spatial in classical mathematics and can
fail to be spatial in constructive mathematics
(Exercise <ref>). In this case, the locale induced by the
topological space of reals should not be confused with the true localic real
line. These locales have the same points, but the former might not be locally compact
while the latter always is.

The set of points of a locale $X$ can be made into a topological space, giving
rise to a functor $\Pt : \Loc \to \Top$. This functor is right adjoint
to the functor $L : \Top \to \Loc$. A locale $X$ is spatial iff the canonical
morphism $L(\Pt(X)) \to X$ is an isomorphism, and a topological space $Y$
is sober iff the canonical morphism $Y \to \Pt(L(Y))$ is a
homeomorphism. The space $\Pt(L(Y))$ is the sobrification of $Y$; for
instance, the sobrification of any inhabited indiscrete space is the one-point

The adjunction $L \dashv \Pt$ restricts to an equivalence between sober
topological spaces and spatial locales. Assuming the law of excluded middle,
both Hausdorff spaces and the schemes from algebraic geometry are sober
(Exercise <ref>), hence the spaces of a wide
range of the mathematical landscape can be faithfully studied as locales.

Since continuous maps between spaces induce locale morphisms, we
have a canonical map $\Hom_\Top(Y,Y') \to \Hom_\Loc(L(Y),L(Y'))$. If $Y'$ is
sober, this map is a bijection. In particular, in this case the set-theoretic points
of $Y'$ and the locale-theoretic points of $L(Y')$ are in canonical
one-to-one correspondence.

§.§ Exercises

[The space of points of a locale]

Devise a canonical topology on the set of points of a locale.

[Sober topological spaces as locales]
Verify the statements made in Remark <ref>.

[Hausdorff spaces are sober]

A meet-irreducible open subset of a topological space $Y$ is an
open subset $W \subseteq Y$ such that $(U \cap V \subseteq W) \Rightarrow (U
\subseteq W) \vee (V \subseteq W)$ for all open subsets $U,V \subseteq Y$ and
such that $Y \not\subseteq W$.

* Assuming the law of excluded middle, show that the completely prime
filters of a topological space are in canonical one-to-one correspondence with
the meet-irreducible open subsets.

Hint. Given a completely prime filter $\fff \subseteq
\OOO(Y)$, the set $\bigcup\{ U \in \OOO(Y) \,|\, U \not\in \fff \}$ is a
meet-irreducible open subset.

* Assuming the law of excluded middle, show that a topological space is
sober in the sense of Remark <ref> if and only if for
every meet-irreducible open subset $W$ there is a unique point $y \in Y$ such
that $W = Y \setminus \overline{\{y\}}$.
(This is a classical definition of sobriety.)

* Assuming the law of excluded middle, show that Hausdorff topological
spaces validate the condition stated in part (b) and hence are sober.

Note. Without the law of excluded middle, Hausdorff spaces
and even metric spaces may fail to be sober. In fact, already the topological
space of rational numbers can fail to be
sober <cit.>.

[Complete metric spaces are sober]
A metric space is a set $Y$ together with a relation $d \subseteq Y
\times Y \times \QQ_{\geq0}$, written “$d(x,y) \leq q$”, such that the
following axioms are satisfied.

\begin{align*}
d(x,y) \leq q \wedge q \leq r &\Longrightarrow d(x,y) \leq r \\
(\forall r \in \QQ_{> q}\+ d(x,y) \leq r) &\Longrightarrow d(x,y) \leq q \\
&\mathrel{\phantom{\Longrightarrow}} \exists q \in \QQ_{\geq0}\+ d(x,y) \leq q \\
&\mathrel{\phantom{\Longrightarrow}} d(x,x) \leq 0 \\
d(x,y) \leq 0 &\Longrightarrow x = y \\
d(x,y) \leq q &\Longrightarrow d(y,x) \leq q \\
d(x,y) \leq q \wedge d(y,z) \leq r &\Longrightarrow d(x,z) \leq q+r
\end{align*}

A Cauchy process (or multi-valued modulated Cauchy sequence) in a metric
space $Y$ is a map $\alpha : \QQ_{>0} \to P(Y)$ such that all the sets $\alpha(q)$
are inhabited and such that $d(x,x') \leq q + q'$ for all $q,q' \in \QQ_{>0}$
and $x \in \alpha(q), x' \in \alpha(q')$. Such a process converges
to $x_0 \in Y$ iff $d(x,x_0) \leq q$ for all $q \in \QQ_{>0}$
and $x \in \alpha(q)$. A metric space $Y$ is complete iff every Cauchy
process in $Y$ converges.

Verify, without using the law of excluded middle, that any complete metric
space is sober.

Note. In the presence of the countable axiom of choice, any
Cauchy process can be refined to a Cauchy sequence. In its absence, however, the
familiar completion construction using equivalence classes of Cauchy sequences
fails to yield a Cauchy-complete space. In contrast, any Cauchy sequence and
more generally any Cauchy process converges in the space of equivalence classes
of Cauchy processes.

[Isomorphisms of frames]

Show that a frame homomorphism $\alpha : A \to A'$ is an isomorphism (that is,
admits an inverse frame homomorphism) if and only if $\alpha$ is surjective and
reflects the ordering (that is, $\alpha(U) \preceq \alpha(V) \Rightarrow U
\preceq V$).

[The covariant approach to locales]
Let $A$ be a frame.

* Show that $A$ contains arbitrary (set-indexed) meets (though they are not
required to be preserved by frame homomorphisms), by the impredicative

\[ \bigwedge_{i \in I} U_i = \bigvee\{ V \in A \,|\, \text{$V \preceq U_i$ for all~$i \in I$}
\}. \]

* What are the arbitrary meets in the frame of open subsets of a
topological space?

* Show that for any frame homomorphism $\alpha : A \to A'$ there exists a
monotone map $\beta : A' \to A$ such that $\beta$ is right adjoint
to $\alpha$, that is such that

\[ \alpha(U) \preceq V \quad\text{iff}\quad U \preceq \beta(V) \]

for all $U \in A$ and $V \in A'$.

Note. Based on the observation in part (c), a
covariant approach to locales can be developed, in which locale maps $X
\to X'$ are defined to be certain kinds of maps $\OOO(X) \to
\OOO(X')$ [51].

[Points as complete prime filters]

Verify that the points of a locale $X$ are in canonical one-to-one correspondence
with the completely prime filters of $\OOO(X)$.

[Dense opens]

An open $U$ of a locale is dense iff for any open $V$, $U \wedge V =
\bot$ implies $V = \bot$.

* Let $M$ be a set and endow it with the discrete topology. Show that an
open $U \in \OOO(L(M))$ is dense iff for any element $x \in M$, $\neg\neg(x \in

* Let $\varphi$ be a truth value, hence an open of the one-point
locale $\pt$. Show that $\varphi$ is dense in $\pt$ iff $\neg\neg\varphi$.

[Characterizing spatial locales]
Let $X$ be a locale. Show that the following conditions are equivalent.

* For any opens $U, V \in \OOO(X)$: If $x \inplus U \Rightarrow y \inplus V$
for all points $x$ of $X$, then $U \preceq V$.

* For any opens $U, V \in \OOO(X)$: If $x \inplus U \Leftrightarrow y \inplus V$
for all points $x$ of $X$, then $U = V$.

* There is a topological space $Y$ and a surjective morphism $L(Y) \to X$
of locales. (A morphism of locales is surjective iff its underlying
frame homomorphism is injective.)

* The canonical morphism $L(\Pt(X)) \to X$ is an isomorphism.

[The frame of radical ideals]

Let $A$ be a ring. We order the set $\Idl(A)$ of ideals of $A$ by inclusion.
(See Section <ref> for some algebraic

* Verify that $\Idl(A)$ has arbitrary meets and joins, given by
intersection and sum of ideals, but that it is in general not a

Hint. The distributive law fails in the polynomial ring $\QQ[X,Y]$.

* Show that the sub-poset $\Rad(A)$ of radical ideals is a frame, with
the same finite meets but with joins given by the radical of the join computed
in $\Idl(A)$.

*  Let $\varphi$ be a truth value. Let $\{\top\,|\,\varphi\}$ be the
subsingleton subset of $\Rad(A)$ which contains the top element $\sqrt{(1)}$
iff $\varphi$. Verify that

\[ \bigvee\{\top\,|\,\varphi\} = \{ f \in A \,|\, \text{$f$ is nilpotent
or~$\varphi$} \} \]

in $\Rad(A)$.

[Coproduct of locales]

* Show that the category of frames has small products.

* Deduce that the category of locales has small coproducts.

Note. The category of locales also has small products;
Exercise <ref> is devoted to this fact.

* Let $M$ be a set and endow it with the discrete topology. Show
that $L(M)$ is the coproduct $\coprod_{x \in M} \pt$.

[Local locales]

A locale $X$ is local iff for any open covering $\top = \bigvee_i U_i$,
there is an index $i$ such that $\top = U_i$. (For instance, the spectrum of a
ring $A$ is local iff $A$ is local.)
Show that any local locale has a canonical point, its focal point.

[Maps into discrete spaces]
Let $X$ be a locale. Let $A$ be a set and endow it with the discrete topology. Show
that morphisms $X \to L(A)$ are in canonical correspondence with
families $(U_a)_{a \in A}$ of opens of $X$ such that $\top = \bigvee_{a \in A}
U_a$ and $U_a \wedge U_b \preceq \bigvee\{ \top \,|\, a = b \}$.

§ GEOMETRIC THEORIES AND SHEAF MODELS

§.§ Geometric theories

A geometric theory consists of

* a set of sorts: $X$, $Y$, $Z$, …
* a set of function symbols: $f : X \times Y \to Z$, …
* a set of relation symbols: $R \hookrightarrow X \times Y \times Z$, …
* a set of geometric sequents as axioms: $\varphi \vdash_{x:X, y:Y} \psi$, …
A geometric sequent (in some context $x_1\?X_1,\ldots,x_n\?X_n$) is a
formula built using only the ingredients ${=}\ {\top}\ {\wedge}\ {\bot}\
{\vee}\ {\bigvee}\ {\exists}$ and the relation symbols (but no ${\Rightarrow}\
{\forall}$). We follow the usual convention that negation is understood as
syntactic sugar for implication to $\bot$. The symbol “$\bigvee$” refers to disjunction of arbitrary
set-indexed families of formulas. The theory proves a sequent $\sigma$ if and
only if there exists a derivation of $\sigma$, where the class of
derivations is inductively generated by the axioms and the rules displayed in
Table <ref>.[Because of the infinitary
disjunctions, some care is needed to not “build in” the axiom of choice in
the definition of derivations. More specifically, we allow inhabited sets of
subdeductions instead of requiring that subdeductions are given by a function.
Details on the implementation in czf can be found in
Ref. <cit.>.]

We refer to Ref. <cit.> for a more detailed
version of Definition <ref>.

The rules of geometric logic0.8

structural rules
a$\phantom{\seq{\vec x}}$$\varphi \seq{\vec x} \varphi$$\varphi \seq{\vec x} \psi$$\psi \seq{\vec x}
\chi$$\varphi \seq{\vec x} \chi$$\varphi \seq{\vec x} \psi$$\varphi[\vec s/\vec x]
\seq{\vec y} \psi[\vec s/\vec x]$[0pt]($\vec y$ not bound)

rules for conjunction
a$\phantom{\seq{\vec x}}$$\varphi \seq{\vec x} \top$$\phantom{\seq{\vec x}}$$\varphi \wedge \psi \seq{\vec x} \varphi$$\phantom{\seq{\vec x}}$$\varphi \wedge \psi \seq{\vec x} \psi$$\varphi \seq{\vec x} \psi$$\varphi \seq{\vec x} \chi$$\varphi \seq{\vec x} \psi \wedge \chi$a

rules for finitary disjunction
a$\phantom{\seq{\vec x}}$$\bot \seq{\vec x} \varphi$$\phantom{\seq{\vec x}}$$\varphi \seq{\vec x} \varphi \vee \psi$$\phantom{\seq{\vec x}}$$\psi \seq{\vec x} \varphi \vee \psi$$\varphi \seq{\vec x} \chi$$\psi \seq{\vec x} \chi$$\varphi \vee \psi \seq{\vec x} \chi$a

rules for infinitary disjunction
a$\phantom{\seq{\vec x}}$$\varphi_{i_0} \seq{\vec x} \bigvee_{i \in I} \varphi_i$$\varphi_i \seq{\vec x} \chi \text{ for each~$i \in I$}$$\bigvee_{i \in I} \varphi_i \seq{\vec x} \chi$a

double rule for existential quantification
a$\varphi \ \fCenter\seq{\vec x, y} \psi$
$\exists y\?Y\+ \varphi\ \fCenter\seq{\vec x} \psi$
[0pt]($y$ not free in $\psi$)

mixed rules (unnecessary in presence of the rule for implication)

a$\phantom{\seq{\vec x}}$
$(\bigvee_i \varphi_i) \wedge \psi \seq{\vec x} \bigvee_i (\varphi_i \wedge \psi)$
$\phantom{\seq{\vec x}}$
$(\exists y\?Y\+ \varphi) \wedge \psi \seq{\vec x} \exists y\?Y\+ (\varphi \wedge \psi)$
[0pt]($y$ none of the $\vec x$)

rules for equality

a$\phantom{\seq{\vec x}}$
$\top \seq{x} x = x$
$\phantom{\seq{\vec x}}$
$(\vec x = \vec y) \wedge \varphi \seq{\vec z} \varphi[\vec y/\vec x]$

(“$\vec x = \vec y\,$” is an abbreviation for “$x_1 = y_1 \wedge \cdots \wedge x_n =

The rules of infinitary intuitionistic first-order logic0.8

(structural rules and rules for ${=}\ {\top}\ {\wedge}\ {\bot}\ {\vee}\ {\bigvee}\
{\exists}$ as in Table <ref>)

rules for infinitary conjunction
a$\phantom{\seq{\vec x}}$$\bigwedge_{i \in I} \varphi_i \seq{\vec x} \varphi_{i_0}$$\psi \seq{\vec x} \varphi_i \text{ for each~$i \in I$}$$\psi \seq{\vec x} \bigwedge_{i \in I} \varphi_i$a

double rule for implication
a$\varphi \wedge \psi\ \fCenter\seq{\vec x} \chi$
$\varphi\ \fCenter\seq{\vec x} \psi \Rightarrow \chi$

double rule for universal quantification
a$\varphi \ \fCenter\seq{\vec x, y} \psi$
$\varphi\ \fCenter\seq{\vec x} \forall y\?Y\+ \psi$
[0pt]($y$ not free in $\varphi$)

Even though superficially similar, geometric theories play a
substantially different role than formal systems such as Peano arithmetic or
Zermelo–Fraenkel set theory. There are a number of notable differences:

* Formal systems are typically of foundational interest and can be
fruitfully employed as metatheories. Geometric theories are more interesting
for specific applications, for instance for presenting spaces. This aspect is discussed
in Section <ref>.

* Formal systems typically come with an intended model; geometric theories
do not. For instance, the geometric theory of groups has all groups as models;
when we are writing down the axioms of a group, we are not setting out to
capture the properties of any one specific group.

* Formal systems are typically required to be recursively
axiomatizable. Many interesting geometric theories are not, and indeed contain
an uncountable number of sorts, function symbols, relation symbols or axioms. Geometric theories also allow for arbitrary
set-indexed disjunctions; for this to make sense, the study of geometric
theories can only be carried out in a sufficiently rich background theory.

* For formal systems, typically a version of Gödel's completeness theorem
holds: A formula is derivable iff it holds in all models. In contrast,
geometric theories can be consistent yet do not admit any set-based models. An
example is the geometric theory of surjections $\NN \twoheadrightarrow \RR$
reviewed below.

* Perhaps the most important difference to formal systems is that geometric
theories, unlike formal systems, often depend on given mathematical objects. For instance, for each
ring $A$, there is the geometric theory of prime filters of $A$. This theory
will play a crucial role in Section <ref>.

A set-based model $M$ (or “Tarski model”) of a
geometric theory $\TT$ consists of

* a set $\brak{X}$ for each sort $X$,

* a function $\brak{f} : \brak{X_1} \times \cdots \times \brak{X_n} \to
\brak{Y}$
for each function symbol $f : X_1 \times \cdots \times X_n \to Y$ and

* a relation $\brak{R} \subseteq \brak{X_1} \times \cdots \times \brak{X_n}$
for each relation symbol $R \hookrightarrow X_1 \times \cdots \times X_n$

such that $M$ validates the axioms of $\TT$.

We explicitly allow empty carriers, that is we do not demand that the
sets $\brak{X}$ are inhabited.
Examples for geometric theories include the following.

* The geometric theory of rings. This theory has one sort, $R$; five function symbols:
$0$ and $1$ (nullary), $-$ (unary), $+$ and $\cdot$ (binary); no relation
symbols; and the usual axioms, such as $\top \vdash_{x:R,y:R} x + y = y + x$.

A set-based model of the theory of rings is an ordinary ring.

By adding the axiom

\begin{align*}
\top &\seq{x:R} (x = 0) \vee (\exists y\?R\+ xy = 1),
\intertext{we describe \emph{geometric fields}, and by additionally adding for
each natural number~$n \geq 1$ the axiom}
\top &\seq{a_0:R,\ldots,a_{n-1}:R} \exists x\?R\+ x^n + a_{n-1}x^{n-1} +
\cdots + a_1x + a_0 = 0,
\end{align*}

we describe algebraically closed geometric fields. (This field
condition is called “geometric” because it can be put as a geometric sequent.
Other, constructively not equivalent conditions such as “any nonzero element
is invertible” or “any nonunit is zero” are not geometric sequents.)

In a similar vein, there is the geometric theory of monoids, of groups, and so
on. Some of these theories use the infinite disjunctions supported by geometric
logic: For instance, the theory of fields of positive characteristic or the
theory of torsion groups have among their axioms

\[ \top \vdash \bigvee_{n \in \NN_{\geq 1}} (\underbrace{1 + \cdots + 1}_{\text{$n$ summands}} = 0)
\quad\text{or}\quad
\top \seq{g:G} \bigvee_{n \in \NN} (g^n = e). \]

* The geometric theory of objects.
This theory has one sort, $X$, and no function
symbols, relation symbols or axioms. A set-based model of this theory is just a

A variant of this theory is the theory of inhabited objects, which has the
axiom $\top \vdash \exists x\?X\+ \top$. Its set-based models are precisely the
inhabited sets.

*  The geometric theory of surjections $f : \NN \twoheadrightarrow
\RR$. This theory has no
sorts; no function symbols; a nullary relation symbol $\varphi_{nx}$ for each
pair $\langle n,x \rangle \in \NN \times \RR$ (to be read as “$f$ maps $n$
to $x$”); and the following axioms:

* For each $n \in \NN$, the axiom $\top \vdash \bigvee_{x \in \RR}
\varphi_{nx}$, expressing that $f$ is total.

* For each $n \in \NN$ and each $x,y \in \RR$, the axiom $\varphi_{nx}
\wedge \varphi_{ny} \vdash \bigvee\{ \top \,|\, x = y \}$,
expressing that $f$ is single-valued.[The disjunction is taken over
the set $\{ \top \,|\, x = y \}$. This is a certain subsingleton set of
formulas; it is inhabited (by the formula $\top$) iff $x = y$. Hence, if $x =
y$, this axiom reads $\varphi_{nx}
\wedge \varphi_{ny} \vdash \top$ and could also be omitted; if $x \neq y$,
this axiom reads $\varphi_{nx} \wedge \varphi_{ny} \vdash \bot$. If we work in
a constructive metatheory, we cannot perform this case distinction.]

* For each $x \in \RR$, the axiom $\top \vdash \bigvee_{n \in \NN}
\varphi_{nx}$, expressing that $f$ is surjective.

A model of this geometric theory consists of an $(\NN \times \RR)$-indexed
family of truth values, that is a subset $G$ of $\NN \times \RR$, satisfying
precisely those axioms which render $G$ the graph of a surjection $\NN
\twoheadrightarrow \RR$.

* The geometric theory of Dedekind cuts.
This theory has no sorts; no
function symbols; nullary relation symbols $\alpha_x$ and $\beta_x$ for each
rational number $x$ (to be read as “$x$ is contained in the lower (upper)
cut”); and the following axioms, spelling out that the cut is bounded,
rounded, open and located:

\begin{align*}
\top &\vdash \textstyle\bigvee_{x \in \QQ} \alpha_x \\
\top &\vdash \textstyle\bigvee_{x \in \QQ} \beta_x \\
\alpha_y &\vdash \alpha_x & \text{(for each~$x,y \in \QQ$ such that~$x < y$)} \\
\beta_x &\vdash \beta_y & \text{(for each~$x,y \in \QQ$ such that~$x < y$)} \\
\alpha_x &\vdash \textstyle\bigvee_{y > x} \alpha_y & \text{(for each~$x \in \QQ$)} \\
\beta_y &\vdash \textstyle\bigvee_{x < y} \beta_x & \text{(for each~$y \in \QQ$)} \\
\alpha_x \wedge \beta_y &\vdash \bot & \text{(for each~$x,y \in \QQ$ such that~$x \geq y$)} \\
\top &\vdash \alpha_x \vee \beta_y & \text{(for each~$x,y \in \QQ$ such that~$x < y$)}
\end{align*}

A model of this geometric theory consists of two families of truth values, both
indexed by the rational numbers, hence two subsets $L,U \subseteq \QQ$, in such
a way that $\langle L,U \rangle$ is a Dedekind cut.

* The geometric theory of prime ideals of a given ring $A$. In classical
commutative algebra, the notion of a prime ideal of a ring $A$ is
fundamental. Corresponding to the definition (recalled in
Section <ref>), the geometric theory of prime
ideals has no sorts; no function
symbols; one relation symbol “$V(x)$” for each element $x \in A$; and the
following axioms:

\begin{align*}
\top &\vdash V(0) \\
V(x) \wedge V(y) &\vdash V(x+y) & \text{(for each~$x,y \in A$)} \\
V(x) &\vdash V(xy) & \text{(for each~$x,y \in A$)} \\
V(1) &\vdash \bot \\
V(xy) &\vdash V(x) \vee V(y) & \text{(for each~$x,y \in A$)}
\end{align*}

For many purposes, the theory of prime filters is actually more
relevant.[This is not to say that all the issues with prime ideals in
constructive mathematics evaporate when turning to prime filters. For a time it
was believed that algebraic geometry could be developed constructively if only
the spectrum of a ring was defined as the topological space of its prime
filters <cit.>, but this hope turned out to be
too naive. André Joyal gave an explicit example of a nontrivial sheaf model of
the theory of rings without any prime filters <cit.>.]
Classically, a prime filter of a ring is simply the complement of a
prime ideal; constructively, it is prudent to turn prime ideals upside down and axiomatize this notion directly.
Hence the theory of prime filters of $A$ has no sorts, no function symbols, one
relation symbol “$D(x)$” for each element $x \in A$ and the following

\begin{align*}
D(0) &\vdash \bot \\
D(x+y) &\vdash D(x) \vee D(y) & \text{(for each~$x,y \in A$)} \\
D(xy) &\vdash D(x) & \text{(for each~$x,y \in A$)} \\
\top &\vdash D(1) \\
D(x) \wedge D(y) &\vdash D(xy) & \text{(for each~$x,y \in A$)}
\end{align*}

* The geometric theory of automorphisms of a field.
Let $L|k$ be a field
extension. The theory of automorphisms $L \to L$ which fix $k$ has
one nullary relation symbol “$\sigma_{xy}$” for each pair $\langle x,y
\rangle \in L$ and the following axioms:

\begin{align*}
\top &\vdash \bigvee_y \sigma_{xy} & \text{(for each~$x \in L$)} \\
\top &\vdash \bigvee_x \sigma_{xy} & \text{(for each~$y \in L$)} \\
\sigma_{xy} \wedge \sigma_{xy'} &\vdash \bigvee\{ \top \,|\, y = y' \} & \text{(for each~$x,y,y' \in L$)} \\
\sigma_{xy} \wedge \sigma_{x'y} &\vdash \bigvee\{ \top \,|\, x = x' \} & \text{(for each~$x,x',y \in L$)} \\
\top &\vdash \sigma_{00} \\
\top &\vdash \sigma_{11} \\
\sigma_{xy} \wedge \sigma_{x'y'} &\vdash \sigma_{x+x',y+y'} & \text{(for each~$x,x',y,y' \in L$)} \\
\sigma_{xy} \wedge \sigma_{x'y'} &\vdash \sigma_{xx',yy'} & \text{(for each~$x,x',y,y' \in L$)} \\
\top &\vdash \sigma_{xx} & \text{(for each~$x \in k$)}
\end{align*}

A model of this theory (can be reorganized to be) an element of the classical
Galois group of $L|k$.

* The inconsistent geometric theory. This theory has no sorts,
function symbols or relations, but the single axiom $\top \vdash \bot$.
This theory does not admit any set-based models.

* The empty geometric theory. This theory does not have any sorts,
function symbols, relations or axioms. There is exactly one set-based model of
this theory, the empty structure.

Extracting constructive content from classical proofs.
Geometric logic strikes a fine balance between being sufficiently expressive in order to
have rich applications and also being sufficiently restrictive so that Barr's
theorem holds. This theorem is concerned with eliminating classical reasoning
from proofs of geometric sequents, and it comes in a simple yet still useful
and a more sophisticated version:

* If infinitary classical logic (classical logic extended by set-indexed
conjunctions and disjunctions) proves a geometric sequent, then so does
geometric logic.

* If a specific version of extensional type theory with the law of excluded
middle and the axiom of choice proves a geometric sequent, then so does
geometric logic.

Barr's theorem has ramifications for constructive algebra, as pointed out by
Gavin Wraith [55].
For instance, the Nullstellensatz is the statement that for any
system $f_1,\ldots,f_n \in K[X_1,\ldots,X_m]$ of polynomials over an
algebraically closed field $K$, either the polynomials $f_i$ have a common zero
or there are polynomials $g_i$ such that $1 = \sum_i f_i g_i$ (such an
expression is an algebraic witness of the nonexistence of a common

The Nullstellensatz is a theorem of classical mathematics whose usual proof employs the
axiom of choice. Since it can be formulated as a geometric sequent over the
geometric theory of algebraically closed geometric fields, Barr's theorem
implies that there is also a constructive proof, in fact even a purely
geometric proof.

The simpler version of Barr's theorem is constructive, and although we will not
use it in the remainder of this text, we use this opportunity to present a
self-contained proof. The proof describes an explicit method for eliminating
the law of excluded middle from proofs of geometric sequents.

In contrast, the full version is not constructive.[
The textbook argument <cit.> establishing
the full version of Barr's theorem requires the axiom of choice. But recently
Michael Rathjen was able to lower the required metatheory
to zf <cit.>, by working internally to a
relative version of Gödel's constructible universe $L$ over a forcing
extension, where the Barwise completeness theorem applies. To our knowledge,
the precise strength of Barr's theorem relative to czf or izf
has not yet been precisely calibrated. In particular, it is an open
question [57] whether Barr's theorem implies the law of
excluded middle, though it would be a major surprise if it did not.]
This puts us in the curious situation that we are promised, unconstructively,
that there exist certain constructive proofs, without being given any indication how
these proofs could be found or what an upper bound on their length is.

However, knowing that these proofs exist platonically is still worthwhile, as
we can be assured that looking for these proofs is not bound to fail. Indeed,
for the example of the Nullstellensatz, a constructive proof is given
in Ref. <cit.>.

Also, if one is interested in constructive proofs not because of their
algorithmic content or of the mathematical insights they communicate but more
pragmatically for their applicability in, for instance, sheaf models, not
having them explicitly available is entirely bearable.

For the precise statement of the simple version of Barr's theorem, we recall
that the rules of geometric logic have been defined in
Table <ref>; that the rules of infinitary intuitionistic
first-order logic have been defined in Table <ref>; and
that infinitary classical logic is infinitary intuitionistic logic extended by
the law of excluded middle.

Let $\TT$ be a geometric theory.
Let $\sigma$ be a geometric sequent over the signature of $\TT$. Then the
following statements are equivalent.

* There is a $\TT$-derivation of $\sigma$ in geometric logic.

* There is a $\TT$-derivation of $\sigma$ in infinitary intuitionistic

* There is a $\TT$-derivation of $\sigma$ in infinitary classical logic.

It is immediate that (1) implies (3).

To show that (3) implies (2), we combine the double negation translation
with Friedman's “nontrivial exit continuation” trick. We give a sketch of the
main thrust of the argument,
omitting lengthy verifications. Let $\sigma \equiv (\alpha \seq{\vec a} \beta)$.
For notational simplicity, we assume that the context $\vec a$ is empty, though
all of the following can be adapted to the nonempty case if care is taken to
avoid variable capture.

We introduce the operator $\nabla$ with $\nabla\varphi \defeqv
((\varphi \Rightarrow \beta) \Rightarrow \beta)$. This operator is a
local operator <cit.> in the sense that
for any formula $\varphi$ in some context $\vec x$, infinitary intuitionistic
logic proves the sequents

\[
\top \seq{\vec x} (\varphi \Rightarrow \nabla\varphi),\
\top \seq{\vec x} (\nabla\nabla\varphi \Rightarrow \nabla\varphi),\
\top \seq{\vec x} ((\nabla\varphi \wedge \nabla\psi) \Leftrightarrow \nabla(\varphi \wedge \psi)).
\]

We then set up the $\nabla$-translation $\varphi \mapsto \varphi^\nabla$
for infinitary first-order formulas over the signature of $\TT$ as described in
Table <ref>.

The definition of the $\nabla$-translation
\begin{align*}
(x = y)^\nabla &\defeqv \nabla(x = y) \\
R(x_1,\ldots,x_n)^\nabla &\defeqv \nabla(R(x_1,\ldots,x_n)) \\
\top^\nabla &\defeqv \top \quad \\
\bot^\nabla &\defeqv \nabla\bot \\
(\varphi \wedge \psi)^\nabla &\defeqv \varphi^\nabla \wedge \psi^\nabla &
\textstyle (\bigwedge_i \varphi_i)^\nabla &\defeqv \textstyle \bigwedge_i \varphi_i^\nabla \\
(\varphi \vee \psi)^\nabla &\defeqv \nabla(\varphi^\nabla \vee \psi^\nabla) &
\textstyle (\bigvee_i \varphi_i)^\nabla &\defeqv \textstyle \nabla(\bigvee_i \varphi_i^\nabla) \\
(\varphi \Rightarrow \psi)^\nabla &\defeqv (\varphi^\nabla \Rightarrow \psi^\nabla) \\
(\forall x\?X\+ \varphi)^\nabla &\defeqv (\forall x\?X\+ \varphi^\nabla) &
(\exists x\?X\+ \varphi)^\nabla &\defeqv \nabla(\exists x\?X\+ \varphi^\nabla)
\end{align*}

Lengthy but straightforward computations by induction on the structure of
formulas or derivations then establish the following properties.

* For any infinitary first-order formula $\varphi$ in some context $\vec y$,
infinitary intuitionistic logic proves $\nabla(\varphi^\nabla) \seq{\vec x} \varphi^\nabla$.

* For any geometric formula $\varphi$ in some context $\vec x$, infinitary
intuitionistic logic proves $\varphi^\nabla \mathrel{\dashv\vdash\!\!\!_{\vec x}} \nabla\varphi$.

* For any derivation of a sequent $\varphi \seq{\vec x} \psi$ in infinitary
classical logic, there is a derivation of $\varphi^\nabla \seq{\vec x}
\psi^\nabla$ in infinitary intuitionistic logic. This property rests on the
fact that the $\nabla$-translation of the law of excluded middle,

\[ \top \seq{\vec x} \nabla(\varphi^\nabla \vee (\varphi^\nabla \Rightarrow \nabla\bot)), \]

is intuitionistically provable.

Combining these ingredients, a given derivation of $\sigma \equiv (\alpha
\vdash \beta)$ in infinitary classical logic can be transformed to give a derivation of

\[
\alpha \vdash
\nabla\alpha \vdash
\alpha^\nabla \vdash
\beta^\nabla \vdash
\nabla\beta \equiv
((\beta \Rightarrow \beta) \Rightarrow \beta) \vdash
\beta
\]

in infinitary intuitionistic logic.

To verify that (2) implies (1), we define a semantics “$\alpha \models
\varphi$” for geometric formulas $\alpha$ and infinitary first-order
formulas $\varphi$ by the clauses in Table <ref>. For
notational simplicity, we restrict to the propositional case, that is assume that the set of
sorts of $\TT$ is empty.
The following properties of the semantics can then be established by induction:

* If $\TT$ proves $\beta \vdash \alpha$ (in geometric logic), then $\alpha \models \varphi$ implies $\beta
\models \varphi$.

* If $\TT$ proves $\alpha \dashv\vdash \bigvee_i \beta_i$ (geometrically) and if $\beta_i \models \varphi$ for
all indices $i$, then $\alpha \models \varphi$.

*  If $\varphi$ is a geometric formula, then $\alpha
\models \varphi$ iff $\TT$ proves $\alpha \vdash \varphi$ (geometrically).

*  If a first-order sequent $(\varphi \vdash \psi)$
is derivable from the axioms of $\TT$ in infinitary intuitionistic logic,
then $\top \models (\varphi \Rightarrow \psi)$.

We can then conclude as follows. Assume that $(\varphi \vdash \psi)$
is derivable in infinitary intuitionistic logic. By (<ref>), we
have $\top \models (\varphi \Rightarrow \psi)$. By the clause for implication
in Table <ref>, we have $\varphi \models \psi$.
By (<ref>), there is a $\TT$-derivation of $\varphi \vdash
\psi$ in geometric logic.

The semantics set up in the proof of Theorem <ref>
coincides with the sheaf semantics of the classifying locale of $\TT$
reviewed in Section <ref> and
Section <ref>. In the nonpropositional case, the semantics
coincides with the slightly more general topos semantics of the
classifying topos of $\TT$ <cit.>. The local
operator defined in the proof cuts out a certain Boolean subtopos of the
classifying topos. An alternative proof proceeds by cut
elimination <cit.>; see also
Ref. dyckhoff-negri:geometrisation, and
Ref. rathjen-toppel:reduction for background on proof-theoretical
reduction, of which Barr's theorem is an example.

The semantics of the classifying topos of $\TT$ (propositional case)
$\alpha \models \beta$    iff    $\TT$ proves $\alpha \vdash \beta$ (in geometric logic)     (for $\beta$ a relation symbol)

$\alpha \models \top$    iff    true

$\alpha \models \varphi \wedge \psi$    iff    $\alpha \models \varphi$ and $\alpha \models \psi$

$\alpha \models \bigvee_i \varphi_i$    iff    there is a family $(\beta_k)_{k \in K}$ of geometric
formulas such that
$\TT$ proves $\alpha \dashv\vdash \bigvee_k \beta_k$ and such for each index $k \in K$,

there is an index $i \in I$ such that $\beta_k \models \varphi_i$

$\alpha \models (\varphi \Rightarrow \psi)$    iff    for any geometric
formula $\beta$ such that $\TT$ proves $\beta \vdash \alpha$,

if $\beta \models \varphi$, then $\beta \models \psi$

§.§ Presenting frames by theories

A geometric theory $\TT$ is propositional if and only
if its set of sorts is empty.

As a consequence, a propositional geometric theory consists just of a set of
nullary relation symbols and a set of axioms. Associated to any such
theory $\TT$ is its Lindenbaum algebra: This is the partially ordered
set of the geometric formulas over the signature of $\TT$ modulo $\TT$-provable
equivalence, equipped with the ordering given by $[\varphi] \preceq [\psi]$ iff $\TT$
proves $\varphi \vdash \psi$.

The Lindenbaum algebra is a frame, with finite meets given by $[\varphi] \wedge
[\psi] = [\varphi \wedge \psi]$ and set-indexed joins given by $\bigvee_i
[\varphi_i] = [\bigvee_i \varphi_i]$;[This short description of the
set-indexed joins picks representatives from each equivalence class and is
hence only sensible in the presence of the axiom of choice. In a
constructive metatheory, we should rather write $\bigvee_{i \in I} M_i =
[\bigvee_{\varphi \in \bigcup_i M_i} \varphi]$.]
we can regard the Lindenbaum algebra as the free
frame generated by the nullary relation symbols of $\TT$ modulo the axioms
of $\TT$. Our interest in the Lindenbaum algebra is because it gives rise to a

The classifying locale $L(\TT)$ of a propositional
geometric theory is the locale which has the Lindenbaum algebra of $\TT$ as its
underlying frame.

It is an instructive exercise to verify that the points of $L(\TT)$ are in
canonical one-to-one correspondence with the set-based models of $\TT$. This
observation also explains why we cannot hope to construct classifying
locales of arbitrary, nonpropositional, geometric theories: Any locale only has
a set of points, but arbitrary geometric theories can have a proper class of
set-based models. (There is, however, a classifying arithmetic
space [35] of any coherent theory and a classifying
topos <cit.> of any geometric theory.)

Many locales are fruitfully described as the classifying locale of a certain
propositional geometric theory. For instance:

* The localic real line is the classifying locale of the theory of
Dedekind cuts. Its points are the models of that theory, that is, the Dedekind
reals, and the induced topology on the set of points coincides with the usual
Euclidean topology on the reals.

The localic open unit interval is the classifying locale of the
same theory but with the additional axiom $\top \vdash \alpha_0 \wedge \beta_1$.

* The locale of surjections $\NN \twoheadrightarrow \RR$ is the
classifying locale of the theory of surjections $\NN \twoheadrightarrow \RR$.

* The spectrum of a ring $A$ is the classifying locale of the
theory of prime filters of $A$. The topological space of points of this locale
is the Zariski spectrum as familiar from algebraic
geometry.[Classically, the spectrum is usually defined as the
topological space of prime ideals instead of prime filters. However,
classically there is a canonical one-to-one correspondence between prime ideals
and prime filters, hence one could just as well use filters instead of ideals
in the definition. The classifying locale of prime ideals of $A$ also exists,
and has the prime ideals of $A$ as its points, but the induced topology on its
topological space of points is the flat topology or co-Zariski
topology [62] instead of the ordinary
Zariski topology <cit.>.]

* The localic Galois group of a field extension $L|k$ is the
classifying locale of the theory of ring automorphisms $L \to L$ which fix $k$.

* The empty locale is the classifying locale of the inconsistent theory.

* The one-point locale is the classifying locale of the empty theory.

Just as we often refer to a topological space only by its points (“the
topological space of prime filters of $A$”), not mentioning its topology, it is
customary to abbreviate “the classifying locale of the propositional geometric
theory of prime filters of $A$” as “the locale of prime filters of $A$”.

The traditional way of constructing the real line or the Zariski
spectrum as a topological space proceeds in three steps: (1) Write down the
axioms (of Dedekind cuts or of prime filters, respectively). (2) Using the powerset
axiom and separation, construct the set of Dedekind reals or the set
of prime filters, respectively. (3) Devise a useful topology on the resulting set.

Locales provide us with a more economic and also more conceptual way of
arriving at these topological spaces: They can be obtained as the topological
space of points of the corresponding classifying locale. In particular,
step (3) of manually devising a topology is not necessary when pursuing the
localic route.

In general, different theories can give rise to isomorphic classifying locales;
such theories are called Morita-equivalent. Olivia Caramello has built a vast research program
on this observation [59].

Conversely, any locale $X$ is the classifying locale of a certain theory, namely
the theory of points of $X$. This theory has one nullary relation
symbol $\varphi_U$ for each open $U \in \OOO(X)$ (read as “the point belongs
to $U$”) and the following axioms:

\begin{align*}
\varphi_U &\vdash \varphi_V & \text{(for all~$U,V \in \OOO(X)$ such that~$U \preceq V$)} \\
\top &\vdash \varphi_\top \\
\varphi_U \wedge \varphi_V &\vdash \varphi_{U \wedge V} & \text{(for all~$U,V \in \OOO(X)$)} \\
\varphi_{\bigvee_i U_i} &\vdash \bigvee_i \varphi_{U_i} & \text{(for each set-indexed family~$(U_i)_i$ of opens)}
\end{align*}

These are exactly the axioms for a completely prime filter of $\OOO(X)$. The
isomorphism from $\OOO(X)$ to the Lindenbaum algebra of this theory maps an
open $U$ to $[\varphi_U]$.

The question whether a given locale is spatial is intimately related with the
existence of appropriate ideal objects whose existence typically hinges
on the axiom of choice or one of its variants. For instance, there are the
following results (where we allow ourselves a modicum of classical logic in
order to state the results in a familiar form).

* The localic spectrum of a ring $A$ is spatial iff every nontrivial ideal
(of a certain class of rings related with $A$) is contained in a prime ideal.

* The localic Galois group of a Galois extension $L|k$ is spatial iff
any $k$-homomorphism $\sigma : E \to L$ defined on a finite intermediate
extension $L|E|k$ admits an extension to a $k$-homomorphism $L \to L$.

* The localic real line is spatial iff every open covering of the
metric space $[0,1]$ of Dedekind reals has a Lebesgue number (that is, if the
metric space $[0,1]$ is Heine–Borel compact).

* The statement that the classifying locale of any propositional coherent
theory (that is, a propositional geometric theory in which only finite
disjunctions occur) is spatial is equivalent to the Boolean Prime Ideal
Theorem .

In this picture, the opens of a locale can be regarded as finite approximations
to the ideal points which potentially belong to them. For instance, the
open $[\sigma_{\sqrt{2},-\sqrt{2}} \wedge \sigma_{\sqrt{3},\sqrt{3}}]$
of the localic Galois group of $\overline{\QQ}|\QQ$ can be regarded as an
approximation to a certain automorphism of $\overline{\QQ}$ about
which $\sqrt{2} \mapsto -\sqrt{2}$ and $\sqrt{3} \mapsto \sqrt{3}$ is known. Over time, this
approximation might be refined to a smaller open, one which contains more
information about the purported automorphism, and eventually we might actually
obtain an automorphism which is defined on all of $\overline{\QQ}$. The opens
make good constructive sense even if the points remain elusive.

The results mentioned above explain why we can, in classical mathematics, where all of the stated
conditions are satisfied, blithely and fruitfully use the topological
spectrum of a ring, the topological Galois group or the topological space of
reals. In classical mathematics, employing their localic counterparts is merely
for convenience or for aesthetic reasons; in constructive mathematics,
localic replacement (or similar replacements in other pointfree approaches to
topology) is vital.

The case of the locale of surjections $\NN \twoheadrightarrow
\RR$ is particular in that there, even the strong existence axioms of
classical mathematics do not suffice to materialize a point. In fact, already
the law of excluded middle or the countable axiom of choice preclude the
existence of points.

§.§ Sheaves on locales

A presheaf $F$ on a locale $X$ is a functor $\OOO(X)^\op \to \Set$, that is

* a set $F(U)$ for each open $U \in \OOO(X)$ and

* a map $(\cdot)|^U_V : F(U) \to F(V)$ for each pair of opens $V \preceq U$

such that $(\cdot)|^U_U = \operatorname{id}_{F(U)}$ for all $U \in \OOO(X)$ and
$(\cdot)|^V_W \circ (\cdot)|^U_V = (\cdot)|^U_W$ for all $W \preceq V
\preceq U$.

Definition <ref>, as well as any other definition in this section,
also makes sense for topological spaces instead of locales, since only the
notion of opens and their inclusion relation is used. The elements of $F(U)$ are
called sections of $F$ over $U$ and the maps $(\cdot)|^U_V$
are called restriction maps. Elements of $F(\top)$ are called
global sections.

When first learning about presheaves, one may feel intimidated by the vast
amount of data encoded in a single presheaf (one set for each open, of which there are often uncountably many). The
situation should be compared to the perhaps more familiar Kripke models for a first-order language $L$. The
preorder $W$ of nodes of such a model is like the frame of opens of a locale, and the
family $(M_w)_{w \in W}$ of $L$-structures, one for each node, is like a
presheaf. In fact, the notion of a locale can be generalized to that of a
site so that both locales and Kripke frames induce sites and that
presheaves on sites can be defined; however, this shall not be pursued here,
a textbook reference is Ref. moerdijk-maclane:sheaves-logic.

The prototypical example of a presheaf (and also a sheaf) is the presheaf $\CCC$ of
continuous real-valued functions on a topological space $X$. For this presheaf, the
set $\CCC(U)$ is the set of continuous real-valued maps $U \to \RR$, and the
maps $(\cdot)|^U_V$ are given by actual restriction of functions to smaller
domains, that is by

\[ \CCC(U) \longrightarrow \CCC(V),\ s \longmapsto s|_V. \]

Any set $M$ gives rise to a presheaf $\underline{M}^\mathrm{pre}$, by
setting $\underline{M}^\mathrm{pre}(U) = M$ for every open $U$ and employing
the identity map as restriction maps. In this way, the universe of sets embeds
into the universe of presheaves.

* A compatible family of a presheaf $F$ with respect to an open
covering $U = \bigvee_i U_i$ is a family $(s_i)_i$ of sections $s_i \in F(U_i)$
such that $s_i|^{U_i}_{U_i \wedge U_j} = s_j|^{U_j}_{U_i \wedge U_j}$ for all
indices $i,j$.

* A presheaf $F$ is a sheaf
iff for any compatible family $(s_i)_i$ with respect to any open covering $U =
\bigvee_i U_i$ there is a unique section $s \in F(U)$ such
that $s|^U_{U_i} = s_i$ for all indices $i$ (“compatible sections glue”).

For instance, the presheaf $\CCC$ of continuous real-valued functions is a sheaf,
while its subpresheaf $\CCC_\text{c}$ of constant real-valued functions is
usually not a sheaf. For instance, on $X = \RR$, the two constant functions $f
: (-1,0) \to \RR,\,x \mapsto -1$ and $g : (0,1) \to \RR,\,x \mapsto 1$ agree on
the intersection of their domains (which is empty), but there is no constant
function $h : (-1,0) \cup (0,1) \to \RR$ which restricts to $f$ on $(-1,0)$ and
to $g$ on $(0,1)$.

There is a general construction called sheafification which turns
presheaves into sheaves. Applied to the presheaf $\CCC_\text{c}$, this process yields the
sheaf of locally constant real-valued functions. Similarly, the
sheafification of the presheaf of bounded functions is the sheaf of locally
bounded functions, and so on; this is a general principle.

The presheaf $\underline{M}^\mathrm{pre}$ associated to a set $M$ is almost
never a sheaf. Its sheafification $\underline{M}$ is the constant sheaf associated
to $M$. On an open $U$, its sections are the locale
morphisms $U \to M$, where $M$ is regarded as the locale induced by
the discrete topological space $M$ and $U$ is regarded as a sublocale of $X$.
By the constant sheaf construction, the universe of sets maps to the universe
of sheaves on $X$. We will not require much more details on this construction
and only note two special cases:

* If the locale $X$ is induced by a topological space $Y$, then

\[ \underline{M}(U) = \{ f : U \to M \,|\, \text{$f$ is locally constant} \}. \]

* If $X$ is the one-point locale, then $\underline{M}(U) = M^U$.

In the other direction, given a point $x$ of a locale $X$, any sheaf $F$ on $X$ gives
rise to a set, namely the stalk of $F$ at $x$. The stalk is the set of
germs of sections of $F$ at $x$, that is the set of all sections of $F$
on opens $U$ such that $x \inplus U$, where two such sections $\langle U,s
\rangle$ and $\langle U',s' \rangle$ are identified iff there is an open $V
\preceq U \wedge U'$ such that $x \inplus V$ and $s|^U_V = s'|^{U'}_V$.

For instance, the stalk at the origin of the sheaf of holomorphic functions
on $\CC$ is in canonical bijection with the set $\CC\{z\}$ of convergent power
series, and the stalks of a constant sheaf $\underline{M}$ are all in canonical
bijection with $M$.

A subsheaf of a sheaf $F$ on a locale $X$ is a
sheaf $F'$ with $F'(U) \subseteq F(U)$ for all opens $U$ and the inherited
restriction maps.

A morphism of presheaves $\eta : F \to G$ on a
locale $X$ is a family $(\eta_U)_{U \in \OOO(X)}$ of maps $\eta_U : F(U) \to
G(U)$ such that for all sections $s \in F(U)$ and all opens $V \preceq U$
of $X$, $\eta_U(s)|^U_V = \eta_V(s|^U_V)$. A morphism of sheaves is a
morphism of the underlying presheaves.

§.§ Sheaf semantics

Motivating the sheaf semantics. Let $F$ be a sheaf on a locale $X$.
What is a sensible reading of the statement “$\forall s\?F\+ (\varphi(s)
\Rightarrow \psi(s))$”? A first answer is “for any global section $s \in
F(X)$ such that $\varphi(s)$, $\psi(s)$”. However, this proposal does not do
justice to the sheaf, whose interesting behavior may well only play out with
its sections on small opens. Indeed, many important sheaves have no or few
global sections. Hence a more sophisticated answer is “for any open $U \in
\OOO(X)$ and any section $s \in F(U)$ with $\varphi(s)$, $\psi(s)$”,
where “$\varphi(s)$” and “$\psi(s)$” have to be interpreted in a similar

Similarly, given a section $s \in F(U)$, what should “$\neg\varphi(s)$” mean?
Since a section may well validate additional properties when we zoom in to
smaller opens, the sheaf-theoretically sensible answer is “except for the
empty open $V = \bot$, $s|^U_V$ does not have property $\varphi$ for any
open $V \preceq U$”, where again “$\varphi(s|^U_V)$” has to be understood in a
sensible way.

As a final motivating example, consider the statement “$\exists s\?F\+
\varphi(s)$”. This should mean that there is an open covering $X = \bigvee_i
U_i$ such that on each open $U_i$, there is a section $s \in F(U_i)$ such
that $\varphi(s)$, properly interpreted. We should not require these individual
sections to agree on the intersections $U_i \wedge U_j$ – by the sheaf
property, this would amount to saying that there is a global section $s \in
F(X)$ with $\varphi(s)$.

The sheaf semantics formalizes the informal language agreement just
outlined. A marvelous fact with wide-ranging applications is that this
semantics is sound with respect to first-order intuitionistic logic (and even
infinitary higher-order intuitionistic logic, and even a suitable version of
extensional type theory, if the semantics is appropriately extended).

That is, if we have established a property $\varphi$ and if there is an
intuitionistic proof that $\varphi$ entails a further property $\psi$, then we
may conclude that also the interpretation of $\psi$ with the sheaf semantics

Hence the sheaf semantics allows us to reason with sheaves in much the same way
as we reason with sets, in a simple element-based language, and to import much
of the already-existing results in constructive mathematics into the world of
sheaves. For instance, any intuitionistic theorem about rings yields a
corresponding theorem about sheaves of rings.

There is only one caveat to keep in mind: Irrespective of its status in the
metatheory, the interpretation of the law of excluded middle with the sheaf
semantics is, for most locales $X$, false (Example <ref>).
Practitioners of other flavors of constructive mathematics should also observe
that the interpretation of any form of the axiom of choice, even countable
choice or weak countable choice, is false for most locales $X$. (About the only
exception are locales induced from discrete topological spaces. For such
locales, the law of excluded middle and countable, dependent or full choice
pass from the metatheory to the universe of sheaves.)

Incidentally, that the sheaf semantics is not sound with respect to classical
logic allows us to illustrate the failure of certain classical theorems in
constructive mathematics by geometric counterexamples and thereby verify their
unprovability in intuitionistic logic.

We now begin the formal development of the sheaf semantics. More background and
examples from theoretical computer science, analysis and differential geometry
are contained in Ref. blechschmidt:custom-tailored, which should be
regarded as a companion paper to this contribution. We also recommend
Christopher Mulvey's tutorial [65], which culminates in a proof
of the Serre–Swan theorem using the sheaf semantics. Standard references for
the sheaf semantics include Refs.
<cit.> and shulman:categorical-logic,
which also gives a detailed account of useful type theory.

Definition and basic properties of the sheaf semantics.
Let $X$ be a locale. A formula over an open $U \in \OOO(X)$ is an
infinitary first-order formula (made up using ${=}\ {\top}\ {\wedge}\ {\bigwedge}\ {\bot}\ {\vee}\
{\bigvee}\ {\Rightarrow}\ {\forall}\ {\exists}$) over the signature which has one sort for
each sheaf $F$, one constant symbol of sort $F$ for each section $s \in F(U)$,
one function symbol $f : F \to G$ for each morphism of sheaves, and so on. As
usual, we define $\neg\varphi$ to be an abbreviation of $(\varphi \Rightarrow
\bot)$.

Table <ref> defines by recursion on the structure of
formulas what it means for a formula $\varphi$ over an open $U$ to be
forced by $U$ or to be true over $U$, written “$U \models \varphi$”. The
main differences with the perhaps more familiar Kripke semantics are marked.
The sheaf semantics is also called Kripke–Joyal semantics.

For the special case that $U$ is the largest open of $X$ we also write “$\Sh(X)
\models \varphi$” or “$X \models \varphi$”.

The (first-order fragment of) the sheaf semantics of a locale $X$
$U \models s =_F t$    iff    $s = t$ when evaluated as elements of $F(U)$

$U \models R(s_1,\ldots,s_n)$    iff    $\langle s_1,\ldots,s_n \rangle \in

(where $R$ is the relation symbol corresponding to

a subsheaf $R \subseteq F_1 \times \cdots \times F_n$)

$U \models \top$    iff    true

$U \models \varphi \wedge \psi$    iff    $U \models \varphi$ and $U \models \psi$

$U \models \bigwedge_k \varphi_k$    iff    for every index $k$, $U \models \varphi_k$

$U \models \bot$    iff    false0pt3pt0pt-2pt $U = \bot$

$U \models \varphi \vee \psi$    iff    $U \models \varphi$ or $U \models \psi$0pt3pt0pt-2pt there exists an open covering $U = \bigvee_i U_i$

such that for all indices $i$: $U_i \models \varphi$ or $U_i \models \psi$

$U \models \bigvee_k \varphi_k$    iff    for some index $k$, $U \models \varphi_k$0pt3pt0pt-2pt there exists an open covering $U = \bigvee_i U_i$

such that for each index $i$, $U_i \models \varphi_k$ for some index $k$

$U \models \varphi \Rightarrow \psi$    iff    for all $V \preceq U$: $V \models \varphi$ implies $V \models \psi$

$U \models \forall s \? F\+ \varphi(s)$    iff    for all $V \preceq U$ and sections $s_0 \in F(V)$: $V \models \varphi(s_0)$

$U \models \exists s \? F\+ \varphi(s)$    iff    there exists $s_0 \in F(U)$ such that $U \models \varphi(s_0)$0pt3pt0pt-2pt

there exists an open covering $U = \bigvee_i U_i$ such that for all $i$:

there exists $s_0 \in F(U_i)$ such that $U_i \models \varphi(s_0)$

Some clauses in Table <ref> contain slight abuses of
notation. Namely, if $\varphi$ is a formula over an open $U$ and if $V$ is an
open such that $V \preceq U$, then “$V \models \varphi$” is formally not
well-defined, as $\varphi$ is not a formula over $V$. When we still write “$V
\models \varphi$”, we mean that any constant symbol $s \in F(U)$ appearing
in $\varphi$ should be interpreted as its restriction $s|^U_V \in F(V)$, so
that the resulting formula is a formula over $V$.

For instance, let $F$ be the sheaf

\[ U \longmapsto \{ f : U \to \CC \,|\, \text{$f$ is continuous and~$f(z)^2 =
z$ for all~$z \in U$} \} \]

on $X = \CC$. The interpretation of the statement “$\exists s\?F\+ \top$” is
false, as on no open which contains the origin a continuous square root
function exists), but the interpretation of “$\neg\neg(\exists s\?F\+ \top)$”
is true: Unrolling the definition, this statement expresses that
the only open $U \preceq X$ which has the property that

${\qquad}$ the only open $V \preceq U$ which has the property that

${\qquad\qquad}$ locally on $V$, there exist continuous square root functions

${\qquad}$ is $V = \bot$

is $U = \bot$.

The principal properties of the sheaf semantics is that it is monotone, local
and sound with respect to (infinitary) intuitionistic first-order logic as
defined in Table <ref> on
page table:first-order-logic:

Let $X$ be a locale. Let $U$ be an open of $X$. Let $\varphi$ be
a formula over $U$.

* If $V$ is an open such that $V \preceq U$, then $U \models
\varphi$ implies $V \models \varphi$.

* Let $U = \bigvee_i U_i$ be an open covering. If $U_i \models
\varphi$ for all $i$, then $U \models \varphi$.

* Let $\psi$ be a further formula over $U$. If $U \models
\varphi$ and if $\varphi$ entails $\psi$ intuitionistically, then also $U
\models \psi$.

The proof of (1) is by a routine induction on the structure
of $\varphi$. For the clauses pertaining disjunction and existential
quantification, the distributive law has to be used.

The proof of (2) is also a routine induction proof. For the clause pertaining
equality, the sheaf condition has to be used.

To verify statement (3), it is prudent to generalize the claim slightly: An
induction on the structure of derivations shows that if a sequent $\varphi
\seq{x_1{:}X_1,\ldots,x_n{:}X_n} \psi$ is derivable in infinitary intuitionistic first-order
logic, then $U \models \forall x_1\?X_1\+ \ldots \forall x_n\?X_n\+ (\varphi
\Rightarrow \psi)$.

The proof of Theorem <ref>
is constructive. Hence, by unrolling the definition of the sheaf semantics, any
proof which uses the sheaf semantics as a simplifying device can mechanically
be unwound to a fully explicit proof which does not reference sheaves or the
sheaf semantics.

In general, the resulting proofs will be longer and less perspicuous
than the original proofs, in particular if the original proofs employed nested
implications (such as double negations). In these cases, there is a certain
“exotic flavor” to the unwound proofs, as with tricks with continuations in
computer science. We display some such proofs which are still readable in
Section <ref>.

Sheaf models.

A sheaf model of a geometric theory $\TT$ over a locale $X$ consists of

* a sheaf $\brak{S}$ on $X$ for each sort $S$,

* a morphism $\brak{f} : \brak{S_1} \times \cdots \times \brak{S_n} \to
\brak{T}$ of sheaves for each function symbol $f : S_1 \times \cdots \times S_n \to T$ and

* a subsheaf $\brak{R} \subseteq \brak{S_1} \times \cdots \times \brak{S_n}$
for each relation symbol $R \hookrightarrow S_1 \times \cdots \times S_n$

such that the axioms of $\TT$ are validated under the sheaf semantics.

The sheaf $\CCC$ of continuous real-valued functions on any
locale $X$ together with appropriate morphisms is a sheaf model of the theory
of rings. For instance, the interpretation of the axiom

\[ \forall f\?\CCC\+ \forall g\?\CCC\+ f + g = g + f \]

with the sheaf semantics amounts to the condition

For any open $U$ and any continuous function $f \in \CCC(U)$,

${\qquad}$ for any open $V$ and any continuous function $g \in \CCC(V)$,

${\qquad\qquad}$ $f|^U_V + g = g + f|^U_V$.

and is readily seen to be fulfilled.

Any sheaf on any locale can be
regarded as a sheaf model of the theory of objects.

Any set-based model $M$ of a geometric theory $\TT$ gives rise to a
sheaf model over the one-point locale, by employing the constant sheaf
construction reviewed on page page:constant-sheaf. An infinitary
first-order formula holds for $M$ iff it holds for the induced sheaf model.
Hence sheaf models are strictly more general than set-based models.

In the special case of nullary function symbols or relations symbols, by
“$\brak{S_1} \times \cdots \times \brak{S_n}$” in
Definition <ref> we mean the empty product of sheaves, the
terminal sheaf $1$ with $1(U) = \{\star\}$ for every open $U$ of $X$.
Morphisms $1 \to F$ are in canonical bijection with global sections of $F$.
Subsheaves $F \subseteq 1$ are in canonical bijection with the opens of $X$
(Exercise <ref>).

With this in mind, we can rephrase Definition <ref> in the
special case of propositional theories in the following simpler form. A
sheaf model of a propositional geometric theory $\TT$ over a locale $X$
consists of a family $(U_\varphi)_\varphi$ of opens of $X$, one open for each
nullary relation symbol $\varphi$ of $\TT$, in such a way that the axioms are
satisfied. For instance, that an axiom “$\alpha \wedge \beta \vdash \bigvee_i
\gamma_i$” is satisfied means that $U_\alpha \wedge U_\beta \preceq \bigvee_i

In other words, a model of a propositional geometric theory $\TT$ over a
locale $X$ is the same as a frame homomorphism $\OOO(L(\TT)) \to \OOO(X)$, hence a
locale morphism $X \to L(\TT)$.

For further reference we state a proposition relating truth in a sheaf model
with truth at all points.

Let $\TT$ be a geometric theory without any axioms. Let $M$ be a sheaf model
of $\TT$ on a locale $X$ (hence just a sheaf structure) and consider
the structures $M_x$ obtained by computing the stalks at points $x \in \Pt(X)$.
Let $\sigma$ be a geometric sequent.

* If $M$ validates $\sigma$, then so does $M_x$ for any point $x \in \Pt(X)$.

* The converse holds if $X$ is spatial.

See <cit.>.

In particular, the stalks of sheaf models of a geometric theory $\TT$ are
set-based models of $\TT$.

The generic model.
A geometric theory can well have no set-based models, but might still be
consistent and allow for a diverse range of sheaf models on a host of different
locales. In fact, any propositional geometric theory always has at least one,
and very peculiar, sheaf model, namely its generic model.

The generic model $U_\TT$ of a propositional geometric
theory $\TT$ is the sheaf model on $L(\TT)$ given by $U_\varphi \defeq
[\varphi]$ for all nullary relation symbols $\varphi$.

Under the view of models as locale morphisms, the generic model $U_\TT$
corresponds to the identity morphism $L(\TT) \to L(\TT)$. If a $\TT$-model $M$ on
a locale $X$ is given by a locale morphism $f : X \to L(\TT)$, we also say
that “$M$ arises from $U_\TT$ by pullback along $f$”.

For instance, there is the generic Dedekind cut, the generic model of
the theory $\TT$ of Dedekind cuts on the classifying locale of $\TT$, the
localic real line. By Example <ref>, any specific Dedekind
real $x$ (that is, any point $x$ of $L(\TT)$) gives rise to a model of $\TT$ on
the one-point locale $\pt$, corresponding to the locale morphism $x : \pt \to

For a geometric sequent $\sigma$ over the signature of a geometric
theory $\TT$, the following statements are equivalent:

* The generic model of $\TT$ validates $\sigma$.

* All sheaf models of $\TT$ on arbitrary locales validate $\sigma$.

* The theory $\TT$ proves $\sigma$.

Hence we may understand the phrase “Let $M$ be a model of $\TT$.” to
implicitly refer to the generic model. The first-order properties of the
generic model need not be shared by all sheaf models and need not be provable
by $\TT$.

The story of generic models is at the same time tautologous and deep, and these
short paragraphs do not do justice to this intriguing aspect of the interplay
between topology (in the form of locales) and logic (in the form of
propositional geometric theories). We strongly
recommend the accessible account by Steve Vickers [5] for a fuller

The traditional way of constructing a map of topological spaces $f : Y \to
Y'$ proceeds in three steps: (1) Write down a map of the underlying sets. (2)
Identify the preimages $f^{-1}[U]$. (3) Verify that these preimages are open.

Continuing Remark <ref>, locales provide more
efficient means for constructing morphisms: To write down a morphism of
locales $X \to X'$, where $X'$ is given as the classifying locale of some
theory $\TT'$, we only need to specify a $\TT'$-model $M'$ on $X$; no separate
verification of continuity is required.

If $X$ classifies a theory $\TT$, such a specification is usually carried out
by constructing $M'$ in terms of the generic model $U_\TT$.
For instance, if $f : A \to B$ is a ring homomorphism, we obtain a locale
morphism $\Spec(B) \to \Spec(A)$ by specifying the model $([D(f(x))])_{x \in
A}$ of the theory of prime filters of $A$ on $\Spec(B)$. On the level of
points, this morphism induces the expected map $\fff \mapsto f^{-1}[\fff]$.

§.§ Exercises

[The theory of finite objects]

* Extend the geometric theory of objects
(page item:theory-of-objects) by relation symbols and axioms, but not by
constant symbols, to ensure that the set-based models are precisely the
two-element sets.

* Write down a geometric theory whose set-based models are precisely the
(Kuratowski-)finite sets.

Hint. Employ countably many relation symbols $R_n
\hookrightarrow X \times \cdots \times X$, where $R_n(x_1,\ldots,x_n)$ should
signify that the elements $x_1,\ldots,x_n$ exhaust all elements of $X$. A
solution to this exercise is given in Ref. <cit.>.

[Issues of size]
Working in izf, show that the Lindenbaum algebra of a propositional
geometric theory $\TT$ can be realized as a set, even though the class of
geometric formulas is typically a proper class.

Hint. Use that any geometric formula is provably equivalent
to one of the form $\bigvee_i \varphi_i$, where each formula $\varphi_i$ is a
conjunction of nullary relation symbols.

[Discrete locales]

* Find a theory which is classified by the two-point locale (the locale
associated to the discrete two-point topological space).

* Let $M$ be a set and endow it with the discrete topology. Find a theory
which is classified by $L(M)$.

[The localic unit interval]
Extend the theory of Dedekind cuts in such a way that its models are those
Dedekind reals which are elements of $[0,1]$.

[More on exotic locales]

* Define the locale of partial surjections $\NN \twoheadrightarrow \NN^\NN$.

Note. In Russian constructivism, as for instance reigning in
the effective topos [70, 71, 72], the Baire space $\NN^\NN$ is subcountable.
However, in this setting any function $\NN \to \NN$ is computable.
The universe of sheaves over this locale was the first example of a setting in
which the Baire space is subcountable and still any external number-theoretic
function can be imported <cit.>.

* Define the locale of injections $\RR \hookrightarrow \NN$.

Note. In classical mathematics, this locale does not have
any points. However there is a variant of the effective topos based on the
infinite-time Turing machines by Joel David Hamkins and Andy
Lewis [74] in which an injection $\RR \hookrightarrow \NN$
exists [75]. See
Ref. <cit.> for an exposition of the

* Define the locale of “open covers of $[0,1]$ by intervals with rational
endpoints such that the union of any finite number of those intervals has total
Lebesgue measure less than $\frac{1}{2}$”.

Note. In the universe of sheaves over this locale, the set
of unit interval Dedekind real numbers fails to be (Heine–Borel) compact and
the localic real line fails to be
spatial <cit.>.

* An open $U$ of a locale $X$ is complemented iff there is an
open $V$ such that $U \vee V = \top$ and $U \wedge V = \bot$. A locale is
zero-dimensional iff any open is a join of complemented opens. Assuming
that any two reals are equal or not, show that the locale of surjections $\NN
\twoheadrightarrow \RR$ is zero-dimensional.

[Models as points]
Let $\TT$ be a propositional geometric theory. Verify that the points
of $L(\TT)$ are in canonical bijection with the set-based models of $\TT$.

[The product of locales]
Let $X$ and $X'$ be locales, classifying propositional geometric
theories $\TT$ and $\TT'$ respectively. Let $\TT + \TT'$ be the combined theory
(whose set of sorts is the disjoint union of the sets of sorts of $\TT$
and $\TT'$, and so on). Show that $L(\TT + \TT')$ is the product of $X$
and $X'$ in the category of locales.

[The coproduct of locales, revisited]
Let $X$ and $X'$ be locales, classifying some propositional geometric
theories $\TT$ and $\TT'$ respectively. Find a theory in terms of $\TT$
and $\TT'$ which is classified by $X \amalg X'$.

[Spatiality of the localic reals]

Let $\RR$ be the localic real line, defined as the classifying locale of the
theory $\TT$ of Dedekind cuts as introduced on
page par:dedekind-cuts. For rational numbers $x,y$, let “$\fa x,y
\fb$” denote the formula $\alpha_x \wedge \beta_y$. Let $(x,y)$ denote the
open interval $\{ \xi \in \Pt(\RR) \,|\, x < \xi < y \}$ in the set of Dedekind reals.

* Extend the notation to allow for $x,y=\pm\infty$.

* Show that the canonical topology on $\Pt(\RR)$, defined in
Exercise <ref>, coincides with the usual Euclidean

* Show that any open of $\RR$ can be written in the form $\bigvee_i
[\fa x_i,y_i \fb]$ with $x_i,y_i \in \QQ \cup \{\pm\infty\}$.

* Let rational numbers be given such that $(x,y) \subseteq \bigcup_i
(x_i,y_i)$ in $\Pt(\RR)$. Assume that this open covering has a Lebesgue number.
Show that $\TT$ proves $\fa x,y \fb \vdash \bigvee_i \fa x_i,y_i \fb$.

* Assume that closed intervals in the set of Dedekind reals are
(Heine–Borel) compact. Then redo part (d), but without the assumption on the
existence of a Lebesgue number.

* Under the same assumption as in part (e), show that the localic real line
is spatial.

Note. Exercise <ref> lists settings in
which the assumption in part (e) is not satisfied. The converse in part (f)
also holds. Incidentally, the spatiality of the localic real line is an example
for a statement which requires the full version of the Heine–Borel property,
not only Heine–Borel for countable covers as it is often studied in reverse
mathematics [76].

[The localic Galois group of a field extension]
Let $L|k$ be a field extension. The localic Galois group $\Gal(L|k)$
is the classifying locale of the theory of automorphisms $L \to L$ which
fix $k$, as described on page par:theory-automorphisms.

* Explain how to obtain a morphism $\Gal(L|k) \to \Gal(L|k)$ which on the
level of points should send an automorphism $\sigma$ to its inverse $\sigma^{-1}$.

* Explain how to obtain a morphism $\Gal(L|k) \times \Gal(L|k) \to \Gal(L|k)$ which on the
level of points should send a pair $\langle \sigma, \tau \rangle$ to $\sigma \circ \tau$.

* Assume from now on that $L$ is a geometric field in the sense that any
element is zero or invertible. Show that the axiom expressing injectivity can
be dropped without changing the set of provable sequents.

* Let $f \in k[X]$ be a monic polynomial such that $f(X) =
(X-x_1)\cdots(X-x_n)$ over $L$. Let $x$ be one of the zeros of $f$. Show that
the theory proves $\top \vdash \bigvee_{i=1}^n \sigma_{x,x_i}$.

* Now furthermore assume that $L$ is Galois over $k$ in the sense that
any element of $L$ is the zero of a monic polynomial $f \in k[X]$ which is
separable (that is, $(f,f') = (1) \subseteq k[X]$) and splits over $L$ into
linear factors. Show that the axioms expressing surjectivity can be dropped.

* Show that the topological space of points of $\Gal(L|k)$ is canonically
homeomorphic to the topological Galois group of $L|k$.

* Show that $\Gal(L|k)$ is spatial in classical mathematics.

[Coherent locales and coherent theories]

An open $U$ of a locale is compact if and only if, whenever $U
\preceq \bigvee_{i \in I} V_i$, there is a (Kuratowski-)finite subset $I'
\subseteq I$ such that $U \preceq \bigvee_{i \in I'} V_i$. A locale is
coherent iff its compact opens are closed under finite meets and if
every open is a join of compact opens. A geometric formula is coherent iff only
finite disjunctions occur in it. A geometric theory is coherent
iff all of its axioms consist of coherent formulas.

* Show that any coherent locale classifies some coherent theory.

* Let $\TT$ be a propositional coherent theory. Show that $L(\TT)$ is

Hint. Proceed similarly as in the proof of
Theorem <ref>. For coherent formulas $\alpha$ and geometric
formulas $\varphi$, define a semantics by the clauses below. Show by an induction on the
structure of geometric derivations that, if $\TT$ proves a geometric
sequent $\varphi \vdash \psi$, then for all coherent formulas $\alpha$ such
that $\alpha \models \varphi$, $\alpha \models \psi$. Show for coherent
formulas $\alpha,\beta$ that $\alpha \models \beta$ iff $\TT$ proves $\alpha
\vdash \beta$. Use these ingredients to show that, if $\alpha$ is a coherent
formula and $(\beta_i)_{i \in I}$ is a family of coherent formulas, if $\TT$
proves $\alpha \vdash \bigvee_{i \in I} \beta_i$ then there is a
(Kuratowski-)finite subset $I' \subseteq I$ such that $\TT$ proves $\alpha
\vdash \bigvee_{i \in I'} \beta_i$.

$\alpha \models \beta$    iff    $\TT$ proves $\alpha \vdash \beta$     (for $\beta$ a nullary relation symbol)

$\alpha \models \top$    iff    true

$\alpha \models \varphi \wedge \psi$    iff    $\alpha \models \varphi$ and $\alpha \models \psi$

$\alpha \models \bigvee_i \varphi_i$    iff    there are coherent
formulas $\alpha_1,\ldots,\alpha_n$ such that
$\TT$ proves $\alpha \dashv\vdash
\alpha_1 \vee \cdots \vee \alpha_n$ and such for each $k \in \{1,\ldots,n\}$,

there is an index $i \in I$ such that $\alpha_k \models \varphi_i$

* Show that an arbitrary (set-indexed) product of coherent locales is

* Deligne's completeness theorem states that coherent locales (and
even coherent toposes) are spatial. Show that Deligne's
result implies that propositional coherent theories
without any set-based models are inconsistent. (This is usually phrased as
“consistent theories have models”.)

[Subsheaves of the terminal sheaf]

Let $X$ be a locale.

* Show that any subsheaf $F \subseteq 1$ of the terminal sheaf on $X$ gives rise
to an open of $X$ by gluing all its sections.

* Show that the construction of part (a) yields a canonical bijection of
the subsheaves of $1$ and the opens of $X$.

[A geometric interpretation of double negation]

Let $\varphi$ be a formula over an open $U$ of a locale $X$.

* Show that there is a largest open,
denoted “$\llbracket\varphi\rrbracket$”, such that $U \models \varphi$.

Hint. Consider the join of all opens $V$ such that $V
\models \varphi$.

* Show that $X \models \neg\neg\varphi$ iff $\llbracket\varphi\rrbracket$
is dense in the sense of Exercise <ref>.

* Give a condition on a locale or a topological space such that its sheaf
semantics validates the law of excluded middle (or equivalently the law of
double negation elimination).

[Unique local existence is global existence]

Let $F$ be a sheaf on a locale $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 \in \OOO(X)$, there is a unique section $s \in F(U)$
such that $U \models \varphi(s)$.

[The sheaf of real functions as a field]
Let $X$ be a topological space. Let $\CCC$ be the sheaf of continuous real-valued
functions on $X$.

* Let $U$ be an open of $X$. Let $f \in \CCC(U)$. Show using the result
of Exercise <ref> that $U \models (\exists g\?\CCC\+ fg =_\CCC
1)$ iff there is a function $g \in \CCC(U)$ such that $fg = 1$.

* Show that $\CCC$ is a field in that
$X \models \forall f\?\CCC\+
\bigl(\neg(\exists g\?\CCC\+ fg = 1)\bigr) \Rightarrow f = 0$.

* 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$.

* Let $X = \CC$ and let $\OOO$ be the sheaf of holomorphic functions on $X$.
Show that, in classical mathematics, the sheaf $\OOO$ is discrete in that
$\Sh(\CC) \models \forall f\?\OOO\+ \forall g\?\OOO\+ f = g \vee \neg(f = g)$.

[The failure of the fundamental theorem of algebra]

Let $F$ be the sheaf of continuous complex-valued functions on $\CC$. Give an
example of a function $f : \CC \to \CC$ such that it is not the case that

\[ \Sh(\CC) \models \exists z\?F\+ z^2 = f. \]

Note. The sheaf $F$ can be obtained by constructing, in the
universe of sheaves on $\CC$, the set of pairs of Dedekind reals. Hence the
example demonstrates that the usual formulation of the fundamental theorem of
algebra does not admit a constructive proof. (However, there are replacements
available [77], and the fundamental theorem does apply to the
Cauchy complex numbers [78] and under weak choice
principles [79]).

[The least number principle]

* A subset $M \subseteq X$ of a set $X$ is detachable iff for any
element $x \in X$, either $x \in M$ or $x \not\in M$. Show that any inhabited
detachable subset $M \subseteq \NN$ contains a minimal element.

* Show that for any inhabited set $M$ of natural numbers, it is the
case that there is a number $n \in M$ such that $n \leq m$ for all $m \in M$.

* Show that for every finitely generated vector space $V$ over a field in the
sense that nonunits are zero, it is the case that $V$ has a basis.

* Verify that the assumption that any inhabited set of natural numbers
contains a minimal element implies the law of excluded middle.

Hint. Consider a set of the form $\{ n \in \NN \,|\, n = 1
\vee \varphi \}$.

* Give an explicit example of a subsheaf $F$ of the constant
sheaf $\underline{\NN}$ on a topological space $X$ such that

\[ \Sh(X) \models \exists n\?F\+ \top
\quad\text{but}\quad
\Sh(X) \not\models \exists n\?F\+ \forall m\?F\+ n \leq m. \]

§ APPLICATIONS IN CONSTRUCTIVE ALGEBRA

We recall from the introduction one way how locales and sheaves yield new
reduction techniques for constructive algebra:

* Instead of replacing a given ring with another ring (for instance a ring $A$ with
one of its stalks $A_\ppp$ at a minimal prime ideal), we replace a given ring
with a sheaf of rings.

* We then maintain the convenient illusion that we are working with a plain old ring
instead of a sheaf by employing the sheaf semantics.

The goal of this section is to give a leisurely introduction to this procedure.
We recall in Section <ref> algebraic
preliminaries. Section <ref> explores the sheaf to use.
There is an interesting origin story to this sheaf, which we tell in
Section <ref>. For computations, it is vital to have an explicit
description of this sheaf available; such a description is presented in
Section <ref>. Finally, we illustrate how to use the technique in
a series of concrete examples in Section <ref>.

§.§ Algebraic preliminaries

By ring, we mean commutative ring with unit. We do not require the unit
to be distinct from the zero; indeed, trivial rings have intriguing
applications [13].

A ring is reduced iff zero is its only nilpotent element; that is, if $x^n = 0$
implies $x = 0$.

An ideal is a subset $\aaa \subseteq A$ such that $0 \in \aaa$, $(x \in
\ppp) \wedge (y \in \ppp) \Rightarrow (x + y \in \ppp)$ and $(x \in
\ppp) \Rightarrow (xy \in \ppp)$ (for any $y \in A$). A family $(x_i)_i$ of
ring elements generates an ideal, also denoted “$(x_i)_i$”, consisting of
(Kuratowski-finite) sums of multiples of the $x_i$.

An ideal $\ppp$ is prime iff $1 \not\in \ppp$ and $(xy
\in \ppp) \Rightarrow (x \in \ppp) \vee (y \in \ppp)$.
A minimal prime ideal is a prime ideal $\ppp$ such that for any prime
ideal $\qqq$ with $\qqq \subseteq \ppp$, $\qqq = \ppp$.

A subset $\fff \subseteq A$ is a prime filter iff
$0 \not\in \fff$, $(x + y \in \fff) \Rightarrow (x \in \fff) \vee (y \in
\fff)$, $1 \in \fff$ and $(xy \in \fff) \Leftrightarrow (x \in \fff) \wedge (y
\in \fff)$.

An ideal $\aaa \subseteq A$ is a radical ideal iff $x^n \in \aaa$
implies $x \in \aaa$ for any $x \in A$ and any natural number $n$. The
radical $\sqrt{\aaa}$ of an arbitrary ideal $\aaa$ is the radical
ideal $\{ x \in A \,|\, \exists n \in \NN\+ x^n \in \aaa \}$.

A ring is local iff a finite sum is invertible only if one of its
summands also is. More precisely, this means that $1 \neq 0$ and that
whenever $a + b$ is invertible, $a$ is invertible or $b$ is invertible.
This definition is an elementary rephrasing of the textbook definition
according to which a ring is local iff it has exactly one maximal ideal. The
elementary definition works better in constructive contexts.

If $S$ is a multiplicatively closed subset of a ring $A$, the
localization $A[S^{-1}]$ is the ring of formal fractions $\frac{a}{s}$ with $a
\in A$ and $s \in S$, where two such fractions $\frac{a}{s}$ and $\frac{b}{t}$ are deemed
equivalent iff there is an element $u \in S$ such that $uta = usb$. We do not
require that $0 \not\in S$; instead we plainly observe that $A[S^{-1}]$ is the
zero ring iff $0 \in S$. We also remark that $\frac{a}{s} = 0$ in $A[S^{-1}]$
iff $ua = 0$ for some element $u \in S$.

An important special case is localizing away from an element: If $f$ is
an element of $A$, then $A[f^{-1}]$ is $A[\{1,f,f^2,f^3,\ldots\}^{-1}]$. This
ring is the zero ring iff $f$ is nilpotent.

The stalk at a prime ideal $\ppp \subseteq A$ is the
localization $A_\ppp \defeq A[(A \setminus \ppp)^{-1}]$. Assuming de Morgan's
laws, such stalks are local rings. The stalk at a prime filter $\fff \subseteq A$ is
defined as $A_\fff \defeq A[\fff^{-1}]$ and is a local ring even
constructively. Conversely, if a localization $A[S^{-1}]$ is local then $S$ can
be saturated to a prime filter.

A property of rings is localization-stable iff it is inherited by any
localization. For instance, if $A$ is a reduced ring, then so is any
localization $A[S^{-1}]$.

§.§ A remarkable sheaf

Let $A$ be a ring. Then there is a certain locale $X$ on which a
certain “mirror image” of $A$ exists, a sheaf $A^\sim$ of rings. On the one hand,
this mirror image is “close to $A$”, such that studying $A^\sim$ pays off for
learning about $A$. On the other hand, it has much better properties than $A$

$A^\sim$ is close to $A$:

There is a canonical isomorphism $A \to A^\sim(X)$ of rings.

$A^\sim$ inherits any property of $A$ which is

A geometric sequent holds for $A^\sim$ iff$^{\star\!\star}$ it holds for all
stalks $A_\fff$.

$^\star$precise formulation in
Proposition <ref>

$^{\star\!\star}$assuming for the “if” direction

$A^\sim$ has better properties than $A$:

*  $A^\sim$ is a local ring.

Assuming that $A$ is reduced:

*  $A^\sim$ is a field: $\forall x\?A^\sim\+ \Bigl((\neg(\exists y\?A^\sim\+ xy = 1)) \Rightarrow x = 0\bigr)$.

*  $A^\sim$ has $\neg\neg$-stable equality:
$\forall x,y\?A^\sim\+ \neg\neg(x = y) \Rightarrow x = y$.

*  $A^\sim$ is anonymously Noetherian.

Recall that when we ascribe some ring-theoretic property to $A^\sim$, we
are implicitly using the sheaf semantics. For instance, when we say
that $A^\sim$ is a local ring, we actually mean

\begin{multline*}
\Sh(X) \models \neg(1 =_{A^\sim} 0) \quad\text{and} \\
\Sh(X) \models \forall x,y\?A^\sim\+ \bigl((\exists z\?A^\sim\+ (x + y)z
=_{A^\sim} 1) \Longrightarrow \\
z\?A^\sim\+ xz =_{A^\sim} 1) \vee (\exists z\?A^\sim\+ yz =_{A^\sim} 1)\bigr).
\end{multline*}

The locale $X$ on which this theater plays out is none other than the
spectrum of $A$ from algebraic geometry, and the sheaf $A^\sim$ is the
sheaf of regular functions, also denoted “$\OOO_{\Spec(A)}$”. We will give details on its construction in
Section <ref>, but first want to reflect on the displayed

A reification of all stalks.
Statement (<ref>) explains that, to a first approximation, the
sheaf $A^\sim$ is a reification of all the stalks of $A$ into a single coherent
entity: The sheaf $A^\sim$ has exactly those properties which are shared by all
the stalks $A_\fff$. For instance, the sheaf $A^\sim$ is an integral domain iff
all the stalks are.

But crucially, this metatheorem only pertains to properties which can be
formulated as geometric sequents. Being an integral domain is such a property
($1 = 0 \vdash \bot$, $xy = 0 \seq{x:R,y:R} x = 0 \vee y = 0$), but many others
are not. The reductive power of harnessing $A^\sim$ stems from the fact
that $A^\sim$ enjoys properties which are not shared by $A$, by its stalks or
indeed by any of its localizations or quotients.

Back and forth.
Statement (<ref>) is a kind of conservativity result.
For instance, if we
want to show that a certain ring element $x \in A$ is zero, we can just as well
show that its mirror image in $A^\sim$ is zero.

For this step to be useful, we need to know what $A^\sim$ looks like.
Statements (<ref>) and (<ref>) both allow us to
transfer our knowledge about $A$ to $A^\sim$; while
statement (<ref>) requires a syntactic restriction on the property
under consideration, statement (<ref>) requires a semantic one.

Not only does the ring $A$ have a mirror image as a sheaf, also
any $A$-module $M$ does. Its mirror image is the quasicoherent
sheaf $M^\sim$ from algebraic geometry. As with $A$ and $A^\sim$, there is a
close connection between $M$ and $M^\sim$; for instance, the module $M$ is
finitely generated over $A$ iff $M^\sim$ is finitely generated over $A^\sim$
(Exercise <ref>).

The field property.
The fact that $A^\sim$ is a field is where $A^\sim$ derives its main usefulness as a reduction technique
from. While statements (<ref>), (<ref>) and
(<ref>) are immediate consequences of the way $A^\sim$ is
constructed (Proposition <ref>), the field property (<ref>)
requires an actual computation for its verification and was a surprising
discovery by Christopher Mulvey in the 1970s.

Myles Tierney commented around that time that the field property “is surely important,
though its precise significance is still somewhat obscure—as is the case with
many such nongeometric formulas” <cit.>. Even though
the property has been known for a long time, only recently was it put in a
wider context (recognizing it as a small shadow of algebraic geometry's
quasicoherence) and its usefulness for constructive algebra
appreciated <cit.>.

The field property is a unique feature of $A^\sim$; it cannot be mimicked by
classical techniques in commutative algebra. Several constructions come close,
but fail in other ways:

* The stalks $A_\mmm$ at maximal ideals: These are not fields.

* The stalks $A_\ppp$ at minimal prime ideals: These are fields, but a ring
element $x \in A$ which is zero in all these stalks $A_\ppp$ is not necessarily
zero in $A$. Also, properties of the stalks tend to only spread to
dense opens of the spectrum, if they do so at all, while properties of $A^\sim$
are in close connection with properties of $A$. For instance, that all
stalks $M_\ppp$ of an $A$-module $M$ at minimal (or, for that matter, all) prime ideals are finitely
generated does not imply that $M$ is finitely generated, while finite
generation of $M^\sim$ does imply finite generation of $M$.

* The quotients $A/\mmm$: These are fields, but an element $x \in A$ which is
zero in all these quotients $A/\mmm$ is not necessarily zero in $A$, and
passing to $A/\mmm$ is not exact (does not preserve injectivity of linear

* The quotients $A/\ppp$ modulo the prime ideals: These are merely integral

The field condition displayed in statement (<ref>) is not the only
field condition used in constructive algebra. Perhaps the most important such
condition is that any element is zero or invertible, not least because this
condition can be expressed as a geometric formula. It is stronger than the
condition that nonunits are zero and is satisfied by $A^\sim$ iff $A$ is reduced
and of Krull dimension $\leq 0$ <cit.>.

Double negation stability.
Generally in constructive mathematics,
two elements being equal does not imply that they are actually equal:

* Sheaves give counterexamples: The interpretation of the statement that
two given sections of a sheaf are equal with the sheaf semantics is
that they agree on a dense open (Exercise <ref>). This
does not generally imply that they agree on all of their domain.

* Realizability gives counterexamples: Realizers of negated statements are
always uninformative; in the case that a statement $\varphi$ has a realizer at
all, the statement $\neg\neg\varphi$ is realized by any number whatsoever.
Only in certain cases, where a realizer can be algorithmically reconstructed
from the mere promise that a realizer exists, is $\neg\neg\varphi \Rightarrow
\varphi$ realizable.

Hence statement (<ref>) comes at a surprise. It is useful to
import some of classical logic into the constructive setting of sheaves
on $\Spec(A)$. For instance, the law of excluded middle is constructively valid
in the form

\[ \neg\neg(\varphi \vee \neg\varphi). \]

Combined with the observation

\[ \bigl(\neg\neg\chi \wedge (\chi \Rightarrow \neg\neg\psi)\bigr) \Longrightarrow \neg\neg\psi \]

we can hence freely use the law of excluded middle in constructive arguments –
but at the price that the conclusion $\neg\neg\psi$ is doubly negated, which is
why typically this observation is not of much use.

However, double negation stability of equality does allow us to conclude $\psi$
from the a priori much weaker premiss $\neg\neg\psi$, if $\psi$ is of the
form $(s =_{A^\sim} t)$.

This stability is a consequence of the field property. In case that the
ring $A$ is not reduced and hence $A^\sim$ is not a field, a substitute is given
in Exercise <ref>. We stress that the proof of
statement (<ref>) does not require double negation stability
of $A$ on the metalevel; in fact, it is fully constructive.

If $A$ is reduced, then the sheaf of rings $A^\sim$ has $\neg\neg$-stable equality:

\[ \Spec(A) \models \forall x,y\?A^\sim\+ \neg\neg(x = y) \Rightarrow x = y. \]

We argue internally in the universe of sheaves, using the sheaf
semantics. Let $x,y \? A^\sim$ be given such
that $\neg\neg(x = y)$. We will verify that $x - y$ is not invertible; by the
field condition, this will imply $x - y = 0$, hence $x = y$.

So assume that $x - y$ is invertible. Then $\neg(x - y = 0)$, since if $x - y =
0$, then $1 = (x-y) (x-y)^{-1} = 0$ in contradiction to $1 \neq 0$. Hence we have a
contradiction to the assumption $\neg\neg(x-y=0)$.

The Noetherian property.

Noetherian conditions are notoriously tricky in constructive algebra, not
least because of their overuse in classical commutative algebra which render
attempts to extract constructive content more challenging.

There are several proposals for constructively sensible definition of
Noetherian rings in the literature on constructive algebra, each with unique
advantages and
disadvantages [81, 26, 82, 83, 84, 85].
Insightful comments on why this is so can be found in the introduction and more
specifically on page 27 of the textbook by Henri Lombardi and Claude
Quitté [14]. To this list of conditions,
we add the following.

A ring is anonymously Noetherian if and only if any of its ideals is
finitely generated.

The assumption that any ideal of $\ZZ$ is finitely generated implies
the law of excluded middle. But we can prove, constructively, that $\ZZ$ is
anonymously Noetherian: Let $\aaa$ be an ideal of $\ZZ$ and assume that $\aaa$
is not finitely generated. Then $1 \not\in \aaa$, as else $\aaa = (1)$ would be
finitely generated. Also $2 \not\in \aaa$, as else (noting
that $1\not\in\aaa$), $\aaa = (2)$. Continuing in this manner, we may
conclude $n \not\in \aaa$ for every number $n \geq 1$. Hence $\aaa = (0)$. But
this is a contradiction to the assumption that $\aaa$ is not finitely

Definition <ref> is at odds with the idea that constructive mathematics should
be informative: It only expresses that it is impossible for no finite
generating family to exist without requiring that such a family should be given
– it may remain anonymous.[We borrowed the term “anonymous”
from type theory, where it is used with a similar meaning (see for instance
Ref. kraus-escardo-coquand-altenkirch:anonymous). However, there is a
subtle difference: The conjunction of “there is at most one element $x$” and
“there is anonymously an element $x$ in the sense of type theory” implies
that there actually exists an element $x$. In contrast, existence does
not.] And while Hilbert's basis theorem, stating that if a ring $B$ is
Noetherian then so is the polynomial ring $B[X]$, does have a constructive
proof for the anonymous version of the Noetherian condition,[For
instance, a careful reading of the textbook proof given
in <cit.> shows that the
basis theorem holds intuitionistically as stated.] this result seems empty: For
it just transforms one unconcrete promise (generators of each ideal of $B$
exist somewhere, platonically) into another (generators for ideals of $B[X]$
exist somewhere, platonically).

Curiously, the anonymous version of the Noetherian condition is still useful in
constructive algebra when interpreted by the sheaf semantics: This is firstly
because it just so happens that $A^\sim$ is anonymously Noetherian if $A$ is reduced,
and secondly because the interpretation of double negation with the sheaf
semantics does have nontrivial content (as evidenced by
statement (<ref>)). The Noetherian condition is also a
unique feature of the sheaf model, not shared by the ring $A$ or its stalks.

If $A$ is reduced, then the sheaf of rings $A^\sim$ is anonymously

We argue internally, under the sheaf semantics. Let $\aaa \subseteq A^\sim$ be an ideal.
Assume that $\aaa$ is not finitely generated. We will verify that then $\aaa =
(0)$, hence that $\aaa$ is finitely generated; contradiction.

Let $x \in \aaa$. If $x$ is invertible, then $\aaa = (1)$ is finitely
generated. Hence $x$ is not invertible. Thus $x = 0$ because $A^\sim$ is a

The condition for a ring to be (anonymously) Noetherian is a
higher-order condition and hence out of scope of the first-order version of the
sheaf semantics presented in Section <ref>. However, the
general version of the sheaf semantics is sound with respect to intuitionistic
higher-order logic, hence the proof of Proposition <ref> is

§.§ An algebraic origin story

The purpose of this section is to properly motivate the construction
leading to $A^\sim$. Briefly, the story is as follows, with details given

* Given a ring $A$, we set out to construct the free local ring
over $A$.

* In the strict sense of the word, this endeavor will fail, but in a wider
sense the quest will succeed and yield the sheaf $A^\sim$.

* It is then a surprising observation that $A^\sim$ is a field, even though
we only set out to construct a local ring.

* The field property of $A^\sim$ should be appropriately appreciated: While
there is a general machinery for free constructions of this generalized kind, this
machinery is not applicable for constructing free fields.

Free constructions.
Let $G$ be a group. Then there is a universal way of turning $G$ into an abelian
group $G^\ab$ equipped with a group homomorphism $G \to G^\ab$, the free
abelian group over $G$. This abelianization has the universal property that
for any homomorphism $G \to M$ into an abelian group, there is exactly one