It might help if more mathematicians were familiar with some basic principles of computer science.

I agree, but I would like to add that it also might help if computer scientists were familiar with some basic principles in mathematics. Coding one thing in terms of another is very acceptable in computer science, since "code" (in a language) and "algorithm" (in a machine) are very acceptable. Mixing languages and bringing in things from the outside is very typical in computer science, but very dubious in mathematics. A typical example of bringing in things from the outside is the function type constructor. Where does it come from? Did it come from the same factory as the types? Another example is 'lambda term'. Computer scientists accept that the "elegant definition" of a lambda term should not be modified, even if, when eventually dealing with substitution, it leads to having "undesirable terms" which need to be handle by "renaming". Computer scientists simply find ways to code one thing in terms of another. "Free and bound variables" is an awful concept, since some symbols, in fact the informal ones, possess a capacity to "bind", a notion which seemingly is not describable in any language but the natural one. --- Types are missing in set theory, and there are approaches to fix that. Category is "too algebraic" (MacClone) about adding "monoidal" (yes, categorists also encode one thing using another thing), but the practical use of may be on its way ("what we want to do with it"). Type theory does not have a proper internalization of type constructors (they are brought in from the outside). --- Having said that, my conviction and suggestion is that set, category and type theory should really engage in dialogue and communication, rather than debate and competition. It's been too many decades of foundations of foundations being claimed not being found over there but over here. It's time to turn page, and move towards the "big cultural difference" being a "big culture" rather than a "cultural difference". --- Best, Patrik On 2020-01-17 13:00, Lawrence Paulson wrote:

It might help if more mathematicians were familiar with some basic principles of computer science. To a computer scientist, it's natural that a say a graphics application might be built on top of certain data structures or libraries for computer graphics, which in turn are built on lower-level numerical libraries, and so on down until raw binary is reached. For mathematics, ZFC typically serves as the equivalent of binary, while category theory, et cetera, are the libraries.

I think there is a big cultural difference here. I've read an account of G??del's theorem that devoted much space to the concept of G??del-numbering, when coding one thing in terms of another is as natural as breathing to a computer scientist.

Larry Paulson On 17 Jan 2020, 03:38 +0000, Foundations of Mathematics <fom@cs.nyu.edu>, wrote:

...

This is based on a confusion. Even if you look at MacClane's Categories for a Working Mathematician, category theory is presented as a development within set theory where a category is defined as a set together with a set of "arrows", etcetera, This is just like a normal development of a special mathematical area within the usual set theoretic foundations of mathematics.

---

FOM mailing list FOM@cs.nyu.edu https://cs.nyu.edu/mailman/listinfo/fom

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]