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: José Manuel Rodriguez Caballero <josephcmac AT gmail.com>
- 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: Wed, 2 May 2018 06:45:09 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=josephcmac AT gmail.com; spf=Pass smtp.mailfrom=josephcmac AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb0-f171.google.com
- Ironport-phdr: 9a23:qOEP1ROMzQgRUreeSHQl6mtUPXoX/o7sNwtQ0KIMzox0Ivz/rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgFOT438G/ZhM9tgqxFvB2svAZwz5LObYyPKPZyYqHQcNUHTmRBRMZRUClBD5u4YYsIFOoGJ/5XoY7nqFsIsBuxGw2sC/vzxD9Pm3D2x6w60+s8EQ7Y3Q0vB8wDv27Po9rvMKcSVf66zLPPzT7eaP5W2zD96JPWfRA5ofGDQbdwftDNxkQ0GAPFi0+fqY3hPz+PyusNtG2b4vNmWOmyhWAnrARxrSKuxscqkoTJh5gaykve+Spn3Yk1OMW0SE9hbt6/CpdcrT+VOJZrQs4kXmpmuz46x6UYtZKneCUG0pcqyh7FZ/CZboSF7AjvWPuTLDtlgn9uZaixiAyo8Ue6z+3xTsm030hOripCitTMs2oC1x3X6sSeSvpy5Vut1S+B1wzO6OxIPFo4laXcK54mzb4wkoQcvV7fES/xnUX6lK6WdkM69ei08+nrfKnqq5uGO4J3igzyKLoiltGxDOgiLwQDXXWX9fy51LL5/E35RLtKjucxkqncqJ3aJ8MbprWnDA9N0oYs9xO/AC2639kDknkHKUhKeBODj4TzJ17OJ/X4Ae+lg1uwiDdr2+zGPrr5D5rRKXjDia7tcqp5605B0wU+1stf5pJRCrEZOv3/QE7xtNrCDh84KQO42ejnCM8unr8ZDGmIG+qSNL7YmV6O/OMmZeeWN6EPvzOoCf8+ZsnLhHkklFsqR66lx5oYdX2qKd9vKUydZXf2hZ9VE2ARsxI+R+njg3WNVDdSYzC5WKdqtWJzM56vEYqWHtPlu7eGxiruRsQHNFADMUiFFDLTT6vBXv4NbCyIJco4y24LULGgT8kq0hT87VammYoiFfLd/2gjjbymzMJ8vrSBmhQ79DgyBMOYgTnUEjNE21gQTjpz55hR5ExwzlDZj/p9iv1cUM1Zv7ZHC1hjc5HbyON+Bpb5XQeTJto=
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?
- [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), 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), 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.