The most powerful language for mathematics according to M. Gromov

Wed Feb 5 02:08:21 EST 2020

Dear Mikhail,
Here is an excerpt from MacLane’s book “Mathematics Form and Function”.
As you will see, he is not satisfied with Sets as a foundation, nor with Categories as a foundation.

Sets and categories together form the foundational tools of many working mathematicians.
We would not know how to think about topological quantum field theory without categories, and 
much of algebraic topology would be unintelligible. For topological quantum field theory it is crucial to understand that a topological space 
can become a morphism in a category of cobordisms. These morphisms are structural, not maps of the underlying sets. And yet the underlying sets are there
as topological spaces as well. A mixture of this sort is the common material of ongoing mathematical work.
Best,
Lou

> On Feb 4, 2020, at 10:34 AM, katzmik at macs.biu.ac.il wrote:

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200205/5a8cede7/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: MacLaneCatSet.pdf
Type: application/pdf
Size: 557509 bytes
Desc: not available
URL: </pipermail/fom/attachments/20200205/5a8cede7/attachment-0001.pdf>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200205/5a8cede7/attachment-0003.html>