# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeDec 10th 2009

created at internal logic an Examples-subsection and spelled out at Internal logic in Set how by turning the abstract-nonsense crank on the topos Set, one does reproduce the standard logic.

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeDec 10th 2009

Somewhere we should say explicitly that the Heyting algebra associated to a topos is the poset of subobjects of the terminal object. Some entries make it sound like it should be the poset of subobjects of the subobject classifier.

• CommentRowNumber3.
• CommentAuthorHarry Gindi
• CommentTimeDec 10th 2009
• (edited Dec 10th 2009)
In the page on Heyting Algebra, I think there's a typo in the universal property. That is, the small arrow on the right side of the "if and only if" should be a \Rightarrow rather than a \rightarrow. I don't know anything about heyting algebras though, so if it's a typo, I'll let you fix it.
• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeDec 10th 2009

also added now a section Internal logic of a presheaf topos in the Examples section at internal logic.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeDec 10th 2009
This comment is invalid XHTML+MathML+SVG; displaying source. <div> <blockquote> I think there's a typo in the universal property. </blockquote> <p>Yes. Fixed it.</p> </div>
• CommentRowNumber6.
• CommentAuthorHarry Gindi
• CommentTimeDec 10th 2009
Alright, I found a couple more errors with that symbol, but I can fix them since I know that I'm right now. You guys must have been using the thin arrow and then someone didn't finish changing it.
• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeDec 10th 2009
• (edited Dec 11th 2009)

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

• CommentRowNumber8.
• CommentAuthorTobyBartels
• CommentTimeDec 10th 2009

@ 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.)

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeApr 26th 2011

at internal logic I have

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

• stated the basic idea of internal logic in the Idea section

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeApr 26th 2011

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

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeNov 30th 2015

This was a nice talk:

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

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

• CommentRowNumber13.
• CommentAuthorUrs
• CommentTimeDec 4th 2015

And here is the video recording.

• CommentRowNumber14.
• CommentAuthorGuest
• CommentTimeOct 4th 2018
The section on internal logic in Set states "These are classified, respectively, by the truth values [...]" but mixes the order up -rKl
• CommentRowNumber15.
• CommentAuthorTodd_Trimble
• CommentTimeOct 4th 2018

Fixed; thanks.

2. adding cohesive topos for modal logic to table of logics and categories

Anonymous

• CommentRowNumber17.
• CommentAuthorDavid_Corfield
• CommentTimeJan 4th 2020

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.

• CommentRowNumber18.
• CommentAuthorMike Shulman
• CommentTimeJan 5th 2020

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.

• CommentRowNumber19.
• CommentAuthorDavid_Corfield
• CommentTimeJan 5th 2020

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

• CommentRowNumber20.
• CommentAuthorMike Shulman
• CommentTimeJan 5th 2020

Sure.

• CommentRowNumber21.
• CommentAuthorDavid_Corfield
• CommentTimeJan 5th 2021

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.

• CommentRowNumber22.
• CommentAuthorUrs
• CommentTimeJan 5th 2021

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… :-/

• CommentRowNumber23.
• CommentAuthorDavid_Corfield
• CommentTimeJan 5th 2021

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?

3. 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!).

• CommentRowNumber25.
• CommentAuthorGuest
• CommentTimeMar 7th 2021
Small typo : "the objects A of C are regarded as collections of things of a given type A" should be written "an object A of C is regarded as a collection of things of a given type A". Vincent Semeria
• CommentRowNumber26.
• CommentAuthorUrs
• CommentTimeMar 23rd 2021

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

Anonymous

• CommentRowNumber28.
• CommentAuthorTim_Porter
• CommentTimeJun 25th 2021

Gave a link to Rob Seely.