Fixing typos and adding notes

Fixing some typos and adding notes about proofs in the chapters on
representation in Q and the incompleteness theorems.

Author: seanrsinclair

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

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$,

incompleteness/arithmetization-syntax/coding-symbols.tex

@@ -64,7 +64,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/incompleteness-provability/lob-thm.tex

@@ -35,7 +35,7 @@
 \item Let $X$ be the sentence, ``If $X$ is true, then Santa Claus
   exists.''
 \item Suppose $X$ is true.
-\item Then what is says is true; i.e., if $X$ is true, then
+\item Then what it says is true; i.e., if $X$ is true, then
   Santa Claus exists.
 \item Since we are assuming $X$ is true, we can conclude that
   Santa Claus exists.
@@ -68,7 +68,7 @@
 & \OProv[T](\gn{!D}) \lif !A \\
 & !D && \text{def of $!D$} \\
 & \OProv[T](\gn{!D}) && \text{by 1} \\
-& !A \\
+& !A
 \end{align*}
 \end{proof}
 

incompleteness/incompleteness-provability/provability-conditions.tex

@@ -51,7 +51,7 @@
 describe the relevant formal proofs. Clauses 1 and 2 are easy; it is
 really clause 3 that requires work. (Think about what kind of work it
 entails\dots) Carrying out the details would be tedious and
-uninteresting, so here we will ask you to take it on faith the
+uninteresting, so here we will ask you to take it on faith that
 $\Th{PA}$ has the three properties listed above. A reasonable choice
 of $\OProv[PA](y)$ will also satisfy
 \begin{enumerate}
@@ -65,7 +65,7 @@
 being now. At the end of the 1931 paper, he sketches the proof of the
 second incompleteness theorem, and promises the details in a later
 paper. He never got around to it; since everyone who understood the
-argument believed that it could be carried out, he did not need to
+argument believed that it could be carried out (he did not need to
 fill in the details.)
 \end{digress}
 

incompleteness/incompleteness-provability/rosser-thm.tex

@@ -11,7 +11,7 @@
 \olsection{Rosser's Theorem}
 
 Can we modify G\"odel's proof to get a stronger result, replacing
-``$\omega$-consistent'' with simply ``consistent''?? The answer is
+``$\omega$-consistent'' with simply ``consistent''? The answer is
 ``yes,'' using a trick discovered by Rosser. Let $\fn{not}(x)$ be the
 primitive recursive function which does the following: if $x$ is the
 code of a formula $!A$, $\fn{not}(x)$ is a code of $\lnot !A$.  To
@@ -48,6 +48,7 @@
 assumption of $\omega$-consistency.)
 
 \begin{digress}
+% This comment doesn't make much sense, what are you trying to get at?
 By comparison to the proof of
 \olref[tcp][inc]{thm:first-incompleteness}, the proofs of
 \olref[1in]{thm:first-incompleteness} and its improvement by Rosser

incompleteness/incompleteness-provability/tarski-thm.tex

@@ -58,7 +58,7 @@
 \[
 H = \Setabs{x}{\Sat{N}{\lexists[y][!D_T(\num e, \num x, y)]}},
 \]
-so $\lexists[y][!D_T(\num e, x, y)]$ defines~$H$ is $\Struct{N}$. 
+so $\lexists[y][!D_T(\num e, x, y)]$ defines~$H$ in $\Struct{N}$. 
 \end{proof}
 
 \begin{prob}
@@ -94,7 +94,7 @@
 `Snow is white' is true if and only if snow is white.
 \end{quote}
 However, for any language strong enough to represent the diagonal
-function, and any linguistic predicate $T(x)$, and can construct a
+function, and any linguistic predicate $T(x)$, we can construct a
 sentence $X$ satisfying ``$X$ if and only if not $T(\text{`$X$'})$.''
 Given that we do not want a truth predicate to declare some sentences
 to be both true and false, Tarski concluded that one cannot specify a

incompleteness/representability-in-q/beta-function.tex

