Consolidated translation findings: 14 source-fix groups with an applicable patch

--- a/content/first-order-logic/completeness/identity.tex
+++ b/content/first-order-logic/completeness/identity.tex
@@ -123,7 +123,7 @@
 !!{predicate}, the last clause of the definition says that
 $\equivrep{t}{\approx} \in \Assign{R}{\equivclass{M}{\approx}}$ iff
 $\Sat{M}{\Atom{R}{t}}$. If for some other term~$t'$ with $t \approx
-t'$, $\Sat/{M}{\Atom{R}{t}}$, then the definition would require
+t'$, $\Sat/{M}{\Atom{R}{t'}}$, then the definition would require
 $\equivrep{t'}{\approx} \notin \Assign{R}{\equivclass{M}{\approx}}$.
 If $t \approx t'$, then $\equivrep{t}{\approx} =
 \equivrep{t'}{\approx}$, but we can't have both $\equivrep{t}{\approx}
--- a/content/first-order-logic/syntax-and-semantics/satisfaction.tex
+++ b/content/first-order-logic/syntax-and-semantics/satisfaction.tex
@@ -170,7 +170,7 @@
 Then instead of saying that, e.g.,
 \iftag{prvEx}{$\lexists[x][!B(x)]$}{$\lforall[x][!B(x)]$} is satisfied
 in~$\Struct M$ iff \iftag{prvEx}{for at least one $m \in
-\Domain{M}$}{for all $m \in \Domain{M}$, $\Sat{M}{!B(m)}$}, we say it
+\Domain{M}$}{for all $m \in \Domain{M}$}, $\Sat{M}{!B(m)}$, we say it
 is satisfied in~$\Struct M$ \emph{relative to}~$s$ iff $!B(x)$ is
 satisfied relative to~$\Subst{s}{m}{x}$ \iftag{prvEx}{for at least
 one}{for every} $m \in \Domain M$.
@@ -210,7 +210,7 @@
   \Value{t_2}{M}[s]}$, is !!a{element} of~$\Assign{R}{M}$. So, e.g., we
 have $\Sat{M}{R(b,f(a,b))}[s]$ since $\tuple{\Value{b}{M},
   \Value{f(a,b)}{M}} = \tuple{2, 3} \in \Assign{R}{M}$, but
-$\Sat/{M}{R(x, f(a,b))}[s]$ since $\tuple{1, 3} \notin \Assign{R}{M}[s]$.
+$\Sat/{M}{R(x, f(a,b))}[s]$ since $\tuple{1, 3} \notin \Assign{R}{M}$.
 
 To determine if a non-atomic formula~$!A$ is satisfied, you apply the
 clauses in the inductive definition that applies to the main
@@ -285,11 +285,11 @@
   First, $\Sat{M}{R(b,x) \lor R(x, b)}[\Subst{s}{1}{x}]$
   ($\Subst{s}{3}{x}$ would also fit the bill).  So,
   $\Sat/{M}{\lnot(R(b,x) \lor R(x,b))}[\Subst{s}{1}{x}]$, thus
