The powerset construction was the force behind set theory as
Ernst Zermelo formulated it in 1908,
but higher order logic became the poor relation of foundational studies
owing to the emphasis on the completeness theorem in model theory.
In this paper the powerset plays the leading role,
and we derive the first order connectives from it in a novel way.
The collection of *all* subsets is also treated in the same way
as the collections of *open* and *recursively enumerable*
subsets in topology and recursion theory.
The underlying formulation in which we do this
is a category with a “truth values” object Σ
for which the adjunction Σ^{(−)}⊣Σ^{(−)} is monadic.
Robert Paré proved in 1974 that any elementary topos has this property,
whilst the category ** LKLoc** of locally compact locales has it too
(§O 5.10 and Theorem B 3.11

Gerhard Gentzen’s natural deduction was
the first *principled* treatment of the logical connectives,
and Per Martin-Löf used the Curry–Howard isomorphism
to extend it in a principled way to type constructors
[ML84].
However, the *natural* conclusion of such an approach
is to say that the existential quantifier is *the same*
as the dependent sum, *i.e*. that a proof of ∃ *x*.φ(*x*)
must always provide a *witness*:
a particular *a* for which φ(*a*) holds.

This conflicts with geometrical usage,
in which we may say that
the Möbius band has two edges, or a complex number two square roots,
*locally* but not globally,
*i.e*. *there exists* an isomorphism between
**2**≡**1**+**1** and the set of edges or roots
*on some open subspace* [Tay99, §2.4].
Similarly, interprovable propositions are, for Martin-Löf’s followers,
*isomorphic* types, not equal ones,
and their account of the powerset is a *bureaucratic* one:
a structure within which to record the histories of formation and proof
of the proposition–types [*op. cit*., §9.5].

The way in which category theory defines the powerset is not, perhaps,
based so firmly on a logical creed as is Martin-Löf type theory,
in that it describes *provability* rather than *proof*,
but it was at least designed for the intuitions of geometry and symmetry.
This notion — the subobject classifier in an elementary topos,
which is readily generalised to the classifier Σ for open subsets
(the Sierpiński space) and recursively enumerable ones —
then obeys the curious equation

σ∧ F(σ)⇔ σ∧ F(⊤)
for all σ∈Σ and F:Σ→Σ, |

which we call the ** Euclidean principle**.
The Frobenius law, which is part of the categorical formulation
of the (geometrical) existential quantifier and was so called by Bill Lawvere,
is an automatic corollary of the Euclidean principle.
From this we develop the connectives of first order categorical logic,
in particular stable effective quotients of equivalence relations.

Whilst set theory and topology have common historical roots
[Hau14],
the motivation for a common treatment of the kind that we envisage
is Marshall Stone’s dictum that we should “always topologize” mathematical objects,
even though they may have been introduced entirely in terms of discrete ideas
[Joh82, Introduction].
For example, the automorphisms of the algebraic closure of ℚ form,
not an *infinite discrete* (Galois) group,
but a *compact topological* group.
Similarly, the powerset of even a discrete set is not itself a discrete set,
but a *non-Hausdorff* topological lattice.
(Steven Vickers has taken the same motivation in a different direction
[Vic98].)

The types in our logic are therefore to be *spaces*.
The topological structure is an indissoluble part of what it is to be
a space: it is not a set of points *together with* a topology,
any more than chipboard (which is made of sawdust and glue) is wood.

When we bring (not necessarily Martin-Löf) type theory
together with categorical logic [Tay99],
logical notions such as the ** quantifiers** acquire meanings
in categories other than

It is well known that the recursively enumerable subsets
of ℕ *almost* form a topology,
since we may form finite intersections and *certain* infinitary unions
of “open” subsets.
However, the unification of topology with recursion theory,
*i.e*. making precise Dana Scott’s thesis that
*continuity* approximates the notion of *computability*,
involves a revolutionary change,
because the classical axiomatisation of
(the frame of open subsets of) a topological space
demands that we may form *arbitrary* unions.

The usual procedure for turning a *base*
(something, like this “topology” on ℕ,
that partially satisfies the axioms for a topological space)
into a topology would make *every* subset of ℕ open,
losing all recursive information.
In particular,
in topology an open subspace is *glued* to its closed complement
by means of a comma square construction that is due to Michael Artin,
but this doesn’t work for recursively enumerable subsets and their
complements [D, Section 4].

Although they are in many respects more constructive, the modern re-axiomatisations of topology in terms of open subsets — the theory of frames or locales [Joh82] that came out of topos theory [Joh77], and Giovanni Sambin’s formal topology [Sam87] motivated by Martin-Löf type theory — have exactly the same fault as Bourbaki’s [Bou66].

The *finite* meets and joins in the theory of frames present no problem,
so what we need is a new way of handling the “purely infinitary”
directed joins.
Here we use an idea to which Scott’s name has become firmly attached
(though it goes back to the Rice–Shapiro and Myhill–Shepherdson theorems
of 1955), that directed joins define a topology.
However, we turn this idea on its head:
by treating frames, not as infinitary algebras over ** Set**,
but as finitary ones over

We do this by postulating that, for the category ** C** of spaces,
the adjunction

be *monadic*,
*i.e*. *C*^{op} is equivalent to the category of Eilenberg–Moore algebras
and homomorphisms over ** C**.
In practice, this is used in the form of Jon Beck’s theorem about

But this category does not have all equalisers, pullbacks and coequalisers.
The impact of this on logic is that
we must also reconsider the notions of ** equality** and inequality,
which we define by saying that
the diagonal subspace is respectively open or closed,

[It will emerge later in the ASD programme that we cannot, after all, do without equalisers and pullbacks, especially when we consider recursion in [E, Section 2].]

Computational considerations also urge such a point of view.
Two data structures *may* represent the same thing
in some ethereal mathematical sense,
for example in that they encode functions that produce the same result
for every possible input value.
However, as we are unable to *test* them against *every* input,
such an equality may be outside our mortal grasp.
A similar argument applies to *inequality* or *distinguishing*
between the two data structures, in particular real numbers.
Equality and inequality, therefore, are *additional structure*
that a space may or may not possess.

Now that equality is no longer to be taken for granted
as has traditionally been done in pure mathematics,
there are repercussions for category theory.
Specifically, Peter Freyd’s unification of products, kernels and
projective limits into the single notion of ** limit** in a category
[Fre66b]
breaks down, because the non-discrete types of diagram depend on equality.
This entails a root-and-branch revision of categorical logic,
which has traditionally relied very heavily on the universal availability
of pullbacks.
In fact, most of this work has already been done in categorical type theory
[Tay99, Chapters VIII and IX].

The duality between equality and inequality
(which also relates ** conjunction** to

This symmetry is a *constructive theorem* (for ** LKLoc**):
as a result of Scott continuity,
the Euclidean principle implies its lattice dual.
Together with monotonicity (the finitary part of Scott continuity),
the two Euclidean principles amount to the

Whilst Scott continuity is obviously an important motivating principle, the Phoa principle alone has been enough to develop quite a lot of general topology, keeping the open–closed symmetry a precise one so far.

In particular we have a *completely symmetrical* treatment
of ** open** and

The topics in general topology that we discuss in the body of the paper
converge on a treatment of overt discrete spaces
(classically, these are sets with the discrete topology),
showing that they form a ** pretopos**.
That is, they admit cartesian products, disjoint unions,
quotients of equivalence relations and relational algebra.
[Assuming Scott continuity, they also admit free monoids and
so form an arithmetic universe [E].]

The whole of the paper therefore concerns the logic of the category of sets,
even though much of it is written in topological language:
what we say about the *subcategory* of overt discrete spaces
is immediately applicable to the *whole* category
when this is ** Set** or an elementary topos.
In this sense,
we have a new account of some of the early work on elementary toposes,
in particular that they satisfy Jean Giraud’s axioms,

The distinction between topology and set theory turns out, therefore, to be measured by the strength of the quantifiers that they admit. The paper concludes with a new characterisation of elementary toposes that is based, like Paré’s theorem, on monadicity of the contravariant powerset, but which makes no reference whatever to subsets.

- 1
- The letters denote the other papers in the ASD programme.
- 2
- This is an aspirated
*p*, not an*f*. Wes Phoa told me that his name should be pronounced like the French word*poire*,*i.e. pwahr*, though maybe this is only helpful to the southern English and his fellow Australians as there is no final*r*.