coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: roconnor AT theorem.ca
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] [Metamath] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)
Date: Fri, 4 May 2018 21:14:36 -0700 (PDT)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=roconnor AT theorem.ca; spf=PermError smtp.mailfrom=roconnor AT theorem.ca; spf=PermError smtp.helo=postmaster AT theorem.ca
Ironport-phdr: 9a23:nU0RlBUaXkF74evSvVayFZ8qN7/V8LGtZVwlr6E/grcLSJyIuqrYYhGGt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/ZisJ+kr9VrxCiqRxxzYHbb52aOeF7fq/BZ94XX3ZNU9xTWiFHH4iyb5EPD+0EPetAtYn9oEcBrRy4BQmqA+Pv0CRFhmP23aIk1OQhCx/J3Ak6E90SqnvZqsj+OqkVUeCw1qbIzDPDYutM2Tr88oTHbgourPeRVrxzacrc0VcjGx/Bg1mKrYHoPSmZ2voTv2SF9eZsSO2ih3IhpgpsuDag3N0shZPMho8NylDL6yF5wIEtKN2kSE50f9mkEIFOuCGfLYd5XtktT3lpuCY81LIGpYa2cDYWxJkj3RLSb/6Kf5KW7h79SuqdOyp0iX15dL6ngha960mgyunyVsmu11ZKqzJIksPLtn8R0BzT7M6HSvxn/kq6xTaP1x7c6uZeIU8qkKrXMYIuzaQompoJrUvDBjP2mFnxjKKOakok/fGo5/37bbXiu5+TLJR5ihr+M6QrgsywG/40MgkIX2iB+OSzzqfv/UPjQOYCsvpjma7A9ZveOM4zp6ijAgYT3JxwxQy4CmK8198fm38ANnpZeB+AlYXsfVrHc6OwNuu2n1n5yGQj/PvBJLC0WsycfEiGq6/oePNG02AZzQMyyd5F4JcNUOMdIP/0QEL08tfRXEFgb16Eht3/AdA47bswHHqVC/bDYr/SvFiS6+dpKODePNZI6ga4EOAs4rvVtVF8mVIZevDzj4cXZXeiE/EgKEzLP3c=

On Fri, 4 May 2018, José Manuel Rodriguez Caballero wrote:

By the way, Emilio, do you think that the incompleteness of arithmetic can be
mechanized in Coq without simulating first-order logic? I think that you can
repeat the Gödel-Rosser argument
by coding CiC by Gödel numbers. I do not see why first-order logic is
essential here.

If higher-order arithmetic is incomplete, then in particular first-order
arithmetic is incomplete too. I wonder if there could be some
simplifications...

The theorem is about the /essetial/ incompletness of theories, proving the essential incompleteness of a weaker theory is a logically stronger result.

--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

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