## Stack Semantics

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:

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!

Note: This entry and its comments have been copied back to the main n-Category Cafe site. Please submit further comments there (unless the comment system there starts to have issues again).

### 14 Responses to “Stack Semantics”

I am intrigued by the role the self-indexing stack $X \mapsto S/X$ (on slide 30) plays.

Do you see a role for the under-self-indexing $X \mapsto X/S$? Elsewhere the claim is that a tremendous amount of interesting geometric information is encoded in the objectwise stabilized/abelianized self-under-indexing of a higher “category of spaces” $S$. This must have a logical counterpart, I suppose.

• Mike Shulman Says:

In brief, no, I don’t see any comparable role for co-slice-categories. One reason is that co-slice categories generally don’t preserve any of the “set-like” behavior which slice categories do. The slice category $S/X$ plays a crucial role in topos theory because its objects can be thought of as “X-indexed familes of sets/objects,” and anything you can do with a single set can be done “family-wise” to a family. Put differently, objects of $S/X$ are “generalized objects of $S$ at stage $X$” as I described on one of the slides. I don’t see any such interpretation for co-slice categories; they are undoubtedly important in mathematics, and maybe they even have their own internal logic, but that logic would be much less familiar, perhaps sort of like a linear logic.

2. Toby Bartels Says:

Well, I haven’t finished writing my response to the paper as you sent it by email (but I like it, I like it!). However, since you asked specifically for terminological advice, here is mine:

* On ‘autological’: I’m wary of any terms derived from ‘separation’, since this is liable to conflict with unrelated topological terminology. The only meaning of ‘autological’ that I know of is in relation to the Grelling–Nelson paradox, where it refers to a self-describing adjective. If you’re happy with invoking that idea, then go for it.

* On ‘well-pointed’: I honestly don’t know why one wouldn’t simply use ‘well-pointed’ period. Is there any literature that studies topos theory from an *externally* constructive perspective that uses that term in the weaker (but classically equivalent) sense? If so, then sure, say ‘constructively well-pointed’ to clarify (and in any case, say ‘classically well-pointed’ for the weaker notion when comparing them). But if not, then use the standard term for what that term really should mean (and already *does* mean, even if one usually simplifies the definition classically).

(H’m, no preview option. Well, I’ll see how this formats.)

• Toby Bartels Says:

Dang, I can’t believe that I wrote that wrong. Of course, ‘autological’ _describes_ a self-describing adjective.

(Now I’ll see how /this/ formats.)

• Mike Shulman Says:

(My computer died this morning, so I am at a public terminal and not able to sign in as myself.)

I have exactly the same feelings about terms derived from ‘separation’. The only objection to ‘autological’ that I’ve heard so far is that it’s a ‘funny-sounding word’.

On ‘well-pointed’, I agree with you. But I’ve talked to some people who feel strongly that the term ‘well-pointed’ is so strongly associated with a classical metatheory that using it to mean anything at all in a constructive one will confuse people. My inclination with this paper is to bend over backward to avoid alienating anyone, since many people have strong and differing feelings in this area. But my current secret hope (hmm, I suppose it’s not so secret any more when I post it on the blog, is it? oh well) is that ‘constructively well-pointed’ will be unambiguous to everyone to start with, and yet clumsy enough that once people get used to using the constructively reasonable notion they will naturally begin dropping the adjective.

• Toby Bartels Says:

If you've found people who strongly object to ‘well-pointed’ in this sense, then that's probably a good strategy. If you consistently use one adjective or another when working within a constructive metatheory, then I agree that the natural thing to do will become obvious. Certainly the classical theorem well-pointed ⇒ boolean is so well-known that it’s good to guard against it.

The danger here is that people will assume that the constructive version is weaker than the classical. That is, they'll think that you avoid the theorem above by using a weaker hypothesis, whereas in fact you avoid it by using a weaker metatheory, even though you use a potentially stronger hypothesis than you might have. But that point will have to be clarified no matter what terminology you use.

