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.

Quentin

]]>added pointer to:

- Jean-Yves Girard (translated and with appendiced by Paul Taylor and Yves Lafont),
*Proofs and Types*, Cambridge University Press (1989) [ISBN:978-0-521-37181-0, webpage, pdf]

added pointer to:

- Jean-Yves Girard (translated and with appendiced by Paul Taylor and Yves Lafont),
*Proofs and Types*, Cambridge University Press (1989) [ISBN:978-0-521-37181-0, pdf]

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

- Jacob Lurie,
*Categorical Logic*, Lecture notes 2018 (web)

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.

]]>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.

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

]]>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.

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.

]]>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*.

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?

]]>Thanks!

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.

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

]]>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.

]]>I added it to history of mathematics.

]]>added to the list of References at *categorical logic* a pointer to