The Coq mailing list

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

Dear Pierre-Yves Strub and Matej Košík,

  As a historical remark, Bourbaki apologized for introducing page numbering before the definition of natural numbers. Nevertheless, the page numbering is not used in Bourbaki's system to prove theorems. Indeed, in Zermelo–Fraenkel set theory (ZF), natural numbers are not used in a mathematical way before their own definition. On the other hand, CiC has the induction definition scheme which allows you to do things parametrized by natural numbers from the beginning.

Russell O'Connor claimed in its PhD thesis: "

I proved the consistency of Peano Arithmetic (PA) by proving that the natural numbers 

form a model"

. The following lines are the main ideas of O'Connor's "proof" that "natural numbers model PA" : http://r6.ca/Goedel/goedel1.html

(1) "LNT : Ensemble" is the language of number theory (Plus, Times, Succ, and Zero with appropriate arities).

(2) "PA : Formula" is Peano arithmetic as an axiomatic system with the induction scheme.

(3) "Consistent E F" is the fact that the set E models the theory F. Let's see the main lines of the original implementation in Coq:

System := Ensemble Formula

Definition SysPrf (T : System) (f : Formula) :=

  exists Axm : Formulas,

    (exists prf : Prf Axm f,

       (forall g : Formula, In g Axm -> mem _ T g)).

Definition Consistent (T : System) := exists f : Formula, ~ SysPrf T f.

(4) O'Connor proved that the type "Consistent LNT PA" is inhabited in CiC. The problem is that, in his proof of "Theorem PAconsistent : Consistent LNT PA" he used 

apply ModelConsistent with (M := natModel) (value := fun _ : nat => 0)

where 

Definition natModel : Model LNT :=

  model LNT nat

    (fun f : Functions LNT =>

     match f return (naryFunc nat (arity LNT (inr (Relations LNT) f))) with

     | Languages.Plus => fun x y : nat => y + x

     | Languages.Times => fun x y : nat => y * x

     | Languages.Succ => S

     | Languages.Zero => 0

     end) (fun r : Relations LNT => match r with

                                    end).

In other words, he used the type "nat" as a model of PA. So, in order to prove that natural numbers satisfy the principle of complete induction from PA, he used the above-mentioned induction definition scheme which allows you to do things parametrized by natural numbers from the beginning.

I do not say that "mechanization" of theorems from Model Theory is not possible in Coq. What I say is that, from the point of view of foundation of mathematics, we need to be open to the possibility that maybe some people are just "proving in Coq" assumptions from CiC in a fancy way. I use the example of O'Connor, because I tried to do a similar project in Model Theory, but I'm not convinced of the efficacy of this approach from a mathematical point of view.

Best Regards,

José M.

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