Not signed in (Sign In)

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory history homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie lie-theory limit limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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 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

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeApr 26th 2011

    added more hyperlinks to the tables

    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


    diff, v64, current

    • 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


    • 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 XX by thinking in terms of the internal logic of YY? 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 GG-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


    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

    added pointer to:

    diff, v74, current

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


    diff, v77, current

    • CommentRowNumber28.
    • CommentAuthorTim_Porter
    • CommentTimeJun 25th 2021

    Gave a link to Rob Seely.

    diff, v78, current

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)