How to prove structural induction theorem I'm currently looking for how to prove the structural induction theorem which states that when you want to prove a statement on every elements of a set defined by induction you have to prove that each element of the base set match with the statement, and then that each rule of construction also holds the statement. I don't know how to prove that kind of induction which seems to be the root of languages definition. Any Idea ? I heard that fixed point theorem from Kleene could be useful for that.
 A: Let's make the claim precise: let $(A, (f_i)_{i\in I})$ be a set and a family of functions $f_i : A \to A$. 
Let $B\subset A$ be any subset and let $C$ be the smallest subset of $A$ containing $B$ and stable under each of the $f_i$. 
Then : 1. $C$ is well-defined.


*For any property $P$ of elements of $A$, to prove $\forall x \in C, P(x)$, it suffices to prove $\forall x\in B, P(x)$ and $\forall i \in I, \forall x \in A, P(x) \implies P(f_i(x))$.


Well for 1., it's pretty easy: $A$ is a subset of $A$ that is closed under the $f_i$'s, and so $C:=\bigcap \{ E\subset A \mid B\subset E$ and $ E$ is closed under the $f_i\}$ is well defined. It is obvious that this set is included in any subset of $A$ closed under the $f_i$, and it is also clear that $C$ itself is closed under the $f_i$'s, which establishes the claim.


*is easily established from 1: let $P$ be any such property, and assume we know $\forall x\in B, P(x)$ and $\forall i \in I, \forall x \in A, P(x) \implies P(f_i(x))$. Let $K:= \{x\in C \mid P(x)\}$. Then clearly, from the assumption, $B\subset K$. Moreover the assumption implies that $K$ is closed under the $f_i$. Therefore $C\subset K$, by definition of $C$. But by definition, $K\subset C$, so $K=C$. Therefore, $\forall x\in C, P(x)$. This establishes claim 2.


Now what you can easily see is that having the $f_i : A\to A$ or $f_i : A^{E_i} \to A$ for some $E_i$ doesn't change anything, the argument can be as easily carried out. Usually, the case will be that the $E_i$'s are some integers (for instance for propositional logic, you'll have $f_{\land} : (P,Q) \to (P\land Q)$ etc.) I'll let you prove this variant if you think that it's not so trivial. 
Now applying this to languages gives you what you want. 
EDIT: To answer to the comments below : 
Claim 1: $C$ is closed under the $f_i$'s: indeed, let $x\in C$. Then for all $E\subset A$ such that $B\subset E$ and $E$ is closed under the $f_i$'s, $x\in E$. THerefore, for all these sets, $f_i(x) \in E$. Therefore, $f_i(x)$ belongs to their intersection, which is $C$, so that $C$ is closed under the $f_i$'s.
Claim 2: $K$ is closed under the $f_i$'s. Let $x\in K$. Then by definition, $x\in C$ and $P(x)$. Therefore, since $\forall y\in A, \forall i\in I, P(y)\implies P(f_i(y))$ (that was our assumption), we have $\forall i\in I, P(x) \implies P(f_i(x))$. Therefore, since $P(x)$ is true, for all $i\in I$,$P(f_i(x))$. Moreover, by claim 1 $C$ is closed under the $f_i$ so that for all $i\in I$, $f_i(x) \in C$ and $P(f_i(x))$. But by definition this implies $f_i(x) \in K$. Therefore, $K$ is closed under the $f_i$'s
A: There is really no separate proof for that. It is really just relying on the recursive definition of a set of objects. That is, if a set of objects $S$ is defined in the folowing way:


*

*A set $A$ of 'atomic' objects is in $S$

*If objects $o_1, ... , o_n$ are in $S$ then objects $f_1(o_1,...,O_n), ...f_m(o_1,...,o_n)$ are in $S$ as well, where $f_i$ is some operator or function that maps objects to objects.

*Nothing else is in $S$ (Or: $S$ is the smallest set satisfying 1 and 2)
Then it is really just obvious that a proof by structural induction that follows this same recursion works. That is, if you can show that:


*

*All the 'atomic' objects in $A$ have some property $P$

*If objects $o_1,...,o_n$ have property $P$ then objects $f_1(o_1,...,o_n), ..., f_m(o_1,...,o_n)$ have property $P$ as well
then that will prove that all objects in $S$ have property $P$.
