[FOM] Foundational Challenge

[Patrik Eklund]

> 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 at 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 at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom