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: Freek Wiedijk <freek AT cs.ru.nl>
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 22:56:06 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=freek AT cs.ru.nl; spf=Pass smtp.mailfrom=freek AT cs.ru.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:9cYNqRISzs8Uf+nO3tmcpTZWNBhigK39O0sv0rFitYgQI/7xwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhikHOTAn7W/ZicJwg61Hrx28pRNwzZXZYJ2JOPdkYq/RYckXSXRHU81MVyJBGIS8b44XAuQBJ+ZXsZfyp1gTphS+BAmjGv7gyj5Khn/1wKY31OohERvY0wM+HNIDq2jbrM7vOKcITOC51q/IzTHaYv5QxDzz65DIfwg8rfyCQL58a9fdxEsgGg/fk1mdqJbpMy6a2+kDq2SW7PRsWfirhmMosQ18rDiiyt0yhoXXhY8YzE3P+z9jz4YvP9K4TVZ2Yd66H5tUsCGXL5B2QsY+Q2FwpSo20KYGtoK6fCcUzpQo2wDQZ+adc4iV+B7jUuKRLS95hHJjZr2/mw6//VWux+HhTMW4zVRHoyVfntXRt30BzQHf58eJR/dl+0euwzeP1wTd6uFeJkA0kLLWK5A7wrEuiJUTsl/OETPtmEnslq+Wa18o+u6s6+j/eLXpuoecN5NoigH5Kqkhhsu/Af0hPgcSW2ib5P+z2ab4/Uz5RbVKluc5nrPYsJDcP8Qbp7S2DxVb0oY5uF6DCGKt181dln0aJnpEfgiGhs7nIQLgOvf9WNmljlmv2AhqyvzHPL6pVpvXI3XAuLz6O6xgrUhYnllghetD7o5ZX+lSaMn4XVX84YSBX00JdjesyuOiM+1Tk4YXWGaBGKicafuAukTO/P9pJe3ePdZJ6ga4EOAs4rvVtVF8gUUUJPH71oBRcm3+GPA0exzEM0qpuc8IFCIxhiR7TOHujwfbAyVWe27rGbk35zw9A4/gF5qFQIT/2LE=

Hi Pierre,

>But it is still just a matter of being careful right? You can
>always reencode a logical system (say S) inside your preferred
>one (say T, more expressive than S) as a regular first class
>definition.

To give this a little twist: is a classical proof that
a constructive proof exists just as good as having a
constructive proof? Or does the latter give you something
extra?

Freek

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