Fixing typos and adding notes about proofs

Fixing several typos in the chapters on recursive functions and
arithmetization of syntax.  Also including some notes on various proofs
which might need to be changed.

Author: seanrsinclair

computability/recursive-functions/bounded-minimization.tex

@@ -26,7 +26,7 @@
 
 In case the bound is $y + 1$ we have three cases: (a) There is an $x <
 y$ such that $R(x, \vec{z})$, in which case $m_R(y+1, \vec{z}) =
-m_R(y, \vec{z})$. (b) There is no such~$x$ but $R(y, \vec{z})$, then
+m_R(y, \vec{z})$. (b) There is no such~$x$ but $R(y, \vec{z})$ holds, then
 $m_R(y+1, \vec{z}) = y$. (c) There is no $x < y+1$ such that $R(x,
 \vec{z})$, then $m_R(y+1,\vec{z}) = 0$. So,
 \begin{align*}

computability/recursive-functions/halting-problem.tex

@@ -74,11 +74,11 @@
 possible cases, 0 and 1.
 \begin{enumerate}
 \item If $h(e_d, e_d) = 1$ then $\cfind{e_d}(e_d) \defined$.  But
-  $\cfind{e_d} = d$, and $d(e_d)$ is defined iff $h(e_d, e_d) = 0$.
+  $\cfind{e_d} \simeq d$, and $d(e_d)$ is defined iff $h(e_d, e_d) = 0$.
   So $h(e_d, e_d) \neq 1$.
 \item If $h(e_d, e_d) = 0$ then either $e_d$ is not the index of a
   partial recursive function, or it is and $\cfind{e_d}(e_d)
-  \undefined$. But again, $\cfind{e_d} = d$, and $d(e_d)$ is undefined
+  \undefined$. But again, $\cfind{e_d} \simeq d$, and $d(e_d)$ is undefined
   iff $\cfind{e_d}(e_d) \defined$.
 \end{enumerate}
 The upshot is that $e_d$ cannot, after all, be the index of a partial

computability/recursive-functions/normal-form.tex

