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)
