fix a few typos

Author: rzach

content/first-order-logic/natural-deduction/quantifier-rules.tex

@@ -49,7 +49,7 @@ \subsection{Rules for $\lexists$}
 \DisplayProof
 \end{defish}
 
-Again, $t$ is a closed term, and $a$ is a constant which does not
+Again, $t$ is a closed term, and $a$ is !!a{constant} which does not
 occur in the premise $\lexists[x][!A(x)]$, in the conclusion~$!C$, or
 any assumption which is !!{undischarged} in the !!{derivation}s ending
 with the two premises (other than the assumptions $!A(a)$). We call

content/incompleteness/representability-in-q/introduction.tex

@@ -39,7 +39,7 @@
 & \lforall[x][\lforall[y][(x < y \liff \lexists[z][\eq[(z' + x)][y]])]] \tag{$!Q_8$}
 \end{align*}
 For each natural number $n$, define the numeral $\num{n}$ to be the
-term $0^{\prime\prime\ldots\prime}$ where there are $n$ tick marks in
+term $\Obj{0}^{\prime\prime\ldots\prime}$ where there are $n$ tick marks in
 all.  So, $\num{0}$ is the !!{constant}~$\Obj{0}$ by itself, $\num{1}$
 is $\Obj{0}'$, $\num{2}$ is $\Obj{0}''$, etc.
 

content/lambda-calculus/introduction/minimization.tex

@@ -10,7 +10,7 @@
 \olsection{The \usetoken{S}{lambda definable} Functions are Closed under Minimization}
 
 \begin{lem}
-Suppose $f(x,y)$ is primitive recursive. Let $g$ be defined by
+Suppose $f(x,y)$ is !!{lambda definable}. Let $g$ be defined by
 \[
 g(x) \simeq \umin{y}{f(x,y)}.
 \]
@@ -61,9 +61,9 @@
 $F(\num{m}, \num{n})$ reduces to any other numeral.
 
 To finish off the proof, let $G$ be $\lambd[x][H(\num 0)]$. Then $G$
-!!{lambda define}s $g$; in other words, for every $m$, $G(\num m)$ reduces to
-reduces to $\overline {g(m)}$, if $g(m)$ is defined, and has no
-normal form otherwise.
+!!{lambda define}s~$g$; in other words, for every~$m$, $G(\num m)$
+reduces to~$\overline {g(m)}$, if $g(m)$ is defined, and has no normal
+form otherwise.
 \end{proof}
 
 \end{document}