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: 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: Sat, 5 May 2018 14:08:16 +0200
Authentication-results: mail3-smtp-sop.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-yw0-f172.google.com
Ironport-phdr: 9a23:Oj4yrBM9j4mgvb496VYl6mtUPXoX/o7sNwtQ0KIMzox0Lfn/rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgFOT438G/ZhM9tgqxFvB2svAZwz5LObYyPKPZyYqHQcNUHTmRBRMZRUClBD5u4YYsIFOoGJ/5XoY7nqFsIsBuxGw2sC/vzxD9Pm3D2x6w60+s8EQ7Y3Q0vB8wDv27Po9rvMKcSVf66zLPPzT7eaP5W2zD96JPWfRA5ofGDQbdwftDNxkQ0GAPFi0+fqY3hPz+PyusNtG2b4vNmWOmyiGAnsxl8riazysookIXEhYIYxkrZ+Sh43Yo5P8C0RUxlbdOiDZBerTuVN5FsTcMnW2xouDg1yrkBuZOjeSgF0pUnxxrGZ/2HfYmE/gvvVOiMLTp6mn5pYr2/hxG18Uivzu3zSNO430pNripAitXMt3YN2ALP6sWfVPdx4kOs1SyM2g3T8O1IPEE5mbfBJ5I8wLM8iIIfsUHZES/3nEX2grWWdkIh+uWw6eTnZa7mqYGEN490lg7+N74hldCkDOQ3NwgBRWmb+eCm2LL/+k35Ra1GjucqnanBrJDaOcMbq7alDA9Sy4Yv8gqwDzO70NsDhnQHN1JEeBefj4fzIV3OIfb4De2+g1u2ijtryerGbfXdBcDGKWGGm7P8d5587VRdwUw914Nx/ZVRX5MGO3PEf0b3qdHcOSU+Pxa1zPvqGuJW34kXXWaCGKjRZKHVqlKQ5ukqKuKka4ocuTK7IP8gsa29xUQlkEMQKPH6laAcb2q1S6w/chepJEH0i9JEKl8k+w83TejkklqHCGcBaHO7XqZ67TY+Wtv/UdXzA7u1ibnE5x+VW4VMbzkfWF+JGHbsMY6DXqVUMX/AEopaijUBEIOZZcoh2BWp7lGozrNmKq/F5XVdu8u8jp564OrckRx0/jtxXZyQ

Tadeusz Litak said
Showing that such models exist requires a bigger and *much* more problematic fragment of ZFC than constructing the standard model of PA in ZF!

I will talk from a practical, Coq-oriented, point of view. Concerning the non-standard models of Peano arithmetic, we do not need to prove in Coq that they exist in order to work with them in an implicit way: just follow Bolzano-Cauchy-Weierstrass approach to avoid infinitesimals, i.e., use quantifiers, quantifiers and more quantifiers.

In this way, I think that it is possible to reformulate in CiC, using quantifiers and more quantifiers in place of non-standard models, the following result due to Kirby & Paris: there is an initial segment M of first-order Peano arithmetic such that Goodstein's theorem does not hold in M, i.e. there is a Goodstein sequence, starting at an element from M, which does not terminate in M.

Re: [Coq-Club] [Metamath] 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