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: José Manuel Rodriguez Caballero <josephcmac AT gmail.com>
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: Sat, 5 May 2018 18:43:51 +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-yb0-f169.google.com
Ironport-phdr: 9a23:UdiZWxXPY16uxWd3a91qvXc+E0PV8LGtZVwlr6E/grcLSJyIuqrYYx2Ht8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W7VhMx+jKxVrhG8qRJh34HZe5uaOOZkc67HYd8WWWhMU8BMXCJBGIO8aI4PAvIFM+ZftIn6vUMBoxykCgmqGePg1DtIiWfq0609zushCwDG3AM9H90QsXXbtMv4O70JXu+vyKnIySvMb+lR2Tzg74XIcBchoeqSUrJoccre1UwvGBnZgViLpozlOima1uUJs2SB8+VgUuevhnchpgpsrDavwcIshZPIhoIT0l3L7z95wYk0Jd2mUkJ7ZsSkEJRWuiqHNIV2WtsvT390tCs+0LELup62cDIUxJg6yRPTceGLfomM7x/lSe2fOy13hGh/d7K6nxuy8Vavyun7VsSs1VZFtCtFkt3VunENzBPf9tGLSvVg8kqg3TuDzQ/T6uZDIUA7karUNYQtzaI3lpoWqUjDHyn2l1vqjKKOaEko5uyl5/7kb7jmvJOQKZJ4hw/kPqgzm8GyBfw0Mg0UUGia/eS82qfj/Ur8QLhSjP02lbLZv47CJcQbuqG5BhVa3Zo45hawCjepytUYnX0dIF1ZfxKHipDlO0vSL/DgEfe/n1OsnS93yPDBJ73tG4nCLnzekLj6Zrt98E5dyA8rzd9F/Z5UC7cBIOjyWkDrrtDYAAU5YESIxLPsD8w43YcDU0qOBLWYOeXcqwym/OUqdsuLfw4inT/7NvUh0MTpgWU4lkIQb56C1JEebHS1BPMud0eeenf0gtwEGGwisQ83Teisg1qHB20AL02uVr4xs2loQLmtCp3OE9j00e6xmRyjF5gTXVhoT1WFEHPmbYKBAq5eZyebI8snmTsBB+H4F90RkCq2vQq/8IJJa/LO83RB553m3dlxoebUkENqrGEmP4Gmy2iIClpMsCYISjsxhv4tpEV8zhKS2/A9jaUGRJpc4PRGVgp8PpnZnbR3

> To say that the memory of a computer is a standard natural number is a
> valid argument in some cases, but maybe this number is so huge that it
> is better to think about is as non-standard.
I am afraid I cannot understand what you mean here.

When I talk about a computer with large memory, I meant a black hole or the universe. The best way to understand this idea is to try to mechanize in Coq the theorems of this paper by Leonard Susskind: https://arxiv.org/abs/hep-th/9409089

If you follow an epsilon-delta approach, it will be very complex. It is better to use non-standard models in order to simplify the proofs.

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