typos reported by W25 Logic III students

Author: rzach

content/computability/computability-theory/computable-sets.tex

@@ -35,7 +35,7 @@
 confused!{} \iftag{TMs}{The Turing machine computing a partial function
   returns the output of the function, for input values at which the
   function is defined; the Turing machine computing a set returns
-  either 1 or 0, after deciding whether or not the input value is in
+  either $1$ or~$0$, after deciding whether or not the input value is in
   the set or not.}{}
 \end{explain}
 

content/computability/computability-theory/introduction.tex

@@ -11,7 +11,7 @@
 
 The branch of logic known as \emph{computability theory} deals with
 issues having to do with the computability, or relative computability,
-of functions and sets. It is a evidence of Kleene's influence
+of functions and sets. It is evidence of Kleene's influence
 that the subject used to be known as \emph{recursion theory}, and
 today, both names are commonly used.
 

content/computability/computability-theory/normal-form.tex

@@ -26,7 +26,7 @@
 
 \begin{thm}[Kleene's Normal Form Theorem]
 \ollabel{thm:normal-form}
-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 computable function, then for some~$e$,
 \[

content/computability/recursive-functions/composition.tex

@@ -10,10 +10,9 @@
 \olsection{Composition}
 
 If $f$ and $g$ are two one-place functions of natural numbers, we can
-compose them: $h(x) = g(f(x))$. The new
-function~$h(x)$ is then defined by \emph{composition} from the
-functions $f$ and~$g$. We'd like to generalize this to functions of
-more than one argument.
+compose them: $h(x) = f(g(x))$. The new function~$h(x)$ is then
+defined by \emph{composition} from the functions $f$ and~$g$. We'd
+like to generalize this to functions of more than one argument.
 
 Here's one way of doing this: suppose $f$ is a $k$-place function,
 and $g_0$, \dots, $g_{k-1}$ are $k$ functions which are all

content/computability/recursive-functions/sequences.tex

@@ -66,8 +66,8 @@
     1 + \bmin{i < s}{R(i, s)} & \text{otherwise}
   \end{cases}
   \]
-  We can use bounded minimization, since there is only one $i$ that
-  satisfies $R(s, i)$ when $s$ is a code of a sequence, and if $i$
+  We can use bounded minimization here, since there is only one $i$ that
+  satisfies $R(i,s)$ when $s$~is a code of a sequence, and if $i$
   exists it is less than~$s$ itself.
 \end{proof}
 

content/incompleteness/arithmetization-syntax/introduction.tex

@@ -43,7 +43,7 @@
 number.
 
 By coding sequences of symbols as sequences of their codes, and by
-chosing a system of coding sequences that can be dealt with using
+choosing a system of coding sequences that can be dealt with using
 computable functions, we can then also deal with G\"odel numbers using
 computable functions.  In practice, all the relevant functions will be
 primitive recursive.  For instance, computing the length of a sequence

content/incompleteness/arithmetization-syntax/proofs-in-nd.tex

@@ -121,7 +121,7 @@
     !!{derivation}s is a special case of the coding of trees introduced in
     \olref[cmp][rec][tre]{sec}, so the primitive recursive function
     $\fn{SubtreeSeq}(d)$ gives a sequence of G\"odel numbers of all
-    sub-!!{derivation}s of~$d$ (of length a most $d$). So we can
+    sub-!!{derivation}s of~$d$ (of length at most $d$). So we can
     define
     \[
     \fn{Assum}(x, d, n) \defiff \bexists{i<d}{(\fn{SubtreeSeq}(d))_i =
@@ -174,7 +174,7 @@
     \concat \fn{EndFmla}((d)_2) \concat \Gn{)}.
   \end{multline*}
 
-  Another simple example if the $\Intro\eq$ rule. Here the premise is
+  Another simple example is the $\Intro\eq$ rule. Here the premise is
   an empty !!{derivation}, i.e., $(d)_1 = 0$, and no discharge label,
   i.e., $n=0$.  However, $!A$ must be of the form $\eq[t][t]$, for a
   closed term~$t$. Here, a primitive recursive definition is
@@ -295,7 +295,7 @@
     \bexists{s<\fn{SubtreeSeq}(d)}{(\fn{Subseq}(s, \fn{SubtreeSeq}(d))
       \land (s)_0 = d \land {}} \\
     \bexists{n<d}{((s)_{\len{s} \tsub 1} = \tuple{0, z, n} \land {}}\\
-      \bforall{i<(\len{s} \tsub 1)}{(\fn{Subderiv}((s)_{i+1}, (s)_i)] \land {}}\\
+      \bforall{i<(\len{s} \tsub 1)}{(\fn{Subderiv}((s)_{i+1}, (s)_i) \land {}}\\
       \fn{DischargeLabel}((s)_{i+1}) \neq n))).
   \end{multline*}
 \end{proof}

content/incompleteness/incompleteness-provability/first-incompleteness-thm.tex

@@ -17,34 +17,34 @@
 represents computable functions and relations.
 
 We have argued that, given a reasonable coding of formulas and proofs
-as numbers, the relation $\Prf[T](x,y)$ is computable, where
-$\Prf[T](x,y)$ holds if and only if $x$ is the G\"odel number of
+as numbers, the relation $\Prf[\Th{T}](x,y)$ is computable, where
+$\Prf[\Th{T}](x,y)$ holds if and only if $x$ is the G\"odel number of
 !!a{derivation} of the !!{formula} with G\"odel number~$y$
 in~$\Th{T}$. In fact, for the particular theory that G\"odel had in
 mind, G\"odel was able to show that this relation is primitive
 recursive, using the list of 45 functions and relations in his
-paper. The 45th relation, $x B y$, is just $\Prf[T](x,y)$ for his
+paper. The 45th relation, $x B y$, is just $\Prf[\Th{T}](x,y)$ for his
 particular choice of~$\Th{T}$. Remember that where G\"odel uses the
 word ``recursive'' in his paper, we would now use the phrase
 ``primitive recursive.''
 
-Since $\Prf[T](x,y)$ is computable, it is representable in $\Th{T}$. We
-will use $\OPrf[T](x,y)$ to refer to the formula that represents
-it. Let $\OProv[T](y)$ be the formula
-$\lexists[x][\OPrf[T](x,y)]$. This describes the 46th relation,
+Since $\Prf[\Th{T}](x,y)$ is computable, it is representable in $\Th{T}$. We
+will use $\OPrf[\Th{T}](x,y)$ to refer to the formula that represents
+it. Let $\OProv[\Th{T}](y)$ be the formula
+$\lexists[x][\OPrf[\Th{T}](x,y)]$. This describes the 46th relation,
 $\fn{Bew}(y)$, on G\"odel's list. As G\"odel notes, this is the only
 relation that ``cannot be asserted to be recursive.''  What he
 probably meant is this: from the definition, it is not clear that it
 is computable; and later developments, in fact, show that it isn't.
 
 Let $\Th{T}$ be an !!{axiomatizable} theory containing~$\Th{Q}$. Then
-$\Prf[T](x, y)$ is decidable, hence representable in~$\Th{Q}$ by
-!!a{formula}~$\OPrf[T](x, y)$. Let $\OProv[T](y)$ be the formula we
+$\Prf[\Th{T}](x, y)$ is decidable, hence representable in~$\Th{Q}$ by
+!!a{formula}~$\OPrf[\Th{T}](x, y)$. Let $\OProv[\Th{T}](y)$ be the formula we
 described above. By the fixed-point lemma, there is a formula
 $!G_\Th{T}$ such that $\Th{Q}$ (and hence $\Th{T}$) !!{derive}s
 \begin{equation}
 \ollabel{eqn:qpf}
-!G_\Th{T} \liff \lnot \OProv[T](\gn{!G_\Th{T}}).
+!G_\Th{T} \liff \lnot \OProv[\Th{T}](\gn{!G_\Th{T}}).
 \end{equation}
 Note that $!G_\Th{T}$ says, in essence, ``$!G_\Th{T}$ is not
 !!{derivable} in~$\Th{T}$.''
@@ -56,11 +56,11 @@
 
 \begin{proof}
 Suppose $\Th{T}$ !!{derive}s $!G_\Th{T}$. Then there \emph{is}
-!!a{derivation}, and so, for some number $m$, the relation $\Prf[T](m,
+!!a{derivation}, and so, for some number $m$, the relation $\Prf[\Th{T}](m,
 \Gn{!G_\Th{T}})$ holds. But then $\Th{Q}$ !!{derive}s the sentence
-$\OPrf[T](\num m, \gn{!G_\Th{T}})$. So $\Th{Q}$ !!{derive}s
-$\lexists[x][\OPrf[T](x,\gn{!G_\Th{T}})]$, which is, by definition,
-$\OProv[T](\gn{!G_\Th{T}})$. By \olref{eqn:qpf}, $\Th{Q}$ !!{derive}s
+$\OPrf[\Th{T}](\num m, \gn{!G_\Th{T}})$. So $\Th{Q}$ !!{derive}s
+$\lexists[x][\OPrf[\Th{T}](x,\gn{!G_\Th{T}})]$, which is, by definition,
+$\OProv[\Th{T}](\gn{!G_\Th{T}})$. By \olref{eqn:qpf}, $\Th{Q}$ !!{derive}s
 $\lnot !G_\Th{T}$, and since $\Th{T}$ extends $\Th{Q}$, so
 does~$\Th{T}$. We have shown that if $\Th{T}$ !!{derive}s $!G_\Th{T}$, then
 it also !!{derive}s $\lnot !G_\Th{T}$, and hence it would be inconsistent.
@@ -95,12 +95,12 @@
 $!G_\Th{T}$ by \olref{lem:cons-G-unprov}. Since there is no
 !!{derivation} of $!G_\Th{T}$ in $\Th{T}$, $\Th{Q}$ !!{derive}s
 \[
-\lnot \OPrf[T](\num 0, \gn{!G_\Th{T}}), \lnot \OPrf[T](\num 1,
-\gn{!G_\Th{T}}), \lnot \OPrf[T](\num 2, \gn{!G_\Th{T}}), \dots
+\lnot \OPrf[\Th{T}](\num 0, \gn{!G_\Th{T}}), \lnot \OPrf[\Th{T}](\num 1,
+\gn{!G_\Th{T}}), \lnot \OPrf[\Th{T}](\num 2, \gn{!G_\Th{T}}), \dots
 \]
 and so does~$\Th{T}$.  On the other hand, by \olref{eqn:qpf}, $\lnot
 !G_\Th{T}$ is equivalent to
-$\lexists[x][\OPrf[T](x,\gn{!G_\Th{T}})]$. So $\Th{T}$ is
+$\lexists[x][\OPrf[\Th{T}](x,\gn{!G_\Th{T}})]$. So $\Th{T}$ is
 $\omega$-inconsistent.
 \end{proof}
 

content/incompleteness/incompleteness-provability/lob-thm.tex

@@ -11,21 +11,21 @@
 \olsection{L\"ob's Theorem}
 
 The G\"odel sentence for a theory~$\Th{T}$ is a fixed point of $\lnot
-\OProv[T](y)$, i.e., !!a{sentence}~$!G$ such that
+\OProv[\Th{T}](y)$, i.e., !!a{sentence}~$!G$ such that
 \[
-\Th{T} \Proves \lnot \OProv[T](\gn{!G}) \liff !G.
+\Th{T} \Proves \lnot \OProv[\Th{T}](\gn{!G}) \liff !G.
 \]
 It is not !!{derivable}, because if $\Th{T} \Proves !G$, (a) by !!{derivability}
-condition~(1), $\Th{T} \Proves \OProv[T](\gn{!G})$, and (b) $\Th{T}
-\Proves !G$ together with $\Th{T} \Proves \lnot \OProv[T](\gn{!G})
-\liff !G$ gives $\Th{T} \Proves \lnot \OProv[T](\gn{!G})$, and so
+condition~(1), $\Th{T} \Proves \OProv[\Th{T}](\gn{!G})$, and (b) $\Th{T}
+\Proves !G$ together with $\Th{T} \Proves \lnot \OProv[\Th{T}](\gn{!G})
+\liff !G$ gives $\Th{T} \Proves \lnot \OProv[\Th{T}](\gn{!G})$, and so
 $\Th{T}$ would be inconsistent.  Now it is natural to ask about the
-status of a fixed point of $\OProv[T](y)$, i.e., !!a{sentence}~$!H$
+status of a fixed point of $\OProv[\Th{T}](y)$, i.e., !!a{sentence}~$!H$
 such that
 \[
-\Th{T} \Proves \OProv[T](\gn{!H}) \liff !H.
+\Th{T} \Proves \OProv[\Th{T}](\gn{!H}) \liff !H.
 \]
-If it were !!{derivable}, $\Th{T} \Proves \OProv[T](\gn{!H})$ by
+If it were !!{derivable}, $\Th{T} \Proves \OProv[\Th{T}](\gn{!H})$ by
 condition~(1), but the same conclusion follows if we apply modus
 ponens to the equivalence above. Hence, we don't get that $\Th{T}$ is
 inconsistent, at least not by the same argument as in the case of the
@@ -34,8 +34,8 @@
 
 We can make headway on this question if we generalize it a bit. The
 left-to-right direction of the fixed point equivalence,
-$\OProv[T](\gn{!H}) \lif !H$, is an instance of a general schema
-called a \emph{reflection principle}: $\OProv[T](\gn{!A}) \lif !A$.
+$\OProv[\Th{T}](\gn{!H}) \lif !H$, is an instance of a general schema
+called a \emph{reflection principle}: $\OProv[\Th{T}](\gn{!A}) \lif !A$.
 It is called that because it expresses, in a sense, that $\Th{T}$ can
 ``reflect'' about what it can !!{derive}; basically it says, ``If $\Th{T}$
 can !!{derive}~$!A$, then~$!A$ is true,'' for any~$!A$.  This is true for
@@ -47,13 +47,13 @@
 
 \begin{thm}\ollabel{thm:lob}
 Let $\Th{T}$ be !!a{axiomatizable} theory extending $\Th{Q}$, and
-suppose $\OProv[T](y)$ is a formula satisfying conditions P1--P3 from
-\olref[2in]{sec}. If $\Th{T}$ !!{derive}s $\OProv[T](\gn{!A}) \lif !A$,
+suppose $\OProv[\Th{T}](y)$ is a formula satisfying conditions P1--P3 from
+\olref[2in]{sec}. If $\Th{T}$ !!{derive}s $\OProv[\Th{T}](\gn{!A}) \lif !A$,
 then in fact $\Th{T}$ !!{derive}s $!A$.
 \end{thm}
 
 Put differently, if $\Th{T} \Proves/ !A$, then $\Th{T} \Proves/
-\OProv[T](\gn{!A}) \lif !A$. This result is known as L\"ob's
+\OProv[\Th{T}](\gn{!A}) \lif !A$. This result is known as L\"ob's
 theorem.
 
 \begin{explain}
@@ -78,41 +78,41 @@
 A formalization of this idea, replacing ``is true'' with ``is
 !!{derivable},'' and ``Santa Claus exists'' with~$!A$, yields the proof of
 L\"ob's theorem. The trick is to apply the fixed-point lemma to the
-!!{formula}~$\OProv[T](y) \lif !A$. The fixed point of that
+!!{formula}~$\OProv[\Th{T}](y) \lif !A$. The fixed point of that
 corresponds to the sentence~$X$ in the preceding sketch.
 \end{explain}
 
 \begin{proof}[Proof of \olref{thm:lob}]
 Suppose $!A$ is !!a{sentence} such that $\Th{T}$ !!{derive}s
-$\OProv[T](\gn{!A}) \lif !A$. Let $!B(y)$ be the !!{formula}~$\OProv[T](y)
+$\OProv[\Th{T}](\gn{!A}) \lif !A$. Let $!B(y)$ be the !!{formula}~$\OProv[\Th{T}](y)
 \lif !A$, and use the fixed-point lemma to find !!a{sentence}~$!D$
 such that $\Th{T}$ !!{derive}s $!D \liff !B(\gn{!D})$. Then each of the
 following is !!{derivable} in $\Th{T}$:
 \begin{align}
-  & !D \liff (\OProv[T](\gn{!D}) \lif !A) \ollabel{L-1}\\
+  & !D \liff (\OProv[\Th{T}](\gn{!D}) \lif !A) \ollabel{L-1}\\
   & \qquad \text{$!D$ is a fixed point of~$!B(y)$}\notag \\
-  & !D \lif (\OProv[T](\gn{!D}) \lif !A) \ollabel{L-2}\\
+  & !D \lif (\OProv[\Th{T}](\gn{!D}) \lif !A) \ollabel{L-2}\\
   & \qquad\text{from \olref{L-1}}\notag\\
-  & \OProv[T](\gn{!D \lif (\OProv[T](\gn{!D}) \lif !A)}) \ollabel{L-3}\\
+  & \OProv[\Th{T}](\gn{!D \lif (\OProv[\Th{T}](\gn{!D}) \lif !A)}) \ollabel{L-3}\\
   & \qquad \text{from \olref{L-2} by condition P1}\notag \\
-  & \OProv[T](\gn{!D}) \lif \OProv[T](\gn{\OProv[T](\gn{!D}) \lif !A})
+  & \OProv[\Th{T}](\gn{!D}) \lif \OProv[\Th{T}](\gn{\OProv[\Th{T}](\gn{!D}) \lif !A})
   \ollabel{L-4}\\
   &\qquad \text{from \olref{L-3} using condition P2}\notag \\
-  & \OProv[T](\gn{!D}) \lif (\OProv[T](\gn{\OProv[T](\gn{!D})}) \lif \OProv[T](\gn{!A})) \ollabel{L-5}\\
+  & \OProv[\Th{T}](\gn{!D}) \lif (\OProv[\Th{T}](\gn{\OProv[\Th{T}](\gn{!D})}) \lif \OProv[\Th{T}](\gn{!A})) \ollabel{L-5}\\
   &\qquad \text{from \olref{L-4} using P2 again} \notag\\
-& \OProv[T](\gn{!D}) \lif \OProv[T](\gn{\OProv[T](\gn{!D})}) \ollabel{L-6}\\
+& \OProv[\Th{T}](\gn{!D}) \lif \OProv[\Th{T}](\gn{\OProv[\Th{T}](\gn{!D})}) \ollabel{L-6}\\
   & \qquad\text{by !!{derivability} condition P3} \notag\\
-  & \OProv[T](\gn{!D}) \lif \OProv[T](\gn{!A}) \ollabel{L-7} \\
+  & \OProv[\Th{T}](\gn{!D}) \lif \OProv[\Th{T}](\gn{!A}) \ollabel{L-7} \\
   &\qquad\text{from \olref{L-5} and \olref{L-6}}\notag\\
-  & \OProv[T](\gn{!A}) \lif !A \ollabel{L-8}\\
+  & \OProv[\Th{T}](\gn{!A}) \lif !A \ollabel{L-8}\\
   &\qquad\text{by assumption of the theorem} \notag\\
-  & \OProv[T](\gn{!D}) \lif !A \ollabel{L-9}\\
+  & \OProv[\Th{T}](\gn{!D}) \lif !A \ollabel{L-9}\\
   &\qquad\text{from \olref{L-7} and \olref{L-8}}\notag\\
-  & (\OProv[T](\gn{!D}) \lif !A) \lif !D \ollabel{L-10}\\
+  & (\OProv[\Th{T}](\gn{!D}) \lif !A) \lif !D \ollabel{L-10}\\
   & \qquad \text{from \olref{L-1}}\notag \\
   & !D \ollabel{L-11}\\
   & \qquad\text{from \olref{L-9} and \olref{L-10}}\notag \\
-  & \OProv[T](\gn{!D}) \ollabel{L-12}\\
+  & \OProv[\Th{T}](\gn{!D}) \ollabel{L-12}\\
   & \qquad\text{from \olref{L-11} by condition~P1}\notag \\
   & !A \qquad\qquad\text{from \olref{L-8} and \olref{L-12}}\notag
 \end{align}
@@ -121,15 +121,15 @@
 With L\"ob's theorem in hand, there is a short proof of the second
 incompleteness theorem (for theories having !!a{derivability} predicate
 satisfying conditions P1--P3): if $\Th{T} \Proves
-\OProv[T](\gn{\lfalse}) \lif \lfalse$, then $\Th{T} \Proves \lfalse$.
+\OProv[\Th{T}](\gn{\lfalse}) \lif \lfalse$, then $\Th{T} \Proves \lfalse$.
 If $\Th{T}$ is consistent, $\Th{T} \Proves/ \lfalse$. So, $\Th{T}
-\Proves/ \OProv[T](\gn{\lfalse}) \lif \lfalse$, i.e., $\Th{T} \Proves/
+\Proves/ \OProv[\Th{T}](\gn{\lfalse}) \lif \lfalse$, i.e., $\Th{T} \Proves/
 \OCon[\Th{T}]$.  We can also apply it to show that~$!H$, the fixed
-point of $\OProv[T](x)$, is !!{derivable}. For since
+point of $\OProv[\Th{T}](x)$, is !!{derivable}. For since
 \begin{align*}
-  \Th{T} & \Proves \OProv[T](\gn{!H}) \liff !H\\
+  \Th{T} & \Proves \OProv[\Th{T}](\gn{!H}) \liff !H\\
   \intertext{in particular}
-    \Th{T} & \Proves \OProv[T](\gn{!H}) \lif !H
+    \Th{T} & \Proves \OProv[\Th{T}](\gn{!H}) \lif !H
 \end{align*}
 and so by L\"ob's theorem, $\Th{T} \Proves !H$.
 
@@ -139,13 +139,13 @@
 
 \begin{prob}
 Let $\Th{T}$ be a computably axiomatized theory, and
-let $\OProv[T]$ be !!a{derivability} predicate for $\Th{T}$. Consider the
+let $\OProv[\Th{T}]$ be !!a{derivability} predicate for $\Th{T}$. Consider the
 following four statements:
 \begin{enumerate}
-\item If $T \Proves !A$, then $T \Proves \OProv[T](\gn{!A})$.
-\item $T \Proves !A \lif \OProv[T](\gn{!A})$.
-\item If $T \Proves \OProv[T](\gn{!A})$, then $T \Proves !A$.
-\item $T \Proves \OProv[T](\gn{!A}) \lif !A$
+\item If $T \Proves !A$, then $T \Proves \OProv[\Th{T}](\gn{!A})$.
+\item $T \Proves !A \lif \OProv[\Th{T}](\gn{!A})$.
+\item If $T \Proves \OProv[\Th{T}](\gn{!A})$, then $T \Proves !A$.
+\item $T \Proves \OProv[\Th{T}](\gn{!A}) \lif !A$
 \end{enumerate}
 Under what conditions are each of these statements true?
 \end{prob}