Methods

Induction

content/methods/induction/induction.tex

% Part: methods% Chapter: induction \documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olchapter{mth}{ind}{Induction}\olimport{introduction}\olimport{induction-on-N}\olimport{strong-induction}\olimport{inductive-definitions}\olimport{structural-induction}\olimport{relations}\OLEndChapterHook\end{document}

content/methods/induction/introduction.tex

% Part: methods% Chapter: induction% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mth}{ind}{int}\olsection{Introduction}Induction is an important proof technique which is used, in differentforms, in almost all areas of logic, theoretical computer science, andmathematics.  It is needed to prove many of the results in logic.Induction is often contrasted with deduction, and characterized as theinference from the particular to the general.  For instance, if weobserve many green emeralds, and nothing that we would call an emeraldthat's not green, we might conclude that all emeralds are green. Thisis an inductive inference, in that it proceeds from many particularcases (this emerald is green, that emerald is green, etc.) to ageneral claim (all emeralds are green).  \emph{Mathematical} inductionis also an inference that concludes a general claim, but it is of avery different kind than this ``simple induction.''Very roughly, an inductive proof in mathematics concludes that allmathematical objects of a certain sort have a certain property.  Inthe simplest case, the mathematical objects an inductive proof isconcerned with are natural numbers.  In that case an inductive proofis used to establish that all natural numbers have some property, andit does this by showing that\begin{enumerate}    \item $0$ has the property, and    \item whenever a number~$k$ has the property, so does~$k+1$.\end{enumerate}Induction on natural numbers can then also often be used to provegeneral claims about mathematical objects that can be assigned numbers. Forinstance, finite sets each have a finite number~$n$ of elements, andif we can use induction to show that every number~$n$ has the property``all finite sets of size~$n$ are \dots'' then we will have shownsomething about all finite sets.Induction can also be generalized to mathematical objects that are\emph{inductively defined}.  For instance, expressions of a formallanguage such as those of first-order logic are defined inductively.\emph{Structural induction} is a way to prove results about all suchexpressions.  Structural induction, in particular, is veryuseful---and widely used---in logic.\end{document}

content/methods/induction/induction-on-N.tex

