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

Discussion Tag Cloud

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
    • CommentTimeOct 30th 2012

    added to the list of References at categorical logic a pointer to

    • CommentRowNumber2.
    • CommentAuthorzskoda
    • CommentTimeOct 30th 2012

    I added it to history of mathematics.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeOct 31st 2012

    Last night over dinner I had a chance to read a bit in Bell’s article. Especially the survey right at the beginning is pretty good. I think it would have helped me had I seen something like this earlier, when I didn’t already know it all….

    Also good is the comprehensive list of references. There are a bunch of pointers to Lawvere’s work that I hadn’t been aware of before.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 1st 2012

    I added also Reyes and Marquis’s History of Categorical Logic, 1963-1977.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2012
    • (edited Nov 1st 2012)


    Looking back at the entries we have, I found their was a stark mismatch between, on the one hand, the entry logic not saying a single word on “categorical logic” but listing references for it, and the entry mathematical logic saying a little bit about “categorical logic” but not giving any references.

    So I have decided to merge the two entries for the moment, the material is now all at logic. At least as long as this is fairly stubby anyway. I think that gives a clearer picture for the reader. Should one day the entry logic grow large and unwieldy, we can still split it up again.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 1st 2012

    Reading the final three paragraphs of Reyes and Marquis takes me back to when I first started looking at category theory in 1990 while in Paris, convinced by reading Lambek and Scott that Lautman had been right in the 30s to see logic as a facet of mathematics, rather than as a separate foundational formalism. But I’m also left wondering whether categorical logic did as well as it might. I see they end with

    The fate of categorical logic is presently intimately tied to theoretical computer science, and to a certain extent to the foundations of homotopy theory and its place in mathematics and mathematical physics.

    So cohesive homotopy type theory ticks all the boxes. But shouldn’t there have been a greater effect of categorical logic already?

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2012
    • (edited Nov 1st 2012)

    But shouldn’t there have been a greater effect of categorical logic already?

    Lawvere has the vision. But how many people 1. understand the intended vision, 2. if they understand it, appreciate its implications?

    What I want to say is: the vision may have been around for a few decades now. But nobody had really investigated it in the past. Isnt’t that right? Even Lawvere himself: the closest to actual physics that I have seen his writings get is the discussion of an ordinary differential equation and a vague hint at extensive/intensive quantities in physics. That’s a little thin, at least as compared to the implicit grand claim.

    And then: if one does go further and tries to find actual fundamental physics in topos theory/logic, it turns out that the proposed 1-toposes in fact don’t work. Much as the word “cohesive \infty-topos” pays tribute to the general idea here, a notable fact is that essentially all of the genuine physics that is axiomatizable inside one collapses entirely if we go to a cohesive 1-topos. So I could argue that only since rather recently the whole program has even reached square 1.

    That’s not to disregard the ingenuity of the vision, just to make plausible why it didn’t have “greater effect already”.

    I am grateful for this quote of Lawvere here, which I found on p. 31 of Marquis-Reyes:

    My own motivation came from my earlier study of physics. The foundation of the continuum physics of general materials, in the spirit of Truesdell, Noll, and others, involves powerful and clear physical ideas which unfortunately have been submerged under a mathematical apparatus including not only Cauchy sequences and countably additive measures, but also ad hoc choices of charts for manifolds and of inverse limits of Sobolev Hilbert spaces, to get at the simple nuclear spaces of intensively and extensively variable quantities. But, as Fichera lamented, all this apparatus may well be helpful in the solution of certain problems, but can the problems themselves and the needed axioms be stated in a direct and clear manner? And might this not lead to a simpler, equally rigorous account?

    I have now added this to the beginning of geometry of physics.

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 2nd 2012

    Is your thought that all of categorical logic has been held back by the failure to look properly at physics, since cohesive homotopy type theory is a natural staging post on path of mathematics’ development? Or does ordinary homotopy type theory have its own intrinsic value, where one might attribute what held up its course to other factors, e.g., a failure to learn properly from homotopy theory?

    [Side thought: will there need to be a directed cohesive homotopy type theory?]

    If you put together Lawvere from p. 29 of Marquis-Reyes,

    …the orientation of many topos theorists could perhaps be more accurately summarized by the observation that what is usually called mathematical logic can be viewed as a branch of algebraic geometry, and it is useful to make this branch explicit in itself.

    with Ben-Zvi here

    currently a big swath of algebraic geometry can be seen as a special easy case of homotopy theory, but with great insight to be gained from the broader perspective,

    you could be led at least to the thought that mathematical logic is a very special case of homotopy theory.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2012
    • (edited Nov 2nd 2012)

    Ah, yes, so I was reacting specifically to the suggestion that you quoted, which said that the fate of categorical logic is tied, among other things, to mathematical physics.

    will there need to be a directed cohesive homotopy type theory?]

    Yes. I was just the other day thinking about that in another thread.

    It’s maybe noteworthy that category objects in a base \infty-topos in particular sit in a cohesive \infty-topos over that whose intrinsic notion of path is the directed morphisms in these internal categories. Mike had been talking about that on the blog a while back, and earlier there was some discussion long these line here, which I now can’t find. In that above comment and in the entry Segal condition I find it kind of curious that category objects and higher category objects all arise as the pullback of a diagram of three cohesive toposes. I am not sure yet how the story should continue, but maybe this is telling us something.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJun 17th 2013
    • (edited Jun 17th 2013)

    Added a pointer to

    Pierre Cartier, Logique, catégories et faisceaux. Séminaire Bourbaki, 20 (1977-1978), Exp. No. 513, 24 p. (numdam)

    to the list of References on categorical logic to logic

    (promted by somebody looking for this reference over on the category theory mailing list).

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeApr 10th 2018

    added pointer to Makkai-Reyes rewritten by Marmolejo 18 on first order categorical logic

    This reminds me that we are still waiting for some kind logic expert to split off an entry “categorical logic” from the entry logic. Presently and since long ago, both terms redirect to the same entry.

    diff, v59, current

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeApr 10th 2018

    Only now do I see the other discussion of this reference here. Not sure what the intention is or was. Let me know if I accidentally created a duplicate now.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJun 9th 2021

    under “References – Categorical logic” I have added pointer to:

    diff, v62, current

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeAug 6th 2022

    added pointer to:

    diff, v67, current

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeAug 6th 2022

    added pointer to:

    diff, v67, current

    • CommentRowNumber16.
    • CommentAuthorGuest
    • CommentTimeOct 27th 2022

    To what extent does the existence of type theory and especially higher inductive types imply that all fields of mathematics are just subfields of logic, and consequently that the foundations of mathematics is just natural deduction? One typically thinks of things like free algebras, field of fractions, Cauchy completion, Kolmogorov quotient, and so on to be in the realm of mathematics, but all of these could be constructed as higher inductive types in the language of natural deduction with rules for formation, introduction, elimination, and computation rules for each of the above notions, putting them in the realm of logic.


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)