The Coq mailing list

[Jose Manuel Rodriguez Caballero <josephcmac AT gmail.com>]

Dear Chlipala and Amorim,

I answer you questions.

Question 1: Is there any formal system that you find good for doing interesting mathematics and is free of foundational problems when applied as an autonomous foundation of mathematics?

Answer: It depends the kind of mathematics you want to do. If you want to mechanize Differential Geometry, Partial Differential Equations and Algebraic Number Theory, then CiC is fine. But if you want to mechanize something which does not assume the definition induction scheme of CiC, you should definitively use another formal system in order to avoid circular reasoning from a metamathematical point of view. In my personal case, I prefer UniMath, but this is just a personal choice. The UniMath library uses only the Martin-Lof type theory fragment of the CiC. This is because my research in Model Theory is in conflict with the definition induction scheme of CiC. I think that there are several mechanized proofs related to foundations of arithmetic which should be looked from a more critical point of view, in particular the so-called proof of the "consistency of arithmetic” (it looks to me like to cure cancer with aids).

Question 2: Many cultures have words for the first few natural numbers but don't recognize an infinity of numbers.

Answer: there are mathematical universes (elementary topoi) without the notion of natural numbers: https://www.youtube.com/watch?v=_7uONqXQvp8&t=1238s

Question 3: it is silly to pretend that inductive definitions need to be justified in terms of the natural numbers

Answer: In CiC the inductive definitions are given in terms of natural numbers from the beginning. This is not the case of ZFC, for example.

Question 4: 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.

Answer: If for you problems of interest are from Differential Geometry, Partial Differential Equations and Algebraic Number Theory, then CiC is for you. On the other hand, for delicate questions concerning the foundation of arithmetic and first-order model theory, CiC is less confortable than  Martin-Lof type theory, because the induction axiom scheme becomes an obstacle and you need to simulate a theory that is weaker than CiC itself (O’Connor approach). 

I think that Coq should have a way to invalide CiC in order to work only with Martin-Lof type theory. That will be helpful for people working in Model Theory and Foundations of Arithmetic.

Kind Regards,

José M.

On May 2, 2018, at 1:57 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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.