The most powerful language for mathematics according to M. Gromov

Tue Feb 4 11:34:00 EST 2020

Thanks for this thought-provoking posting, Jose.

Type theory was of course the preferred "language" that Abraham Robinson chose
to express his framework for analysis with infinitesimals.  Moreover, Robinson
specifically and explicitly stated that he does not accept set theory as
having any special foundational claim (I have quoted him on this in some of my
papers).

One of the FoM participants asked me privately to provide some details
concerning the work of Corry and others on Bourbaki failure to adopt a
category-theoretic approach, and I thought perhaps other participants may be
interested as well.  Here are some of the references:

1. http://www.tau.ac.il/~corry/publications/articles/Bourbaki%20-%20OHHM.html

2. Krömer, Ralf.  Tool and object.  A history and philosophy of category
theory. Science Networks. Historical Studies, 32. Birkhäuser Verlag,
Basel, 2007.

3. Krömer, Ralf.  La "machine de Grothendieck'' se fonde-t-elle seulement
sur des vocables métamathématiques? Bourbaki et les catégories au
cours des années cinquante.  [Is the "Grothendieck machine'' based only on
metamathematical vocabulary?  Bourbaki and categories during the 1950s] Rev.
Histoire Math.  12 (2006), no. 1, 119-162 (2007).

I my original posting, I meant to mention (but forgot) that there are of
course bi-interpretability results relating set theory and category theory,
but they don't affect the practical issue concerning which foundations are
found to be more convenient by the actual practitioners in the field.

I am glad that the famed topologist Louis Kauffman joined the discussion.  It
was one of the hoped-for outcomes of my posting that experts in specific
fields might comment on this issue.  If I understood Louis' comment correctly,
he seemed to conclude that both set theory and category theory are
indispensable.  I wonder though whether the kind of set theory he has in mind
is actually the metalanguage (rather than object language).  If MacLane ever
made comments about set theory being indispensable, I would assume that he was
referring to metalanguage as well.  At any rate I would be interested in
substantiation of the claim that MacLane made such indispensability "perfectly
clear", and where.

Mikhail Katz

On Mon, February 3, 2020 03:13, José Manuel Rodríguez Caballero wrote:
> Dear FOM members,
>   I would like to share the following quotations from M. Gromov concerning
> the most powerful language for mathematics according to him. In his paper
> on entropy, M. Gromov wrote (page 2 of [1]) :
>
> Arguably, the category language, some call it abstract, reflects mental
>> undercurrents that surface as our intuitive reasoning; a comprehensive
>> mathematical description of this reasoning, will be, probably, even further
>> removed from the real world than categories and functors.
>
>
> In his second lecture about his paper [1], M. Gromov (min 21 of [2])
> continues his defense of the language of categories:
>
> If you cannot say something in categorical language, possibly go to the
>> higher level, but more likely you are just stupid enough that you do not
>> know how to say it. And people hate categories, because they do not know
>> how to say [...] Categories is the most primitive language available to us
>> and therefore the most powerful.
>
>
> It would be interesting to know whether or not there are mathematicians in
> this list who disagree with this point of view and which language they
> would like to propose as the most powerful for mathematics?
>
> In my opinion, the language of simple type theory is enough for the sort of
> mathematics that I encounter in my personal research (quantum cryptography,
> elementary number theory, context-free grammar) and it is the most powerful
> for me because of automation in proof assistants. Nevertheless,
> mathematicians working in other areas of mathematics may have their own
> preferred languages, e.g., for Voevodsky [4], following Grothendieck [3],
> it was homotopy type theory rather than category theory his preferred
> language (homotopy type theory can be developed independently of category
> theory [5]).
>
> Kind regards,
> Jose M.
>
> References:
> [1] Gromov, M., 2013. In a search for a structure, part 1: On entropy.
> Entropy, 17, pp.1273-1277.
> URL =
> https://pdfs.semanticscholar.org/3137/66d8f87b29eeae9004d8c1eb5f8a8fb26cf3.pdf
>
> [2] Lecture: Mikhael Gromov - 2/6 Probability, symmetry, linearity
> URL = https://youtu.be/Vci3C6yAzRE?t=1307
> <https://youtu.be/Vci3C6yAzRE?t=1279>
>
> [3] Grothendieck, A., 1997. Esquisse d'un programme. London Mathematical
> Society Lecture Note Series, pp.5-48.
>
> [4] Voevodsky, V., 2011, May. Univalent foundations of mathematics. In
> International Workshop on Logic, Language, Information, and Computation
> (pp. 4-4). Springer, Berlin, Heidelberg.
>
> [5] Bauer, A., Gross, J., Lumsdaine, P.L., Shulman, M., Sozeau, M. and
> Spitters, B., 2017, January. The HoTT library: a formalization of homotopy
> type theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on
> Certified Programs and Proofs (pp. 164-172).
>