@@ -49,7 +49,7 @@
 same remainder when divided by $c$.
 \end{defn}
 
-Here is the \emph{Chinese remainder theorem}:
+Here is the \emph{Chinese Remainder theorem}:
 \begin{thm}
 Suppose $x_0,\dots,x_n$ are (pairwise) relatively prime. Let
 $y_0$, \dots, $y_n$ be any numbers. Then there is a number $z$ such that
@@ -61,7 +61,7 @@
 \end{eqnarray*}
 \end{thm}
 
-Here is how we will use the Chinese remainder theorem: if
+Here is how we will use the Chinese Remainder theorem: if
 $x_0,\dots,x_n$ are bigger than $y_0,\dots,y_n$ respectively, then
 we can take $z$ to code the sequence $\langle y_0,\dots,y_n\rangle$. To recover
 $y_i$, we need only divide $z$ by $x_i$ and take the remainder. To use
@@ -113,13 +113,14 @@
 We can then show that all of the following are in $C$:
 \begin{enumerate}
 \item The pairing function, $J(x,y) = \frac{1}{2}[(x+y)(x+y+1)] + x$
+% maybe explain more what is going on here, a bit confusing.
 \item Projections 
 \[
-K(z) = \mu {x \leq q} \; (\lexists[y \leq z][z = J(x,y)])
+K(z) = \mu {x \leq q} \; (\lexists[y \leq z] \, [z = J(x,y)])
 \]
 and
 \[
-L(z) = \mu {y \leq q} \; (\lexists[x \leq z][z = J(x,y)]).
+L(z) = \mu {y \leq q} \; (\lexists[x \leq z]\, [z = J(x,y)]).
 \]
 \item $x < y$
 \item $x \mid y$
@@ -146,7 +147,7 @@
 \]
 and let $d_1 = j\fac$. By the observations above, we know that $1+d_1,
 1+2 d_1, \dots, 1+(n+1) d_1$ are relatively prime and all are bigger
-than $a_0,\dots,a_n$. By the Chinese remainder theorem there is a
+than $a_0,\dots,a_n$. By the Chinese Remainder theorem there is a
 value $d_0$ such that for each $i$,
 \[
 d_0 \equiv a_i \mod (1+(i+1)d_1)
@@ -155,7 +156,7 @@
 \[
 a_i = \fn{rem}(1+(i+1)d_1,d_0).
 \]
-Let $d = J((d)_0,(d)_1)$. Then for each $i$ from $0$ to $n$, we have
+Let $d = J(d_0,d_1)$. Then for each $i$ from $0$ to $n$, we have
 \begin{eqnarray*}
 \beta(d,i) & = & \beta^*(d_0,d_1,i) \\
 & = & \fn{rem}(1+(i+1) d_1,d_0) \\

incompleteness/representability-in-q/c-representable.tex

@@ -49,7 +49,7 @@
 requires some care. Note also that although we are using induction, it
 is induction \emph{outside} of $\Th{Q}$.
 
-We will be able to represent zero, successor, plus, times, and the
+We will be able to represent zero, successor, plus, times, the
 characteristic function for equality, and projections. In each case,
 the appropriate representing function is entirely straightforward; for
 example, zero is represented by the formula
@@ -97,7 +97,7 @@
 like to find a formula $!A_f(\vec z,y)$ representing $f$. Here is
 a natural choice:
 \[
-!A_f(\vec z,y) \ident !A_g(y,\vec z,0) \land \lforall[w][(w < z
+!A_f(\vec z,y) \ident !A_g(y,\vec z,0) \land \lforall[w][(w < y
 \lif \lnot !A_g(w,\vec z,0))].
 \]
 

incompleteness/representability-in-q/c.tex

@@ -20,7 +20,7 @@
 \end{enumerate}
 and closed under
 \begin{enumerate}
-\item composition and
+\item composition, and
 \item unbounded search, applied to regular
 functions. 
 \end{enumerate}