Fix a typo in the proof that regular minimization is representable

in Q, making the variables make more sense.

Author: beastaugh

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

@@ -123,16 +123,16 @@
 Now for the inductive step. We prove the case for $n+1$, assuming the
 case for~$n$. So suppose $a < \num {n+2}$. Again using $!Q_3$ we can
 distinguish two cases: $\eq[a][\Obj 0]$ and for some $b$,
-$\eq[a][c']$. In the first case, $\eq[a][\Obj 0] \lor \dots \lor
-\eq[a][\num{n+1}]$ follows trivially. In the second case, we have $c'
-< \num {n+2}$, i.e., $c' < \num{n+1}'$. By axiom~$!Q_8$, for some $d$,
-$\eq[(d'+c')][\num{n+1}']$. By axiom $!Q_5$,
-$\eq[(d'+c)'][\num{n+1}']$. By axiom~$!Q_1$, $\eq[(d'+c)][\num{n+1}]$,
-and so $c < \num{n+1}$ by axiom~$!Q_8$. By inductive hypothesis,
-$\eq[c][\Obj 0] \lor \dots \lor \eq[c][\num{n}]$. From this, we get
-$\eq[c'][\Obj 0'] \lor \dots \lor \eq[c'][\num{n}']$ by logic, and so
+$\eq[a][b']$. In the first case, $\eq[a][\Obj 0] \lor \dots \lor
+\eq[a][\num{n+1}]$ follows trivially. In the second case, we have $b'
+< \num {n+2}$, i.e., $b' < \num{n+1}'$. By axiom~$!Q_8$, for some $c$,
+$\eq[(c'+b')][\num{n+1}']$. By axiom $!Q_5$,
+$\eq[(c'+b)'][\num{n+1}']$. By axiom~$!Q_1$, $\eq[(c'+b)][\num{n+1}]$,
+and so $b < \num{n+1}$ by axiom~$!Q_8$. By inductive hypothesis,
+$\eq[b][\Obj 0] \lor \dots \lor \eq[b][\num{n}]$. From this, we get
+$\eq[b'][\Obj 0'] \lor \dots \lor \eq[b'][\num{n}']$ by logic, and so
 $\eq[a][\num{1}] \lor \dots \lor \eq[a][\num{n+1}]$ since
-$\eq[a][c']$.
+$\eq[a][b']$.
 \end{proof}
 
 \begin{lem}