You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (May 09 2022 at 20:58):This Thursday (12th of May) at 17:00 UTC
Andrej Bauer: The countable reals
Joint work with James E. Hanson from the University of Maryland, james-hanson.github.io.
In 1874 Georg Cantor published a theorem stating that every sequence of reals is avoided by some real, thereby showing that the reals are not countable. Cantor's proof uses classical logic. There are constructive proofs, although they all rely on the axiom of countable choice. Can the real numbers be shown uncountable without excluded middle and without the axiom of choice? An answer has not been found so far, although not for lack of trying.
We show that there is a topos in which the real numbers are countable, i.e., there is an epimorphism from the object of natural numbers to the object of Dedekind reals. Therefore, higher-order intuitionistic logic cannot show the reals to be uncountable.
The starting point of our construction is a sequence of reals, shown to exist by Joseph S. Miller from University of Wisconsin–Madison, with a strong counter-diagonalization property: if an oracle Turing machine computes a specific real number, when given any oracle representing Miller's sequence, then the number appears in the sequence. One gets the idea that the reals ought to be countable in a realizability topos built from Turing machines with oracles for Miller's sequence. However, we cannot just use ordinary realizability, because all realizability toposes validate countable choice and consequently the uncountability of the reals.
To obtain a topos with countable reals, we define a variant of realizability which we call parameterized realizability. First we define parameterized partial combinatory algebras (ppca), which are partial combinatory algebras whose evaluation depends on a parameter. We then define parameterized realizability toposes. In these realizers witness logical statements uniformly in the parameters. The motivating example is the parameterized realizability topos built from the ppca of oracle Turing machines parameterized by oracles for Miller's sequence. In this topos, Miller's sequence is the desired epimorphism from natural numbers to Dedekind reals.
Zoom: https://topos-institute.zoom.us/j/84392523736
YouTube: https://youtu.be/4CBFUojXoq4
Morgan Rogers (he/him) (May 10 2022 at 07:51):This is great, Ingo Blechschmidt mentioned to me last year that he had been searching for a topos where the reals are countable. Mind-bending stuff..!
David Michael Roberts (May 12 2022 at 22:07):Can anyone give a quick impression? I've yet to watch the recording
Jacques Carette (May 12 2022 at 22:18):Roughly: By using a family of oracles, given through a classical construction, you can show that you can't simultaneously diagonalize against all of them. But you can build a topos starting from those same oracles, using constructions from realizability, that ends up doing what you need.
The key is indeed those 'parameters' of the abstract: because you have to be uniform in the parameters, you end up not being able to diagonalize against all of them at once.
Mike Shulman (May 12 2022 at 22:22):This was a great talk; thanks Andrej!
But it confirmed my feeling that realizability is a wild and woolly wilderness, where people are still just making up entire new classes of toposes. When someone defines a new Grothendieck topos, I understand how they do it -- they write down a site. When someone defines a new realizability topos, I can understand if they do it by writing down a PCA. But it seems that often that's not enough, and people still keep inventing new PCA-like things that give realizability-like toposes, without a unifying framework.
Or should I view the tripos as analogous to a site? A tripos feels like such a "large" object, it's more than halfway to a topos already, rather than something "small" like a site or a PCA.
David Michael Roberts (May 12 2022 at 23:44):@Jacques Carette So it's a bit like constructing a non-cocomplete elementary topos like uniformly continuous actions of a topological group on sets? Things that would allow infinitary-ish stuff can't work due to lack of uniformity? From how you describe it, it feels somehow like a limit of realisability toposes, but I'll have to watch the talk and see (which I'm just off to do, now).
Jacques Carette (May 12 2022 at 23:46):I think we'll have to summon @Andrej Bauer to answer that.
Tom Hirschowitz (May 13 2022 at 08:29):@Mike Shulman There is at least a tentative unifying framework.
Matteo Capucci (he/him) (May 13 2022 at 10:18):Mike Shulman said:
Or should I view the tripos as analogous to a site? A tripos feels like such a "large" object, it's more than halfway to a topos already, rather than something "small" like a site or a PCA.
Yeah a tripos is definitely too broad of a notion to faithfully represent 'realizability'-like constructions. All topoi can be presented as tripos-to-topos constructions, since the doctrine of subobjects of any topos is a tripos.
Jon Sterling (May 13 2022 at 13:52):I would say that a tripos is conceptually very different from a site in at least one way. If you define a site over a topos , then the corresponding topos of sheaves is an -topos. But this is not what happens when you turn a tripos into a topos... The relationship gets flipped, as I suppose you can view as a topos over .
On the other hand, Frey and Streicher have argued that triposes are kind of like localic geometric morphisms, except where you do not require the existence of a direct image functor. https://arxiv.org/pdf/2005.06019.pdf. But the connection is not perfect...
Mike Shulman (May 13 2022 at 17:01):Matteo Capucci (he/him) said:
All topoi can be presented as tripos-to-topos constructions, since the doctrine of subobjects of any topos is a tripos.
I guess you mean any topos can be presented as a tripos-to-topos construction over some base topos, where you take the base topos to be the original topos itself. But if you're allowed to do that sort of tautologous construction, you can equally well say that all topoi can be presented as sheaves on a site over some base topos, namely sheaves on the trivial site internal to the original topos itself.
Mike Shulman (May 13 2022 at 17:04):@Tom Hirschowitz Does that framework include Andrej's parametrized realizability topos?
Nikolaj Kuntner (May 15 2022 at 18:49):The topos depends on the oracle and doesn't validate LEM and countable choice, so that diagonalization doesn't block the existence of the epimorphism.
Do weaker variants of countable choice still hold in that topos, such as countable choice principles that restrict the cardinalities of the sets the function picks its values from, or choice principles that have something to say about what kind of functions can still be granted to exist (e.g. in terms of the hierarchies)?
Without reference to what that topos actually validates, if somebody knows off the top of their heads, one may ask a related question: In the intuitionistic context, how strong of a countable choice principle is used to prove the classical result about the uncountability of Dedekind reals?
David Michael Roberts (May 15 2022 at 19:15):In the proof that Andrej showed, it was dependent choice, where the choice was taken from a two-element set each time. He then gave it as an exercise that only countable choice is needed
David Michael Roberts (May 15 2022 at 19:20):So very mild, indeed! And it's really a discrete two-element set, namely two specific closed subintervals of [0,1] with explicit rational endpoints.
Tom Hirschowitz (May 16 2022 at 07:03):Mike Shulman said:
Tom Hirschowitz Does that framework include Andrej's parametrized realizability topos?
Excellent question! :innocent:
Matteo Capucci (he/him) (May 16 2022 at 10:35):Mike Shulman said:
Matteo Capucci (he/him) said:
All topoi can be presented as tripos-to-topos constructions, since the doctrine of subobjects of any topos is a tripos.
I guess you mean any topos can be presented as a tripos-to-topos construction over some base topos, where you take the base topos to be the original topos itself. But if you're allowed to do that sort of tautologous construction, you can equally well say that all topoi can be presented as sheaves on a site over some base topos, namely sheaves on the trivial site internal to the original topos itself.
I meant every topos over Set can be presented as a tripos-to-topos construction. This is a fact I've learned from Pasquali.
Mike Shulman (May 16 2022 at 15:59):Matteo Capucci (he/him) said:
I meant every topos over Set can be presented as a tripos-to-topos construction. This is a fact I've learned from Pasquali.
Every topos over Set can be presented by a tripos-to-topos construction where Set is the base category of the tripos?? Whoa! What is the tripos for, say, a presheaf topos? Or take just the topos of actions of a group?
Matteo Capucci (he/him) (May 16 2022 at 19:27):I remember how to it for a localic topos : send a set to , with the obvious action on morphisms. You can find this construction in van Oosten's book on Categorical realizability. So I think this covers the case for the topos of actions of a group?
For the general case I don't remember the details.
Matteo Capucci (he/him) (May 16 2022 at 19:29):OTOH I think I misunderstood/misread your previous message, because I thought you were complaining about the base of the topos, whereas you're talking about the tripos. The general construction I had in mind (also what Pasquali exhibits) send a topos to a tripos over , so it is indeed quite tautological.
Mike Shulman (May 16 2022 at 20:29):The topos of actions of a group is not localic. I'm familiar with the construction for a localic topos. I don't think a non-localic Grothendieck topos can be presented using a tripos over Set.
Ross Tate (May 18 2022 at 03:05):Mike Shulman said:
Tom Hirschowitz Does that framework include Andrej's parametrized realizability topos?
Short answer: almost certainly and, more importantly, in a very straightforward answer.
Long answer: I couldn't find the precise definitions, so I'm inferring from what I got from the talk. But, given that evidenced frames are complete with respect to Set-based triposes (using the older/stronger definition of triposes where all fibred products satisfy Beck-Chevalley, not just simple fibred products), it's almost guaranteed that they cover parameterized realizability toposes. Nonetheless, I think ease of construction is what's more important.
It's already easy to construct an evidenced frame from a PCA. From what I inferred, a parameterized PCA is an indexed collection of PCAs that share the same carrier set and SKI combinators. This means the evidenced frames resulting from these PCAs share the same interpretation of top and conjunction and the same algebra of evidences; the only things that differ are their interpretation of universal implication and their evidence relations. Furthermore, the interpretations of propositions has an ordering (by set inclusion) with meets that respect the evidence relations, and the semantics of their evidence for introducing universal implication (i.e. creating lambdas) is independent of the parameter (because creating a lambda does not use the oracle - it's a "pure" operation). In such a scenario (call it, say, a parameterized evidenced frame), I was able to quickly prove in Coq today that the intersection of these evidence relations is a valid evidence relation for the obvious evidenced frame interpreting universal implication as the meet of the parameterized interpretations of universal implication. That intersected evidence relation is precisely the definition in the talk where a code is evidence of entailment only if it works for reduction with respect to all choices of oracle.
So the construction seems to be: Tripos-To-Topos(Evidenced-Frame-To-Tripos(Intersect-Parameterized-Evidenced-Frame(oracle => PCA-To-Evidenced-Frame(PCA-Using-Oracle(oracle)))))
(Obviously this has nothing to do with the real key insights of this cool talk, but it's nice to see that our broader framework could have offered more helpful flexibility and eliminated some boilerplate.)
Mike Shulman (May 18 2022 at 03:49):Hmm. I assume that "evidenced frames are complete with respect to Set-triposes" means that every Set-tripos arises from an evidence frame? If so, then are evidenced frames really any more of a unifying framework than triposes themselves?
Ross Tate (May 18 2022 at 13:14):That's a good question, and I think it boils down to what a "unifying framework" is and what a unifying framework's utility is. Let me try to boil things down with evidenced frames and triposes to tease that apart.
In this talk, the tripos is constructed by modeling predicates on X as functions from X to some set of propositions, and by modeling that predicate phi implies predicate psi as "there exists uniform evidences that, for every x, phi(x) entails psi(x)". That is, entailment on predicates is reduced to uniform pointwise entailment on propositions. This way, when an entailment holds, you can extract the evidence, i.e. realizer, of the entailment.
We developed evidenced frames to be a smallest structure that enables this "uniform families" tripos construction. We did this because in earlier work, like in this talk, we had a model that was clearly computational but which did not form a PCA (in our case it was because it used state, whereas in the talk it's because they use oracles). Like in this talk, this let us build a realizibility model that does not exhibit common properties of PCA-based realizability triposes; for example, we built a model in which weak countable choice fails to hold. We built (and are still building) a bunch of models, and it's way easier to build an evidenced frame than it is to (directly) build a tripos, so they were a huge time saver.
Originally that was all their purpose was, but we were surprised to realize that, because we had sufficiently abstracted what "evidence" was, every tripos could be represented as an evidenced frame. (Technically, we built a biadjoint biequivalence between relevant preordered categories.) In particular, given a tripos, one can define "evidence" to be an (external) relation between propositions for which "uniform" entailment holds internally (where the definition of "uniform" is more than I can go into here, but relies on fibred products satisfying Beck-Chevalley - "reflected axiom schema" is the relevant definition in the paper). Now, if one takes an evidenced frame and turns it into a tripos, the reflected axiom schemas of that tripos are precisely the relations between propositions for which there exists uniform evidence of entailment in the evidenced frame. But a key detail is that the evidence only exists, you can't functionally extract it. So the completeness is in a logical sense, but in a functional/constructive sense there's some lossiness in triposes. So, from our perspective, a tripos is an evidenced frame that has "forgotten" its evidence.
Okay, so why is this useful? For one, there's utility in simply eliminating the boilerplate, making it easier to build models by just defining things in propositions and automatically extending to predicates in a uniform manner. For another, there's utility in being broader, since we've seen that there are interesting realizability models that are not constructed directly from PCAs, i.e. are not "traditional" realizability triposes. And, as we've seen, you can combine evidenced frames in useful and interesting ways. But, besides building realizability models, it also gives us a framework for asking questions. For example, we can ask what properties do or do not hold for triposes/toposes derived from evidenced frames with Nat (or isomorphic to Nat) evidence. That subset of evidenced frames seems particularly relevant to models related to computation (and I'm sure not all triposes fall within that subset). And at the same time, it makes fairly minimal assumptions that do not impose particular interpretations of what computation is, and as such it accommodates computation with non-determinism, state, exceptions, continuations, and (as we see now) underdetermined oracles. So we can furthermore explore what the implications of giving the algebraic structure on evidence equational properties that further encode assumptions about computational behavior.
I'm not sure we can combine triposes in the same way we can combine evidenced frames (though the converse might be true to). And I'm pretty sure we can't ask the same questions about triposes that we can ask about evidenced frames (without going through evidenced frames). For example, the triposes derived from evidenced frames with Nat evidence versus those derived from just countable evidence both have a set of reflected axiom schemas that is only countable and not isomorphic to Nat, which suggests that its much harder to reason about what the computational behavior of these reflected axiom schemas might be than it would be in evidenced frames where you have direct access to the evidence. All this is why I suspect evidenced frames are a better unifying framework for realizability models, even if triposes can technically be made into an evidenced frame and a sort of realizability model. That said, it's all new, so we're only just beginning to explore these questions ourselves.
Tom Hirschowitz (May 18 2022 at 13:52):I vaguely remember from a talk by @Étienne Miquey and the ensuing discussion that the notion of morphism between evidenced frames seemed to be crafted to make the biequivalence work, and that an alternative notion would make the bifunctor from evidenced frames to triposes essentially surjective, but not faithful.
This has to do with evidenced frames being intuitively more proof-relevant than triposes.
Is this right, @Ross Tate ?
If so, adopting this alternative notion of morphism, is it reasonable to think of evidenced frames as some sort of presentations of triposes? (Indeed, the main role of presentations is to save boilerplate...)
Tom Hirschowitz (May 18 2022 at 14:20):An older tentative framework is Longley's computability structures.
Ross Tate (May 18 2022 at 14:56):Ah, yeah. That connects to that idea of "forgetting" evidence. Evidenced frames have an algebra, so you'd expect a morphism of evidenced frames to be a standard morphism of algebras. If we did that, we get a more proof-relevant notion of morphism, and we still get an adjunction. However, the unit on the evidenced-frame side is not invertible in this notion of morphism due to the lossy nature of triposes discussed above. So, we used a definition of morphism that just focuses on the logical behavior (i.e. does an entailment hold, rather than how) in the paper, and with that definition the inverse of the unit exists. So your intuition there is right.
Also, thanks for the cool reference!
Mike Shulman (May 18 2022 at 17:10):Thanks Ross, that's very interesting. Here's a possible analogy that occurs to me: every Grothendieck topos can be presented as the category of sheaves on some subcanonical site with finite limits. In fact it is the category of sheaves for the canonical topology on itself, but we can also make the site small by taking a generating set of objects closed under finite limits. But in practice, it is often useful to present toposes as sheaves on some site that isn't subcanonical and/or doesn't have finite limits, since such examples arise naturally. Would you say the trio (Grothendieck topos, subcanonical finitely-complete site, arbitrary site) is at all similar to the trio (triposable topos, tripos, evidenced frame)?
Mike Shulman (May 18 2022 at 17:16):One thing that puzzles me is that a (Set-)tripos is a large object, in the set-theoretic sense, and I never thought that it was determined by a small amount of information in general. It's not clear to me from a quick skim whether an evidenced frame is intended to be potentially large, since it is stated to have a "collection" of evidence rather than a "set", but it looks like the particular evidenced frame you construct from a tripos in section V is small, since its evidence is the set of reflected axiom schemas, which is a subset of . So is it true, then, that an arbitrary Set-tripos actually is determined by a small amount of information? If so, can you give some intuition for why this should be?
Ross Tate (May 19 2022 at 17:42):That analogy seems reasonable, though unfortunately I don't have sufficient background to say that with high confidence. I guess I think of the connection as three different perspectives on the same concept: models of (dependent) higher-order logic. Toposes are the categorical perspective (albeit of a particularly strong class of models); triposes are the fibred perspective; and evidenced frames are the realizability perspective. (Note, in all cases, these models have requirements that do not always hold for (even dependent) HOL models, such as the fact that every (external) predicate has a corresponding (internal) predicate is modeled by an external existential quantifier rather than just an internal one.) (Also, we've been focusing on Set-based triposes, but there seems to be a straightforward way to generalize evidenced frames to other base categories with a dash of Set-like structure.)
I can speak with more confidence on your latter puzzle though. First, we should recognize that are many definitions of tripos that are similar but often differ in details such as size. Nonetheless, I think in all cases there's a good intuition for why they're "essentially" small due to our finding. For example, even if you allow a large class of predicates over any given base object X, every such predicate has some corresponding morphism in the base category from X to , and similarly given such a morphism there is some corresponding predicate; so the small set of morphisms from X to essentially describes all the relevant structure on predicates over X (yes, some predicates might have the same corresponding morphism, but that loss of equality is not observable in the logic, as the logic can only reason about equality wrt its base-category's objects).
I'm guessing all that wasn't what you're asking about though. Rather, the bigger surprise it that even though a tripos describes a large set of inequalities—for each base object, an inequality on the predicates over that base object—that large set of inequalities can itself be described by a small set, namely a subset of . I think the intuition you're looking for comes from the fact that any two predicates on X can be described by a morphism from X to whose image is an element of . So, conceptually, with some manipulation we show that the entailment holds if and only if the set of pointwise pairs this entailment implies, i.e. , is a reflected axiom schema.
This manipulation relies on our observation that being a model of dependent higher-order logic over Set means that there is some pretty close connections between the internal logic of the model and the external logic of Set. For example, with a standard realizability tripos one can define a predicate that has realizers if and only if some value exists in Set, and internally once you see one of these realizers you know internally that that value exists. (Trying to understand this concrete example of what we called predicate reflection more generally is actually what led us to the completeness theorem in the first place.)
Did that manage to provide the intuition you were hoping for?
Mike Shulman (May 19 2022 at 17:56):You're right, your third paragraph is what I was asking about. But I don't feel like I understand it intuitively yet: there's too much swept under the rug by "some manipulation". Why should the entailment only depend on the image of ?
Ross Tate (May 19 2022 at 20:19):I'm happy to illustrate the manipulation, but I'm worried that's not the intuition you're looking for, so let me try something else first.
A reflected axiom scheme is some relation in Set that satisfies the following: . Let's walk through what this means in a realizability tripos. In a realizability tripos, this holds if there is some uniform evidence that can take any realizers of and of and convert them to realizers of . Now, the realizers of don't have any computational meaning; it either has no realizers are all realizers depending on whether holds (in Set). Of course, the evidence gets to assume its given a realizer of this predicate, so the entailment holds if and only if there is some uniform evidence that, assuming holds, can convert realizers of into realizers of ; that is, if and only if there is some uniform evidence that can convert realizers of into realizers of for all and related by . In other words, viewing as a collection of potential proposition entailments, is a reflected axiom schema if there is a uniform evidence that works across all of those proposition entailments.
Now consider the relation for two predicates and on a set . Hopefully it's clear that, in a realizability tripos, this relation will be an internal axiom schema precisely when there is a uniform realizer of the entailment of and for all in . So, for realizability triposes, our notion of reflected axiom schemes precisely corresponds to entailment. Conceptually, the context is the universal context to be uniform over, and all other contexts can factor through it.
Now, that reasoning was all for realizability triposes. But what we showed is that the proof relies only on the ability to define reflection of external predicates as internal predicates, i.e. , and the behavior of that reflection with respect to constructs such as existential quantifiers and conjunctions. And we showed that, because arbitrary fibred products satisfy Beck-Chevalley, such a predicate reflection can be defined in any Set-based tripos. Thus predicate entailment in all (such) Set-based triposes can be described entirely by reflected axiom schemas; every entailment is essentially a substitution of the entailment for some reflected axiom schema .
Did that do a better job of providing the intuition you were hoping for?
Mike Shulman (May 20 2022 at 16:35):Yes, that helps! Thanks. That's kind of amazing, and also kind of amazing that no one ever noticed it before. I'll need to take a closer look at your paper when I find the time.
Tom Hirschowitz (Sep 23 2022 at 10:34):Sorry for the delay, but in fact didn't Alexandre Miquel notice this before, since he has a similar completeness result with implicative algebras?
Ross Tate (Sep 23 2022 at 13:27):Funnily enough, at first glance it doesn't appear like much of a delay since you happened to post 1 year and 1 day after Mike, but Zulip does not display the year :)
As for your question, we discuss Miquel's equivalence in the paper and its limitations. In particular, unlike our equivalence between triposes and evidenced frames, Miquel's tripos-to-implicative-algebra-to-tripos construction does not model the same HOL sentences as the original tripos. This is because Miquel's construction raises the cardinality of the model of propositions (by using a subset of the powerset of the original model of propositions); it does so specifically in order to be able to give its model of propositions the (meet semi-lattice) structure required of implicative algebras. So it would seem that entailment in triposes cannot be completely described be implicative algebras.
Tom Hirschowitz (Sep 23 2022 at 15:09):Very interesting, thanks! So his equivalence is more like an equivalence between theories? Well, I should go and read the paper.
PS: this is not May 20, is it?!
Ross Tate (Sep 23 2022 at 15:26):Hahah, no it isn't. I apparently misinterpreted the user interface and didn't even bother to process what the dates actually mean. I'll blame my error on having stayed up all night with the baby!
The weaker equivalence he ensures preserves HOL sentences that only use predicates "extensionally", including respecting extensional equivalence thereon. Much of the literature uses this weaker notion of equivalence for triposes because it is enough the tripos-to-topos constructions are indeed equivalent toposes (because such toposes quotient predicates by their extensional behavior). But if you care about triposes as themselves models of HOLs are as stepping stones to quasitoposes and intensional type theories, then you want the stronger equivalence we ensure.