Transitive closure proof (Pierce, ex. 2.2.7) Simple exercise taken from the book Types and Programming Languages by Benjamin C. Pierce.
This is a definition of the transitive closure of a relation R.
First, we define the sequence of sets of pairs:
$$R_0    = R$$
$$R_{i+1}  = R_i \cup \{ (s, u) | \exists t, (s, t) \in R_i, (t, u) \in R_i \}$$
Finally, define the relation $R^+$ as the union of all the $R_i$:
$$R^+=\bigcup_i R_i$$
Show that $R^+$ is really the transitive closure of R.
Questions:


*

*I would like to see the proof (I don't have enough mathematical background to make it myself).

*Isn't the final union superfluous? Won't $R_n$ be the union of all previous sequences?


We need to show that $R^+$ contains $R$, is transitive, and is minmal among all such relations.
$R\subseteq R^+$ is clear from $R=R_0\subseteq \bigcup R_i=R^+$.
Transitivity:
By induction on $j$, show that $R_i\subseteq R_j$ if $i\le j$.
Assume $(a,b), (b,c)\in R^+$. Then $(a,b)\in R_i$ for some $i$ and $(b,c)\in R_j$ for some $j$. This implies $(a,b),(b,c)\in R_{\max(i,j)}$ and hence $(a,c)\in R_{\max(i,j)+1}\subseteq R^+$. 
Now for minimality, let $R'$ be transitive and containing $R$.
By induction show that $R_i\subseteq R'$ for all $i$, hence $R^+\subseteq R'$, as was to be shown.
As for your specific question #2:
Yes, $R_n$ contains all previous $R_k$ (a fact, the proof above uses as intermediate result). But neither is $R_n$ merely the union of all previous $R_k$, nor does there necessarily exist a single $n$ that already equals $R^+$.
For example, on $\mathbb N$ take the realtaion $aRb\iff a=b+1$. Then $aR^+b\iff a>b$, but $aR_nb$ implies that additionally $a\le b+2^n$.
