The Coq mailing list

[Pierre-Yves Strub <pierre-yves AT strub.nu>]

I don't understand. IMO, any text on PA will at some point relies on
"non-formal" natural numbers (being a bit provocative : starting with
the page number, when referring to Lemma X at page Y :) ) In that
perspective, I join Matej Košík in his question.

Best. Pierre-Yves.

2018-05-02 6:45 GMT+02:00 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?
>
>