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)

From: Andrej Bauer <andrej.bauer AT andrej.com>
To: Coq Club <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 11:59:22 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=andrej.bauer AT andrej.com; spf=None smtp.mailfrom=andrej.bauer AT andrej.com; spf=None smtp.helo=postmaster AT mail-it0-f54.google.com
Ironport-phdr: 9a23:AvbaHh3foMYUBUflsmDT+DRfVm0co7zxezQtwd8Zse0fKPad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7Vq4/Vyi84Kh3SR/okCYHOCA/8GHLkcx7kaZXrAu8qxBj34LYZYeYP+d8cKzAZ9MXXWtBUcRfVyJBDI2ybJYBAfQdMuhXtIT9u0IOoAGiCQWwGO/iyDlFjWL2060g1OQhFBnL0RAmH90TqnTbstf1P7oPXO+v0anH0y/DZO5R1Djn7ojHbwohru+OXb5qasXe01QvGB3fjliLs4PlOS6a1v4TvGiZ9eZvSeWvi2s+pgx3vzOhxd8sh5HXio4Jzl3I7yZ0zYYvKdGmVUJ2bsSoHZtfui2CKod7Rs0vT3tqtSs40LEKpJG2cSsQxJg6yRPSavqKeJWS7B35TuaeOzJ4iWpleL2hgxay9lCtyujmWcm11FZGtytFksXQunwU2Rze6seKRuFy/kem3jaP2ATT5f9eLU8okqrbLoYtwr82lpUNrUTOBjH6lFnygaOMdUgp+vKk5/r6brjpvJORN4B5hhn7Mqs0m8y/Beo4MhIJX2ie4emzzrvj8lDjQLpUjP06iLLWv4rHJcsFvK60GBVa0oA+5BalETim0s4UkmUALFJAYB6HlZTmO0nSIPDkCveym0ijkDByx/zfIrLhBojNIWPYnbf6fbd97lZcxxApwdBe4ZJUELABL+jpVk//rtyLRiM+Ziez2q7MDMh3ntcVXnvKCauEOovTt0WJ76QhOb/fSpUSvWPULfQ/6vymp3YklEVVKaCv0YEaajayF+lrOW2QZ3b2j9VHGmAP6FltBNf2gUGPBGYAL025WLgxs3RiUNr/XNXzA7u1ibnE5x+VW5hfZ2RIEFeJSC26foOIQfoOLimVJ505y2BWZf2aU4YkkCqWmkri0bM+dLjd/CECuJCl399wtbWKyEMCsAdsBsHY6FmjCmF5mmRSGm0z1aF75E1hkhKNjPQ+jPtfGtheofhOV1ViOA==

On Wed, May 2, 2018 at 6:45 AM, José Manuel Rodriguez Caballero
<josephcmac AT gmail.com>
wrote:
> 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.

I did not remark on these because there isn't anything to remark on.

You are regurtitating well known points that have long ceased to be
interesting, as they are well understood. From all points of view.

With respect,

Andrej

Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), (continued)