@@ -11,7 +11,7 @@
 
 \begin{thm}[Kleene's Normal Form Theorem]
 \ollabel{thm:kleene-nf}
-There are a primitive recursive relation $T(e, x, s)$ and a primitive
+There is a primitive recursive relation $T(e, x, s)$ and a primitive
 recursive function $U(s)$, with the following property: if $f$ is any
 partial recursive function, then for some~$e$,
 \[

computability/recursive-functions/partial-functions.tex

@@ -23,7 +23,7 @@
 
 The way out is to allow \emph{partial} functions to come into play. We
 will see that it \emph{is} possible to enumerate the partial
-computable functions.\iftag{TMs}{in fact, we already pretty much know
+computable functions.\iftag{TMs}{ In fact, we already pretty much know
   that this is the case, since it is possible to enumerate Turing
   machines in a systematic way.}{} We will come back to our diagonal
 argument later, and explore why it does not go through when partial
@@ -48,7 +48,7 @@
 is defined at $x$, i.e., $x$ is in the domain of $f$; and $f(x)
 \undefined$ to mean the opposite, i.e., that $f$ is not defined at~$x$.
 We will use $f(x) \simeq g(x)$ to mean that either $f(x)$ and $g(x)$
-are both undefined, or they are both defined and equal. We will these
+are both undefined, or they are both defined and equal. We will use these
 notations for more complicated terms as well. We will adopt the
 convention that if $h$ and $g_0$, \dots,~$g_k$ all are partial functions,
 then

computability/recursive-functions/sequences.tex

@@ -12,7 +12,7 @@
 The set of primitive recursive functions is
 remarkably robust. But we will be able to do even more once we have
 developed an adequate means of handling \emph{sequences}.  We will
-identify finite sequences of natural numbers with natural numbers, in
+identify finite sequences of natural numbers with natural numbers in
 the following way: the sequence $\langle a_0, a_1, a_2, \dots, a_k \rangle$
 corresponds to the number
 \[
@@ -67,15 +67,15 @@
 $(s)_0$, \dots,~$(s)_{k-1}$.
 
 It will be useful for us to be able to bound the numeric code of a
-sequence, in terms of its length and its largest element. Suppose $s$
+sequence in terms of its length and its largest element. Suppose $s$
 is a sequence of length $k$, each element of which is less than equal
 to some number $x$. Then $s$ has at most $k$ prime factors, each at
 most $p_{k-1}$, and each raised to at most $x+1$ in the prime
 factorization of $s$. In other words, if we define
 \[
 \fn{sequenceBound}(x,k) = p_{k-1}^{k \cdot (x+1)},
 \]
-then the numeric code of the sequence~$s$ described above, is at
+then the numeric code of the sequence~$s$ described above is at
 most~$\fn{sequenceBound}(x,k)$.
 
 Having such a bound on sequences gives us a way of defining new

incompleteness/arithmetization-syntax/coding-formulas.tex

@@ -24,6 +24,7 @@
 \]
 \item there are $z_1, z_2 < x$ such that $x = z_1 \concat \Gn{\eq}
   \concat \eq z_2$ and $\fn{Term}(z_1)$ and $\fn{Term}(z_2)$.
+% Missing the case for bottom
 \end{enumerate}
 \end{proof}
 

incompleteness/arithmetization-syntax/coding-symbols.tex

@@ -44,6 +44,7 @@
 \item If $s$ is the $i$-th variable $\Obj x_i$, then $\scode s = \tuple{1, i}$.
 \item If $s$ is the $i$-th $n$-ary !!{constant}~$\Obj c_i^n$, then
   $\scode s = \tuple{2, n, i}$.
+% n-ary constant symbols?
 \item If $s$ is the $i$-th $n$-ary !!{function}~$\Obj f_i^n$, then
   $\scode s = \tuple{3, n, i}$.
 \item If $s$ is the $i$-th $n$-ary !!{predicate}~$\Obj P_i^n$, then

incompleteness/arithmetization-syntax/coding-terms.tex

@@ -35,7 +35,7 @@
 \item $s_i$ is a variable~$\Obj v_j$, or
 \item $s_i$ is a !!{constant}~$\Obj c_j$, or
 \item $s_i$ is built from $n$ terms $t_1$, \dots, $t_n$ occurring
-  prior to place~$i$ in using an $n$-place function symbol~$\Obj f^n_j$.
+  prior to place~$i$ using an $n$-place function symbol~$\Obj f^n_j$.
 \end{enumerate}
 To show that the corresponding relation on G\"odel numbers is
 primitive recursive, we have to express this condition primitive

incompleteness/arithmetization-syntax/proofs-in-lk.tex

@@ -41,7 +41,7 @@
   \Gn{\Pi''}}$ if $\Pi$ ends in an inference with two premises, $k$ is
   given by the following table according to which rule was used in the
   last inference, and $\Pi'$, $\Pi''$ are the the immediate subproof
-  ending in the laft and right premise of the last inference,
+  ending in the left and right premise of the last inference,
   respectively.
 
 \begin{tabular}{lcccc}
@@ -80,7 +80,7 @@
 variable~$x$ and a closed term~$t$ such that $\Gamma = \Gamma'$,
 $\Subst{!A}{t}{x} \in \Delta'$, $\lexists[x][!A] \in \Delta$, and for
 every $!B \in \Delta$, either $!B = \lexists[x][!A]$ or $!B \in
-\Gamma'$.  We just have to translate into G\"odel numbers.  If $s =
+\Delta'$.  We just have to translate into G\"odel numbers.  If $s =
 \Gn{\Gamma \Sequent \Delta}$ then $(s)_0 = \Gn{\Gamma}$ and $(s)_1 =
 \Gn{\Gamma}$. So:
 \begin{align*}

incompleteness/arithmetization-syntax/substitution.tex

@@ -10,7 +10,7 @@
 \olsection{Substitution}
 
 \begin{prop}
-There is a primitive recursive function $\fn{Subst}(x, y, z)$ with
+There is a primitive recursive function $\fn{Subst}(x, y, z)$ with the property that
 \[
 \fn{Subst}(\Gn{!A}, \Gn{t}, \Gn{x}) = \Gn{\Subst{!A}{t}{x}}
 \]
@@ -23,6 +23,7 @@
 recursive.  We can then define a function $\fn{Subst}'$ by primitive
 recursion as follows:
 
+% Also need to ensure that y is free for z in x as well.
 \begin{align*}
 \fn{Subst}'(0, x, y, z) & = \emptyseq \\
 \fn{Subst}'(i + 1, x, y, z) & =