Gave a link to Rob Seely.

]]>one only needs a pre-lextensive category for disjunctive logic.

Anonymous

]]>added pointer to:

- Francis Borceux, Section 6 of:
*Handbook of Categorical Algebra*, Vol 3:*Categories of Sheaves*, Encyclopedia of Mathematics and its Applications**50**

One place where the internal logic is undeniably helpful is with regard to logic itself. For example, the topos theoretic account of forcing is very insightful, and (at least to someone used to thinking conceptually in the sense of category theory), simpler/easier to understand and get to the heart of. More philosophically/generally, internal logic *is* really the bridge between logic and category theory, which is certainly important (e.g. the applications of category theory to computer science).

Outside of logic, I have some sympathy for the point of view that the internal logic has yet to prove its worth. I do really like Ingo’s work, etc, but I’m not aware of any significant instance of a result being proven by working internally and then externalising. It should be possible, though.

Something I occasionally dream of approaching in this way, which might interest Michael Harris, is to show that Grothendieck’s hypothèse inspiratrice is undecidable. This is still kind of a logical application, but at least it is to a non-logical question. The idea would be to use two forms of ’homotopy logic’, one in which the hypothesis is true (which should be easy, by copying the proof for sets internally), and one in which it is false (which I don’t know how to do!).

]]>Thanks!

So we might describe the Blakers-Massey case as

A result in one setting is found to correspond to the external interpretation in some particular category of some internal reasoning valid in categories of that kind. The internal reasoning then shows that some result holds in all such X-categories, and there may be new results from interpreting it in newly considered X-categories. It may also give rise to a new proof in the original X-category.

It may also lend itself to generalizations (here other modalities, that is, factorization systems (L,R) in which the left class is stable by base change).

Do I take it that this version of modality was an existing concept, extracted from the standard setting?

]]>When Felix (then: Wellen, now: Cherubini) started his thesis work on formulating $G$-structures in higher toposes, he first followed the “external” diagrammatic proofs that I had given. But then midway through the thesis, he saw how everything has a slick internal formulation in terms of the naive-seeming intuitive notion of infinitesimal neighbours, much as originally envisioned in SDG but now brought out in full beauty in HoTT.

One can see him amplify this, starting about half an hour into his HIM talk from 2018 (here), and from the get-go in his CMU talk from 2019 (here).

Of course you are asking for the opposite direction: A situation where the internal formulation was understood first, helping bring about the external formulation.

That would have happened next! :-), had Felix not quit academia… :-/

]]>I’m having a discussion with Michael Harris and trying to persuade him that there’s a point to thinking in terms of internal logic. I’ve pointed him to a talk Ingo Blechschmidt’s site, but this doesn’t seem to speak to him. Urs’s FOM post may help.

Do we have any cases of someone being led to construction $X$ by thinking in terms of the internal logic of $Y$? Perhaps, Urs, steps in your formulation of differential cohomology that were guided by internal logic considerations.

]]>Sure.

]]>Perhaps we could put ’cohesive modal logic’ and have it link to cohesive homotopy type theory.

]]>There are *specific* modal logics and modal type theories that can be internal languages for cohesive toposes, but the general notion of “modal logic” is of course much more general. So I agree that the way Anonymous added it is misleading, but there’s something useful that could probably be said.

That’s not quite right, is it? Cohesive toposes are defined via a string of modalities, but this doesn’t mean that modal logic (and this could be a number of things) is an internal language for it.

]]>adding cohesive topos for modal logic to table of logics and categories

Anonymous

]]>Fixed; thanks.

]]>And here is the video recording.

]]>Thanks Urs! I’ll try to also add some of the material to more specific pages on the nLab in the coming weeks.

]]>This was a nice talk:

- Ingo Blechschmidt,
*Using the internal language of toposes in algebraic geometry*, talk at Toposes at IHES, November 2015 (pdf)

I have added this pointer to *algebraic geometry* and to *internal logic*.

added more hyperlinks to the tables

I have added a stub for disjunctive logic. What’s would be a reference to point to here?

]]>at internal logic I have

added more hyperlinks to the tables and elsewhere;

added some subsections in the section “Internal first-order logic”

stated the basic idea of internal logic in the Idea section

@ Urs #2

It should be the poset of subobjects of the terminal object, or equivalently the poset of global elements of the subobject classifier. So it's easy to mix those up and write something incorrect.

Also note that there is also an *internal* Heyting algebra, which is the subobject classifier itself. (In Set, the internal and external Heyting algebras of truth values are the same poset, but in any other topos that doesn't make any sense.)

Yes, I guess so. The single arrow should denote the morphisms in the poset, the double arrow the internal hom, yes.

]]>```
<div>
<blockquote>
I think there's a typo in the universal property.
</blockquote>
<p>Yes. Fixed it.</p>
</div>
```

]]>