The Coq mailing list

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

Dear Andrej,

Thank you by the recommendation of Pohlers' book (I already borrowed this book in 2016 during a course of Axiomatic Set Theory). I remarked that you didn't explicitly argue against the main points of my post: 

(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",

 

(2) my conclusion: 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. 

You disagree that "Coq cannot prove the consistency of PA". I recall that I'm talking from the point of view of foundation of mathematics as the title of my post suggests. The following two remarks to you statements will clarify this point.

Statement 1. Already Gentzen showed the consistency of PA by using induction up to ordinal ∊₀

Remark 1. The primitive recursive arithmetic with the additional principle of quantifier-free transfinite induction up to the ordinal ε0, is neither weaker nor stronger than the system of Peano axioms. So, what Gentzen really proved was an equiconsistency. Indeed, in my above-mentioned reference to Voevodsky's conjecture that PA is inconsistent, he explained the problem with Gentzen's argument: https://video.ias.edu/voevodsky-80th

Statement 2. There is a proof of consistency of PA in CiC. But to prove consistency of CiC itself requires a still stronger theory. This is all very well known and is not mysterious at all. 

Remark 2. So, from a foundational perspective, it is useless to prove the consistency of PA in CiC because of this well-known reason. Indeed, CiC can be used to mechanize a lot of mathematics, but it cannot be used to prove the consistency of arithmetic without begging the question.

Best Regards,

José M.

2018-05-02 0:11 GMT+02:00 Matej Košík <mail AT matej-kosik.net>:

Hi,

On 05/01/2018 08:59 PM, Jose Manuel Rodriguez Caballero wrote:
>
> 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

Are you referring to the fact that universes are indexed/designated/identified by natural numbers
or do you have something else in mind?