The Coq mailing list

[Matej Košík <mail AT matej-kosik.net>]

Hi,

On 05/02/2018 10:48 AM, José Manuel Rodriguez Caballero wrote:
> Dear Pierre-Yves Strub and Matej Košík,
> 
> As a historical remark, Bourbaki apologized for introducing page numbering 
> before the definition of natural numbers.

That is a nice joke :-)

Seriously though: we have to distinguish between
- mathematics
  (juggling in some calculus)
- metamathematics/philosophy
  (a language we can use, e.g. to define some calculus and prove properties 
about the calculus we have just defined)

> Nevertheless, the page numbering is not used in Bourbaki's system to prove
> theorems.

No surprise. Mathematics is a strict subset of metamathematics/philosophy.

> 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.

I am not exactly sure what you mean by "do things parametrized by natural 
numbers from the beginning".

What I see is that:

  If you want, you can define objects that can be regarded as natural numbers
  and if you want, you can *prove* the corresponding induction principle (by 
relying on "Ind" rule of CiC.

Not only that. In addition to natural numbers, you can define any other 
useful objects and *prove* the corresponding induction principle (by relying 
on "Ind" rule of CiC).

  - Induction principles in CiC are theorems.
  - Analogous induction principles in metamathematics (and non CiC calculi I 
have seen) are, unfortunatelly, axioms.

In other words

  - On a metamathematical/philosophical level, we have infinite axioms / 
inference rules.
  - In CiC we have finite axioms / inference rules.
    (regardless of how many inductive types we choose to define)

Metamathematics, just like any religous belief, is dealing with imaginary 
objects.

Metamathematics, unlike any of the religious beliefs
- is dealing with *useful imaginary objects*
- and its infinite set of axioms is mutually consistent.

In mathematics (such as based on CiC) you only restrict yourself to a finite 
set of axioms / inference rules with all its advantages
(it is, unlike religions, more universally acceptable)
and its disadvantages
(one may not (yet) be able to reason about all the pressing issues one is 
able to reason about at the mathematical/philosophical level).

> 
> 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 
> <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
>  
> <mailto: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
>  
> <mailto: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 
> <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
>  
> <mailto: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
>  
> <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?
>     >
>     >
> 
>