coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)
Chronological Thread
- From: Matej Košík <mail AT matej-kosik.net>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)
- Date: Thu, 3 May 2018 10:24:11 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT matej-kosik.net; spf=SoftFail smtp.mailfrom=mail AT matej-kosik.net; spf=SoftFail smtp.helo=postmaster AT matej-kosik.net
- Autocrypt: addr=mail AT matej-kosik.net; prefer-encrypt=mutual; keydata= xsFNBFnmLGQBEACspBbw6ph3XMaOWbIcJr5VVE8n64CSAFd/+mLOYc7qCMm4L1xV8Nqlek7A /c1q6yzgrFL7mUKMJsFnt35grPdYb0jRWZxn7vy+iirAt3BTdK4NuPG2c/DO9bAGe5Qndtm5 eln4zlQPGkXDsHYn5jdHDKDJPoIKGp1pBBlc0P2xE43R1awX5hqQenJXC6qI/MQdS3PqZgEF pvXlw7lnQ8KeXl9rzTg8izpVDnhLVZSdKKmFqaCdbOepvCgsJIrImylx+QDB8xcpn/fqkJES pzvTVTjmc/FV+djJ1groVAOkRdelaIrSpdSDr5GUM35sx//hR+ncH5aL6o+OxjJdTrwjQsgC iBW7IjP5PqoTWxHvk7nFqYvbsZUgWLmpkmSbT4WP7hbIoNVqF8zhjK82hNP+ZEQGp0DrJBF1 D577tBXWwZep+qD2vYh/c93ONXYxEdOLX7LjhOj/ETS/jN4qKvbnX3FC97stJiozFy27lb07 ctWnhfyD5fsudWYxzUsUoFlU4NTlds4lpz6VIOlMch5EO7iTmPgSoFwDWrK6VrdwUcLDOf+6 tLRhWXdiIFsDfW2Oyq1z4zAqDGamW60Y5wwbXB4UirLOeml7MJ2G1Dl0ejs1k092uBYvTvUd LHZBDSPi5kZWUWUryXYFpDvKGLT+WZ6I6YQ3LlpbNxKK2hWD3QARAQABzSRNYXRlaiBLb8Wh w61rIDxtYWlsQG1hdGVqLWtvc2lrLm5ldD7CwY4EEwEIADgWIQQc1B0KUjGdx6vBt59Qr/oS jOSGSQUCWeYsZAIbIwULCQgHAgYVCAkKCwIEFgIDAQIeAQIXgAAKCRBQr/oSjOSGSURJEACd Sg/AOyCv6/yhLuzisU8XeELgc/jkkVs7eZ0AqNbZiKZde8VWszq8i4uCkbL43bkTEYM7msdv vmBwZJwYgCNqlIecJJxdmr6U/lxYICFnXyEdSiZKlH8IDZfIOYA+UbdSdmQGdYr6Wvjjn5uh FhVSf2uqM+xK9G/uzxyBLu8/gcb1YUTAkifbzzo7tMjMV0QpHh1x5tA0LbpOWFTc+HKFhMcA xX3qgF1gOumyh7ojYmNGz+Fj2RAQWqdBGaey70fbkTn1wQtyM7zOStPadE36T5aP/4oNA6oD YdhtFuNxz1kgroSPstfDEjgeq7ldIGRJNCQmujfEUDFNkfP94Rl82Zy/1treCw1Z2bqhUAYz ZxYadLFC84YoCm7VzTuwCPmUoNCpke+kFvDIvtYh80s1CbUkMNHHWV7SV+PkUVdNF1jZrTID VCsdjZepbbG/48u56TyV7fTdHX5kJcUz4qhxX34NTDT3Vm0LiVV2LiogVeUp1+GXc8ghvVvB 35s4JG9JOaN9sRki3VuTssVzL45cgwg4MFDCdHiwwKgiLD9HahXyOIyqzAH1YwnmCZdGz/l2 j4r7ZzADcD8YMXtNJ0XHITpfa15pAx3j3ihoXfFV7jl5mtYVy8P3QPy6LA4HaJhZO+11rVuC bH2WegIPjsheXQ+wucELg7TkwrlRq4fQOc7BTQRZ5ixkARAAuZorllJ3c5j0R0rbbs6OFwUW bM2If75vlI2go9WFJcwZjqWz58fmu3xQQiAKWA2UIdzoTBabBIsI8Yf3Djg5yZsxn+kMcLCC T1i7JIaZyfREvnEhcURYbBZX1qnOK1SvlThFgQ0CCbz7hiPYZSXQTsrAUhskxBTE8tNfTFB7 V+cpgNwWTy/rQyYqGHY1iMThDRhq8ImdpNKjnvq3V7+7aT0atBdHaIfIb4wHIACa7MbPOXwd MPaKqsfhuhxJwQP4OXZNDsAbXFKuaLGAcnjjIsnLYQrSXcy14CINOkaGCJ8ZUdxn8MeuWY27 tR7h/19D2U+0JjmyZ5GB0aUo8LahWCXLJ02vQEF4yWQfwgrjrPT9LM+VZOSqGzFwU4sbaLqN mD49N93bFK80v4Q8bxKKC3WPcnQdI/JHz6FdM53TT51IwyaRPansf5bfpU8DS0i3tf/Stq9D ic38VRLlZxbaWNmbTm+/iwxn6XDJ+VVFOVPdYHb07Ml7tl7eANpmkiBHD1z0JzGMvAWI04xv ZHpLjQG5GhSti2u6H1cE5htAxlUAGQ96yAxUHAW1up7x0+H9FJFuo9HV8toZWJZ5DrUEr4b6 70JW72lj/i/bE0IY6PvcJE7vAZG8kYHvHnKEbIsDtd41BLu13NBXNqFPcKTONLaU/ymECjqA FgCROkvidzEAEQEAAcLBdgQYAQgAIBYhBBzUHQpSMZ3Hq8G3n1Cv+hKM5IZJBQJZ5ixkAhsM AAoJEFCv+hKM5IZJ14sP/3AFubatbWs6MQD+K38zE9bkWavnO4vOkNh328OTV1/iqYBQ4lPS liQ0kljvNu06OUJ7dSoa0k5nWDZDaDkbxpm/+AGBJ+arUEr+VoMKVYOSb/LzyUxQH8uDQbqV lCtXQ1qObLa6b5zT7KCaa7AqDp5CDydqXtAWSu2nHr/41vd21gQEFu1J4K/VrzWvgn+GVMup +VVeXhWBzub+9z9d+q9g6Qi4s5ecXXcEhCWtEhG318tiDMjxT+yI+qWosOlvKjyeaEGFxy6N 9eOI6Ux6tlUiBuVL95X+Ce1/UF1I45Dzfx1KQXc6QQC0SS2r3d27S82MTL7P+XeUMwhm+l/V KHS47vJl9aKQU9mQTKABl5V3gLDN+tuIbOUQl56UY/BOtub4a+Q2e7PU3Ys9D9RJH6oiGnLm 8fsf0w3xUrNUmvSBt3eNQqAuBIs91YOkXj2e6obrA3WYOAc6sPqaHrIj9CpsBGGV3N9BFZB6 QxKjvUCCCFeVrbMmDWRp5+CnzmtE3n1NClu0UzEYvl+MTjXveWWm7a3QRgk0Nd9eqCFhh2R+ tNWpC0LFNJnAV4Ka+tRXmtdMDrVKi130vIA/gxhq0fWrHmYIEeJOHQlL70IYdw/blqdbAHxP MpNpB/ycoDv4xZrwmFOZVnLnwnV9iJF1bnLno5yp0f4FKplO9LpC/2/2
- Ironport-phdr: 9a23:LLJWsxInmLXwTZAGw9mcpTZWNBhigK39O0sv0rFitYgRL/rxwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhjoZOT438G/ZicJ+g6xUrx2juxNxzJXZYJ2WOfdkYq/RYd0XSGhHU81MVyJBGIS8b44XAuQGJ+lYs5fyp1kTphW7AgmvC/3oyjxVjXLx2K01yeUhEQXd0QwlBd0OrGrbrNfsOKcRVuC116jIzTbZY/NQxzj99JHFfxY8qv+CWrJwdNDeyUgpFw7dlFWdqJbpMC+P2egVsmiU9fFgWfixhGE6tgF8pCWkyMQ0ioTRm44YxVDJ+T9nzIs7IdC0Uk12bNC+HJdNqy2XN5N6Tt4gTmxroio3xaAKtYSmcCUIypkr3QDTZvybf4WO/xntTvyeIS1ii3JgYL+/hwi98UynyuDkU8m7ykpKoTRHktXVtXAN0AfT6smESvdn+EeuxyqP2xjS6uFCP080ibLWJ4Muz7MwjJYfr0rOEyvslEj1gqKabFgo9vSo5uj/Z7XpvJ6cN4t6igHkNaQun9SyAeEiPQgPW2iW4uG826f//ULnQrVGl/42kq7CsJDbJsQXvKi5DBFJ0oo78RawEy+m0MgEnXkANF9KZBWHj5HwN17SJPD4EOywjk+3kDZrwvDGJqfuDo/MLnjFirfhfKxy51RSyAopnphj4MdfDahEK/buUGfwssbZB1k3KV+a2eHiXfB0yo4cEUGI8CqaePfXuF6MzucmP+SOIYwSozf+bf4o+6i93jcChVYBcPzxjtMsY3eiE6E+ehTLUT/Xmt4EVFwykE87Re3uhkeFVGcMNXO7Q68+ozI8E4OlS4HOWtL22eDT7GKABpRTI1t+JBWUC36xKNeBUusBameRJdRgkXoCWKTzE9Z8hyHrjxfzzv9cFsSR+iAcssu8ht18++DR0BI17j13ScKQzzPWQg==
- Openpgp: id=1CD41D0A52319DC7ABC1B79F50AFFA128CE48649; url=http://matej-kosik.net/doc/kosik.asc
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?
> >
> >
>
>
- [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Jose Manuel Rodriguez Caballero, 05/01/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Andrej Bauer, 05/01/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Matej Košík, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Pierre-Yves Strub, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Matej Košík, 05/03/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), R. Pollack, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Arthur Azevedo de Amorim, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Siddharth Bhat, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Siddharth Bhat, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), R. Pollack, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Andrej Bauer, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Adam Chlipala, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Pierre-Yves Strub, 05/02/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
Archive powered by MHonArc 2.6.18.