[FOM] Foundational Challenge

[Sam Sanders]

Dear Larry,

While I agree that it would be helpful that mathematicians knew some basic CS (and the same perhaps for basic physics), 
it should be noted that even coding continuous functions causes problems in e.g. reverse mathematics, as explored by 
myself in the following note:   

https://arxiv.org/abs/1910.07913

In a nutshell, the logical strength of basic theorems of ordinary mathematics varies a lot based on whether 
we use “second-order codes for continuous functions" or “third-order functions that are continuous in the usual sense”.  

The difference for a well-known version of the Tietze extension theorem is "provable in Kohlenbach's base theory" vs "equivalent to ACA_0”.

Similar results are obtained for Ekeland’s variational principle, with a more dramatic difference in strength (crossing the boundary of the impredicative).  

My results are quite basic: they essentially go back to Kohlenbach’s formalisation of Grilliot’s trick and are not earth shattering 
in any technical sense.   On a conceptual level, the sky just fell on your head if you take seriously the following claim concerning reverse math:

"Such a procedure may be appropriate for
Bishop since his goal is to replace ordinary mathematical theorems by
their “constructive” counterparts. However, as explained in chapter I,
our goal is quite different. Namely, we seek to draw out the set existence
assumptions which are implicit in the ordinary mathematical theorems
as they stand. "

(“as they stand” is italicised in the original, SOSOA, p. 137)

Best,

Sam

PS: The aforementioned results regarding Ekeland’s variational principle are formulated over Baire and Cantor space.  
Lest we go off on a tangent here, let me be absolutely clear: the coding of real numbers has nothing to do with the observed 
“coding problems” of Ekeland’s variational principle: it is exclusively a problem of coding continuous functions.


> On 17 Jan 2020, at 12:00, Lawrence Paulson <lp15 at cam.ac.uk> 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