diff --git a/content/incompleteness/representability-in-q/representable-comp.tex b/content/incompleteness/representability-in-q/representable-comp.tex index af6691bd..4949f2d1 100644 --- a/content/incompleteness/representability-in-q/representable-comp.tex +++ b/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