The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 05/02/2018 12:45 AM, José Manuel Rodriguez Caballero wrote:

(1) Voevodsky's argument: "CIC is not cleaned defined, because it is an initial model of a theory which itself requires natural numbers to be specified",

Let me give an engineer's (e.g., my) perspective on these questions.

All of our deliberations are based on human mental hardware.  Tree structures are built into our brains, in the modules for processing natural language.  I believe results from cognitive science, including surveys of cultures around the world, establish that natural numbers are actually not such a natural (inborn) concept, while parsing language into trees is universal!  (Many cultures have words for the first few natural numbers but don't recognize an infinity of numbers.)  Therefore, it is silly to pretend that inductive definitions need to be justified in terms of the natural numbers.  Human brains do the opposite.

We are going to accept some set of axioms, and it is economical to pick ones that map well to the proof-checking hardware -- our brains.  CIC is so simple that all highly educated people across all societies can understand the proof-validity judgment and apply it identically, and at the same time CIC is expressive enough that it can be used to encode all the problems of interest.  I see little practical value in rejecting any system with those properties, when unsoundness hasn't been found empirically after extensive use.