-  $\Sat/{M}{\lforall[x][\lnot((R(b,x) \lor R(x,b))]}[s]$, and
-  therefore $\Sat{M}{\lnot\lforall[x][\lnot((R(b,x) \lor
+  $\Sat/{M}{\lforall[x][\lnot(R(b,x) \lor R(x,b))]}[s]$, and
+  therefore $\Sat{M}{\lnot\lforall[x][\lnot(R(b,x) \lor
   R(x,b))]}[s]$. On the other hand,
   \[
-  \Sat/{M}{\lexists[x][(R(b,x) \land R(x,b))],}[s].
+  \Sat/{M}{\lexists[x][(R(b,x) \land R(x,b))]}[s].
   \]
   That's because $\Sat{M}{\lforall[x][\lnot(R(b,x) \land
   R(x,b))]}[s]$, since for no $m \in \Domain M$, $\Sat{M}{R(b,x) \land
@@ -306,7 +306,7 @@
   \]
   First, $\Sat{M}{R(x,a) \lif R(a,x)}[\Subst{s}{m}{x}]$ for all $m \in
   \Domain M$ ($\Sat{M}{R(a,x)}[\Subst{s}{1}{x}]$ and
-  $\Sat/{M}{R(a,x)}[\Subst{s}{m}{x}]$ for $m = 2$, $3$, or~$4$).
+  $\Sat/{M}{R(x,a)}[\Subst{s}{m}{x}]$ for $m = 2$, $3$, or~$4$).
   Thus, there is no $m \in \Domain M$ such that
   $\Sat{M}{\lnot(R(x,a) \lif R(a,x))}[\Subst{s}{m}{x}]$ and hence
   $\Sat/{M}{\lexists[x][\lnot(R(x,a) \lif R(a,x))]}[s]$. Therefore,
@@ -328,7 +328,7 @@
 Since $\Sat/{M}{R(a,x)}[\Subst{s}{3}{x}]$ and
 $\Sat/{M}{R(a,x)}[\Subst{s}{4}{x}]$, the interesting cases where we
 have to worry about the consequent of the conditional are only $m = 1$
-and $ = 2$. Does $\Sat{M}{\lexists[y][R(x,y)]}[\Subst{s}{1}{x}]$
+and $m = 2$. Does $\Sat{M}{\lexists[y][R(x,y)]}[\Subst{s}{1}{x}]$
 hold? It does if there is at least one $n \in \Domain M$ so that
 $\Sat{M}{R(x,y)}[\Subst{\Subst{s}{1}{x}}{n}{y}]$. In fact, if we take
 $n = 1$, we have $\Subst{\Subst{s}{1}{x}}{n}{y} = \Subst{s}{1}{y} =
@@ -344,7 +344,7 @@
 $\Sat{M}{R(x,y)}[\Subst{s_2}{3}{y}]$ since $\tuple{2,3} \in
 \Assign{R}{M}$, and so $\Sat{M}{\lexists[y][R(x,y)]}[s_2]$.
 
-So, for all $n \in \Domain M$, either
+So, for all $m \in \Domain M$, either
 $\Sat/{M}{R(a,x)}[\Subst{s}{m}{x}]$ (if $m = 3$, $4$) or
 $\Sat{M}{\lexists[y][R(x,y)]}[\Subst{s}{m}{x}]$ (if $m = 1$, $2$), and so
 \[
@@ -356,7 +356,7 @@
 \]
 We have $\Sat{M}{R(a,x)}[\Subst{s}{m}{x}]$ only for $m = 1$ and $m =
 2$. But for both of these values of~$m$, there is in turn an $n \in
-\Domain M$, namely $n = 4$, so that
+\Domain M$, namely $n = 4$ when $m = 1$ and $n = 1$ when $m = 2$, so that
 $\Sat/{M}{R(x,y)}[\Subst{\Subst{s}{m}{x}}{n}{y}]$ and so
 $\Sat/{M}{\lforall[y][R(x,y)]}[\Subst{s}{m}{x}]$ for $m = 1$ and $m =
 2$. In sum, there is no $m \in \Domain M$ such that $\Sat{M}{R(a,x)
--- a/content/incompleteness/representability-in-q/sigma1-completeness.tex
+++ b/content/incompleteness/representability-in-q/sigma1-completeness.tex
@@ -165,7 +165,7 @@
     If $\Value{t}{N} = 0$ then the left-hand side of the
     equivalence is provable in~$\Th{Q}$, because there is no
     $x<\num 0$ by \olref[inc][req][min]{lem:less-zero}.
-    Similarly, we can take an empty disjunction to be simply
+    Similarly, we can take an empty conjunction to be simply
     $\ltrue$, which is also provable in~$\Th{Q}$.
     %
     We therefore suppose that $\Value{t}{N} = k+1$ for some
--- a/content/lambda-calculus/lambda-definability/arithmetical-functions.tex
+++ b/content/lambda-calculus/lambda-definability/arithmetical-functions.tex
@@ -117,7 +117,7 @@
 \begin{prob}
 Multiplication can be !!{lambda define}d by the term
 \[
-  \fn{Mult}' \ident \lambd[ab][a (\fn{Add}\, a) \num{0}].
+  \fn{Mult}' \ident \lambd[ab][a (\fn{Add}\, b) \num{0}].
 \]
 Explain why this works.
 \end{prob}
--- a/content/lambda-calculus/lambda-definability/fixpoints.tex
+++ b/content/lambda-calculus/lambda-definability/fixpoints.tex
@@ -21,7 +21,7 @@
 side. Such recursive definitions involving self-reference
 are not part of the lambda calculus. Defining a term, e.g., by
 \[
-\fn{Mult} \ident \lambd[ab][a (\fn{Add}\, a) 0]
+\fn{Mult} \ident \lambd[ab][a (\fn{Add}\, b) \num{0}]
 \]
 only involves previously defined terms in the right-hand side, such as
 $\fn{Add}$. We can always remove $\fn{Add}$ by replacing it with its
@@ -160,8 +160,8 @@
 \[
 Y_C \ident \lambd[g][(\lambd[x][g(xx)])(\lambd[x][g(xx)])].
 \]
-Church's combinator is a bit weaker than Turing's in that $Yg
-\equal[\beta] g(Yg)$ but not $Yg \bred g(Yg)$. Let $V$ be the term
+Church's combinator is a bit weaker than Turing's in that $Y_Cg
+\equal[\beta] g(Y_Cg)$ but not $Y_Cg \bred g(Y_Cg)$. Let $V$ be the term
 $\lambd[x][g(xx)]$, so that $Y_C \ident \lambd[g][VV]$. Then
 \begin{align*}
   VV & \ident (\lambd[x][g(xx)])V \red g(VV)
--- a/content/lambda-calculus/lambda-definability/minimization.tex
+++ b/content/lambda-calculus/lambda-definability/minimization.tex
@@ -27,12 +27,12 @@
 
 \begin{proof}
   Suppose the lambda term~$F$ $\lambda$-defines the regular
-  function $f(\vec x, y)$. To !!{lambda define}~$h$ we use a search
+  function $f(\vec x, y)$. To !!{lambda define}~$g$ we use a search
   function and a fixpoint combinator:
   \begin{align*}
     \fn{Search} & \ident \lambd[g][\lambd[f\,\vec{x}\,y][
-        \fn{IsZero} (f\, \vec{x}\, y)\, y\, (g\, \vec{x} (\fn{Succ}\, y)]]\\
-    H & \ident \lambd[\vec x][(Y \, \fn{Search}) F\, \vec{x}\, \num{0}],
+        \fn{IsZero} (f\, \vec{x}\, y)\, y\, (g\, f\, \vec{x} (\fn{Succ}\, y))]]\\
+    G & \ident \lambd[\vec x][(Y \, \fn{Search}) F\, \vec{x}\, \num{0}],
   \end{align*}
   where $Y$ is any fixpoint combinator. Informally speaking,
   $\fn{Search}$ is a self-referencing function: starting with~$y$,
@@ -51,7 +51,7 @@
     \intertext{otherwise. Since $f$ is regular, $f(n_1, \dots, n_k, y)
       = 0$ for some $y$, and so}
     (Y \, \fn{Search}) F \num{n_1} \dots\num{n_k}\,\num{0}
-    & \red \num{h(n_1, \dots, n_k)}.
+    & \red \num{g(n_1, \dots, n_k)}.
     \end{align*}
 \end{proof}
 
--- a/content/lambda-calculus/lambda-definability/primitive-recursive-functions.tex
+++ b/content/lambda-calculus/lambda-definability/primitive-recursive-functions.tex
@@ -31,8 +31,8 @@
 \begin{lem}
   \ollabel{lem:comp} Suppose the $k$-ary function $f$, and $n$-ary
   functions $g_0, \dots, g_{k-1}$, are !!{lambda definable} by terms
-  $F$, $G_0$, \dots, $G_k$, and $h$ is defined from them by composition.
-  Then $H$ is !!{lambda definable}.
+  $F$, $G_0$, \dots, $G_{k-1}$, and $h$ is defined from them by composition.
+  Then $h$ is !!{lambda definable}.
 \end{lem}
 
 \begin{proof}
@@ -65,12 +65,13 @@
   Recall that $h$ is defined by
   \begin{align*}
     h(x_1, \dots, x_n, 0) &= f(x_1, \dots, x_n)\\
-    h(x_1, \dots, x_n, y+1) & = h(x_1, \dots, x_n, y, h(x_1, \dots, x_n, y)).
+    h(x_1, \dots, x_n, y+1) & = g(x_1, \dots, x_n, y, h(x_1, \dots, x_n, y)).
   \end{align*}
-  Informally speaking, the primitive recursive definition iterates the
-  application of the function $h$ $y$ times and applies it to $f(x_1,
-  \dots, x_n)$. This is reminiscent of the definition of Church
-  numerals, which is also defined as a iterator.
+  Informally speaking, keep $x_1, \dots, x_n$ fixed and start with the
+  pair $(0,f(x_1, \dots, x_n))$. Iterate the state update
+  $(j,z) \mapsto (j+1,g(x_1, \dots, x_n,j,z))$ exactly $y$ times.
+  The second component is then $h(x_1, \dots, x_n,y)$. This is
+  reminiscent of Church numerals, which act as iterators.
 
   For simplicity, we give the definition and proof for a single
   additional argument~$x$. The function $h$ is !!{lambda define}d by:
--- a/content/lambda-calculus/lambda-definability/truth-values.tex
+++ b/content/lambda-calculus/lambda-definability/truth-values.tex
@@ -22,7 +22,7 @@
 $\fn{false}\, M N$ always reduces to~$N$.
 
 \begin{defn}
-We call a relation $R \subseteq \Nat^n$ !!{lambda definable} if there is
+We call a relation $R \subseteq \Nat^k$ !!{lambda definable} if there is
 a term~$R$ such that
 \begin{align*}
   R\, \num{n_1} \dots \num{n_k} & \bred \fn{true}
--- a/content/model-theory/lindstrom/lindstrom-proof.tex
+++ b/content/model-theory/lindstrom/lindstrom-proof.tex
@@ -71,7 +71,7 @@
 the language by the same objects; furthermore, since there are only
 finitely many atomic !!{sentence}s in the language, we may also assume
 that they satisfy the same atomic !!{sentence}s (we can take a
-subsequence of the $\Struct{M}$'s otherwise). Let $\Struct{M}$ be the
+subsequence of the $\Struct{M}_n$'s otherwise). Let $\Struct{M}$ be the
 union of all the $\Struct{M}_n$'s, i.e., the unique minimal
 !!{structure} having each $\Struct{M}_n$ as a substructure.  As in the
 proof of \olref[lsp]{thm:abstract-p-isom}, let $\Struct{M}^*$ be the