5
$\begingroup$

This question is partly motivated by an interest in foundations of mathematics, and partly by a practical interest in type theory based proof assistants.

The calculus of inductive constructions (CIC) extends the calculus of constructions (COC) with inductively defined types.

We can use these to do inductive proofs over inductively defined types.

However, it seems to me that we can do the same by instead doing inductive proofs on the basis of explicit axioms about well orderedness so that the induction happens "within" the type system rather than "next to it". I.e. induction is an explicitly defined feature of a type, in terms of propositions (also types). This seems to me to be a much more principled way of doing induction, since we are atating our assumptions more explicitly.

What is the benefit of having induction added to CoC? In particular, in the context of the foundations of mathematics, am I right that we can do with CoC what we can with CIC, and that CIC is in some sense less principled than CoC?

$\endgroup$

1 Answer 1

5
$\begingroup$

It is more powerful, induction is not derivable in CoC.

With regards to being more or less "principled", we have to strike a balance between foundational minimalism and practicality. In contrast to set theory, type theory is more concerned with practicality than minimalism. However, minimalism is still desirable when we want to study the metatheory of type theories.

The minimalist implementation of inductive types would be to assume W-types and no other inductive type, since all indexed inductive types can be reduced to W-types and the identity type. However, this is practically cumbersome, and we lose some desirable computational properties when going through the W-type encoding.

So we could use more complex encodings of inductive types which are more convenient to use, which is the way CiC is defined. In any case, it is desirable to show that more complex encodings can be reduced to minimal encodings (perhaps up to changing strict computation rules to propositional equalities).

However, if we can develop adequate metatheory of inductive types without going through a reduction to minimal basis, that's also fine! It's just that, from historical experience, not using the simplest available notion of model for a type theory makes life really difficult.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .