Liberating synthetic quasi-coherence from syntax

Add to your list(s) Download to your calendar using vCal

• David Jaz Myers (Topos Institute)
• Friday 07 November 2025, 14:00-15:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Ioannis Markakis.

In usual foundations like ZFC , we perform all of our mathematical constructions out of bare sets. The axiom of choice ensures these sets are “extremally disconnected”—- Cantor dust. We make the mathematical objects built out of this dust to hang together with various binders and glue, but we must then constantly check that all further constructions respect this gunk. Worse, the underlying dustiness of bare sets leads to endless monster-barring in an attempt to preserve the intuitive dualities relating spaces and the algebras of intensive (functional) and extensive (distributional) quantities varying over them.

In synthetic mathematics, we instead work in the internal logic of a topos, baking in the variation of our notions with respect to an appropriately chosen class of test objects. The theory of these test objects is positive (roughly, inductive). But when the test objects are internalized as the universal model of their theory, they pick up beautiful negative properties which characterize their fundamental dualities.

In this talk, I’ll conjecturally reformulate Ingo Blechschmidt’s “synthetic quasi-coherence” axiom — or more precisely his “general nullstellensatz” which identifies these extra negative properties — as a lifting property inspired by Ivan Di Liberti’s work on coherent toposes and ultrastructures. This lifting property shows that synthetic quasi-coherence can be derived from a sort of “directed path induction” for toposes, suggesting the possibility of an internal logic for all toposes in which the axioms for any sort of synthetic mathematics would compute. (Based on joint work with Mitchell Riley)

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Martin's interesting talks
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list
• yk449

Note that ex-directory lists are not shown.