### (Infinity, 1)-logic

#### Posted by David Corfield

We’re having a chat over here about what an $(\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 $(\infty, 1)$-logic to be extracted from $(\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 $(\infty, 1)$-topos will have to be interpretable as a ‘logic of space’? If $Set$ 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 $(\infty, 1)$-topos of $\infty$-groupoids, $\infty Gpd$, does the same for $(\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 $Set$ and I can make a start.

I can convey quite a lot about logic with the sets 1, 2, $H$ (the set of humans), and $D$ (the set of dogs). E.g., the predicate ‘French’ is a map $H \to 2$, the function ‘owner’ is a map $D \to H$, composing gives me the dog predicate ‘owned by a French person’. Then ‘Fido’ is an arrow $1 \to D$, ‘True’ is an arrow $1 \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 $\infty Gpd$ similarly by picking out a couple of spaces and then analogues of $1$ and $2$? $2$ is the subobject classifier in $Set$. We have that object classifiers are supposed to be the analogues of subobject classifiers. $1$ is a generator in $Set$ and generators for $(\infty, 1)$-categories are being discussed here.

I just wonder if a simple look at maps between spaces might not suggest what $(\infty, 1)$-logic is like. If we have spaces like the surface of the globe and the interval $[0, \infty)$, and the temperature map between them, won’t $(\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.

## Re: (Infinity, 1)-logic

Hi David,

if possible, let’s look at a bunch of baby-examples to get a feeling for what internal $(\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 $Set$ the following baby exercise in ordinary internal logic:

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 $Set$. 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 $Set$ replaced by $\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

meansas we look at it from the point of view of $\infty$-logic.Then when we have discussed the $(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.

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?