*[HoTT] [FOM] Why Voevodsky was concerned about the foundations of the natural numbers?@ 2018-08-08 6:18 José Manuel Rodriguez Caballero0 siblings, 0 replies; only message in thread From: José Manuel Rodriguez Caballero @ 2018-08-08 6:18 UTC (permalink / raw) To: fom;+Cc:HomotopyTypeTheory [-- Attachment #1: Type: text/plain, Size: 2033 bytes --] Dear FOM members, Here is an speculative hypothesis about Voevodsky's motivations concerning the foundations of natural numbers. It would be interesting to know some opinions about this possibility or new alternative hypothesis. I just try to explain to myself the following strange quotation from Voevodsky: "CIC [...] has this induction definition scheme which allows you to do things parametrized by natural numbers. I think this is wrong, foundationally speaking, in this sense that CIC is not cleanly defined, because it is an initial model of a theory which itself requires natural numbers to be specified" (Univalent Model Talk at CMU, Feb. 4, 2010). 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 Piraha 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 Benabou's language, the word "very" is a sort of fossil from a time when the Western civilization didn't have natural numbers. Reference: Benabou 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 Sincerely yours, José M. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 4157 bytes --] ^ permalink raw reply [flat|nested] only message in thread

only message in thread, other threads:[~2018-08-08 6:18 UTC | newest]Thread overview:(only message) (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-08-08 6:18 [HoTT] [FOM] Why Voevodsky was concerned about the foundations of the natural numbers? José Manuel Rodriguez Caballero

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).