% Part: methods% Chapter: induction% Section: induction-on-N\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mth}{ind}{inN}\olsection{Induction on~$\Nat$}In its simplest form, induction is a technique used to prove resultsfor all natural numbers. It uses the fact that by starting from $0$and repeatedly adding~$1$ we eventually reach every natural number. Soto prove that something is true for every number, we can (1)~establishthat it is true for $0$ and (2)~show that whenever it is true for anumber~$n$, it is also true for the next number~$n+1$.  If weabbreviate ``number~$n$ has property $P$'' by $P(n)$ (and ``number~$k$has property $P$'' by $P(k)$, etc.), then a proof by induction that$P(n)$ for all $n \in \Nat$ consists of:\begin{enumerate}\item a proof of $P(0)$, and\item a proof that, for any~$k$, if $P(k)$ then $P(k+1)$.\end{enumerate}To make this crystal clear, suppose we have both (1) and~(2).  Then(1) tells us that $P(0)$ is true.  If we also have~(2), we know inparticular that if $P(0)$ then $P(0+1)$, i.e., $P(1)$. This followsfrom the general statement ``for any~$k$, if $P(k)$ then $P(k+1)$'' byputting~$0$ for~$k$. So by modus ponens, we have that~$P(1)$. From (2)again, now taking $1$ for~$n$, we have: if $P(1)$ then~$P(2)$. Sincewe've just established~$P(1)$, by modus ponens, we have~$P(2)$. And soon.  For any number~$n$, after doing this $n$~times, we eventuallyarrive at~$P(n)$.  So (1) and~(2) together establish~$P(n)$ for any $n\in \Nat$.Let's look at an example.  Suppose we want to find out how manydifferent sums we can throw with $n$ dice.  Although it might seemsilly, let's start with $0$ dice.  If you have no dice there's only onepossible sum you can ``throw'': no dots at all, which sums to~$0$. Sothe number of different possible throws is~$1$. If you have only onedie, i.e., $n=1$, there are six possible values, $1$ through~$6$. Withtwo dice, we can throw any sum from $2$ through $12$, that's $11$possibilities.  With three dice, we can throw any number from $3$ to$18$, i.e., $16$ different possibilities.  $1$, $6$, $11$, $16$: lookslike a pattern: maybe the answer is $5n+1$?  Of course, $5n+1$ is themaximum possible, because there are only $5n+1$ numbers between $n$,the lowest value you can throw with $n$ dice (all $1$'s) and $6n$, thehighest you can throw (all $6$'s).\begin{thm}  With $n$ dice one can throw all $5n+1$ possible values between $n$  and $6n$.\end{thm}\begin{proof}Let $P(n)$ be the claim: ``It is possible to throw any number between$n$ and~$6n$ using $n$~dice.''  To use induction, we prove:\begin{enumerate}\item The \emph{induction basis} $P(1)$, i.e., with just one die,  you can throw any number between $1$ and $6$.\item The \emph{induction step}, for all $k$, if $P(k)$ then~$P(k+1)$.\end{enumerate}(1) Is proved by inspecting a $6$-sided die. It has all 6 sides, andevery number between $1$ and~$6$ shows up one on of the sides. So itis possible to throw any number between $1$ and~$6$ using a singledie.To prove (2), we assume the antecedent of the conditional, i.e.,$P(k)$. This assumption is called the \emph{inductive hypothesis}.  Weuse it to prove~$P(k+1)$. The hard part is to find a way of thinkingabout the possible values of a throw of $k+1$ dice in terms of thepossible values of throws of $k$~dice plus of throws of the extra$k+1$-st die---this is what we have to do, though, if we want to usethe inductive hypothesis.The inductive hypothesis says we can get any number between $k$and~$6k$ using $k$~dice.  If we throw a~$1$ with our $(k+1)$-st die,this adds $1$ to the total. So we can throw any value between $k+1$and $6k+1$ by throwing $k$~dice and then rolling a~$1$ with the$(k+1)$-st die.  What's left?  The values $6k+2$ through $6k+6$.  Wecan get these by rolling $k$ $6$s and then a number between $2$ and$6$ with our $(k+1)$-st die. Together, this means that with $k+1$ dicewe can throw any of the numbers between $k+1$ and $6(k+1)$, i.e.,we've proved~$P(k+1)$ using the assumption~$P(k)$, the inductivehypothesis.\end{proof}Very often we use induction when we want to prove something about aseries of objects (numbers, sets, etc.) that is itself defined``inductively,'' i.e., by defining the $(n+1)$-st object in terms ofthe $n$-th.  For instance, we can define the sum~$s_n$ of the naturalnumbers up to~$n$ by\begin{align*}  s_0 & = 0\\  s_{n+1} & = s_n + (n+1)\end{align*}This definition gives:\begin{align*}  s_0 & = 0,\\  s_1 & = s_0 + 1 && = 1,\\  s_2 & = s_1 + 2 && = 1 + 2 = 3\\  s_3 & = s_2 + 3 && = 1 + 2 + 3 = 6, \text{ etc.}\end{align*}Now we can prove, by induction, that $s_n = n(n+1)/2$.\begin{prop}  $s_n = n(n+1)/2$.\end{prop}\begin{proof}  We have to prove (1) that $s_0 = 0\cdot(0 + 1)/2$ and (2) if $s_k =  k(k+1)/2$ then $s_{k+1} = (k+1)(k+2)/2$.  (1) is obvious. To prove  (2), we assume the inductive hypothesis: $s_k = k(k+1)/2$. Using it,  we have to show that $s_{k+1} = (k+1)(k+2)/2$.  What is $s_{k+1}$?  By the definition, $s_{k+1} = s_k + (k+1)$.  By  inductive hypothesis, $s_k = k(k+1)/2$. We can substitute this into  the previous equation, and then just need a bit of arithmetic of  fractions:  \begin{align*}    s_{k+1} & = \frac{k(k+1)}{2} + (k+1) = {}\\    & = \frac{k(k+1)}{2} + \frac{2(k+1)}{2} = {}\\    & = \frac{k(k+1) + 2(k+1)}{2} = {}\\    & = \frac{(k+2)(k+1)}{2}.  \end{align*}\end{proof}The important lesson here is that if you're proving something aboutsome inductively defined sequence $a_n$, induction is the obvious wayto go. And even if it isn't (as in the case of the possibilities ofdice throws), you can use induction if you can somehow relate the casefor~$k+1$ to the case for~$k$.\end{document}

content/methods/induction/strong-induction.tex

% Part: methods% Chapter: induction% Section: strong-induction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mth}{ind}{str}\olsection{Strong Induction}In the principle of induction discussed above, we prove $P(0)$ andalso if $P(k)$, then $P(k+1)$.  In the second part, we assume that$P(k)$ is true and use this assumption to prove $P(k+1)$.Equivalently, of course, we could assume $P(k-1)$ and use it to prove$P(k)$---the important part is that we be able to carry out theinference from any number to its successor; that we can prove theclaim in question for any number under the assumption it holds for itspredecessor.There is a variant of the principle of induction in which we don'tjust assume that the claim holds for the predecessor $k-1$ of $k$, butfor all numbers smaller than~$k$, and use this assumption to establishthe claim for~$k$. This also gives us the claim $P(n)$ for all~$n \in\Nat$.  For once we have established $P(0)$, we have therebyestablished that $P$ holds for all numbers less than~$1$.  And if weknow that if $P(l)$ for all $l<k$, then $P(k)$, we know this inparticular for $k=1$.  So we can conclude $P(1)$.  With this we haveproved $P(0)$ and $P(1)$, i.e., $P(l)$ for all $l<2$, and sincewe have also the conditional, if $P(l)$ for all $l<2$, then $P(2)$, wecan conclude~$P(2)$, and so on.In fact, if we can establish the general conditional ``for all $k$, if$P(l)$ for all $l<k$, then $P(k)$,'' we do not have to establish$P(0)$ anymore, since it follows from it.  For remember that a generalclaim like ``for all $l<k$, $P(l)$'' is true if there are no $l<k$.This is a case of vacuous quantification: ``all $A$s are $B$s'' istrue if there are no $A$s, $\lforall[x][(!A(x) \lif !B(x))]$ is trueif no $x$ satisfies~$!A(x)$. In this case, the formalized versionwould be ``$\lforall[l][(l < k \lif P(l))]$''---and that is true ifthere are no $l < k$.  And if $k=0$ that's exactly the case: no $l<0$,hence ``for all $l<0$, $P(0)$'' is true, whatever $P$ is.  A proof of``if $P(l)$ for all $l<k$, then $P(k)$'' thus automaticallyestablishes~$P(0)$.This variant is useful if establishing the claim for~$k$ can't be madeto just rely on the claim for $k-1$ but may require the assumptionthat it is true for one or more $l<k$.  \end{document}

