The Coq mailing list

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

Dear Coq users,

   I want to share some personal doubts with you about the rôle of Coq in the foundation of mathematics, in particular with respect a claim due to Russell O’Connor: “Peano Arithmetic (PA) is proved to be consistent in Coq's type theory and therefore is incomplete”. This is not the first criticism of his claim (I’m only responsible for my own criticism, not for other people’s criticism): http://www.jamesrmeyer.com/ffgit/review-oconnor.html

 I recall that the Calculus of Inductive Constructions (CIC) is the formalism behind the interactive proof assistant Coq version V7. The underlying formalism of Coq version V8 and up is the calculus the Predicative Calculus of Inductive Constructions (pCIC). In my personal experience I find CIC uncomfortable to mechanize arguments in Model Theory (to have more expressive power is not an advantage in Model Theory, on the contrary).

Vladimir Voevodsky remarked that "CIC is not cleaned defined, because it is an initial model of a theory which itself requires natural numbers to be specified" (Talk at CMU, Feb. 4, 2010). Link to the quotation: https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/VTS_01_2.mp4

The foundational problem is that when we write

Inductive nat : Set :=

  | O : nat

  | S : nat -> nat.

we are not defining the “natural numbers” for the first time (in the edifice of foundations of mathematics), because we already assumed the existence of natural numbers in the structure of CIC. Indeed, nat is the “datatype of natural numbers”, but it is not the definition of natural numbers in foundations of mathematics as a whole. On the other hand, when we write

Inductive Z :=

  | Nonnegative : nat -> Z 

  | Negative : nat -> Z.

we are defining something new from the point of view of foundations of mathematics: the integers.

This is one of the reasons why I have some problems to trust proofs of properties of natural numbers formalized in CIC : Are some people “proving” properties of natural numbers that are already assumed in order to define CIC ?

The typical example is the mechanization of the “Essential Incompleteness of Arithmetic” due to Russell O’Connor: https://arxiv.org/pdf/cs/0505034.pdf

I quote O’Connor’s paper  (version: 11 May 2006) “Coq is sufficiently powerful to prove the consistency of PA by proving that the natural numbers model PA”. Here there is a confusion between “proof” and “presupposition”. Coq cannot prove the consistency of PA: no one can do it (Coq is not supernatural, to say it in a funny way). Indeed,  Voevodsky conjectured that PA is inconsistent. Link to this controversial conjecture and the explanation of the problem with Gentzen’s argument for the consistency of PA : https://video.ias.edu/voevodsky-80th

My modest conclusion is that Russell O’Connor formally mimicked the Gödel-Rosser argument in Coq, but he did not considered the rôle of Coq in the foundation of mathematics as a whole. To claim to have proved “the incompleteness of arithmetic”, just because “Coq is sufficiently powerful”  to prove something that Coq really assumed from the beginning, is not a valid move in foundations of mathematics.

Finally, statements like 

"A CONSTRUCTIVE proof of the Gödel-Rosser incompleteness theorem has been completed using the Coq proof assistant”

are very dangerous, because we should add to the actual construction in CIC all the metamathematical presuppositions about CIC. Indeed, there are elementary topoi without natural number object. 

Personally, I enjoyed reading O’Connor’s paper, his research is very interested, but the foundations of mathematics is a very delicate subject and even great logicians like Frege, Gödel and Church made mistakes.

Sincerely yours,

José Manuel Rodriguez Caballero

Département de Mathématiques

Université du Québec à Montréal

rodriguez_caballero.jose_manuel AT uqam.ca

https://josephcmac.wixsite.com/vitae