Re: [HoTT] Re: A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)

[Andrej Bauer <andrej...@andrej.com>]

I doubt much can be added to a discussion of "using natural numbers
before defining natural numbers" on this list, but just because this
list if about type theory, let me point out two things.

1. Various worries about non-standard natural numbers and lack of
absolute definitions are an artifact of first-order logic and the
insistence that natural numbers be defined on their own, without
reference to anything at all. As soon as one realizes that the natural
numbers can be characterized by a universal property within a larger
universe (either as an initial algebra in a category, or a type with a
suitable elimnator in type theory), the mystery goes away. Within any
universe of mathematics, the natural numbers are unique up to unique
isomprphism. And since there are many universes of mathematics, it is
not suprising that we see many incarnations of natural numbers. But
each one first perfectly and uniquely in the ambient in which it
lives. (In case this isn't clear, the non-standard models of PA
constructed with ultrapowers are just normal natural numbers objects
in an ultrapower model of set theory).

2. The idea that there can be no natural numbers before we define
natural numbers, as well as statements such as "it is impossible to
avoid circularity in foundations" arises from mistaken and unrealistic
expectations that it is the task of the foundations of mathematics to
provide something out of nothing. I explain to myself the yearning for
such foundations from the fact that the human psyche is comforted by
an illusion of absolute security. I have written about this on
Mathoverflow (https://mathoverflow.net/a/23077/1176).

With kind regards,

Andrej