coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: José Manuel Rodriguez Caballero <josephcmac AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Berry paradox in Coq?
- Date: Tue, 8 May 2018 01:41:22 +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-it0-f48.google.com
- Ironport-phdr: 9a23:7N6tuxXSKr/EiTeoVVbJPsY+IjLV8LGtZVwlr6E/grcLSJyIuqrYYxyFt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XhMJ+j79Vrgy9qBFk2YHYfJuYOeBicq/Bf94XQ3dKUMZLVyxGB4Oxd48BD+0aPeFCt4bzoEEBrR2jBQayAOPg0iNGhnjr0q0g0uQhHhzG0xIhHt0Wrnnbts76O70WUeCx0qbI1zLDZO5R1Df/74jIaQ4uoemMXb1sdMre01UgGhjKjlWVs4PlPjeV2v4RvGic6uptTOSigHMppQF2pzig3MYsio/Ri4Iay1DE6SV5wJsuKtGiVEF7ZtukHZ1NvC+ZL4t7Wt0uT31stSogybALuYS3cDYXxJko3RLSZP+Kfo6V6Rz5TumROy13hHd9dbK/mRmy9U+gx/X5Vsau0VZKqjNJktjQtnwRzhDT5MeKR/hn8keu3jaP0A/T6uVaLkwuiaXbLJshzqYxlpoVr0vDAjf7lFvqgKKSbEkp+eil5/75brn7qZKQLYB5hwLmPqQrgMO/AOA4MgYUX2ic/OSxzL/j/UriQLpUlv02krXWsJXAKssHvaO5DApV3Zwi6xa7FTupzNMYnXwfIFJfZB2Hl5TpO03JIP3gEfi/hE2snC53yPDCI73uGY7ALmPDkbfkZbZy8VRQyAs1zdBF5pJbEKsNIPzpWhy5iNuNBRggdgew3uzPCdNn14pYV3jcLLWeNfbwtkQJ0ccmJfSBYLgvvzrnKvc46uzZpnYzkFsZcLOulc8Vb2u1BvRtJkySSXXpi9YFV2wNu1xtH6TRlFSeXGsLND6JVKUm62RjUdP0PcL4XomoxYe58mK+F5xSaHpBDwnVQ3jtfoSAHfwLbXDLe5Mzonk/TbGkDrQZ+1S2rgajkuhoK+PV/msTspexjIEotd2Wrgk78HlPN+rY02yJSDspzGYBRjtz3bwn5EIhmhGM1q93h/EeHttWtatE
Hi, I know that there is a project of formalization of Coq in Coq: https://github.com/coq-contribs/coq-in-coq
I would like to know if the following (informal) argument can be formalized in Coq as a theorem (it is my version of Berry paradox).
Let Coq(n) be the largest natural number that can be defined in Coq using at most n characters from the keyboard of the programmer. It can be computed just checking all the possible arrays of n characters. It easily follows that the function fun (n : nat) => Coq(n) is non-decreasing and the limit of Coq(n) is infinite when n goes to infinite.
For all n, Coq(10^n) contains n+6 characters, where "10^n" is just a notation (we should write in Coq the actual number) . Let k be the number of characters of the implementation of the function fun (n : nat) => Coq(n) in Coq. So, Coq(n+k+6) is at least Coq(10^n) for all n, because Coq(10^n) is a chain of n+6 characters in Coq and we can implement the function n -> Coq(n) using k characters. For each n large enough, Coq(t) is constant for all t in the interval [n+k+6 .. 10^n]. We can substitute n by n+1, in order to obtain that Coq(t) is constant for all t in [n+k+7 .. 10^(n+1)] for all n large enough. So, Coq(t) is constant for all t in [n+k+6 .. 10^(n+1)] for all n large enough. Hence, Coq(n) is constant for all n large enough, but this is absurd.
Therefore, the function fun (n : nat) => Coq(n) cannot be implemented in Coq.
Thank you in advance,
José M.
- [Coq-Club] Berry paradox in Coq?, José Manuel Rodriguez Caballero, 05/08/2018
- Re: [Coq-Club] Berry paradox in Coq?, Jasper Hugunin, 05/08/2018
Archive powered by MHonArc 2.6.18.