\documentclass[fleqn]{article}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[mathscr]{eucal}
\newcommand{\ie}{i.\,e.}
\newcommand{\eg}{e.\,g.}

\newtheorem{defn}{Defn}
\newtheorem{prop}{Prop}
\newtheorem{exer}{Exercise}

\usepackage{code}
\input{cs221-style}
\input{cs221-macros}


\begin{document}
\handout{1}{Sept 29, 2011}{Induction Tutorial}

\section{Basic concepts}

\begin{defn}[poset]
A \textbf{poset} is a structure
$\langle A, \leq \rangle$ where $A$ is a set and $\leq$ is a binary
relation on $A$, such that $\leq$ is reflexive, antisymmetric, and
transitive. (Usual derivative relations: $<$, $\ge$, $>$.)
\end{defn}

\begin{defn}[total order]
A \textbf{poset} is \textbf{totally ordered} (\emph{linearly ordered}, a \emph{chain})
if any two elements are comparable, \ie, given two elements $a$ and
$b$, either $a \le b$ or $b \le a$.
\end{defn}

\begin{defn}[well founded]
A poset $\langle A, \leq \rangle$ is \textbf{well founded} if every
non-empty subset of $A$ contains a minimal element.
\end{defn}

\begin{defn}[DCC]
A poset $\langle A, \leq \rangle$ satisfies the \textbf{Decending Chain Condition}
(DCC) if there does not exist an infinite decending chain of elements
of $A$, \ie, an infinite sequence $a_0 > a_1 > a_2 > \cdots$ where each
successive element is strictly less than its predecessor.
\end{defn}

\begin{prop}
A poset $\langle A, \leq \rangle$ is well founded iff it satisfies the
DCC.
\end{prop}

\begin{defn}[well ordered]
A poset $\langle A, \leq \rangle$ is \textbf{well ordered} if every
non-empty subset of $A$ contains a \emph{least} (or \emph{minimum}) element.
\end{defn}

\begin{prop}
A poset is well ordered iff it is well founded and totally ordered.
\end{prop}

\noindent
\textbf{Examples}: well founded posets
\begin{enumerate}
\item $\poset{\mathbb{N}}{\le}$, the natural numbers with the usual ordering
\item $\poset{\mathscr{P}(\{0,\ldots,100\})}{\subseteq}$,
  subsets of the set $\{0, \ldots, 100\}$, ordered by the subset relation.
\item $\poset{\mathbb{N}\times\mathbb{N}}{\le_L}$, where
  $\le_L$ is the \emph{lexicographical} ordering of pairs of numbers:
  $(a_1,b_1) \le_L (a_2,b_2)$ iff $a_1 < a_2$ or $a_1 = a_2$ and $b_1
  \le b_2$. 
\item $\poset{\mathbb{N}\times\mathbb{N}}{\le_P}$, where
  $\le_P$ is the \emph{pointwise} ordering of pairs of numbers:
  $(a_1,b_1) \le_P (a_2,b_2)$ iff $a_1 \le a_2$ and $b_1 \le b_2$.
\item $\poset{\mathbb{N}\cup\{\infty\}}{\le}$, the natural
  numbers extended with an infinite element $\infty$, where $n <
  \infty$ for all $n \in \mathbb{N}$ (this is the same as the ordinal
  number $\omega+1$).
\end{enumerate}

\noindent
\textbf{Examples}: non-well-founded posets
\begin{enumerate}
\item $\langle\mathbb{N},\,\ge\rangle$, the natural numbers with the
  inverse ordering.
\item $\langle\mathscr{P}(\mathbb{N}),\,\subseteq\rangle$
\item $\langle\mathscr{P}(S),\,\subseteq\rangle$ for any infinite set S.
\end{enumerate}

\begin{exer}
Let $A$ be the aphabetic characters $\{a,\ldots,z\}$ with the usual
ordering, and let $A^*$ be the set of finite strings of
characters. For $s, t \in A$, define $s \le t$ as the usual
lexicographic (\ie dictionary) ordering of strings. Is $\langle A^*,
\le\rangle$ a well founded set?
\end{exer}

\begin{exer}
Give an infinite set $S$, show how to construct an inifinite
descending chain of subsets of $S$.
\end{exer}

\section{Well Founded Induction}

The \emph{Principle of Well Founded Induction} (WFI) is defined as follows.
Given a well founded poset $\poset{A}{\le}$, and a unary relation $P$
on $A$ (in other words, a subset of $A$),
\[
\forall x . ((\forall y.\; y < x \Rightarrow P(y)) \Rightarrow P(x))
\Rightarrow \forall z. P(z)
\]
where the quantifiers are understood to range over $A$.
Saying this another way, if for any element $x \in A$, from the
\emph{induction hypothesis} $\forall y.\; y < x \Rightarrow P(y)$
(\ie, the property $P$ holds for all elements less than $x$) we can
prove that $P(x)$ holds, then $P$ holds for every element of $A$.
We can prove that WFI is true for any well founded poset.

\begin{prop}
For any well founded poset $\poset{A}{\le}$, 
\[
\forall x . ((\forall y.\; y < x \Rightarrow P(y)) \Rightarrow P(x))
\Rightarrow \forall z. P(z)   \qquad \text{(WFI)}
\]
\end{prop}
\noindent
\textbf{Proof}: Assume $P$ is some predicate satisfying the hypothesis
of the WFI formula.
\[
(1) \quad \forall x . ((\forall y.\; y < x \Rightarrow P(y)) \Rightarrow P(x))
\]
Let $S \subseteq A$ be the set of elements $a \in A$ such that
$\not P(a)$. Assume $S \neq \emptyset$, then since A is well founded,
$S$ will have a minimal element $s$, and by the definition of $S$ that
means that $\forall y.\; y < s \Rightarrow P(y)$. But then by (1),
it follows that $P(s)$, a contradiction. So $S = \emptyset$, meaning
$forall x. P(x)$.$\Box$

\noindent
\textbf{Example}. Let us use this induction principle to prove the
following statement about natural numbers.

\begin{prop}
If $n \ge 2$ then $n$ is divisible by a prime.
\end{prop}
\textbf{Proof}: Since $\poset{\mathbb{N}}{\le}$ is well founded, the Principle
of Well Founded Induction applies.  Let
\begin{equation*}
P(x) ~\equiv ~ x < 2 ~ \vee ~ \exists p \in \mathrm{Primes}.\; p | x
\end{equation*}
We want to show that 
\[
(1) \quad (\forall y.\; y < x \Rightarrow P(y)) \Rightarrow P(x)
\]
So, given an arbitrary $x \in \mathbb{N}$, we assume the \emph{Induction Hypothesis}
\[
(\mathrm{IH}) \quad \forall y.\; y < x \Rightarrow P(y)
\]
If $x < 2$ then P(x) is immediate. If $2 \le x$ and $x$ is prime, then
$x$ is divisible by a prime, namely itself. If $x$ is composite, then
$x = uv$ for some $u,v$ such that $2 \le u < x$ and $2 \le v < x$. By (IH), we
have P(u), and since $2 \le u$ we must have $p | u$ for some prime
$p$.  But then $p | x$.  So we have proved statement (1), and hence by
the Principle of Well Founded induction, we can conclude $\forall
x. P(x)$. $\Box$

\noindent
This is called a proof by \emph{course-of-values} induction or
\emph{complete} induction on the natural numbers.
A more common form of induction on the natural numbers is expressed
by the following general argument: If we can prove
\begin{eqnarray*}
(1) & & P(0) \\
(2) & & \forall n . P(n) \Rightarrow P(n+1)
\end{eqnarray*}
then we can conclude $\forall n. P(x)$.
Statement (1) is called the \emph{base} case, and (2) is the
\emph{inductive} case. Such a proof is based on the \emph{Principle of Induction over
$\mathbb{N}$} expressed as:
\[
P(0) \, \wedge \, (\forall n . P(n) \Rightarrow P(n+1)) ~ \Rightarrow
~ \forall n. P(n)
\]
Here is an example of a typical proof by induction over $\mathbb{N}$.
This should be familiar.

