Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

February 25, 2010

(Infinity, 1)-logic

Posted by David Corfield

We’re having a chat over here about what an (,1)(\infty, 1)-logic might look like. The issue is that if we can extract a (1)-logic from ordinary toposes, shouldn’t there be an (,1)(\infty, 1)-logic to be extracted from (,1)(\infty, 1)-toposes. This post originated as an ordinary comment, but as things have gone a little quiet at the Café (10 days without a post!), I thought I’d promote it.

Won’t there be a sense in which this internal logic to an (,1)(\infty, 1)-topos will have to be interpretable as a ‘logic of space’? If SetSet is an especially nice topos which being well-pointed allows us to understand 1-logic internally and externally, we might hope that the well-pointed (,1)(\infty, 1)-topos of \infty-groupoids, Gpd\infty Gpd, does the same for (,1)(\infty, 1)-logic, given \infty-groupoids are models for spaces.

Had I not known anything about logic beyond that it is a language used to formulate statements in a domain and to represent valid reasoning, then had I been asked to extract such a thing given the definition of a topos, that would seem to be a tricky task. But give me SetSet and I can make a start.

I can convey quite a lot about logic with the sets 1, 2, HH (the set of humans), and DD (the set of dogs). E.g., the predicate ‘French’ is a map H2H \to 2, the function ‘owner’ is a map DHD \to H, composing gives me the dog predicate ‘owned by a French person’. Then ‘Fido’ is an arrow 1D1 \to D, ‘True’ is an arrow 121 \to 2, as is ‘Fido is owned by a French person’, and so on. I can then work up an account of variables, quantifiers, etc.

So can I not get going with Gpd\infty Gpd similarly by picking out a couple of spaces and then analogues of 11 and 22? 22 is the subobject classifier in SetSet. We have that object classifiers are supposed to be the analogues of subobject classifiers. 11 is a generator in SetSet and generators for (,1)(\infty, 1)-categories are being discussed here.

I just wonder if a simple look at maps between spaces might not suggest what (,1)(\infty, 1)-logic is like. If we have spaces like the surface of the globe and the interval [0,)[0, \infty), and the temperature map between them, won’t (,1)(\infty, 1)-logic capture something of our everyday talk about global temperature?

I suppose connectedness will be covered: I can’t reach Washington DC from London by land, but I can reach Glasgow. In fact I can reach Glasgow in several different ways, although some of these ways are essentially the same.

Posted at February 25, 2010 9:28 AM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2172

14 Comments & 1 Trackback

Re: (Infinity, 1)-logic

Hi David,

if possible, let’s look at a bunch of baby-examples to get a feeling for what internal (,1)(\infty,1)-logic is like. I have currently little idea, beyond some vague general statements.

A while ago, I started spelling out at internal logic – In SetSet the following baby exercise in ordinary internal logic:

Baby exercise. Rephrase all of standard logic from the internal point of view as the logic internal to the topos SetSet.

I didn’t take the time to drive this very far there, just stated very explicitly for the record how the primitive logical operations arise from limits, colimits and internal homs in SetSet. This is tautological to everyone who ever thought about it, but not to everyone who never thought about it. So it’s good to think about it once. :-)

If possible, let’s do the following: let’s go step-by-step through the notes as at the above link, and translate it all into the analogous constructions with SetSet replaced by Grpd\infty Grpd. What the abstract constructions in terms of limits, colimits and internal homs are is clear, but let’s think a bit about what this now means as we look at it from the point of view of \infty-logic.

Then when we have discussed the (1(,1))(1 \mapsto (\infty,1))-translation of the stuff at the above link, let’s go further and look at the corresponding translation of more nontrivial constructions in internal logic.

(,1)(\infty,1)-Baby exercise. Translate step-by-step the above baby exercise from the 1-topos Set=(0,0)CatSet = (0,0)Cat to the (,1)(\infty,1)-topos Grpd=(,0)Cat\infty Grpd = (\infty,0)Cat.

Here is a piece of scratch paper for everyone who wants to give it a try.

Does that sound like a good plan to get a foot on the ground here?

Posted by: Urs Schreiber on February 25, 2010 4:33 PM | Permalink | Reply to this

Re: (Infinity, 1)-logic

Sounds like a good plan. As added to the scratch pad, I think we need equivalents for the one element set, as generator, and the two element set as subobject classifier.

Posted by: David Corfield on February 25, 2010 5:32 PM | Permalink | Reply to this

object classifier in ooGrpd

As we said, the next thing we want to get hold of is the object classifier in Grpd\infty Grpd

I have now added the relevant definitions and propositions to object classifier.

Then in the query box there, I develop a bit further the thoughts about the object classifier in Grpd\infty Grpd for given cardinality bound κ\kappa.

I think we had stated the basic idea several times before, as archived for instance at generalized universal bundle as well as at stuff, structure, property:

