Merge branch 'seanrsinclair-master'

Author: rzach

computability/recursive-functions/bounded-minimization.tex

@@ -21,12 +21,12 @@
 \end{prop}
 
 \begin{proof}
-Note than there can be no~$x < y$ such that $R(x, \vec{z})$ since
-there is no $x < y$ at all.  So $m_R(x, 0) = 0$.
+Note than there can be no~$x < 0$ such that $R(x, \vec{z})$ since
+there is no $x < 0$ at all.  So $m_R(x, 0) = 0$.
 
 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

@@ -11,7 +11,7 @@
 
 The \emph{halting problem} in general is the problem of deciding,
 given the specification~$e$ (e.g., program) of a computable function
-and a number~$n$, whether the computation of the function on input~$e$
+and a number~$n$, whether the computation of the function on input~$n$
 halts, i.e., produces a result.  Famously, Alan Turing proved that
 this problem itself cannot be solved by a computable function, i.e.,
 the function
@@ -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/non-pr-functions.tex

@@ -42,7 +42,7 @@
 essentially the function $G(x) = g_x(x)$, and one can show that this
 grows faster than any primitive recursive function.
 
-Let use return to the issue of enumerating the primitive recursive
+Let us return to the issue of enumerating the primitive recursive
 functions. Remember that we have assigned symbolic notations to each
 primitive recursive function; so it suffices to enumerate
 notations. We can assign a natural number $\#(F)$ to each notation $F$,

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

@@ -16,14 +16,20 @@
 
 \begin{proof}
 The number $x$ is the G\"odel number of an atomic !!{formula} iff
+one of the following holds:
 \begin{enumerate}
-\item there are $n$, $j < x$, and $z < x$ such that for each $i < n$,
+\item There are $n$, $j < x$, and $z < x$ such that for each $i < n$,
   $\fn{Term}((z)_i)$ and
 \[
-x = \Gn{\Obj P^n_j(} \concat \fn{flatten}(z) \concat \Gn{)} \text{, or}
+x = \Gn{\Obj P^n_j(} \concat \fn{flatten}(z) \concat \Gn{)}.
 \]
-\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)$.
+\item There are $z_1, z_2 < x$ such that $\fn{Term}(z_1)$,
+  $\fn{Term}(z_2)$, and 
+\[
+x = z_1 \concat \Gn{\eq} \concat z_2.
+\]
+  \tagitem{prvFalse}{$x = \Gn{\lfalse}$.}{}
+  \tagitem{prvTrue}{$x = \Gn{\ltrue}$.}{}
 \end{enumerate}
 \end{proof}
 

incompleteness/arithmetization-syntax/coding-symbols.tex

@@ -42,8 +42,8 @@
 \end{array}
 \]
 \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}$.
+\item If $s$ is the $i$-th !!{constant}~$\Obj c_i^n$, then
+  $\scode s = \tuple{2, i}$.
 \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
@@ -63,7 +63,7 @@
 \end{prop}
 
 \begin{defn}
-If $\tuple{s_0, \dots, s_n}$ is a sequence of symbols, its
+If $s_0, \dots, s_n$ is a sequence of symbols, its
 \emph{G\"odel number} is $\tuple{\scode{s_0}, \dots, \scode{s_n}}$.
 \end{defn}
 

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*}