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: Adam Chlipala <adamc AT csail.mit.edu>
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 10:56:20 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:pJZx/xY9YMLLsiOClowU6xX/LSx+4OfEezUN459isYplN5qZoM69bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAk7m/XhMx+gqFVrh2vqBNwwZLbbZqPO/ZiZK7QZ88WSGRDU8tXSidPApm8b4wKD+cZIetXspPyp14TphagBQmsAOLvyidSiX/yx6IxzuMsHhvb0wM6GtIBrG/Zo8nuNKgIUOC1yLPEzTDCb/NKwzvy9pXHcg04rPyKQLl+ctLRxFEyGw/bjVics4LoMy+P2ugTqWSX8fdsWf63h2I6tQ18oSKjy8kwhoXTgo8Z1ErI+TtnzIooI9CzVVR1bsS+EJRKsiGXL4t2Td0mQ2FvoCs6zaAGuYK0fCgNyZQnwRHfZ+Wcc4iU+B3jSPyeLS1ki3J+Yr2/hhKy/VKlyu39Ssm4ykhFoTdYktXUt3AN0QLc6tSfR/dg4Eus2iyD2g7P5u1eP0w4j7TXJ4M9zrIok5ocq0XDHiv4mEXsi6+Wc10p9fK15Ov9Z7XpuoSROJNvig7kM6QuntazAeE5MggSRWSU5/mz1KD78U3jXLpKluE2krXesJ3COcsbobe5DxZJ3YYn9hawFCyr0M8YnHkCNFJKYgiLj4nvO1HUIfD3F+2zg1q2kGQj+/eTNbr4R57JM3LrkbH7fL875VQP5hA0yIV265tRQpoBJPPrU0v4/IjRAhY8OCS/2O/mDJN4159YVG6SVPzKeJjOuEOFs7p8a9KHY5UY7W6keqoVosX2hHp8omczOKyg3J8Zcne9R6k0KF6QYH6qh9YdV2oGo1hnFbC4uBi5STdWIk2Kceck/DhiVdCtFo7CQsaogaDH0SumTMUPOzJ2T2uUGHKtTL2qHvcBbCXJep1mjyALUrmnRMo6yRiyvUnx0LNmKqzR+zFeuJ7+hoB4

On 05/02/2018 10:51 AM, Jose Manuel Rodriguez Caballero wrote:

Question 3: it is silly to pretend that inductive definitions need to be justified in terms of the natural numbers

Answer: In CiC the inductive definitions are given in terms of natural numbers from the beginning. This is not the case of ZFC, for example.

I disagree. It's natural to understand inductive definitions as syntax, much like the syntax of natural language, which we are built to understand (at least in spoken form). Natural numbers don't appear in that presentation at all.

I think your disagreement is going to reduce to unjustifiable philosophical axioms, which is fine, but it suggests further discussion on coq-club won't be very fruitful.

I think that Coq should have a way to invalide CiC in order to work only with Martin-Lof type theory. That will be helpful for people working in Model Theory and Foundations of Arithmetic.

Maybe so, but I believe a very small fraction of Coq users work on those subjects, and I wouldn't want Coq to become clunkier for applications in computer science, just to support those less-popular applications.

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