[FOM] Why Voevodsky was concerned about the foundations of the natural numbers?

[Sam Sanders]

Dear All,

Let me chime in here:  

I believe we are not giving “very”, and other qualitative statements, enough scientific credit, when we say:

> In Jean B?nabou's language, the word "very” is a sort of fossil from a time when the Western civilization didn't have natural numbers.


If you talk to people in physics, CS, engineering, applied math, … you will hear oodles of statements such as the following:

“If variable x is not too close to y, then f(x) does not come near z ever” (*)

Only in very few situations do we have direct access to exact/enough numerical results, 
but we can always provide descriptions like (*) based on limited data.  In fact, Science 
as we know it would come to a grinding halt without qualitative description as embodied by (*).  

Moreover, we use language as in (*) to explain math and provide intuition to our students, or even
non-expert colleagues.  It is a huge challenge (but I believe the future) to teach computers
to reason as in (*).  

The above does relate to the foundations of math: writing fully formal proofs is incredibly time
consuming at the moment and people will of course respond 

“It’s the price you pay for being truly certain"

It would help the adoption of formal proofs if the process of writing them can be streamlined.  
I would bet money on the fact that a big improvement of this process will come from computers
being able to reason qualitatively (which is only in its infancy right now).

Best,

Sam

PS: For comic relief, check Logicomix’ take on Russell’s proof of 1+1=2 on p. 185.