Small typo (already used variable name) in Functions Representable in Q are Computable

content/incompleteness/representability-in-q/representable-comp.tex

@@ -27,17 +27,17 @@
   The ``if'' part is
 \olref[int]{defn:representable-fn}\olref[int]{defn:rep:a}. The ``only
 if'' part is seen as follows: Suppose $\Th{Q} \Proves !A_f(\num{n_0},
-\dots, \num{n_k}, \num{m})$ but $m \neq f(n_0, \dots, n_k)$. Let $k =
+\dots, \num{n_k}, \num{m})$ but $m \neq f(n_0, \dots, n_k)$. Let $l =
 f(n_0, \dots, n_k)$. By
 \olref[int]{defn:representable-fn}\olref[int]{defn:rep:a}, $\Th{Q}
-\Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{k})$. By
+\Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{l})$. By
 \olref[int]{defn:representable-fn}\olref[int]{defn:rep:b},
-$\lforall[y][(!A_f(\num{n_0}, \dots, \num{n_k}, y) \lif \num{k} =
+$\lforall[y][(!A_f(\num{n_0}, \dots, \num{n_k}, y) \lif \num{l} =
 y)]$. Using logic and the assumption that $\Th{Q} \Proves
 !A_f(\num{n_0}, \dots, \num{n_k}, \num{m})$, we get that $\Th{Q}
-\Proves \eq[\num{k}][\num{m}]$. On the other hand, by
+\Proves \eq[\num{l}][\num{m}]$. On the other hand, by
 \olref[bre]{lem:q-proves-neq}, $\Th{Q} \Proves
-\eq/[\num{k}][\num{m}]$. So $\Th{Q}$ is inconsistent. But that is
+\eq/[\num{l}][\num{m}]$. So $\Th{Q}$ is inconsistent. But that is
 impossible, since $\Th{Q}$ is satisfied by the standard model (see
 \olref[int][def]{def:standard-model}), $\Sat{N}{\Th{Q}}$, and
 satisfiable theories are always consistent by the Soundness Theorem