\begin{prop}
For any $n \in \Nat$:
\[\sum_{i=0}^n i ~ = ~ \frac{n(n + 1)}{2}
\]
\end{prop}

\noindent
\textbf{Proof}: We want to prove $\forall n. P(n)$ for the predicate
\[
P(n) ~ \equiv ~ \sum_{i=0}^n i ~ = ~ \frac{n(n + 1)}{2}
\]
The argument breaks down into two cases corresponding to the formulas
(1) and (2) above.

\noindent
\textbf{Base case}: n = 0.
We show that $P(0)$ by direct calculation:
\[
\sum_{i=0}^0 i ~ = ~ 0 ~ = \frac{0(0 + 1)}{2}
\]
Next we need to prove for an arbitrary number $m$ that $P(m)$ implies $P(m+1)$.

\noindent
\textbf{Inductive case}: n = m+1.
We assume as the \emph{Inductive Hypothesis}, $P(m)$; that is
\[
(IH) \quad \sum_{i=0}^m i ~ = ~ \frac{m(m + 1)}{2}
\]
then
\begin{alignat*}{3}
\sum_{i=0}^n i &= \left(\sum_{i=0}^m i\right) + n &&= \frac{m(m + 1)}{2} + n \quad
\text{(by IH)} \\
 && &= \frac{m(m + 1)}{2} + m + 1 \\
 && &= \frac{m(m + 1)}{2} + \frac{2m + 2}{2} \\
 && &= \frac{m^2 + 3m + 2}{2} \\
 && &= \frac{(m+1)(m+2)}{2} \\
 && &= \frac{n(n+1)}{2}
\end{alignat*}
and we have established the desired $P(n)$.

\noindent
Now the Induction Principle for $\Nat$ gives the conclusion $\forall
n. P(n)$. $\Box$

\noindent
Next we show that the Principle of Induction over $\Nat$ is
actually a consequence of the more general Principle of Well Founded Induction,
given that $\poset{\Nat}{\le}$ is a well founded poset.

\begin{prop}
For any unary predicate $P$ over $\Nat$, 
\[
P(0) ~ \wedge ~ \forall x.(P(x) \Rightarrow P(x+1)) ~ \Rightarrow
\forall x. P(x)
\]
\end{prop}
\noindent
\textbf{Proof}: We will give a stylized proof as a numbered sequence of
justified assertions.
\begin{tabbing}
\hspace{2em}\=\hspace{2em}\=\hspace{2em}\=\hspace{8cm}\= \kill
(0) $P(0) ~ \wedge ~ \forall x.(P(x) \Rightarrow P(x+1)) ~
\Rightarrow \forall x. P(x)$ \>\>\>\>TBS \\
(1) $P(0)$                                  \>\>\>\>Hypo (0)\\
(2) $\forall x.(P(x) \Rightarrow P(x+1))$   \>\>\>\>Hypo (0)\\
(3) \textbf{Lemma} $\forall x. (\forall y. y < x \Rightarrow P(y)) \Rightarrow P(x)$ \+\\
(4) Let $x \in \Nat$ \>\>\>Defn\\
(5) $\forall y. y \le x \Rightarrow P(y)$     \>\>\>Hypo (3) \\
(6) By cases on $n$ \+\\
(7) Case $x = 0$ \+\\
(8) $P(0)$                              \>(1)\\
(9) $P(x)$                              \>(8, Case defn (7))\-\\
(10) Case $x = z+1$\+\\
(11) $z < x$                          \>(defn $<$)\\
(12) $P(z)$                             \>(5)\\
(13) $P(z+1)$                          \>(2)\\
(14) $P(x)$                             \>(Case defn (10))\-\\
(15) $P(x)$                             \>\>(Cases, 8, 14)\-\\
(16) QED (3)\-\\
(17) $\forall x.P(x)$                 \>\>\>\>(3, WFI)\\
(18) QED (0)                          \>\>\>\>(17 / 1,2)
\end{tabbing}