the (relatively κ\kappa-compact) object classifier in Grpd\infty Grpd is the corresponding universal op-fibration in \infty-groupoids

Core(Z| Grpd κ op) Core(Grpd κ) \array{ Core(Z|_{\infty Grpd_{\leq \kappa}}^{op}) \\ \downarrow \\ Core(\infty Grpd_{\leq \kappa}) }

I’ll suppress the core in the following, notationally.

Now, by the (,1)(\infty,1)-Grothendieck construction we know that \infty-functors XGrpdX \to \infty Grpd classify \infty-Grothendieck op-fibrations in \infty-groupoids over XX.

But since XX is itself an \infty-groupoid, every \infty-functor out of another \infty-groupoid into it will be such. Use for instance HTT, prop. 3.3.1.8, which says that every coCartesian fibration over a Kan complex – and our op-fibration in \infty-groupoids = left Kan fibration is one – is equivalently a categorical fibration: but every morphism of simp-sets EXE \to X factors as an equivalence followed by a categorical fibration.

Posted by: Urs Schreiber on February 25, 2010 8:04 PM | Permalink | Reply to this

Re: (Infinity, 1)-logic

I prefer to distinguish between the internal type theory of a category and the internal logic which sits on top of that type theory. The type theory is about constructing objects, while the logic is about constructing subobjects. For instance, limits and colimits, exponentials, and object classifiers belong to the type theory, while images, dual images, intersections, unions, and subobject classifiers belong to the logic.

Some further explanation of this distinction is at type theory, along with remarks on the natural semantics. The semantics of (extensional) type theory naturally lies in a category with certain category-theoretic structure like limits, colimits, and exponentials, while the semantics of logic over that type theory naturally lies in some indexed poset over that category. We commonly take the indexed poset to consist of the subobjects in the category in question, in which case additional “logical” structure on the category is required.

In an elementary 1-topos, all of the “logical” structure is not usually included in the definition, because it comes for free once you have power objects. But I don’t know whether object classifiers are as powerful as power objects in this respect – I suspect not. So I think that for purposes of studying the internal logic (and not just the internal type theory) of an (,1)(\infty,1)-topos, we should include both the type-theoretic structure and the logical structure, and in particular we should consider both the object classifier and the subobject classifier. I’ll write more about how I think these should go in a bit.

(Confusing the whole issue is the “propositions as types” viewpoint according to which one uses objects to describe logic as well as type theory. Categorically, this corresponds to studying the logic of a free exact completion.)

Posted by: Mike Shulman on February 25, 2010 10:45 PM | Permalink | PGP Sig | Reply to this

Re: (Infinity, 1)-logic

The type theory is about constructing objects, while the logic is about constructing subobjects. For instance, limits and colimits, exponentials, and object classifiers belong to the type theory, while images, dual images, intersections, unions, and subobject classifiers belong to the logic.

Ah, okay. I hadn’t appreciated this point of view so far.

we should include both the type-theoretic structure and the logical structure, and in particular we should consider both the object classifier and the subobject classifier. I’ll write more about how I think these should go in a bit.

Sounds very good. That would give a nice rational for why every (,1)(\infty,1)-topos does happen to have a sub-object classifier on top of its object classifier.

The sub-object classifier for Grpd\infty Grpd, by the way, is just {,}\{\top, \bottom\}, as for SetSet. So are we headed now in the direction that we say Grpd\infty Grpd has the same logic as SetSet, but much richer type theory ?

Posted by: Urs Schreiber on February 26, 2010 12:40 AM | Permalink | Reply to this

Re: (Infinity, 1)-logic

So are we headed now in the direction that we say ∞Grpd has the same logic as Set, but much richer type theory?

Perhaps “the same” is perhaps too strong, but I think it is certainly true that the logic of Gpd\infty Gpd should be Boolean and satisfy a suitable version of the axiom of choice, and have other properties of the logic of SetSet which one expects to fail in other (nn-)topoi. And of course SetSet can be identified with the full subcategory of discrete objects in Gpd\infty Gpd.

Posted by: Mike Shulman on February 26, 2010 1:46 AM | Permalink | PGP Sig | Reply to this

Re: (Infinity, 1)-logic

I think talking about “logic of space” is a bit misleading, since the use of “space” in a statement like “spaces model \infty-groupoids” is fairly different from its use in, for instance, the theory of “space and quantity.” For instance, to take your example, the interval [0,)[0,\infty) is contractible, and thus as an \infty-groupoid it is the same as the terminal object. So the internal logic of Gpd\infty Gpd won’t tell you much about temperature. You could look at an (,1)(\infty,1)-topos of sheaves on some space, but you could also look at a 1-topos of sheaves on the same space, and you might learn just as much about temperature from the latter.

Posted by: Mike Shulman on February 25, 2010 10:49 PM | Permalink | PGP Sig | Reply to this

