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: Matej Košík <mail AT matej-kosik.net>
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: Wed, 2 May 2018 00:11:32 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT matej-kosik.net; spf=SoftFail smtp.mailfrom=mail AT matej-kosik.net; spf=SoftFail smtp.helo=postmaster AT matej-kosik.net
Autocrypt: addr=mail AT matej-kosik.net; prefer-encrypt=mutual; keydata= xsFNBFnmLGQBEACspBbw6ph3XMaOWbIcJr5VVE8n64CSAFd/+mLOYc7qCMm4L1xV8Nqlek7A /c1q6yzgrFL7mUKMJsFnt35grPdYb0jRWZxn7vy+iirAt3BTdK4NuPG2c/DO9bAGe5Qndtm5 eln4zlQPGkXDsHYn5jdHDKDJPoIKGp1pBBlc0P2xE43R1awX5hqQenJXC6qI/MQdS3PqZgEF pvXlw7lnQ8KeXl9rzTg8izpVDnhLVZSdKKmFqaCdbOepvCgsJIrImylx+QDB8xcpn/fqkJES pzvTVTjmc/FV+djJ1groVAOkRdelaIrSpdSDr5GUM35sx//hR+ncH5aL6o+OxjJdTrwjQsgC iBW7IjP5PqoTWxHvk7nFqYvbsZUgWLmpkmSbT4WP7hbIoNVqF8zhjK82hNP+ZEQGp0DrJBF1 D577tBXWwZep+qD2vYh/c93ONXYxEdOLX7LjhOj/ETS/jN4qKvbnX3FC97stJiozFy27lb07 ctWnhfyD5fsudWYxzUsUoFlU4NTlds4lpz6VIOlMch5EO7iTmPgSoFwDWrK6VrdwUcLDOf+6 tLRhWXdiIFsDfW2Oyq1z4zAqDGamW60Y5wwbXB4UirLOeml7MJ2G1Dl0ejs1k092uBYvTvUd LHZBDSPi5kZWUWUryXYFpDvKGLT+WZ6I6YQ3LlpbNxKK2hWD3QARAQABzSRNYXRlaiBLb8Wh w61rIDxtYWlsQG1hdGVqLWtvc2lrLm5ldD7CwY4EEwEIADgWIQQc1B0KUjGdx6vBt59Qr/oS jOSGSQUCWeYsZAIbIwULCQgHAgYVCAkKCwIEFgIDAQIeAQIXgAAKCRBQr/oSjOSGSURJEACd Sg/AOyCv6/yhLuzisU8XeELgc/jkkVs7eZ0AqNbZiKZde8VWszq8i4uCkbL43bkTEYM7msdv vmBwZJwYgCNqlIecJJxdmr6U/lxYICFnXyEdSiZKlH8IDZfIOYA+UbdSdmQGdYr6Wvjjn5uh FhVSf2uqM+xK9G/uzxyBLu8/gcb1YUTAkifbzzo7tMjMV0QpHh1x5tA0LbpOWFTc+HKFhMcA xX3qgF1gOumyh7ojYmNGz+Fj2RAQWqdBGaey70fbkTn1wQtyM7zOStPadE36T5aP/4oNA6oD YdhtFuNxz1kgroSPstfDEjgeq7ldIGRJNCQmujfEUDFNkfP94Rl82Zy/1treCw1Z2bqhUAYz ZxYadLFC84YoCm7VzTuwCPmUoNCpke+kFvDIvtYh80s1CbUkMNHHWV7SV+PkUVdNF1jZrTID VCsdjZepbbG/48u56TyV7fTdHX5kJcUz4qhxX34NTDT3Vm0LiVV2LiogVeUp1+GXc8ghvVvB 35s4JG9JOaN9sRki3VuTssVzL45cgwg4MFDCdHiwwKgiLD9HahXyOIyqzAH1YwnmCZdGz/l2 j4r7ZzADcD8YMXtNJ0XHITpfa15pAx3j3ihoXfFV7jl5mtYVy8P3QPy6LA4HaJhZO+11rVuC bH2WegIPjsheXQ+wucELg7TkwrlRq4fQOc7BTQRZ5ixkARAAuZorllJ3c5j0R0rbbs6OFwUW bM2If75vlI2go9WFJcwZjqWz58fmu3xQQiAKWA2UIdzoTBabBIsI8Yf3Djg5yZsxn+kMcLCC T1i7JIaZyfREvnEhcURYbBZX1qnOK1SvlThFgQ0CCbz7hiPYZSXQTsrAUhskxBTE8tNfTFB7 V+cpgNwWTy/rQyYqGHY1iMThDRhq8ImdpNKjnvq3V7+7aT0atBdHaIfIb4wHIACa7MbPOXwd MPaKqsfhuhxJwQP4OXZNDsAbXFKuaLGAcnjjIsnLYQrSXcy14CINOkaGCJ8ZUdxn8MeuWY27 tR7h/19D2U+0JjmyZ5GB0aUo8LahWCXLJ02vQEF4yWQfwgrjrPT9LM+VZOSqGzFwU4sbaLqN mD49N93bFK80v4Q8bxKKC3WPcnQdI/JHz6FdM53TT51IwyaRPansf5bfpU8DS0i3tf/Stq9D ic38VRLlZxbaWNmbTm+/iwxn6XDJ+VVFOVPdYHb07Ml7tl7eANpmkiBHD1z0JzGMvAWI04xv ZHpLjQG5GhSti2u6H1cE5htAxlUAGQ96yAxUHAW1up7x0+H9FJFuo9HV8toZWJZ5DrUEr4b6 70JW72lj/i/bE0IY6PvcJE7vAZG8kYHvHnKEbIsDtd41BLu13NBXNqFPcKTONLaU/ymECjqA FgCROkvidzEAEQEAAcLBdgQYAQgAIBYhBBzUHQpSMZ3Hq8G3n1Cv+hKM5IZJBQJZ5ixkAhsM AAoJEFCv+hKM5IZJ14sP/3AFubatbWs6MQD+K38zE9bkWavnO4vOkNh328OTV1/iqYBQ4lPS liQ0kljvNu06OUJ7dSoa0k5nWDZDaDkbxpm/+AGBJ+arUEr+VoMKVYOSb/LzyUxQH8uDQbqV lCtXQ1qObLa6b5zT7KCaa7AqDp5CDydqXtAWSu2nHr/41vd21gQEFu1J4K/VrzWvgn+GVMup +VVeXhWBzub+9z9d+q9g6Qi4s5ecXXcEhCWtEhG318tiDMjxT+yI+qWosOlvKjyeaEGFxy6N 9eOI6Ux6tlUiBuVL95X+Ce1/UF1I45Dzfx1KQXc6QQC0SS2r3d27S82MTL7P+XeUMwhm+l/V KHS47vJl9aKQU9mQTKABl5V3gLDN+tuIbOUQl56UY/BOtub4a+Q2e7PU3Ys9D9RJH6oiGnLm 8fsf0w3xUrNUmvSBt3eNQqAuBIs91YOkXj2e6obrA3WYOAc6sPqaHrIj9CpsBGGV3N9BFZB6 QxKjvUCCCFeVrbMmDWRp5+CnzmtE3n1NClu0UzEYvl+MTjXveWWm7a3QRgk0Nd9eqCFhh2R+ tNWpC0LFNJnAV4Ka+tRXmtdMDrVKi130vIA/gxhq0fWrHmYIEeJOHQlL70IYdw/blqdbAHxP MpNpB/ycoDv4xZrwmFOZVnLnwnV9iJF1bnLno5yp0f4FKplO9LpC/2/2
Ironport-phdr: 9a23:zsyXbBdUPBub+SVO8uI8A05rlGMj4u6mDksu8pMizoh2WeGdxcu+YB7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM37X/ZisJwgqxYrhyuqRNwzIzIb4+aL/d+YqDQcMkGSWZdUMtcVSpMCZ68YYsVCOoBOP5VoY7nqFsSsxS+BxSnCuboyjxHmHj23rAx3uMkEQ7c3QwgG8kDsHHOo9XpKqgSU/m5zKrPzTXYbvNW2i3x6I7WfRA9uPyBW697f8TWyUkqDQzFj1OQpJTkPzyPzeQBqXaU4Pd9Ve+plmUpqBlxryCyysojioTFnJwZx17A+Cljw4s4K8e0RFNnbdOkCJdcqiOXOohsTs4tXm1kojs2x78EtJKhYiQHyIgryhjCYPKdaYeI+AjsVOOJLDd4mn1lfLW/ig638Ue61u3zSMu03E9JripCidnMt3MN2wbV6seZVvtx5kah2TCR2ADP8uxIPE85mKrBJ5I/zLM9koAfvEfNEyPshUn6kK+bel0h+uey6uTnZrvmpoWbN49xkgz+N74hms27AekjNwgBRXSb9vq+1LH6/k35R65Kjvw1kqXDtpDVO9gbqrajAwBJyoYj9wq/DzC+3dsEmnkHNUtJdw6Dj4j0IF7DO+v4DPe6g1S0ijhn3fHGPrv7ApXMNHfPirnhfawuo3JbnQE01JVU449eIrAHOvP6HEHr5/LCCRpsFgWozuSvK9KPU4BWDWeGA6uxNarOvF3N5eU0IurKYoIJ7mWuY8M57uLj2Cdq0WQWerOkiMNOOSKIW89+KkDcWkLCx9IIEGMEpA07FbO4jVSeXDwWZHGpXqF64DwnWtn/UdXzA7u1ibnE5x+VW4VMbzkZWFWFDXrqMoaDQPYPLiSfPp05y2FWZf2aU4YkkCqWmkr6xr5gd7WG/yQEuJCm199u5u6Vkxwup2d5
Openpgp: id=1CD41D0A52319DC7ABC1B79F50AFFA128CE48649; url=http://matej-kosik.net/doc/kosik.asc

Hi,

On 05/01/2018 08:59 PM, Jose Manuel Rodriguez Caballero wrote:
>
> Vladimir Voevodsky remarked that "CIC is not cleaned defined, because it is
> an initial model of a theory which itself requires natural numbers to be
> specified" (Talk at CMU, Feb. 4, 2010). Link to the
> quotation:
> https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/VTS_01_2.mp4

Are you referring to the fact that universes are
indexed/designated/identified by natural numbers
or do you have something else in mind?

[Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Jose Manuel Rodriguez Caballero, 05/01/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Andrej Bauer, 05/01/2018
  - Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), ikdc, 05/01/2018
- Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Matej Košík, 05/02/2018
  - Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
    - Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Pierre-Yves Strub, 05/02/2018
      - Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
        
        Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
        
        Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Matej Košík, 05/03/2018
    - Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018
      - Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), R. Pollack, 05/02/2018
        
        Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), José Manuel Rodriguez Caballero, 05/02/2018
        
        Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Arthur Azevedo de Amorim, 05/02/2018
        
        Re: [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument), Emilio Jesús Gallego Arias, 05/02/2018