\noindent
This streamlined style of presentation of a proof consists of numbered
statements constituing the steps of reasoning, with the justification
of each step given in the right-hand column. Some lines (\eg, (4))
introduce local variables, some introduce subcase arguments ((7),
(10)) and some introduce Lemmas ((3)).  Abbreviations are: TBS -- ``to
be shown''; Defn -- ``defining (or introducing) a local variable;
Hypo -- ``a hypothesis from the current proposition or lemma''.
The actual inference process for a given line is usually obvious,
given the earlier statements from which it is derived. For instance,
line (12) is derived by instantiating the universally quantified 
variable $y$ from line (5) with $z$ and then applying Modus Ponens with the
previous line (11). In the common case where a line derives from
the previous line, we do not explicitly mention the previous line
number in the justification.


\section{Terms}

Many computational models involve the concept of
\emph{terms}\footnote{We also use the word \emph{expressions} as
a synonym for terms.} In particular, the abstract syntax of
programming languages is typically expressed using terms, and
computational models often manipulate terms.

Informally, a term is either a constant symbol or the application of
a function symbol to a finite sequence of arguments, which are terms.
Examples expressed in conventional notation are:
\[
  A, F(A), F(G(A,B),H(C))
\]
For the moment, we are not concerned with assigning \emph{arities} to
our function symbols and requiring well-formedness with respect to
function arities, so a term like $F(F)$ will be accepted.

More formally, we can define the general universe of terms as follows:

\begin{enumerate}
\item $\mathscr{F} = \{A, B, C, \ldots, F, G, H, \ldots\}$ is a
(countable) set of function symbols. By convention we use capitalized
alphanumeric identifiers for function symbols.

\item $\mathscr{T} = \mathscr{F} \times \mathscr{T}^*$ is the set of
general terms, where $\mathscr{T}^*$ denotes the set of all finite
sequences of terms (using the Kleene star notation from regular
expression).
\end{enumerate}
We abbreviate $(A,())$ as $A$, calling this an \emph{atomic} term or \emph{constant},
and $(F, (t_1,t_2,\ldots,t_n))$ as $F(t_1,t_2,\ldots,t_n)$, called a \emph{compound}
term or function \emph{application}.