Re: (Infinity, 1)-logic

Good points! So might we say that the internal logic of \infty-Grpd is a logic of homotopy?

Your mountain guide tells you, “from this base camp there is only one way up the mountain”. As your party ascends one of the members makes a slight detour to take a picture. You then ask of your guide whether that person or the rest of the group are on “the one way up”, and which can still reach the top. So the guide replies “You can’t deduce that someone can’t now reach the top with (,1)(\infty, 1)-logic. I meant there is only one way up up to equivalence.”

Posted by: David Corfield on February 26, 2010 9:47 AM | Permalink | Reply to this

Re: (Infinity, 1)-logic

So might we say that the internal logic of Grpd\infty-Grpd is a logic of homotopy?

That makes sense to me.

Posted by: Mike Shulman on March 7, 2010 5:04 AM | Permalink | Reply to this

Re: (Infinity, 1)-logic

From Steve Awodey’s Type Theory and Homotopy:

…intensional type theory can be seen as a “logic of homotopy theory”. (p. 9)

Searching for “logic of homotopy” on Google throws up 3 hits: this discussion, Awodey’s paper, and a draft paper by Jean-Pierre Marquis, Mathematical Forms and Forms of Mathematics: The metaphysics and epistemology of homotopy types, which is very handy since I’ve been invited to Paris in March to speak about such matters. I’ll need to pick some brains around here before then.

Posted by: David Corfield on January 5, 2011 11:33 AM | Permalink | Reply to this

Re: (Infinity, 1)-logic

I have now added most of what I know and think about type theory and logic in an (,1)(\infty,1)-topos to the nLab page internal logic of an (∞,1)-topos.

Posted by: Mike Shulman on February 26, 2010 5:36 AM | Permalink | Reply to this
Read the post In Praise of Dependent Types
Weblog: The n-Category Café
Excerpt: Dependent types should be everyone's friend!
Tracked: March 3, 2010 6:39 PM

Re: (Infinity, 1)-logic

I’ve been trying to think of things we could say in (,1)(\infty,1)-logic that would have a useful meaning in an (,1)(\infty,1)-topos, but at the moment I’m kind of blocked by not yet knowing enough about what one does in an (,1)(\infty,1)-topos. This is entirely my own fault and something I can and should rectify.

But for the moment, starting by analogy, one of the most basic things about 1-logic in a 1-topos is that a morphism f:ABf\colon A\to B is an epimorphism if and only if the statement “for every bBb\in B there exists an aAa\in A with f(a)=bf(a)=b” is true in the internal logic. Similarly, in a 2-topos, ff is a “strong 1-epic” iff the statement “for every bBb\in B there exists an aAa\in A with f(a)bf(a)\cong b” is true in the internal 2-logic. I presume something similar will be true in an (,1)(\infty,1)-topos for the appropriate sort of epimorphism.

We also have a similar characterization of monomorphisms: ff is monic in a 1-topos iff “whenever f(a 1)=f(a 2)f(a_1)=f(a_2), then a 1=a 2a_1=a_2” is true internally. Similarly, in a 2-topos we can characterize the 1-monics, aka fully-faithful maps, by “every arrow f(a 1)f(a 2)f(a_1)\to f(a_2) is the image of a unique arrow a 1a 2a_1\to a_2”. But I’m less sure about the right thing to say in an (,1)(\infty,1)-topos; here it seems like we might need infinitely many statements in the internal logic to characterize the monomorphisms.

I’m also starting to worry about whether hypercompleteness, or lack thereof, is going to rear its head at some point.

Posted by: Mike Shulman on March 7, 2010 5:15 AM | Permalink | Reply to this

Re: (Infinity, 1)-logic

…it seems like we might need infinitely many statements in the internal logic to characterize the monomorphisms.

Can this worry be seen to arise from the following definition of monomorphism in an (,1)(\infty, 1)-category,

Equivalently this means that for every object XCX \in C the induced morphism

C(X,f):C(X,Y)C(X,Z) C(X,f) : C(X,Y) \to C(X,Z)

of \infty-groupoids is such that its image in the homotopy category exhibits C(X,Y)C(X,Y) as a direct summand in a coproduct decomposition of C(X,Z)C(X,Z),

in that in the internal language we’d need to express this condition for infinitely many XX?

Posted by: David Corfield on January 20, 2011 11:57 AM | Permalink | Reply to this

Re: (Infinity, 1)-logic

we’d need to express this condition for infinitely many X?

No, that’s just as true for 1-topoi, and it’s taken care of by the Kripke-Joyal semantics of internal logic. Instead I was worried about the fact that there are infinitely many higher homotopy groups that we need to assert an isomorphism of.

Posted by: Mike Shulman on January 20, 2011 9:01 PM | Permalink | Reply to this

Post a New Comment