Using structural induction to show derivablity

Question

To prove a judgement is derivable by induction on it's derivation tree seems circular to me. From what I understand, structural induction works by proving a property $P$ for the base case of the tree (in this case axioms) and then showing it propagates along the tree. If $P$ is derivabilty though, by the definition of the derivation tree, every step is already derivable, so how is using induction any different to just finding the derivation tree for a judgement? All the examples I see are for properties not directly related to the construction of the tree, but provable for it's constructors. In this case it is definitionally true for the constructors?

This question arises from trying to prove weakening is admissible in dependent type theory. Specifically, to prove the following by using induction simultaneously on the if clauses:

• If $(\Gamma, \Delta)$ ctx is derivable, then $(\Gamma, x:X, \Delta)$ ctx is derivable;

• If $\Gamma, \Delta \vdash A$ type is derivable, then $\Gamma, x:X, \Delta \vdash A$ type is derivable;

• If $\Gamma, \Delta \vdash u:A$ is derivable, then $\Gamma, x:X, \Delta \vdash u:A$is derivable;

• If $\Gamma, \Delta \vdash A = B$ type is derivable, then $\Gamma, x:X, \Delta \vdash A = B$ is derivable;

• If $\Gamma, \Delta \vdash u = v: A$ type is derivable, then $\Gamma, x:X, \Delta \vdash u = v: A$.

Answer 1

When you prove a claim by structural induction, that claim must quantify over all of the instances of that structure. This is often done implicitly, but if you're having trouble I recommend that you get in the habit of making it explicit each time.

Here is how it would work in this example.

For every derivation $D$:

• If $D$ is $(\Gamma, \Delta) \text{ ctx}$, then $(\Gamma, x:X, \Delta) \text{ ctx}$ is derivable.
• If $D$ is $\Gamma, \Delta \vdash A \text{ type}$, then $\Gamma, x:X, \Delta \vdash A \text{ type}$ is derivable
• etc.

The induction is on the structure of $D$. In the induction steps, you can use the induction hypothesis on the sub-derivations.

---

Another possibility is to rephrase it in terms of natural numbers.

For every natural number $n$: If $D$ is a derivation using $n$ derivation steps, then:

• If $D$ is $(\Gamma, \Delta) \text{ ctx}$, then $(\Gamma, x:X, \Delta) \text{ ctx}$ is derivable.
• If $D$ is $\Gamma, \Delta \vdash A \text{ type}$, then $\Gamma, x:X, \Delta \vdash A \text{ type}$ is derivable
• etc.

Here the induction on $n$ is just the usual induction on natural numbers (which can also be seen as structural induction). Then, since any derivation uses some number of steps, the previous claim consequently holds.