[FOM] proof assistants and foundations of mathematics

[José Manuel Rodriguez Caballero]

I guess that Voevodsky was motivated to worry about the foundations of the
natural numbers by his intuition from elementary topos theory, where a
natural number object does not always exist. Indeed, he was motivated by
the formalisation of category theory in UniMath.

Cultures without numbers, or with only one or two precise numbers, include
the Munduruku and Pirahã in Amazonia. Researchers have also studied some
adults in Nicaragua who were never taught number words. So, it seems that
natural numbers are a cultural phenomenon of some civilizations rather than
a knowledge given a priori. 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.

Reference: Bénabou J, Loiseau B. Orbits and monoids in a topos. Journal of
Pure and applied algebra. 1994 Feb 18;92(1):29-54.

Link to the paper: https://core.ac.uk/download/pdf/82030505.pdf

Link to a lecture about the paper:
https://www.youtube.com/watch?v=_7uONqXQvp8

José M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180807/05b83a28/attachment.html>