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

[Josef Urban]

I have always believed these are two quite separate lines of research:

1. Coming up with clearly defined "more natural/convenient" foundational or
automation mechanisms. Like nonstandard analysis/set theory, little
theories, treatment of isomorphisms, fuzzy logic, etc.

2. Coming up with contextual (and often combining statistical and semantic)
mechanisms that disambiguate and "compile" our compressed, natural-language
and context-dependent math statements/proofs into precise statements/proofs
in existing foundations and formal proof systems.

I have almost convinced myself that (2) can be done already today, with the
existing formal proof systems and AI tools.

Obviously, progress in (1) is very useful and can also help (2).

But I really think a lot of progress in computer understanding of math can
be done using (2) right now, without a major progress in (1).

Josef


On Thu, Aug 9, 2018 at 11:30 AM, Sam Sanders <sasander at me.com> wrote:

> 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.
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180810/0ce532d8/attachment.html>