Question on inductive {definitions, proof}

Consider the following inductive definition:

Define the set $\Lambda$ as follows (where the $\langle x, y, z\rangle$ denote ordered triples):

1. if $n \in \mathbb{N},$ then $\langle 0, n, n\rangle \in \Lambda \;$;
2. if $n \in \mathbb{N}$ and $x \in \Lambda$ then $\langle 1, n, x \rangle \in \Lambda \;$;
3. if $x, y \in \Lambda$, then $\langle 2, x, y \rangle \in \Lambda$.

Now define the function $\ell:\Lambda \to \mathbb{N}$ recursively as follows:

1. $\ell(\langle 0, n, n \rangle) = 1, \forall \; n \in \mathbb{N}$;
2. $\ell(\langle 1, n, x \rangle) = 1 + \ell(x), \forall \; n \in \mathbb{N}$ and $x \in \Lambda$;
3. $\ell(\langle 2, x, y \rangle) = \ell(x) + \ell(y), \forall \; x, y \in \Lambda$.

It is obvious that $\ell(x) > 0, \forall \; x \in \Lambda$, but I don't know how to prove it. It looks like a case for proof by induction, but induction on what?

Thanks!

-
– Zhen Lin Dec 25 '11 at 1:09

What you want is known as structural induction, or more vaguely as "the induction principle implied by the inductive definition".

The crucial point is that every element of $\Lambda$ is there by virtue of one of your three rules -- this is sometimes hinted at by a fourth rule reading: "Nothing else is in $\Lambda$". Your inductive definition is really shorthand for the following set-theoretic construction:

• Given any set $A$, define $$\Phi(A) = \{\langle 0,n,n\rangle\mid n\in \mathbb N\} \cup (\{1\}\times \mathbb N \times A) \cup (\{2\}\times A\times A)$$
• Let $A_0=\varnothing$ and $A_{n+1}=\Phi(A_n)$ for all $n\ge 0$.
• Let $\Lambda$ be the union of all $A_n$. In other words $\Lambda=\bigcup_{n\in \mathbb N}A_n$.

Now, the structural induction principle says: In order to prove that some property holds for all $x\in\Lambda$ it suffices to prove for an arbitrary $A$ that if all $x\in A$ has the property, then the property holds for all $a\in\Phi(A)$.

This can principle can be justified by ordinary mathematical induction on $n$ for the statement that the property holds for every $x\in A_n$. When this is true for all $n$, then since every $x\in\Lambda$ is in some $A_n$, the property holds for every such $x$.

-
@kjo: To put it a little more colorfully, you can think of the $n$ at which a member of $\Lambda$ first appears in Henning’s construction as its ‘birthday’. The induction is then on the birthdays of the elements of $\Lambda$: if $\ell(x)>0$ for every $x$ whose birthday precedes $n$, then the construction of $\Lambda$ ensures that $\ell(x)>0$ for every $x$ whose birthday is $n$. – Brian M. Scott Dec 25 '11 at 1:59
@Henning: Perhaps you should also say something about why we don't need the full power of transfinite/well-founded induction here. (It has to do with the fact that all the constructors are finitary.) – Zhen Lin Dec 25 '11 at 4:34