The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 10/15/2010 09:03 PM, Chris Casinghino wrote:
> Hi all,
>
> I'm curious about how much of the metatheory of Coq (or similar type
> theories) has been formalized in Coq itself.  I'm particularly
> interested in proofs of strong normalization/logical consistency.  I
> know that Barras and Werner mechanized strong normalization of CC in
> the "Coq in Coq" paper.  Has anyone done more?  In particular, has
> anyone added data types, recursion, large eliminations, or a universe
> hierarchy to these proofs?  Is there any speculation about how far one
> could get before running up against Godel?
>
>    
Hi Chris,

As you have guessed, my thesis only deals with the syntactic metatheory 
of CIC (without coinductive types), up to decidability of type-checking, 
assuming strong normalization.

Regarding strong normalization, I guess "Coq in Coq" is still the 
largest fragment of CIC formalized in Coq. Last year, I started 
formalizing set theoretical models of various type theories, starting 
from CC with universes. Since then, I have added natural numbers (with 
strong elimination) and have proved both consistency and strong 
normalization. In the consistency model, pattern-matching and fixpoint 
are separated, as in the implementation, but termination of recursive 
definitions is checked by tagging inductive types with size information 
(denoting ordinals). The normalization proof only supports the recursor, 
and it's a bit of work to model the reduction of the fixpoint operator 
alone. [see my paper in the Journal of Formalized Reasoning for the 
consistency model of CC+Nat]

I am almost done with (Brouwer) ordinals. I still need a lemma about 
cardinals, but I'd rather avoid relying on the axiom of choice (and the 
excluded-middle). Extending the results to the W type (which captures 
the full power of inductive types) should be straightforward.

Going back to your question about Godel, you could prove the consistency 
of CC with universes within ZF (Luo's thesis), so presumably in Coq 
without axiom. However, inductive types make universes much bigger, and 
Werner's "sets in types, types in sets" paper shows[*] that you probably 
need n inaccessible cardinals to model CIC with n universes. It's 
reasonable to conjecture that you can build a model of CIC with a finite 
number of universes within Coq, but this hasn't been established yet.

Bruno.

[*] in fact you need ZFC + inaccessible cardinals to model CIC + axiom 
of choice + a description axiom, but it's not clear whether you actually 
need the axiom of choice or the full power of inaccessible cardinals to 
build a model of CIC.