coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Consistency of Coq ?

From: Amin Timany <amintimany AT gmail.com>
To: coq-club AT inria.fr
Cc: Bas Spitters <b.a.w.spitters AT gmail.com>
Subject: Re: [Coq-Club] Consistency of Coq ?
Date: Fri, 7 Jul 2017 10:02:58 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=amintimany AT gmail.com; spf=Pass smtp.mailfrom=amintimany AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f170.google.com
Ironport-phdr: 9a23:sZCRDhSOz3xi6yIGf/J+0P6yK9psv+yvbD5Q0YIujvd0So/mwa6zZBGN2/xhgRfzUJnB7Loc0qyN4v+mATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbF/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRBDI2/c4QAAPcPM+haoIfjqVsAqgCzChOwCOPq0DJIhmP60K883u88EQ/GxgsgH9cWvXnIqdX1NaESWv2rwqnJyDXMdfVW2Dfg44XPaB8hpPCMXbRsccrQzEkgDQXFj1WLpIzqOjOazOUNs2yB4+V8UuKvjncqpgdsqTahwccsj5PGhoMTyl3c7yp52ok0JdymSEJhZt6kCpRQuzmbN4twWMMiQntntDw0yr0coZK7ZC8KyJAnxh7DdfOIb4iI4hTiVOaIPDd3mmhpeLylhxu07EOuyfX8W9Gq3FpWqidJiNrBu3AX2xDO9MSKSeFx8lqj1DqTzwzf9PtLLVwqmafeNZIu3rE9moYWvEnDAiP6hED7g7WKekk4++Wl7uDqbqnlq5KYMoJ7lA7zP6Uhl8G6H+s1NhQBUHWe9OmzyrHj80z0TbNXhfMsiKbZqorVJcEDq665HQBV1oEj5g66Dzi80dQYmWALLVxfeB6bloTpNUzCLfLkAfuljFSslzBrx//CPrL/GJnCMn/DkLL5cbZ87U5T1hYzwMhB655IDrwNOvH+V0/ruNDFEBM0MBa4z/vlBdlhzo8eXHiAAq6dMKPcq1+I4ecvLvGWa48QuTb9LeQl5//rjXAjn18cfbKk3ZQSaH+iH/RmJ1+VbmbrgtcECWsKpBYxTPT2iF2eVj5ef2q9X6Ul5j0iFI2mCZrDSZu2jbya3Ca7G4VWaXpcBlCNF3fobYSEVO0WZCKcOM8y2gADALOmUsoq0QyknA780btuaOTOqQMCspe2/d104aXvlBQ78y08W82Y0meRTmR9mHIgSDo/3aQ5qkt4nATQmZNkiuBVQIQAr8hCVR03YNuFl7R3

Hi Bas,

It is indeed one of them. This paper establishes consistency by constructing a set theoretic model and showing the interpretation of the type false is indeed empty. Another one is Bruno Barras’ habilitation http://www.lix.polytechnique.fr/~barras/habilitation/. He proves strong normalization for CIC and all proofs are also formalized Coq itself on top of an axiomatization of IZF (Intuitionistic ZF).

It should be noted though that these are not formalizing exactly what we in Coq but they are pretty close. For example, if I’m not mistaken, neither of them considers inductive types in Prop or eta expansion.

Regards,

Amin

On 7 Jul 2017, at 09:07, Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

https://coq.inria.fr/faq
"Proofs of consistency of *subsystems* of the theory of Coq can be
found in the literature."

Is this what is intended?
Proof-irrelevant model of CC with predicative induction and judgmental equality
Lee-Werner
https://arxiv.org/abs/1111.0123

It might be good to add some references to the FAQ.

[Coq-Club] Consistency of Coq ?, Bas Spitters, 07/07/2017
- Re: [Coq-Club] Consistency of Coq ?, Amin Timany, 07/07/2017
  - Re: [Coq-Club] Consistency of Coq ?, Bas Spitters, 07/07/2017
    - Re: [Coq-Club] Consistency of Coq ?, Bas Spitters, 07/07/2017
      - Re: [Coq-Club] Consistency of Coq ?, Frédéric Blanqui, 07/07/2017