Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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.
also added now a section Internal logic of a presheaf topos in the Examples section at internal logic.
<div>
<blockquote>
I think there's a typo in the universal property.
</blockquote>
<p>Yes. Fixed it.</p>
</div>
Yes, I guess so. The single arrow should denote the morphisms in the poset, the double arrow the internal hom, yes.
@ 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.)
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
added more hyperlinks to the tables
I have added a stub for disjunctive logic. What’s would be a reference to point to here?
This was a nice talk:
I have added this pointer to algebraic geometry and to internal logic.
Thanks Urs! I’ll try to also add some of the material to more specific pages on the nLab in the coming weeks.
And here is the video recording.
Fixed; thanks.
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.
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.
Perhaps we could put ’cohesive modal logic’ and have it link to cohesive homotopy type theory.
Sure.
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 by thinking in terms of the internal logic of ? Perhaps, Urs, steps in your formulation of differential cohomology that were guided by internal logic considerations.
When Felix (then: Wellen, now: Cherubini) started his thesis work on formulating -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… :-/
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?
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!).
added pointer to:
Looking at the entry, that should indeed be what is actually meant: “” does not denote the terminal object in the ambient category, but in the poset of subobjects of and as such indeed .
But the entry leaves some room to say this more clearly.
1 to 30 of 30