Stack Semantics

Note: This is being reposted from the temporary site, with existing comments copied over so that discussion can continue here.

Today I’m blogging from Washington D.C., at the Annual Meeting of the Association for Symbolic Logic. The ASL is mostly populated with material set theorists and classical logicians, but this year they had a special session on Categorical Logic, and another one on Logic and the Foundations of Physics (including lots of categorical quantum mechanics)—a promising sign for the recognition of category theory. I was invited to speak at the former session this afternoon, about stack semantics and 2-categorical logic.

And not-entirely-coincidentally, at long last I’ve put online a draft of my (first) paper about the stack semantics and comparing material and structural set theories. You can get it from my nlab page:

• The stack semantics

There are also slides from today’s talk and one from last November.

In brief, the idea of the stack semantics is to extend the internal logic of a topos to a language which can talk about unbounded quantifiers (quantifiers of the form “for all sets” rather than “for all elements of A” for some fixed set A). In this extended language, we can then state topos-theoretic axiom schemas which are as strong as the full separation and replacement axioms of ZF. (Ordinary topos theory is only equiconsistent with bounded Zermelo set theory, which is much weaker than ZF.) This generalization is extremely easy—even easier than some presentations of the ordinary internal logic—and is in fact implicit throughout topos theory, but has seemingly never been written down precisely before.

If that intrigues you, then you may want to look first at the talk from November; it’s aimed at category theorists without much experience in categorical logic. Then you can go on to look at the paper itself, most of which should (I hope) also be fairly accessible. Comments are welcome!