content/methods/induction/inductive-definitions.tex

% Part: methods% Chapter: induction% Section: inductive-definitions\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mth}{ind}{idf}\olsection{Inductive Definitions}In logic we very often define kinds of objects \emph{inductively},i.e., by specifying rules for what counts as an object of the kind tobe defined which explain how to get new objects of that kind from oldobjects of that kind.  For instance, we often define special kinds ofsequences of symbols, such as the terms and !!{formula}s of alanguage, by induction.  For a simple example, consider stringsconsisting of letters $\mathrm{a}$, $\mathrm{b}$, $\mathrm{c}$,$\mathrm{d}$, the symbol~$\circ$, and brackets $[$ and $]$, such as``$[[\mathrm{c} \circ \mathrm{d}][$'', ``$[\mathrm{a}[]\circ]$'',``$\mathrm{a}$'' or ``$[[\mathrm{a} \circ \mathrm{b}]\circ\mathrm{d}]$''.  You probably feel that there's something``wrong'' with the first two strings: the brackets don't``balance'' at all in the first, and you might feel that the``$\circ$'' should ``connect'' expressions that themselves makesense. The third and fourth string look better: for every ``$[$''there's a closing ``$]$'' (if there are any at all), and for any$\circ$ we can find ``nice'' expressions on either side,surrounded by a pair of parentheses.We would like to precisely specify what counts as a ``nice term.''First of all, every letter by itself is nice.  Anything that's notjust a letter by itself should be of the form ``$[t \circ s]$'' where$s$ and $t$ are themselves nice. Conversely, if $t$ and $s$ are nice,then we can form a new nice term by putting a $\circ$ between them andsurround them by a pair of brackets.  We might use these operationsto \emph{define} the set of nice terms.  This is an \emph{inductive  definition}.\begin{defn}[Nice terms]  The set of \emph{nice terms} is inductively defined as follows:  \begin{enumerate}  \item Any letter $\mathrm{a}$, $\mathrm{b}$, $\mathrm{c}$,    $\mathrm{d}$ is a nice term.  \item If $s_1$ and $s_2$ are nice terms, then so    is $[s_1 \circ s_2]$.  \item Nothing else is a nice term.  \end{enumerate}\end{defn}This definition tells us that something counts as a nice term iff itcan be constructed according to the two conditions (1) and~(2) in somefinite number of steps. In the first step, we construct all nice termsjust consisting of letters by themselves, i.e.,\[\mathrm{a}, \mathrm{b}, \mathrm{c}, \mathrm{d}\]In the second step, we apply (2) to the terms we've constructed. We'll get\[[\mathrm{a} \circ \mathrm{a}], [\mathrm{a} \circ \mathrm{b}],[\mathrm{b} \circ \mathrm{a}], \dots, [\mathrm{d} \circ \mathrm{d}]\]for all combinations of two letters. In the third step, we apply (2)again, to any two nice terms we've constructed so far. We get new niceterm such as $[\mathrm{a} \circ [\mathrm{a} \circ    \mathrm{a}]]$---where $t$ is $\mathrm{a}$ from step~1 and $s$ is$[\mathrm{a} \circ \mathrm{a}]$ from step~2---and $[[\mathrm{b} \circ    \mathrm{c}] \circ [\mathrm{d} \circ \mathrm{b}]]$ constructed outof the two terms $[\mathrm{b} \circ \mathrm{c}]$ and $[\mathrm{d}  \circ \mathrm{b}]$ from step~2. And so on.  Clause (3) rules outthat anything not constructed in this way sneaks into the set of niceterms.Note that we have not yet proved that every sequence of symbols that``feels'' nice is nice according to this definition. However, itshould be clear that everything we can construct does in fact ``feelnice'': brackets are balanced, and $\circ$ connects parts that arethemselves nice.The key feature of inductive definitions is that if you want to provesomething about all nice terms, the definition tells you which casesyou must consider.  For instance, if you are told that $t$ is a niceterm, the inductive definition tells you what $t$ can look like: $t$can be a letter, or it can be $[s_1 \circ s_2]$ for some pair ofnice terms $s_1$ and~$s_2$. Because of clause (3), those are the onlypossibilities.When proving claims about all of an inductively defined set, thestrong form of induction becomes particularly important. For instance,suppose we want to prove that for every nice term of length~$n$, thenumber of $[$ in it is~$< n/2$.  This can be seen as a claim aboutall~$n$: for every $n$, the number of $[$ in any nice term oflength~$n$ is $< n/2$.\begin{prop}  For any $n$, the number of $[$ in a nice term of length~$n$ is  $< n/2$.\end{prop}\begin{proof}To prove this result by (strong) induction, we have to show that thefollowing conditional claim is true:\begin{quote}  If for every $l < k$, any nice term of length~$l$ has $< l/2$  $[$'s, then any nice term of length~$k$ has $< k/2$ $[$'s.\end{quote}To show this conditional, assume that its antecedent is true, i.e.,assume that for any $l<k$, nice terms of length~$l$ contain $< l/2$$[$'s.  We call this assumption the inductive hypothesis. We want toshow the same is true for nice terms of length~$k$.So suppose $t$ is a nice term of length~$k$.  Because nice terms areinductively defined, we have two cases: (1)~$t$ is a letter byitself, or (2)~$t$ is $[s_1 \circ s_2]$ for some nice terms $s_1$ and~$s_2$.\begin{enumerate}\item $t$ is a letter.  Then $k = 1$, and the number of $[$ in $t$is~$0$. Since $0 < 1/2$, the claim holds.\item $t$ is $[s_1 \circ s_2]$ for some nice terms $s_1$ and~$s_2$.  Let's let $l_1$ be the length of~$s_1$ and $l_2$ be the length  of~$s_2$.  Then the length~$k$ of $t$ is $l_1+l_2+3$ (the lengths of  $s_1$ and $s_2$ plus three symbols $[$, $\circ$, $]$). Since  $l_1+l_2+3$ is always greater than $l_1$, $l_1 < k$. Similarly, $l_2  < k$. That means that the induction hypothesis applies to the terms  $s_1$ and~$s_2$: the number~$m_1$ of $[$ in $s_1$ is $< l_1/2$, and  the number~$m_2$ of $[$ in~$s_2$ is $< l_2/2$.  The number of $[$ in $t$ is the number of $[$ in~$s_1$, plus the  number of $[$ in~$s_2$, plus~$1$, i.e., it is $m_1 + m_2 + 1$. Since $m_1  < l_1/2$ and $m_2 < l_2/2$ we have:  \[  m_1 + m_2 + 1 < \frac{l_1}{2} + \frac{l_2}{2} + 1 = \frac{l_1+l_2+2}{2} < \frac{l_1+l_2+3}{2} = k/2.  \]\end{enumerate}In each case, we've shown that the number of $[$ in $t$ is $< k/2$ (onthe basis of the inductive hypothesis). By strong induction, theproposition follows.\end{proof}\begin{prob}  Define the set of supernice terms by  \begin{enumerate}  \item Any letter $\mathrm{a}$, $\mathrm{b}$, $\mathrm{c}$,    $\mathrm{d}$ is a supernice term.  \item If $s$ is a supernice term, then so is $[s]$.  \item If $s_1$ and $s_2$ are supernice terms, then so    is $[s_1 \circ s_2]$.  \item Nothing else is a supernice term.  \end{enumerate}  Show that the number of $[$ in a supernice term~$t$ of length~$n$ is    $\le n/2 +1$.\end{prob}\end{document}

content/methods/induction/structural-induction.tex

% Part: methods% Chapter: induction% Section: structural-induction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mth}{ind}{sti}\olsection{Structural Induction}So far we have used induction to establish results about all naturalnumbers. But a corresponding principle can be used directly to proveresults about all !!{element}s of an inductively defined set.  Thisoften called \emph{structural} induction, because it depends on thestructure of the inductively defined objects.Generally, an inductive definition is given by (a)~a list of``initial'' !!{element}s of the set and (b)~a list of operations whichproduce new !!{element}s of the set from old ones. In the case of niceterms, for instance, the initial objects are the letters. We only haveone operation: the operations are\begin{align*}  o(s_1, s_2) = & [s_1 \circ s_2]\end{align*}You can even think of the natural numbers~$\Nat$ themselves as beinggiven by an inductive definition: the initial object is~$0$, and theoperation is the successor function~$x + 1$.In order to prove something about all elements of an inductivelydefined set, i.e., that every !!{element} of the set has aproperty~$P$, we must:\begin{enumerate}\item Prove that the initial objects have~$P$\item Prove that for each operation~$o$, if the arguments have~$P$,  so does the result.\end{enumerate}For instance, in order to prove something about all nice terms, wewould prove that it is true about all letters, and that it is trueabout $[s_1 \circ s_2]$ provided it is true of $s_1$ and $s_2$individually.\begin{prop}  The number of $[$ equals the number of $]$ in any nice term~$t$.\end{prop}\begin{proof}We use structural induction.  Nice terms are inductively defined, withletters as initial objects and the operation $o$ for constructing newnice terms out of old ones.\begin{enumerate}\item The claim is true for every letter, since the number of $[$ in a  letter by itself is~$0$ and the number of $]$ in it is also~$0$.\item Suppose the number of $[$ in $s_1$ equals the number of $]$, and  the same is true for $s_2$. The number of $[$ in $o(s_1, s_2)$, i.e., in    $[s_1 \circ s_2]$, is the sum of the number of $[$ in $s_1$ and      $s_2$ plus one. The number of $]$ in $o(s_1, s_2)$ is the sum of the number    of $]$ in $s_1$ and $s_2$ plus one. Thus, the number of $[$ in $o(s_1, s_2)$    equals the number of $]$ in $o(s_1,s_2)$.\end{enumerate}\end{proof}\begin{prob}  Prove by structural induction that no nice term starts with~$]$.\end{prob}Let's give another proof by structural induction: a proper initialsegment of a string~$t$ of symbols is any string~$s$ that agrees with$t$ symbol by symbol, read from the left, but $t$ is longer. So,e.g., $[a \circ {}$ is a proper initial segment of $[a \circ b]$, butneither are $[b \circ {}$ (they disagree at the second symbol) nor $[a\circ b]$ (they are the same length).\begin{prop}\ollabel{prop:initial}  Every proper initial segment of a nice term~$t$ has more $[$'s than    $]$'s.\end{prop}\begin{proof}  By induction on~$t$:  \begin{enumerate}  \item $t$ is a letter by itself: Then $t$ has no proper initial segments.  \item $t = [s_1 \circ s_2]$ for some nice terms $s_1$ and~$s_2$. If $r$ is    a proper initial segment of $t$, there are a number of    possibilities:    \begin{enumerate}    \item $r$ is just $[$: Then $r$ has one more $[$ than it does~$]$.    \item $r$ is $[r_1$ where $r_1$ is a proper initial segment      of~$s_1$: Since $s_1$ is a nice term, by induction hypothesis, $r_1$      has more $[$ than $]$ and the same is true for $[r_1$.    \item $r$ is $[s_1$ or $[s_1 \circ {}$: By the previous result, the      number of $[$ and $]$ in~$s_1$ are equal; so the number of $[$      in $[s_1$ or $[s_1 \circ {}$ is one more than the number of~$]$.    \item $r$ is $[s_1 \circ r_2$ where $r_2$ is a proper initial segment      of~$s_2$:  By induction hypothesis, $r_2$ contains more $[$ than      $]$. By the previous result, the number of $[$ and of      $]$ in~$s_1$ are equal. So the number of $[$ in $[s_1 \circ r_2$      is greater than the number of~$]$.    \item $r$ is $[s_1 \circ s_2$: By the previous result, the number of      $[$ and $]$ in $s_1$ are equal, and the same for~$s_2$. So there      is one more $[$ in $[s_1 \circ s_2$ than there are~$]$.    \end{enumerate}  \end{enumerate}\end{proof}\end{document}

content/methods/induction/relations.tex

% Part: methods% Chapter: induction% Section: relations\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mth}{ind}{rel}\olsection{Relations and Functions}When we have defined a set of objects (such as the natural numbers orthe nice terms) inductively, we can also define \emph{relations on}these objects by induction.  For instance, consider the followingidea: a nice term~$t_1$ is a subterm of a nice term~$t_2$ if it occurs asa part of it.  Let's use a symbol for it: $t_1 \sqsubseteq t_2$. Everynice term is a subterm of itself, of course: $t \sqsubseteq t$. We cangive an inductive definition of this relation as follows:\begin{defn}  The relation of a nice term~$t_1$ being a subterm of~$t_2$, $t_1  \sqsubseteq t_2$, is defined by induction on~$t_2$ as follows:  \begin{enumerate}  \item If $t_2$ is a letter, then $t_1 \sqsubseteq t_2$ iff $t_1 = t_2$.  \item If $t_2$ is $[s_1 \circ s_2]$, then $t_1 \sqsubseteq t_2$ iff $t_1 =    t_2$, $t_1 \sqsubseteq s_1$, or $t_1 \sqsubseteq s_2$.  \end{enumerate}\end{defn}This definition, for instance, will tell us that $\mathrm{a}\sqsubseteq [\mathrm{b} \circ \mathrm{a}]$. For (2) says that$\mathrm{a} \sqsubseteq [\mathrm{b} \circ \mathrm{a}]$ iff $\mathrm{a}= [\mathrm{b} \circ \mathrm{a}]$, or $\mathrm{a} \sqsubseteq b$, or$\mathrm{a} \sqsubseteq \mathrm{a}$. The first two are false:$\mathrm{a}$ clearly isn't identical to $[\mathrm{b} \circ  \mathrm{a}]$, and by~(1), $\mathrm{a} \sqsubseteq \mathrm{b}$ iff$\mathrm{a} = \mathrm{b}$, which is also false. However, also by~(1),$\mathrm{a} \sqsubseteq \mathrm{a}$ iff $\mathrm{a} = \mathrm{a}$,which is true.It's important to note that the success of this definition depends ona fact that we haven't proved yet: every nice term~$t$ is either aletter by itself, or there are \emph{uniquely determined} nice terms$s_1$ and $s_2$ such that $t = [s_1 \circ s_2]$.  ``Uniquelydetermined'' here means that if $t = [s_1 \circ s_2]$ it isn't\emph{also} $= [r_1 \circ r_2]$ with $s_1 \neq r_1$ or $s_2 \neq r_2$.If this were the case, then clause~(2) may come in conflict withitself: reading $t_2$ as $[s_1 \circ s_2]$ we might get $t_1\sqsubseteq t_2$, but if we read $t_2$ as $[r_1 \circ r_2]$ we mightget not $t_1 \sqsubseteq t_2$.  Before we prove that this can'thappen, let's look at an example where it \emph{can} happen.\begin{defn}  Define \emph{bracketless terms} inductively by  \begin{enumerate}  \item Every letter is a bracketless term.    \item If $s_1$ and $s_2$ are bracketless terms, then $s_1 \circ s_2$ is      a bracketless term.    \item Nothing else is a bracketless term.  \end{enumerate}\end{defn}Bracketless terms are, e.g., $\mathrm{a}$, $\mathrm{b} \circ\mathrm{d}$, $\mathrm{b} \circ \mathrm{a} \circ \mathrm{b}$. Now if wedefined ``subterm'' for bracketless terms the way we did above, thesecond clause would read\begin{center}  If $t_2 = s_1 \circ s_2$, then $t_1 \sqsubseteq t_2$ iff $t_1 = t_2$, $t_1  \sqsubseteq s_1$, or $t_1 \sqsubseteq s_2$.\end{center}Now $\mathrm{b} \circ \mathrm{a} \circ \mathrm{b}$ is of the form $s_1\circ s_2$ with \begin{align*}  s_1 & = \mathrm{b} \text{ and} & s_2 & = \mathrm{a} \circ \mathrm{b}.\intertext{It is also of the form $r_1 \circ r_2$ with}  r_1 & = \mathrm{b} \circ \mathrm{a} \text{ and} & r_2 &= \mathrm{b}.\end{align*}Now is $\mathrm{a} \circ \mathrm{b}$ a subterm of $\mathrm{b} \circ\mathrm{a} \circ \mathrm{b}$?  The answer is yes if we go by the firstreading, and no if we go by the second.The property that the way a nice term is built up from other niceterms is unique is called \emph{unique readability}. Since inductivedefinitions of relations for such inductively defined objects areimportant, we have to prove that it holds.\begin{prop}  Suppose $t$ is a nice term. Then either $t$ is a letter by itself,  or there are uniquely determined nice terms $s_1$, $s_2$ such that~$t =  [s_1 \circ s_2]$.\end{prop}\begin{proof}  If $t$ is a letter by itself, the condition is satisfied. So assume  $t$ isn't a letter by itself. We can tell from the inductive  definition that then $t$ must be of the form $[s_1 \circ s_2]$ for some  nice terms $s_1$ and~$s_2$. It remains to show that these are uniquely  determined, i.e., if $t = [r_1 \circ r_2]$, then $s_1 = r_1$ and $s_2 = r_2$.  So suppose $t = [s_1 \circ s_2]$ and also $t = [r_1 \circ r_2]$ for nice terms  $s_1$, $s_2$, $r_1$, $r_2$. We have to show that $s_1 = r_1$ and $s_2 = r_2$.  First, $s_1$ and $r_1$ must be identical, for otherwise one is a proper  initial segment of the other. But by \olref[sti]{prop:initial}, that  is impossible if $s_1$ and~$r_1$ are both nice terms.  But if $s_1 = r_1$,  then clearly also $s_2 = r_2$.\end{proof}We can also define functions inductively: e.g., we can define thefunction~$f$ that maps any nice term to the maximum depth of nested$[\dots]$ in it as follows:\begin{defn}  \ollabel{defn:depth} The \emph{depth} of a nice term, $f(t)$, is  defined inductively as follows:  \[  f(t) = \begin{cases}    0 & \text{ if $t$ is a letter}\\    \max(f(s_1), f(s_2)) + 1 & \text{ if $t = [s_1 \circ s_2]$.}  \end{cases}  \]\end{defn}For instance\begin{align*}  f([\mathrm{a} \circ \mathrm{b}]) & =     \max(f(\mathrm{a}),f(\mathrm{b})) + 1 = \\   &= \max(0, 0) + 1 = 1, \text{ and}\\  f([[\mathrm{a} \circ \mathrm{b}] \circ \mathrm{c}]) & =     \max(f([\mathrm{a} \circ \mathrm{b}]), f(\mathrm{c})) + 1 = \\   & = \max(1,0) + 1 = 2.\end{align*}Here, of course, we assume that $s_1$ an $s_2$ are nice terms, and makeuse of the fact that every nice term is either a letter or of the form$[s_1 \circ s_2]$. It is again important that it can be of this form inonly one way. To see why, consider again the bracketless terms wedefined earlier. The corresponding ``definition'' would be:\[  g(t) =   \begin{cases}    0 & \text{ if $t$ is a letter}\\   \max(g(s_1), g(s_2)) + 1 & \text{ if $t = s_1 \circ s_2$.}  \end{cases}\]Now consider the bracketless term $\mathrm{a} \circ \mathrm{b} \circ\mathrm{c} \circ \mathrm{d}$. It can be read in more than one way,e.g., as $s_1 \circ s_2$ with \begin{align*}  s_1 & = \mathrm{a} \text{ and} &   s_2 & = \mathrm{b} \circ \mathrm{c} \circ \mathrm{d},\intertext{or as $r_1 \circ r_2$ with}  r_1 & = \mathrm{a} \circ b \text{ and} &   r_2 &= \mathrm{c} \circ \mathrm{d}.\end{align*}Calculating $g$ according to the first way of reading it would give\begin{align*}  g(s_1 \circ s_2) & =  \max(g(\mathrm{a}), g(\mathrm{b} \circ \mathrm{c} \circ \mathrm{d})) + 1 =\\ & =  \max(0,2) + 1 = 3  \intertext{while according to the other reading we get}  g(r_1 \circ r_2) & =  \max(g(\mathrm{a} \circ \mathrm{b}), g(\mathrm{c} \circ \mathrm{d})) + 1=\\ &  = \max(1,1) + 1 = 2\end{align*}But a function must always yield a unique value; so our ``definition''of~$g$ doesn't define a function at all.\begin{prob}  Give an inductive definition of the function $l$, where $l(t)$ is  the number of symbols in the nice term~$t$.\end{prob}\begin{prob}  Prove by structural induction on nice terms $t$ that $f(t) < l(t)$ (where  $l(t)$ is the number of symbols in~$t$ and $f(t)$ is the depth of  $t$ as defined in \olref[mth][ind][rel]{defn:depth}).\end{prob}\end{document}