Inductive definition of terms in "The Calculus of Constructions"

Question

I'm reading the paper "The Calculus of Constructions" by Thierry Coquand and Gerard Huet, and I'm having trouble with their inductive definition of $\Lambda$, starting on the second page. When I think of induction I usually think of there being a base step and an induction step. I'm not sure what either would be in this case.

What strikes me as most bizarre is the quantification rule: $$[x:M]N \in \Lambda_0^n \text{ if } M \in \Lambda^n, N \in \Lambda_0^{n+1}$$ So the definition of $\Lambda^n_0$ is in terms of $\Lambda^{n+1}_0$, which is then defined in terms of $\Lambda^{n+2}_0$ and so on. I'd think that an inductive definition of $\Lambda^n_0$ defines it in terms of $\Lambda^{n-1}_0$ and a base case $\Lambda^n_0$ but this can't be whats intended. I'm not sure then what the induction is supposed to be here at all.

I've noticed there are a lot more complicated inductive definitions in logic/computer science (e.g. BNF notation to define pre-terms of the lambda calculus) and I've always felt rather awkward carrying out those arguments. It's difficult to distinguish poor notation and not actually understanding it, so if Its relevant I'm also wondering how you go about these proofs/definitions in a systematic way.

Answer 1

An inductive type is defined with a list of 'constructors', that are simply rules specifying how to build terms of the type, either from scratch, or using previously built terms.

Here $\Lambda$ is defined together with $\Lambda_0^n$ and $\Lambda_1^n$ for all $n$ , with a list of rules given in page 2 and 3 of the article.

The rule $variables$ shows you how to build some terms for all $\Lambda_1^n$; the rule $universe$ shows you how to build some terms for all $\Lambda_0^n$. So with these 2 rules you can define terms of $\Lambda^n$.

Now you have a way to apply the $quantification$ rule, using a term $M$ of $\Lambda^n$, and a term $N$ of $\Lambda_0^{n+1}$. This will give you a new term of $\Lambda_0^n$, and therefore of $\Lambda^n$. And so on... As you see, it is perfectly possible to build a term of $\Lambda_0^n$ using a previously built term of $\Lambda_0^{n+1}$ !

By combining the different constructors in all the possible ways, you define 'the' terms of $\Lambda$ "by induction".