What is the meaning (\emph{semantics}) of a definition like this? We
can explain it in terms of a fixed-point construction over a universe
$U$, which we assume to be a set containing $\mathscr{F}$ and closed
under the formation of finite sequences of elements of $U$ (i.e. if
$u_1, \ldots, u_n \in U$, then $(u_1, \ldots, u_n) \in U$.\footnote{We
  take it for granted that such a universe $U$ exists, but we can
  construct such a universe set-theoretically.}

An alternate way of expressing the inductive definition of general
terms is:

\begin{enumerate}
\item $F$ is a term, for any $F \in \mathscr{F}$.
\item If $t_1, \ldots, t_n$ are terms and $F \in \mathscr{F}$ then
  $F(t_1,\ldots,t_n)$ is a term.
\item Nothiing else is a term.
\end{enumerate}
Clause 1 is the base case, clause 2 is the inductive case, and clause
3 expresses \emph{minimality}: $\mathscr{T}$ is the smallest set that
is closed with respect to clauses 1 and 2.

\noindent
We define a \emph{closure function} $\mathbf{Cl}$ on the powerset of
$U$ as follows:
\[
\mathbf{Cl} : \mathscr{P}(U) \rightarrow \mathscr{P}(U)
\]
\begin{equation}
\mathbf{Cl}(X) = \mathscr{F}\times X^*
\end{equation}
And we note that $\mathbf{Cl}(X)$ is monotonic with respect to the
subset ordering on $\mathscr{P}(U)$: $X \subseteq Y
\Longrightarrow \mathbf{Cl}(X) \subseteq \mathbf{Cl}(Y)$.
To establish that there is a set X satisfying equation (1), we will
invoke a version of the Tarski Fixed Point Theorem.

\begin{defn}[least fixed point]
If \poset{A}{\le} is a poset, and $F: A \rightarrow A$ is a function
over $A$, then $a \in A$ is a \textbf{fixed point} of $f$ if $f(a) = a$. An
element $a$ is a \textbf{least fixed point} of $f$ if $a$ is a fixed
point of $f$ and if $b$ is also a fixed point of $f$, then $a \le b$.
A point $x \in A$ is a \textbf{pre-fixed point} of $f$ if $f(x) \le x$.
\end{defn}

\noindent
The following is a specialized version of the Tarski (or
Tarski-Knaster) theorem proving the existence of least fixed points
of a monotonic function on a powerset ordered by the subset relation.

\begin{prop}[Tarski]
Given a set $S$ and a monotonic function $f: \mathscr{P}(S)
\rightarrow \mathscr{P}(S)$ over the poset
\poset{\mathscr{P}(S)}{\subseteq},
there exists a set $X \in \mathscr{P}(S)$ that is a least fixed point for $f$.
\end{prop}
\noindent
\textbf{Proof}: We will define a set $P$ as the intersection of all
pre-fixed points of $F$, and then show that $P$ is actually the least
fixed point of $F$.
\begin{tabbing}
\hspace{2em}\=\hspace{2em}\=\hspace{2em}\=\hspace{8cm}\= \kill
(1) $F$ monotonic                         \>\>\>\>Hypo\\
(2) Let $\mathit{Pre} = \{X | F(X) \subseteq X\}$\>\>\>\>Defn\\
(3) Let $P = \bigcap\mathit{Pre}$         \>\>\>\>Defn\\
(4) Let $X \in \mathit{Pre}$              \>\>\>\>Defn\+\\
(5) $F(X) \subseteq X$                    \>\>\>(pre-fixed point)\\
(6) $P \subseteq X$                       \>\>\>(intersection)\\
(7) $F(P) \subseteq F(X)$                 \>\>\>(1,6,monotonic)\\
(8) $F(P) \subseteq X$                    \>\>\>(5,7,transitivity)\-\\
(9) $\forall X \in \mathit{Pre}.\;F(P) \subseteq X$ \>\>\>\>(8,generalization)\\
(10) $F(P) \subseteq \bigcap\mathit{Pre}$ \>\>\>\>(intersection)\\
(11) $F(P) \subseteq P$                   \>\>\>\>(3)\\
(12) $F(F(P)) \subseteq F(P)$             \>\>\>\>(1,11,monotonic)\\
(13) $F(P) \in \mathit{Pre}$              \>\>\>\>(2)\\
(14) $P \subseteq F(P)$                   \>\>\>\>(intersection)\\
(15) $F(P) = P$                           \>\>\>\>(set equality)\\
(16) $P$ is a fixed-point of $F~\Box$     \\
(17) Let $Q$ be a fixed point of $F$     \>\>\>\>Defn\+\\
(18) $F(Q) = Q$                          \>\>\>(17)\\
(19) $F(Q) \subseteq Q$                  \>\>\>(set equality)\\
(20) $Q \in \mathit{Pre}$                \>\>\>(2)\\
(21) $P \subseteq Q$                     \>\>\>(3,intersection)\-\\
(22) $P$ is the least fixed point of $F$   \>\>\>\>QED
\end{tabbing}

\noindent
Now, since we know that $\mathbf{Cl}$ is monotonic, we can define the set of terms by:
\[
\mathscr{T} = \mbox{least fixed point of}~\mathbf{Cl}
\]

\noindent
This notion of term is a bit too general, since it allows all the
following to be considered valid terms (where $F \in \mathscr{F}$ is a
function symbol):
\[
F,~~F(F),~~F(F,F),~~F(F,F,F),~~\ldots
\]
We normally want a more restricted notion of terms where our function
symbols are assigned \emph{arities} (natural numbers) to specify how
many arguments they take, and we want terms to be well-formed in the
sense that they respect the assigned arities.  An assignment of
arities is called a signature, and we normally restrict ourselves to
a finite set of chosen function symbols. If we want to be explicit,
we can indicate the arity of a function symbol as a superscript. So
\[
F^2(A^0, B^0),  ~~ F^2(A^0,G^1(B^0))
\]
are legal, but 
\[
F^2, ~~ F^2(A^0),  ~~ F^2(A^0,G^1,B^0)
\]
are not well formed and are not considered valid terms.

\subsection{Another Fixed Point Construction}
\noindent
In the proof of Tarski's Theorem, the least fixed point is defined
``from the outside'' as the intersection of the set of all pre-fixed
points of $f$. Another way of defining the least fixed point is to build it
incrementally, ``from the inside''. We perform the following
construction.

\noindent
We define a sequence of sets $P_n$ as follows:
\begin{eqnarray*}
P_0 & = & \emptyset \\
P_{n+1} & = & f(P_n)
\end{eqnarray*}
Since $f$ is assumed to be monomorphic, we can prove by induction
on $n$ that $P_n \subseteq P_{n+1}$.  We define $P$ to be the union
of the sets $P_n$:
\begin{equation}
P = \bigcap_{n \in \mathbb{N}} P_n
\end{equation}
Now assume that
\begin{equation}
f(\bigcap_{n \in \mathbb{N}} P_n)= \bigcap_{n \in \mathbb{N}} f(P_n)
\end{equation}
then
\begin{equation}
f(P) = f(\bigcap_{n \in \mathbb{N}} P_n) = \bigcap_{n \in \mathbb{N}}
f(P_n) = \bigcap_{n \in \mathbb{N}} P_{n+1} = P
\end{equation}
This is a nice short argument, but the flaw is that equation (4) is
not true in all cases. However, it will be true if $f$ is
\emph{continous}.

\begin{defn}[continous]
A function $f: \mathscr{P}(S) \rightarrow \mathscr{P}(S)$ is \textbf{continous}
if for any increasing sequence of sets $A_0 \subseteq A_1 \subseteq
A_2 ~\ldots$,
\[
f(\bigcap_{n \in \mathbb{N}} A_n) = \bigcap_{n \in \mathbb{N}} f(A_n)
\]
\end{defn}
So if $f$ is continous as well as monotonic, equation (4) will hold
and we 

\noindent
Not all monotonic functions are continous, but, fortunately, there is a
useful class of continuous functions that
includes most of the closure functions occurring in our inductive definitions.
\begin{defn}[finitary function] A function $f: \mathscr{P}(S)
  \rightarrow \mathscr{P}(S)$ is \textbf{finitary} if whenever
$a \in f(A)$, there is a finite subset $A_0 \subseteq A$ such
that $a \in f(A_0)$.
\end{defn}
Now we can show the following:
\begin{prop}
If $f: \mathscr{P}(S) \rightarrow \mathscr{P}(S)$ is monotonic and
finitary, then it is continuous.
\end{prop}

\noindent
\textbf{Proof}: Exercise.

\noindent
So assuming our closure function is finitary (why is this true of
$\mathbf{Cl}$ above?), we have establised that $P$ is a fixed point of
$f$, and it remains to show that $P$ is the least fixed point.
So assume $Q$ is some other fixed point of $f$; we need to show
that $P \subseteq Q$:
\begin{tabbing}
\hspace{2em}\=\hspace{2em}\=\hspace{2em}\=\hspace{8cm}\= \kill
(0) $P \subseteq Q$                         \>\>\>\>TBS\\
(1) $f$ monotonic                           \>\>\>\>Hypo\\
(2) $f(Q) = Q$                              \>\>\>\>Hypo\\
(3) $\forall n. P_n \subseteq Q$            \>\>\>\>\textbf{Lemma}\+\\
(4) by induction on n                       \+\\
(5) Case n = 0:                             \>\>case defn\+\\
(6) $P_0 = \emptyset \subseteq Q$           \>defn $P_0$, sets\-\\
(7) Case n = m+1:                           \>\>case defn\+\\
(8) $P_m \subseteq Q$                       \> I.H.\\
(9) $f(P_m) \subseteq f(Q)$                 \> 1, 8\\
(10) $P_{m+1} \subseteq f(Q)$               \> defn $P_k$\\
(11) $P_n \subseteq f(Q)$                   \> 7\\
(12) $P_n \subseteq Q$                      \> 2\-\-\\
(13) QED 3                                  \>\>\>\-\\
(14) $\bigcup\{P_n | n \in \mathbb{N}\} \subseteq Q$  \>\>\>\>3, sets\\
(15) $P \subseteq Q$                        \>\>\>\>defn $P$\\
(16) QED 0
\end{tabbing}

\noindent
Since the least fixed point of a function is unique, these two
constructions produce the same set.  Also if $x \in P$, the least
fixed point of $f$, then we can define $\mathrm{rank}(x)$ to be the
least $n$ such that $x \in P_n$.

\subsection{Examples}
\noindent
(1) The natural numbers as terms.

\noindent
Our signature is
\[
\mathscr{F} = \{\Zero^0,\Succ^1\}
\]
where of course $\Zero^0$ represents the constant zero, and $\Succ^1$
represents the unary successor operation, and we have the
correspondence:
\begin{eqnarray*}
0 & \rightarrow & \Zero \\
1 & \rightarrow & \Succ(\Zero)\\
2 & \rightarrow & \Succ(\Succ(\Zero))\\
& \cdots
\end{eqnarray*}
The set of number terms is defined by the recursive equation
\begin{equation*}
\mathscr{N} = \{\Zero^0\} \cup (\{\Succ^1\} \times \mathscr{N})
\end{equation*}
or, $\mathscr{N}$ is the least fixed point of a closure operator
\begin{eqnarray*}
\mathbf{Cl}(X) & : & \mathscr{U} \rightarrow \mathscr{U} \\
 & = & \{\Zero^0\}\,\cup\,(\{\Succ^1\} \times X)
\end{eqnarray*}
\begin{equation*}
\mathscr{N} = \mathbf{Cl}(\mathscr{N})
\end{equation*}
$\mathbf{Cl}$ is monotonic because union and product are monotonic.
It is also finitary, since a new term is included based on at most one
precurser subterm.

\noindent
We have other standard ways of specifying the set of terms generated
inductively over a signature. It is common to use a pseudo-BNF
notation like the following:
\[
e ~ \mathrm{::=} ~ \Zero ~|~ \Succ(e)
\]
where $e$ is a metavariable ranging over the set of terms being
defined. This definition is analagous to the ML datatype declaration
\begin{code}
datatype e = Z | S of e
\end{code}

\noindent
We can define an ordering on terms in $\mathscr{N}$ derived from the
immediate subterm relation, \ie, $t\;R\;\Succ(t)$. $R$ is an \emph{acyclic
binary relation}\footnote{Binary relation $R$ is \emph{acyclic} if there is
no sequence $a = a_0 R a_1 R a_2\; \ldots\; a_{n-1} R a_n = a$, \ie,
there is no cycle in the graph generated by $R$.}
because if $t_1\;R\;t_2$ we will have $\mathrm{rank}(t_1) <
\mathrm{rank}(t_2)$, where rank is defined based on the iterative fixed
point construction as discussed above. This also means that we can
complete the $R$ relation to obtain a partial ordering $\le$ on terms by taking
reflexive, transitive closureo f $R$. This partial ordering will also
be well founded because an infinite descending chain would imply
an infinite decending chain of the corresponding ranks, which are
natural numbers, contradicting the fact that $\mathbb{N}$ is well founded. Thus
we can prove properties of terms in $\mathscr{N}$ by well founded
induction with respect to this partial ordering induced by the 
immediate subterm relation.  This ordering on terms clearly agrees with the
standard ordering on the natural numbers corresponding to the terms.

\noindent
But there is a specialized induction principle for proving that a
property $P$ holds for all terms in $\mathscr{N}$:
\[
P(\Zero) ~\wedge~ (\forall t.\, P(t) \Rightarrow P(\Succ(t)))
~\Rightarrow~ \forall t.\,P(t)
\]
As for Proposition 6, this induction principle can be proved using
the more general well founded induction principle.  The pattern for
an inductive proof then will take the following form:

\begin{quote}
Base case: $t = \Zero$\\
\hspace*{1.5em}Show $P(\Zero)$, hence $P(t)$ \\
Ind. case: $t = \Succ(u)$ \\
\hspace*{1.5em}Assume Induction Hypothesis: $P(u)$ \\
\hspace*{1.5em}Show $P(\Succ(u))$, hence $P(t)$ \\
Conclude $\forall t.\,P(t)$
\end{quote}

\end{document}

