[FOM] proof assistants and foundations of mathematics
José Manuel Rodriguez Caballero
josephcmac at gmail.com
Tue Aug 7 12:09:54 EDT 2018
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
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:
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the FOM