Life in Johnstone's Topological Topos 3 -- Bonus Axioms
03 Jul 2024 - Tags: life-in-the-topological-topos , topos-theory
In the first post of the series, we talked about what the topological
topos is, and how we can think about its objects (and, importantly,
how we can relate computations in the topos
In that post we alluded to the presence of ~bonus axioms~ that allow us
to reason in
In this post we’ll spend some time talking about these bonus axioms, and proving that they’re true (since a lot of these facts are basically folklore).
Let’s get to it!
First, let’s take a second to recall the definition of the grothendieck
topology
For the site with two objects,
, every (nonempty) family of arrows is covering. So the interesting question is what a covering family of looks like. If
is an infinite subset of , we write for the unique monotone map whose image is . A family
is covering if and only if both
- It contains every constant map
- For every infinite
, there is a further infinite subset with in the family In particular, if a family contains every constant map
and a “tail of an infinite sequence” for some , then that family is covering. So, roughly, to prove that something “merely exists” in
, we have to provide a witness for every finite , and these witnesses should converge to the witness for .
If we want to use the site with one object
, the condition is almost exactly the same. A family of maps is covering if and only if both
- every constant map
is in the family - For each infinite
, there’s a further infinite so that is in the family. This, unsurprisingly, doesn’t make too much difference.
Dependent Choice
To start,
Say you have a relation
Then DC says for each
This is intuitively obvious. After all, we start with
Thus, DC basically tells us that recursive definitions work, even if we
don’t have a canonical way to choose one of many options at each
recursive stage. Indeed, most recursive definitions work by first choosing
an
For those who like type theory,
DC says that for every binary relation
or, cashing out these
Here’s an idiomatic example of dependent choice in action: The Baire Category Theorem for complete metric spaces.
Let
Then the countable intersection
The usual proof (say, from Karagila’s notes) doesn’t use LEM, so it goes through unchanged. We’ll present it here paying special attention to the use of DC.
Since
- the (strongly closed) ball
is contained in
By dependent choice (and strong density of each
- the (strongly closed) ball
is contained in .
By construction, then, the
Can you build a relation
This will let you see precisely how dependent choice is used above.
Dependent Choice implies Countable Choice, which itself implies
Weak Countable Choice. But WCC4 implies that the
dedekind reals and the cauchy reals agree. And indeed one
can show directly that in
Brouwer’s Principle
The next ~bonus axiom~ we’ll talk about is
Brouwer’s Continuity Principle that
“Every function
Precisely5:
In fact, this is true for any (external) metric spaces
Note that it’s crucial here that we use the truncated
Regardless, it’s shockingly hard to find this continuity principle written down anywhere, but it’s cited in lots of places! It’s definitely part of the folklore, and I’m happy to share a full proof! It’s a bit long, though, so I’m leaving it as an “appendix” at the bottom of this post. If you know of a reference, or of a slicker proof than the one I found, I would REALLY love to hear about it6!
Regardless, the truth of Brouwer’s principle tells us that
In
Omniscience Principles
We can ask about other nonconstructive principles too. For instance, Bishop’s Principles of Omniscience!
First, let’s look at the Limited Principle of Omniscience (LPO):
The Limited Principle of Omniscience:
says that every sequence of bits is either
In the presence of countable choice (which we have in
and is further equivalent to the type-theoretic condition that the obvious embedding
is an isomorphism.
It’s clear from the last condition that LPO is false in
That said, it can be hard to find example computations of people statements internal to a topos to statements in the real world, so just for fun let’s prove this again in a more complicated way:
Here
Let’s take
Now what would it mean to have
Now restricting
Is it possible that
Is it possible for
So we see that LPO externalizes to a false claim, and thus is not validated
by
As an easy exercise, can you use LPO to build a function
In fact, we don’t even need Bouwer’s principle to contradict! By yoneda,
Next, let’s look at the Lesser Limited Principle of Omniscience (LLPO):
The Lesser Limited Principle of Omniscience says that
This is equivalent to a kind of de Morgan’s law
and, as before, under countable choice this is equivalent to the analytic LLPO,
This turns out to be true7! Just to show more ways to reason about the
internal logic of topoi, we’ll prove this one by working with the category
Now showing
But by the universal property of the pushout, we get a map
Moreover, since both
As a nice exercise, check that internal to
and use this fact to give a purely type theoretic proof of that LLPO
holds in
As another nice (but quite tricky!) exercise, try externalizing the statement of LLPO and proving it “directly” by seeing that it externalizes to something true!
Next on this list is Markov’s Principle (MP):
Markov’s Principle says that
Again this is equivalent (under CC) to an analytic version9
Here
MP is true in
so we fix a convergent sequence
then we must have
To show this existential claim, we need to provide a conergent sequence
Now WLPO is easy:
The Weak Limited Principle of Omniscience says that
This is equivalent to a kind of excluded middle, and as expected there’s an analytic version (equivalent in the presence of CC):
Now, it’s easy to see that MP + WLPO
If
So
As an aside, in all of these statements we’re using the “truncated”
It’s a theorem of Martín Escardó that
- truncated and untruncated LPO are equivalent
- truncated and untruncated WLPO are equivalent, and are equivalent to untruncated LLPO
- truncated LLPO is weaker than untruncated LLPO
In fact, in his agda files, Martín wonders if there’s a place in the literature where untruncated LLPO and WLPO are shown to be inequivalent.
He mentions that
Bar and Fan Theorems
The Bar and Fan theorems are closely related to the nice properties of baire space and cantor space (respectively) as spaces rather than as locales. The locales are always well behaved, but in some topoi these locales fail to have enough points, so that the baire space and cantor space as sets of points may be lacking.
Since we showed in part 1 that spatial sequential regular locales always have
enough points in
This is also the best we can do. Since the Full Bar Theorem is known to
imply LPO, and
As a not-so-hard exercise, verify the decidable fan theorem by hand! That is, prove
Or, entirely in symbols, prove
Note that
As a ~bonus exercise~, use what you know about
discrete topological spaces and subobjects in
discussion of the ~bonus exercise~
The idea here is that a general subobject of a sequential space X is a subset of the points of X equipped with some topology making the inclusion continuous. A decidable subobject is a clopen subset of the points ofDe Morgan and LEM
Obviously LEM fails, since
It turns out that
being an isomorphism being injective
But we can show both of these are false
(thus giving two proofs that
For
For
This was a long one! Multiple months in the making, and easily the most research I’ve ever done for a blog post (both in terms of reading done and original proofs). It was super rewarding, though, and I feel way better about the topological topos and its internal logic, as well as about topos theory more broadly ^_^.
Hopefully I was able to explain it clearly enough to be useful to all of you too! I know it’s a TON of information, and in the process of revising this I really struggled to tell if it’s well exposited or not since it kind of feels like this
But even though it’s a ton of information, hopefully each section is digestible!
Thanks again for reading all. I have other posts planned, about my thesis work for a change, but I think I’m going to take a break from writing after this, haha.
Stay safe, and talk soon! 💖
Appendix: A Proof that Johnstone’s Topos Models Brouwer’s Continuity Principle
If you’re not super familiar with externalizing formulas, you might want to read my old blog post with a bunch of simpler examples before trying to tackle this one!
We’ll be doing this computation using the site with one object
We’ll prove a kind of “theorem schema”. Every metric space is sequential,
so for any metric spaces
Precisely:
Cashing out the universal quantifiers, we want to show that
for any continuous functions
To witness the existential quantifier, we need to find a cover
of
Finding a cover basically amounts to finding a cofinite subset of
Then, let
- For all
, we have
In condition (3) we’ve used the fact that
Now we take as our covering familiy
- the constant functions
for any infinite subset .
As a reminder, the function
Now on each member
Cashing out the last universal quantifier, we need to know that for all
If
So let’s build such a
First, if
If
Of course, this is easy to arrange by taking
Second, if
Then we define
If
But since
so that we can compute
As desired.
-
You might wonder why we need a “nonconstructive” axiom to do this. Why can’t we use induction on
?After all, we can prove (constructively, in type theory) that
(and this makes a nice exercise!)
The difference lies in
vs ! To build a term of type is to build a function that eats an and returns a alongside a proof that . This gives us a canonical choice in – just use the one this function gave us!Dependent choice works with something much weaker. It says we can build such a function even when there merely exists such a
, without being handed a witness! (Of course, the function we’re given only merely exists too)Think about the semantics in
for a moment. Here, to say that is to say that there’s an open cover of and a local witness on each element of the cover. But it’s entirely possible for these witnesses to not glue into a global witness! ↩ -
I don’t know if there are constructive subtleties with the notion of cauchy completeness which might be relevant here, and since I really want to get this blog post out I don’t want to read a bunch of literature on constructive metric spaces to try and figure it out…
If anyone happens to know some facts about constructive metric spaces, though, I would love to hear about them! But for now, treat this example as being more to showcase how dependent choie works than to say anything profound about the topological topos. ↩
-
A set
is called Strongly Dense if for any inhabited open set we know that is inhabited. ↩ -
Thanks to Madeleine Birchfield for pointing out that I originally linked the wrong “Weak Countable Choice” here. I didn’t realize that there are two things, both called “weak countable choice”, and both implied by either CC or LEM! The one that proves the dedekind and cauchy reals agree is unambiguously called
. At time of writing it’s listed as “another weak countable choice” on nlab, and it means that every -indexed sequence of inhabited subsets of has a choice function. ↩ -
This is the first time in a while I’ve actually written down the definition of (metric space) continuity in full! No wonder students struggle with this, haha. I’ve forgotten what a mouthful it is! ↩
-
Here we have to refer to external metric spaces, and we prove a kind of “theorem schema”. I suspect something like this is true purely internally, if we can find the right definition of a “metric space” in
. Obviously we want a distance function satsifying the usual axioms. But we also need to know that the topology puts in agrees with the intrinsic topology on !Since
is externally continuous we know that metric-open balls will always be open in , so I think the condition is something like “every open of contains an open ball” or maybe “every open of is the union of the open balls inside it”.This should be expressible in the internal logic since the opens of
are exactly the inhabitants of where is the sierpinski space.I know that Davorin Lešnik has thought about this, but I really want to get this post out (and ideally turn it into a paper) so unfortunately I won’t be pursuing this any further… for now! ↩
-
This realization has probably been made by many people, but it was added to the nlab by Mike Shulman. ↩
-
This is the quotient type in the sense of Li’s PhD thesis, not the (higher!) quotient type in the sense of HoTT… Though the quotient type I mean is almost certainly the
-truncation of the higher inductive quotient type.I’ve been meaning to spend some time thinking about how you can prove theorems about a 1-topos by working in HoTT and truncating everything at the end, but I haven’t had the time. ↩
-
Actually, I think I remember reading somewhere that the analytic omniscience principles are always statements about the cauchy reals. The reason countable choice makes them properties of the dedekind reals is because under CC the dedekind and cauchy reals agree.
If an expert sees this and happens to know offhand if that’s true, I would love to know for sure!
Edit (July 10, 2024): Thanks again to Madeleine Birchfield for clarifying on zulip that the omniscience principles for
are probably equivalent to the analytic omniscience principles for the cauchy reals. I would still love a proper reference if someone has one, but at least there’s now a mathoverflow question with a proof in the LPO case. ↩