# Types and Programming Languages - proof for theorem about principles of induction of terms

Types and Programming Languages book introduces a theorem about principles of induction on term (p. 31, theorem 3.3.4):

Suppose P is a predicate on terms.

Induction on depth:

If, for each term s, given P (r) for all r such that depth(r) < depth(s) we can show P(s), then P(s) holds for all s.

Proof of this theorem is left as the exercise for the reader. The solution to the exercise given in the book hints at defining a new predicate Q(n) on natural numbers such as:

∀s with depth(s) = n. P(s)

and apply the principle of complete induction on natural number (p. 19, axiom 2.4.2):

If, for each natural number n, given P(i) for all i < n we can show P(n), then P(n) holds for all n.

Since I lack experience in writing mathematical proofs, I'm struggling with applying the hint from the book and proving that theorem.

Given that:

• n = i + 1
• for all natural numbers i less than i + 1, the predicate Q(i) holds (from the induction axiom)

How do I prove that Q(n) (or Q(i + 1)) is true? Should I use depth function definition introduced previously for the simple arithmetic language?

• I'm voting to close this question as off-topic because it belongs to Mathematics. – Yuval Filmus Sep 17 '19 at 21:33

Given any set $$S$$ and any function $$f:S\to\mathbb N$$, the theorem will hold. That is, $$(\forall s\in S.(\forall r\in S.f(r) < f(s) \to P(r))\to P(s))\to \forall s\in S.P(S)$$
How useful this theorem is depends on $$f$$. For example, if $$f$$ is a constant function then this theorem simplifies to $$(\forall s\in S.P(s))\to(\forall s\in S.P(s))$$ which isn't very useful.
To prove this via complete induction, you should, as is always a helpful strategy, write out the definitions, in this case, of complete induction. Complete induction states: $$(\forall n\in\mathbb N.(\forall m\in\mathbb N.m < n\to Q(m))\to Q(n))\to\forall n\in\mathbb N.Q(n)$$
So the bulk of the task is choosing an appropriate $$Q$$ to get the result that you want. As the hint states, the fairly obvious choice is $$Q(n)\equiv\forall s\in S.f(s)=n\to P(s)$$. If you stick this $$Q$$ into the formula for complete induction, you can simplify it into the first formula. All the work comes down basically to showing that $$\forall n\in\mathbb N.\forall s\in S.f(s)=n\to P(s)\iff\forall s\in S.P(s)$$ which is a simple and purely logical exercise. Indeed, we don't even need the fact that $$\mathbb N$$ is the naturals to prove this lemma, though we do need that fact to apply complete induction for the theorem overall.