Admissible rules in dependent type theory

Question

From the nlab article on Martin-Löf dependent type theory:

The weakening and substitution rules are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations.

Similarly, exercise E2.7 from the classic article "Syntax and Semantics of Dependent Types" by Martin Hofmann:

Show that for any type theory containing some or all of the type formers described above the rules Weak and Subst are admissible.

This was actually where, coming from the mathematical side, I prematurely ended my last incursion into type theory.

Now, in the hope to establish an entry point for anyone in a similar position: There must be a clear write-up of this somewhere, as it seems pointless to continue into type theory without having solved a point as fundamental as that. Is it just me or is this really nowhere to be found on the net?

I would appreciate answers demonstrating the admissibility of the aforementioned rules, or pointers to relevant sources. This is less about the results for their own sake than about seeing type theory at work supporting itself before serving as a foundation for other things. The scarcity (?) of hands-on demonstrations in this vein seems a major roadblock to entering the field, at least trustwise. It could be removed easily by material just plainly showing how these fundamental aspects are handled at a basic level (one that should really be routine for a seasoned type theorist?). Thanks!

Answer 1

I disagree with the premise that not having a full proof of the admissibility of substitution spelt out anywhere is a "major roadblock" to entering the field of type theory, at least as a user; but anyway, the reason it is not usually spelt out is that it is incredibly tedious and devoid of any mathematical content. Whether substitution is built-in or admissible is nothing more than an implementation detail.

As an example, assume we have $\Gamma \vdash t : X$, and let us try to prove that type substitution is admissible, i.e.

$$\frac{\Gamma, x : X, \Delta \vdash T\text{ type}}{\Gamma, \Delta[t/x] \vdash T[t/x]\text{ type}}$$

We proceed by structural induction on the premise. Let us only look at one case: the formation rule for dependent pair types, which has the following form here.

$$\frac{\Gamma, x : X, \Delta \vdash A\text{ type} \quad \Gamma, x : X, \Delta, a : A \vdash B\text{ type}}{\Gamma, x : X, \Delta \vdash \sum\limits_{a : A} B\text{ type}}$$

The induction hypothesis gives us the substituted judgements

$$\Gamma, \Delta[t/x] \vdash A[t/x]\text{ type} \qquad \Gamma, \Delta[t/x], a : A[t/x] \vdash B[t/x]\text{ type}$$

whence we conclude by the formation rule for dependent pair types

$$\Gamma, \Delta[t/x] \vdash \sum_{a : A[t/x]} B[t/x]\text{ type}$$

and that's it. It might seem like we haven't done anything at all, but it's useful to have in mind that (and how) alternative presentations of type theory can fail to have admissible substitution.

For instance, the nLab page on dependent sum types gives the following introduction rule:

$$\frac{\Gamma \vdash A\text{ type} \quad \Gamma, a : A \vdash B\text{ type}}{\Gamma, a : A, b : B \vdash (a, b) : \sum\limits_{a : A} B}$$

instead of the more conventional

$$\frac{\Gamma \vdash A\text{ type} \quad \Gamma, a : A \vdash B\text{ type} \quad \Gamma \vdash u : A \quad \Gamma \vdash v : B[u/a]}{\Gamma \vdash (u, v) : \sum\limits_{a : A} B}$$

effectively restricting the pair constructor to variables. In this presentation, term substitution is not admissible, so we would have to add a built-in substitution rule.

Indeed, if we tried the same proof by induction as above, we would need to unify $\Gamma, x : X, \Delta$ with $\Gamma, a : A, b : B$; this is fine as long as $a$ and $b$ end up in $\Delta$, but if $x = a$ or $x = b$ then the proof can't go through. Intuitively, substituting $t$ for $a$ or $b$ in $(a, b)$ would now result in an ill-typed term unless $t$ is a variable.

Answer 2

The proofs you are asking for are rarely found in published papers, at least not detailed versions, because an experienced reader is able to reconstruct them easily enough. They always proceed by some sort of structural induction, usually on the derivation of the judgement. The trickiest bit, always, is how to strengthen the induction hypothesis. That is, the statement we usually want to prove cannot be proven directly by induction, instead one looks for a sligthly stronger statement that does. (For instance in Naïm's answer he strengthened the substitution rule so that also part of the context undergoes a substitution, which is necessary as soon as one considers a rule that introduces a new variable into the context in one of its premises.)

The place to look are PhD theses, these more commonly contain detailed proofs. My student Philipp Haselwarter produced detailed proofs for a wide class of type theories, see Effective Metatheory for Type Theory:

• Admissibility of weakening is Proposition 2.2.2. Note that when Philipp says that "most cases are straightforward" this actually means that by the time you write them down you also see that they hold because nothing is going on, one literally just applies the induction hypothesis.
• Admissibility of substitution is in Section 2.1.1.1. This is more complicated, it's a whole section.
• There are other admissibility results, for example, if you can derive that $e$ has type $A$, then you should be able to derive that $A$ is a type, yes? That's Theorem 2.2.18.

This is not the only thesis containing such results (although I would be hard pressed to point to another one that achieves this level of generality), it's just one that I know well, as an advisor. We can go one step further and ask for formalized proofs of admissibility etc. I am not sure a comprehensive library is available, if someone knows of one, I'd like to know too.

But most importantly, Naïm has a point. Wittgensteing wrote:

6.54 My propositions are elucidatory in this way: he who understands me finally recognizes them as senseless, when he has climbed out through them, on them, over them. (He must so to speak throw away the ladder, after he has climbed up on it.) He must surmount these propositions; then he sees the world rightly.

To bring this down to earth and closer to the present case: yes, it is elucidatory to work out the details of the syntax of type theory and belabor the syntactic meta-theorems involving renamings and substitution – but these are just a "ladder" one climbs to arrive at a better, mathematically more meaningful, understanding of what type theory is and how it works. So, after reading Philipp's thesis, you should read Ambrus Kaposi's thesis, and Jon Sterling's thesis, too :-)