(Warning: more formatting experimentation.)

3. Andrej Bauer Says:

Slide on page 7: do you really mean that BZ only reaches up to Aleph_omega or up to V_{omega+omega}. I suppose what I am asking is: how do you know that Aleph_omega is in V_{omega+omega}?

• Mike Shulman Says:

Of course Aleph_omega needn’t itself be in V_{omega+omega} (which models BZ); for instance if GCH holds then it isn’t. I really meant cardinal numbers equal to or greater than Aleph_omega are unreachable, not “strictly greater than”. Of course V_{omega+omega} is the more precise statement, with Beth_omega in between, but I chose to mention only Aleph_omega because I thought it would be more familiar to more people, and the people who are familiar with Beths and the V hierarchy should be able to figure out that that’s what I mean.

4. johncarlosbaez Says:

I’m very happy to see you are developing “2-logic“, and I’m sure David Corfield will be happy too.

But what exactly do you mean by this:

I prefer to say: Sets are already analogous to truth values in a 1-topos, via Curry-Howard.

It seems like something I should understand and like, but somehow I don’t get the reference to Curry-Howard.

Are you saying sets are to the topos Set as truth values are to the set {F,T}? Or what?

5. johncarlosbaez Says:

Or are you saying that characteristic functions of sets are valued in truth values?

• dcorfield Says:

While you’re here, let’s see if we can tease out the difference between taking categorified logic to have truth values as sets and keeping truth values as {F, T}.

Mike mentioned and a gave a link to this difference here.

I thought from the Baez-Dolan perspective, something like type theory spontaneously emerges by categorification.

So 0-logic is propositional logic: we have a collection of symbols and axioms. In a model symbols take values in truth values, satisfying the axioms. Models form a set.

1-logic is typed predicate logic: we have a collection of types, and typed relations + axioms. In a model types are assigned sets, relations are assigned subsets of the corresponding sets. Models form a category.

2-logic: we have a collection of metatypes, a collection of types which are metatyped, and a collection of typed relations + axioms. In a model, metatypes are assigned categories, types are assigned presheafs over the corresponding product of categories, typed relations are then subsets.

Modal logic is a form of 2-logic, with a single metatype the category of worlds. Types are presheafs over these worlds (cf. Awodey and Kishida).

But we can also have a single metatype, $C$, and then types as presheafs on $C \times C$, i.e., types dependent on pairs of objects in $C$.

• Mike Shulman Says:

That sounds like almost exactly what I mean by 2-logic. I prefer to say “1-type, 0-type, (-1)-type” instead of “metatype, type, relation” since then the pattern is clearer. To be more precise, relations are dependent (-1)-types (non-dependent ones merely being truth values), and in 2-logic as you describe it, the “types” are what I would call dependent 0-types (dependent on a 1-type).

What I was trying to get at in the slides John referred to was that n-types don’t have to depend only on (n+1)-types; they can already depend on other n-types. For (-1)-types this isn’t interesting, but for 0-types it is. My use of “analogous” was meant to refer to the table on the previous slide, which summarized a bit of the Curry-Howard correspondence between logical operations on dependent (-1)-types and set/type-theoretic operations on dependent 0-types. That is, we don’t need 2-logic in order to “treat sets as being like truth values” — the Curry-Howard analogy already does that for us. (I don’t like to call Curry-Howard an “isomorphism” since in my mind, there is a difference between propositions (i.e. (-1)-types) and types (i.e. 0-types); there’s just an analogy, plus we can use the latter to describe proofs of the former.)

6. Roger Witte Says:

I note you have slides for category theorists who don’t know a lot about categorial logic, and there seem to be plenty of papers/notes etc running in this direction. However there is precious little running in the opposite direction – ie stuff for people who are happy with logic and/or material set theory who need to acquire enough category theory to understand categorial logic.

Meanwhile I am finding your paper very interesting so far (but, as yet I am only on page 4).