content/incompleteness/representability-in-q/representability-in-q.tex
1% Part: incompleteness2% Chapter: representability-in-q3\documentclass[../../../include/open-logic-chapter]{subfiles}5\begin{document}7\olchapter{inc}{req}{Representability in $\Th{Q}$}9\olimport{introduction}11\olimport{representable-comp}13\olimport{beta-function}15\olimport{prim-rec}17\olimport{basic-representable}19\olimport{composition-representable}21\olimport{minimization-representable}23\olimport{comp-representable}25\olimport{representing-relations}27\olimport{undecidability}29\olimport{sigma1-completeness}31\OLEndChapterHook33\end{document}
content/incompleteness/representability-in-q/introduction.tex
1% Part: incompleteness2% Chapter: representability-in-q3% Section: introduction4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{inc}{req}{int}10\olsection{Introduction}11The incompleteness theorems apply to theories in which basic facts13about computable functions can be expressed and proved. We will14describe a very minimal such theory called ``$\Th{Q}$'' (or, sometimes,15``Robinson's $Q$,'' after Raphael Robinson). We will say what it means16for a function to be \emph{representable} in $\Th{Q}$, and then we17will prove the following:18\begin{quote}19 A function is representable in $\Th{Q}$ if and only if it is computable.20\end{quote}21For one thing, this provides us with another model of22computability. But we will also use it to show that the set23$\Setabs{!A}{\Th{Q} \Proves !A}$ is not decidable, by reducing the24halting problem to it. By the time we are done, we will have proved25much stronger things than this.26The language of $\Th{Q}$ is the language of28arithmetic; $\Th{Q}$ consists of the following axioms29(to be used in conjunction with the other axioms and rules of30first-order logic with !!{identity}):31\begin{align*}32& \lforall[x][\lforall[y][(\eq[x'][y'] \lif \eq[x][y])]] \tag{$!Q_1$}\\33& \lforall[x][\eq/[\Obj 0][x']] \tag{$!Q_2$}\\34& \lforall[x][(\eq[x][\Obj 0] \lor \lexists[y][\eq[x][y']])] \tag{$!Q_3$}\\35& \lforall[x][\eq[(x + \Obj 0)][x]] \tag{$!Q_4$}\\36& \lforall[x][\lforall[y][\eq[(x + y')][(x + y)']]] \tag{$!Q_5$}\\37& \lforall[x][\eq[(x \times \Obj 0)][\Obj 0]] \tag{$!Q_6$}\\38& \lforall[x][\lforall[y][\eq[(x \times y')][((x \times y) + x)]]] \tag{$!Q_7$}\\39& \lforall[x][\lforall[y][(x < y \liff \lexists[z][\eq[(z' + x)][y]])]] \tag{$!Q_8$}40\end{align*}41For each natural number $n$, define the numeral $\num{n}$ to be the42term $\Obj{0}^{\prime\prime\ldots\prime}$ where there are $n$ tick marks in43all. So, $\num{0}$ is the !!{constant}~$\Obj{0}$ by itself, $\num{1}$44is $\Obj{0}'$, $\num{2}$ is $\Obj{0}''$, etc.45As a theory of arithmetic, $\Th{Q}$ is \emph{extremely} weak; for47example, you can't even prove very simple facts like48$\lforall[x][\eq/[x][x']]$ or $\lforall[x][\lforall[y][(x + y) = (y +49 x)]]$. But we will see that much of the reason that $\Th{Q}$ is so50interesting is \emph{because} it is so weak. In fact, it is just51barely strong enough for the incompleteness theorem to hold. Another52reason $\Th{Q}$ is interesting is because it has a \emph{finite} set53of axioms.54A stronger theory than $\Th{Q}$ (called \emph{Peano arithmetic} $\Th{PA}$)56is obtained by adding a schema of induction to~$\Th{Q}$:57\[58(!A(\Obj 0) \land \lforall[x][(!A(x) \lif !A(x'))]) \lif \lforall[x][!A(x)]59\]60where $!A(x)$ is any formula. If $!A(x)$ contains free !!{variable}s61other than $x$, we add universal quantifiers to the front to bind all62of them (so that the corresponding instance of the induction schema is63!!a{sentence}). For instance, if $!A(x, y)$ also contains the64!!{variable}~$y$ free, the corresponding instance is65\[66\lforall[y][((!A(\Obj 0) \land \lforall[x][(!A(x) \lif !A(x'))]) \lif67 \lforall[x][!A(x)])]68\]69Using instances of the induction schema, one can prove much more from70the axioms of~$\Th{PA}$ than from those of $\Th{Q}$. In fact, it takes71a good deal of work to find ``natural'' statements about the natural72numbers that can't be proved in Peano arithmetic!{}73\begin{defn}75\ollabel{defn:representable-fn}76 A function $f(x_0,\ldots,x_k)$ from the natural numbers to77 the natural numbers is said to be {\em representable in $\Th{Q}$} if78 there is a formula $!A_f(x_0,\dots,x_k,y)$ such that whenever79 $f(n_0,\dots,n_k) = m$, $\Th{Q}$ proves80\begin{enumerate}81\item\ollabel{defn:rep:a} $!A_f(\num{n_0}, \dots, \num{n_k}, \num{m})$82\item\ollabel{defn:rep:b} $\lforall[y][(!A_f(\num{n_0}, \dots,83\num{n_k}, y) \lif \num{m} = y)]$.84\end{enumerate}85\end{defn}86There are other ways of stating the definition; for example, we could88equivalently require that $\Th{Q}$ proves $\lforall[y][(!A_f(\num{n_0}, \dots,89\num{n_k}, y) \liff \eq[y][\num{m}])]$.90\begin{thm}92\ollabel{thm:representable-iff-comp}93A function is representable in $\Th{Q}$ if and only if it is computable.94\end{thm}95There are two directions to proving the theorem. The left-to-right97direction is fairly straightforward once arithmetization of syntax is98in place. The other direction requires more work. Here is the basic99idea: we pick ``general recursive'' as a way of making ``computable''100precise, and show that every general recursive function is101representable in~$\Th{Q}$. Recall that a function is general recursive102if it can be defined from $\Zero$, the successor function~$\Succ$, and the103projection functions~$\Proj{n}{i}$, using composition, primitive recursion,104and regular minimization. So one way of showing that every general105recursive function is representable in~$\Th{Q}$ is to show that the106basic functions are representable, and whenever some functions are107representable, then so are the functions defined from them using108composition, primitive recursion, and regular minimization. In other109words, we might show that the basic functions are representable, and110that the representable functions are ``closed under'' composition,111primitive recursion, and regular minimization. This guarantees that112every general recursive function is representable.113It turns out that the step where we would show that representable115functions are closed under primitive recursion is hard. In order to116avoid this step, we show first that in fact we can do without117primitive recursion. That is, we show that every general recursive118function can be defined from basic functions using composition and119regular minimization alone. To do this, we show that primitive120recursion can actually be done by a specific regular minimization.121However, for this to work, we have to add some additional basic122functions: addition, multiplication, and the characteristic function123of the identity relation~$\Char{=}$. Then, we can prove the theorem124by showing that all of \emph{these} basic functions are representable125in~$\Th{Q}$, and the representable functions are closed under126composition and regular minimization.127\end{document}
content/incompleteness/representability-in-q/representable-comp.tex
1% Part: incompleteness2% Chapter: representability-in-q3% Section: representable-comp4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{inc}{req}{rpc}10\olsection{Functions Representable in $\Th{Q}$ are Computable}11We'll prove that every function that is representable in~$\Th{Q}$ is13computable. We first have to establish a lemma about functions14representable in~$\Th{Q}$.15\begin{lem}\ollabel{lem:rep-q}17 If $f(x_0,18 \dots, x_k)$ is representable in~$\Th{Q}$, there is19 !!a{formula}~$!A(x_0, \dots, x_k, y)$ such that20 \[21 \Th{Q} \Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{m})22 \quad\text{iff}\quad m = f(n_0, \dots, n_k).23 \]24\end{lem}25\begin{proof}27 The ``if'' part is28\olref[int]{defn:representable-fn}\olref[int]{defn:rep:a}. The ``only29if'' part is seen as follows: Suppose $\Th{Q} \Proves !A_f(\num{n_0},30\dots, \num{n_k}, \num{m})$ but $m \neq f(n_0, \dots, n_k)$. Let $l =31f(n_0, \dots, n_k)$. By32\olref[int]{defn:representable-fn}\olref[int]{defn:rep:a}, $\Th{Q}33\Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{l})$. By34\olref[int]{defn:representable-fn}\olref[int]{defn:rep:b},35$\lforall[y][(!A_f(\num{n_0}, \dots, \num{n_k}, y) \lif \num{l} =36y)]$. Using logic and the assumption that $\Th{Q} \Proves37!A_f(\num{n_0}, \dots, \num{n_k}, \num{m})$, we get that $\Th{Q}38\Proves \eq[\num{l}][\num{m}]$. On the other hand, by39\olref[bre]{lem:q-proves-neq}, $\Th{Q} \Proves40\eq/[\num{l}][\num{m}]$. So $\Th{Q}$ is inconsistent. But that is41impossible, since $\Th{Q}$ is satisfied by the standard model (see42\olref[int][def]{def:standard-model}), $\Sat{N}{\Th{Q}}$, and43satisfiable theories are always consistent by the Soundness Theorem44(\tagrefs{prfAX/{fol:axd:sou:cor:consistency-soundness},45prfSC/{fol:seq:sou:cor:consistency-soundness},46prfND/{fol:ntd:sou:cor:consistency-soundness},47prfTab/{fol:tab:sou:cor:consistency-soundness}}).48\end{proof}49\begin{lem}51Every function that is representable in $\Th{Q}$ is computable.52\end{lem}53\begin{proof}55Let's first give the intuitive idea for why this is true. To56compute~$f$, we do the following. List all the possible57!!{derivation}s~$\delta$ in the language of arithmetic. This is58possible to do mechanically. For each one, check if it is59!!a{derivation} of !!a{formula} of the form~$!A_f(\num{n_0}, \dots,60\num{n_k}, \num{m})$ (the !!{formula} representing $f$ in~$\Th{Q}$61from \olref{lem:rep-q}). If it is, $m = f(n_0, \dots, n_k)$ by62\olref{lem:rep-q}, and we've found the value of~$f$. The search63terminates because $\Th{Q} \Proves !A_f(\num{n_0}, \dots, \num{n_k},64\num{f(n_0, \dots, n_k)})$, so eventually we find a $\delta$ of the65right sort.66This is not quite precise because our procedure operates on68!!{derivation}s and !!{formula}s instead of just on numbers, and we69haven't explained exactly why ``listing all possible !!{derivation}s''70is mechanically possible. But as we've seen, it is possible to code71terms, !!{formula}s, and !!{derivation}s by G\"odel numbers. We've72also introduced a precise model of computation, the general recursive73functions. And we've seen that the relation $\Prf[\Th{Q}](d,y)$, which74holds iff $d$ is the G\"odel number of !!a{derivation} of the !!{formula}75with G\"odel number~$y$ from the axioms of~$\Th{Q}$, is (primitive)76recursive. Other primitive recursive functions we'll need are77$\fn{num}$ (\olref[art][trm]{prop:num-primrec}) and $\fn{Subst}$78(\olref[art][sub]{prop:subst-primrec}). From these, it is possible to79define~$f$ by minimization; thus, $f$ is recursive.80First, define82\begin{multline*}83 A(n_0, \dots, n_k, m) = \\84 \fn{Subst}(\fn{Subst}(\dots\fn{Subst}(\Gn{!A_f}, \fn{num}(n_0), \Gn{x_0}),\\ \dots),85 \fn{num}(n_k), \Gn{x_k}), \fn{num}(m), \Gn{y})86\end{multline*}87This looks complicated, but it's just the function $A(n_0, \dots, n_k,88m) = \Gn{!A_f(\num{n_0}, \dots, \num{n_k}, \num{m})}$.89Now, consider the relation~$R(n_0, \dots, n_k, s)$ which holds if91$(s)_0$ is the G\"odel number of !!a{derivation} from~$\Th{Q}$ of92$!A_f(\num{n_0}, \dots, \num{n_k}, \num{(s)_1})$:93\[94R(n_0, \dots, n_k, s) \quad\text{iff}\quad \Prf[\Th{Q}]((s)_0, A(n_0,95\dots, n_k, (s)_1))96\]97If we can find an~$s$ such that $R(n_0, \dots, n_k, s)$ holds, we have98found a pair of numbers---$(s)_0$ and~$(s)_1$---such that $(s)_0$ is99the G\"odel number of !!a{derivation} of~$A_f(\num{n_0}, \dots,100\num{n_k}, (s)_1)$. So looking for~$s$ is like looking for the pair101$d$ and $m$ in the informal proof. And a computable function that102``looks for'' such an $s$ can be defined by regular minimization.103Note that $R$ is regular: for every $n_0$, \dots, $n_k$, there is104!!a{derivation}~$\delta$ of $\Th{Q} \Proves !A_f(\num{n_0}, \dots,105\num{n_k}, \num{f(n_0, \dots, n_k)})$, so $R(n_0, \dots, n_k, s)$106holds for $s = \tuple{\Gn{\delta}, f(n_0, \dots, n_k)}$. So, we can107write $f$ as108\[109f(n_0,\dots,n_{k}) = (\umin{s}{R(n_0, \dots, n_k, s)})_1.110\]111\end{proof}112\end{document}
content/incompleteness/representability-in-q/beta-function.tex
1% Part: incompleteness2% Chapter: representability-in-q3% Section: beta-function4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{inc}{req}{bet}10\olsection{The Beta Function Lemma}11In order to show that we can carry out primitive recursion if14addition, multiplication, and $\Char{=}$ are available, we need to15develop functions that handle sequences. (If we had exponentiation as16well, our task would be easier.) When we had primitive recursion, we17could define things like the ``$n$-th prime,'' and pick a fairly18straightforward coding. But here we do not have primitive19recursion---in fact we want to show that we can do primitive recursion20using minimization---so we need to be more clever.21\begin{lem}23\ollabel{lem:beta}24There is a function $\beta(d,i)$ such that for every sequence $a_0$,25\dots,~$a_n$ there is a number~$d$, such that for every $i \le n$,26$\beta(d,i) = a_i$. Moreover, $\beta$ can be defined from the basic27functions using just composition and regular minimization.28\end{lem}29Think of $d$ as coding the sequence $\tuple{a_0, \dots, a_n}$, and31$\beta(d,i)$ returning the $i$-th element. (Note that this ``coding''32does \emph{not} use the power-of-primes coding we're already familiar33with!). The lemma is fairly minimal; it doesn't say we can concatenate34sequences or append elements, or even that we can \emph{compute}~$d$35from $a_0$, \dots,~$a_n$ using functions definable by composition and36regular minimization. All it says is that there is a ``decoding''37function such that every sequence is ``coded.''38The use of the notation $\beta$ is G\"odel's. To repeat, the hard part40of proving the lemma is defining a suitable~$\beta$ using the41seemingly restricted resources, i.e., using just composition and42minimization---however, we're allowed to use addition, multiplication,43and~$\Char{=}$. There are various ways to prove this lemma, but one of44the cleanest is still G\"odel's original method, which used a45number-theoretic fact called Sunzi's Theorem46(traditionally, the ``Chinese Remainder Theorem'').47\begin{defn}49Two natural numbers $a$ and $b$ are \emph{relatively prime} iff their50greatest common divisor is~$1$; in other words, they have no other51divisors in common.52\end{defn}53\begin{defn}55Natural numbers $a$ and $b$ are \emph{congruent modulo~$c$},56$a \equiv b \mod c$, iff $c \mid (a-b)$, i.e., $a$ and $b$ have the57same remainder when divided by~$c$.58\end{defn}59Here is Sunzi's Theorem:61\begin{thm}62Suppose $x_0$, \dots,~$x_n$ are (pairwise) relatively prime. Let63$y_0$, \dots,~$y_n$ be any numbers. Then there is a number $z$ such that64\begin{align*}65z & \equiv y_0 \mod x_0 \\66z & \equiv y_1 \mod x_1 \\67& \vdots \\68z & \equiv y_n \mod x_n.69\end{align*}70\end{thm}71Here is how we will use Sunzi's Theorem: if $x_0$,73\dots,~$x_n$ are bigger than $y_0$, \dots,~$y_n$ respectively, then we74can take $z$ to code the sequence $\tuple{y_0, \dots,y_n}$. To75recover~$y_i$, we need only divide $z$ by~$x_i$ and take the76remainder. To use this coding, we will need to find suitable values77for $x_0$, \dots,~$x_n$.78A couple of observations will help us in this regard. Given80$y_0$, \dots,~$y_n$, let81\begin{align*}82j &= \max(n, y_0 + 1, \dots, y_n + 1), \\83m &= \lcm(1,\dots,j),84\end{align*}85and let86\begin{align*}87x_0 & = 1 + m \\88x_1 & = 1 + 2 \cdot m \\89x_2 & = 1 + 3 \cdot m \\90& \vdots \\91x_n & = 1 + (n+1) \cdot m92\end{align*}93Then two things are true:94\begin{enumerate}95\item\ollabel{rel-prime} $x_0,\dots,x_n$ are relatively prime.96\item\ollabel{less} For each $i$, $y_i < x_i$.97\end{enumerate}98To see that \olref{rel-prime} is true, note that if $p$ is a prime number99and $p \mid x_i$ and $p \mid x_k$, then $p \mid 1 + (i+1) m$ and100$p \mid 1 + (k+1) m$. But then $p$ divides their difference,101\[102(1 + (i+1)m) - (1+ (k+1)m) = (i-k) m.103\]104Since $p$ divides $1 + (i+1)m$, it can't divide $m$ as well105(otherwise, the first division would leave a remainder of~$1$). So $p$106divides $i-k$, since $p$ divides $(i-k)m$. But $\left|i-k\right|$ is at107most~$n$, and we have chosen $j \geq n$, so this implies that108$p \mid m$, again a contradiction. So there is no prime number dividing109both $x_i$ and $x_k$. Clause~\olref{less} is easy:110we have $y_i < j \leq m < x_i$.111Now let us prove the $\beta$ function lemma. Remember that we can use113$0$, successor, plus, times, $\Char{=}$, projections, and any function114defined from them using composition and minimization applied to115regular functions. We can also use a relation if its characteristic116function is so definable. As before we can show that these relations117are closed under Boolean combinations and bounded quantification; for118example:119\begin{align*}120\fn{not}(x) & \defis \Char{=}(x,0)\\121\bmin{x \leq z}{R(x,y)} & \defis \umin{x}{(R(x,y) \lor x = z)}\\122\bexists{x \leq z}{R(x,y)} & \defiff R(\bmin{x \leq z}{R(x,y)}, y)123\end{align*}124We can then show that all of the following are also definable without125primitive recursion:126\begin{enumerate}127\item The pairing function, $J(x,y) = \frac{1}{2}[(x+y)(x+y+1)] + x$;128% maybe explain more what is going on here, a bit confusing.129\item the projection functions130\begin{align*}131K(z) & = \bmin{x \leq z}{\bexists{y \leq z}{z = J(x,y)}},\\132L(z) & = \bmin{y \leq z}{\bexists{x \leq z}{z = J(x,y)}};133\end{align*}134\item the less-than relation $x < y$;135\item the divisibility relation $x \mid y$;136% \item $x \tsub y$137% \item $\fn{Prime}(x)$138% \item Assuming $p$ is prime, the relation ``$x$ is a power of $p$'':139% \[140% \bforall{y \leq x}{(y \mid x \lif y = 1 \lor y = x)}.141% \]142\item the function $\fn{rem}(x,y)$ which returns the remainder when143 $y$ is divided by~$x$.144\end{enumerate}145Now define146\begin{align*}147\beta^*(d_0,d_1,i) & = \fn{rem}(1+(i+1) d_1,d_0) \text{ and}\\148\beta(d,i) & = \beta^*(K(d),L(d),i).149\end{align*}150This is the function we want. Given $a_0,\dots,a_n$ as above, let151\[152j = \max(n,a_0+1,\dots,a_n+1),153\]154and let $d_1 = \lcm(1,\dots,j)$. By \olref{rel-prime} above,155we know that $1+d_1$, $1+2 d_1$, \dots, $1+(n+1) d_1$ are relatively156prime, and by~\olref{less} that all are greater than $a_0,\dots,a_n$.157By Sunzi's Theorem there is a value~$d_0$ such that for each~$i$,158\[159d_0 \equiv a_i \mod (1+(i+1)d_1)160\]161and so (because $d_1$ is greater than~$a_i$),162\[163a_i = \fn{rem}(1+(i+1)d_1,d_0).164\]165Let $d = J(d_0,d_1)$. Then for each $i \le n$, we have166\begin{align*}167\beta(d,i) & = \beta^*(d_0,d_1,i) \\168& = \fn{rem}(1+(i+1) d_1,d_0) \\169& = a_i170\end{align*}171which is what we need. This completes the proof of the172$\beta$-function lemma.173\begin{prob}175 Show that the relations $x < y$, $x \mid y$, and the176 function~$\fn{rem}(x,y)$ can be defined without primitive recursion.177 You may use $0$, successor, plus, times, $\Char{=}$, projections,178 and bounded minimization and quantification.179\end{prob}180\end{document}
content/incompleteness/representability-in-q/prim-rec.tex
1% Part: incompleteness2% Chapter: representability-in-q3% Section: prim-rec4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{inc}{req}{pri}10\olsection{Simulating Primitive Recursion}11Now we can show that definition by primitive recursion can be13``simulated'' by regular minimization using the beta function. Suppose14we have $f(\vec x)$ and $g(\vec x, y, z)$. Then the function~$h(x,\vec15z)$ defined from $f$ and~$g$ by primitive recursion is16\begin{align*}17h(\vec x, 0) & = f(\vec x) \\18h(\vec x, y+1) & = g(\vec x, y, h(\vec x, y)).19\end{align*}20We need to show that $h$ can be defined from $f$ and~$g$ using just21composition and regular minimization, using the basic functions and22functions defined from them using composition and regular minimization23(such as~$\beta$).24\begin{lem}26\ollabel{lem:prim-rec}27If $h$ can be defined from $f$ and $g$ using primitive recursion, it28can be defined from $f$, $g$, the functions $\Zero$, $\Succ$,29$\Proj{n}{i}$, $\Add$, $\Mult$, $\Char{=}$, using composition and30regular minimization.31\end{lem}32\begin{proof}34First, define an auxiliary function $\hat h(\vec x, y)$ which returns35the least number~$d$ such that $d$ codes a sequence which satisfies36\begin{enumerate}37\item $(d)_0 = f(\vec x)$, and38\item for each $i < y$, $(d)_{i+1} = g(\vec x, i, (d)_i)$,39\end{enumerate}40where now $(d)_i$ is short for $\beta(d,i)$. In other words, $\hat h$41returns the sequence $\tuple{h(\vec x, 0), h(\vec x, 1), \dots, h(\vec42x, y)}$. We can write $\hat h$ as43\[44\hat h(\vec x, y) = \umin{d}{(\beta(d,0) = f(\vec x) \land \bforall{i <45 y}{\beta(d,i+1) = g(\vec x, i,\beta(d,i)})}.46\]47Note: no primitive recursion is needed here, just minimization. The48function we minimize is regular because of the beta function lemma49\olref[bet]{lem:beta}.50But now we have52\[53h(\vec x, y) = \beta(\hat h(\vec x, y), y),54\]55so $h$ can be defined from the basic functions using just composition56and regular minimization.57\end{proof}58\end{document}
content/incompleteness/representability-in-q/basic-representable.tex
1% Part: incompleteness2% Chapter: representability-in-q3% Section: basic-representable4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{inc}{req}{bre}10\olsection{Basic Functions are Representable in~$\Th{Q}$}11First we have to show that all the basic functions are representable13in~$\Th{Q}$. In the end, we need to show how to assign to each $k$-ary14basic function $f(x_0,\dots,x_{k-1})$ !!a{formula}15$!A_f(x_0,\dots,x_{k-1},y)$ that represents it.16We will be able to represent zero, successor, plus, times, the18characteristic function for equality, and projections. In each case,19the appropriate representing function is entirely straightforward; for20example, zero is represented by the formula $y = \Obj 0$, successor is21represented by the !!{formula} $x_0' = y$, and addition is represented22by the !!{formula} $(x_0 + x_1) = y$. The work involves showing that23$\Th{Q}$ can prove the relevant !!{sentence}s; for example, saying24that addition is represented by the !!{formula} above involves showing25that for every pair of natural numbers $m$ and $n$, $\Th{Q}$ proves26\begin{align*}27& \eq[\num n + \num m][\num {n+m}] \text{ and}\\28& \lforall[y][(\eq[(\num n + \num m)][y] \lif \eq[y][\num{n+m}])].29\end{align*}30\begin{prop}32\ollabel{prop:rep-zero}33The zero function $\Zero(x) = 0$ is represented in~$\Th{Q}$ by34$!A_{\Zero}(x,y) \ident \eq[y][\Obj 0]$.35\end{prop}36\begin{prop}38\ollabel{prop:rep-succ}39The successor function $\Succ(x) = x+1$ is represented in~$\Th{Q}$ by40$!A_{\Succ}(x,y) \ident \eq[y][x']$. 41\end{prop}42\begin{prop}44\ollabel{prop:rep-proj}45The projection function $\Proj{n}{i}(x_0, \dots, x_{n-1}) = x_i$ is46represented in~$\Th{Q}$ by \[!A_{\Proj{n}{i}}(x_0, \dots, x_{n-1}, y) \ident \eq[y][x_i].\]47\end{prop}48\begin{prob}50Prove that $\eq[y][\Obj 0]$, $\eq[y][x']$, and $\eq[y][x_i]$ represent51$\Zero$, $\Succ$, and $\Proj{n}{i}$, respectively.52\end{prob}53\begin{prop}55\ollabel{prop:rep-id}56The characteristic function of~$=$,57\[58\Char{=}(x_0, x_1) =59\begin{cases}60 1 & \text{if } x_0 =x_1\\61 0 & otherwise62\end{cases}63\]64is represented in~$\Th{Q}$ by65\[66 !A_{\Char{=}}(x_0, x_1, y) \ident (\eq[x_0][x_1] \land \eq[y][\num{1}]) \lor (\eq/[x_0][x_1] \land67\eq[y][\num{0}]).68\]69\end{prop}70The proof requires the following lemma.72\begin{lem}74\ollabel{lem:q-proves-neq} Given natural numbers $n$ and $m$, if $n75\neq m$, then $\Th{Q} \Proves \eq/[\num n][\num m]$.76\end{lem}77\begin{proof}79Use induction on $n$ to show that for every $m$, if $n \neq m$, then80$Q \Proves \eq/[\num n][\num m]$.81In the base case, $n = 0$. If $m$ is not equal to $0$, then $m = k +831$ for some natural number $k$. We have an axiom that says84$\lforall[x][\eq/[0][x']]$. By a quantifier axiom, replacing $x$ by85 $\num k$, we can conclude $\eq/[0][\num k']$. But $\num k'$ is just86 $\num m$.87In the induction step, we can assume the claim is true for $n$, and89consider $n+1$. Let $m$ be any natural number. There are two90possibilities: either $m = 0$ or for some $k$ we have $m = k+1$. The91first case is handled as above. In the second case, suppose $n+1 \neq92k+1$. Then $n \neq k$. By the induction hypothesis for $n$ we have93$\Th{Q} \Proves \eq/[\num n][\num k]$. We have an axiom that says94$\lforall[x][\lforall[y][\eq[x'][y'] \lif \eq[x][y]]]$. Using a95quantifier axiom, we have $\eq[\num n'][\num k'] \lif \eq[\num n][\num96 k]$. Using propositional logic, we can conclude, in $\Th{Q}$,97$\eq/[\num n][\num k] \lif \eq/[\num n'][\num k']$. Using modus98ponens, we can conclude $\eq/[\num n'][\num k']$, which is what we want,99since $\num k'$ is $\num m$.100\end{proof}101\begin{explain}103Note that the lemma does not say much: in essence it says that $\Th{Q}$ can104prove that different numerals denote different objects. For example,105$\Th{Q}$ proves $0'' \neq 0'''$. But showing that this holds in general106requires some care. Note also that although we are using induction, it107is induction \emph{outside} of $\Th{Q}$.108\end{explain}109\begin{proof}[Proof of \olref{prop:rep-id}]111If $n = m$, then $\num{n}$ and $\num{m}$ are the same term, and112$\Char{=}(n, m) = 1$. But $\Th{Q} \Proves (\eq[\num{n}][\num{m}] \land113\eq[\num{1}][\num{1}])$, so it proves $!A_=(\num{n}, \num{m},114\num{1})$. If $n \neq m$, then $\Char=(n, m) = 0$. By115\olref{lem:q-proves-neq}, $\Th{Q} \Proves \eq/[\num{n}][\num{m}]$ and116so also $(\eq/[\num{n}][\num{m}] \land \Obj 0 = \Obj 0)$. Thus $\Th{Q}117\Proves !A_=(\num{n}, \num{m}, \num{0})$.118For the second part, we also have two cases. If $n = m$, we have to120show that $\Th{Q} \Proves \lforall[y][(!A_=(\num{n}, \num{m}, y)121 \lif \eq[y][\num{1}])]$. Arguing informally, suppose $!A_=(\num{n},122\num{m}, y)$, i.e.,123\[124(\eq[\num{n}][\num{n}] \land \eq[y][\num{1}]) \lor125(\eq/[\num{n}][\num{n}] \land \eq[y][\num{0}])126\]127The left disjunct implies $\eq[y][\num{1}]$ by logic; the right128contradicts $\eq[\num{n}][\num{n}]$ which is provable by logic.129Suppose, on the other hand, that $n \neq m$. Then $!A_=(\num{n},131\num{m}, y)$ is132\[133(\eq[\num{n}][\num{m}] \land \eq[y][\num{1}]) \lor134(\eq/[\num{n}][\num{m}] \land \eq[y][\num{0}])135\]136Here, the left disjunct contradicts $\eq/[\num{n}][\num{m}]$, which is137provable in $\Th{Q}$ by \olref{lem:q-proves-neq}; the right disjunct138entails $\eq[y][\num{0}]$.139\end{proof}140\begin{prop}142\ollabel{prop:rep-add}143The addition function $\Add(x_0, x_1) = x_0+x_1$ is represented144in~$\Th{Q}$ by145\[146 !A_{\Add}(x_0, x_1, y) \ident \eq[y][(x_0 + x_1)].147\]148\end{prop}149\begin{lem}151\ollabel{lem:q-proves-add}152$\Th{Q} \Proves \eq[(\num{n} + \num{m})][\num{n+m}]$153\end{lem}154\begin{proof}156We prove this by induction on~$m$. If $m = 0$, the claim is that157$\Th{Q} \Proves \eq[(\num{n} + \Obj 0)][\num{n}]$. This follows by158axiom~$!Q_4$. Now suppose the claim for $m$; let's prove the claim159for $m+1$, i.e., prove that $\Th{Q} \Proves \eq[(\num{n} +160 \num{m+1})][\num{n+m+1}]$. Note that $\num{m+1}$ is just $\num{m}'$,161and $\num{n+m+1}$ is just $\num{n+m}'$. By axiom $!Q_5$, $\Th{Q}162\Proves \eq[(\num{n} + \num{m}')][(\num{n}+\num{m})']$. By induction163hypothesis, $\Th{Q} \Proves \eq[(\num{n} + \num{m})][\num{n+m}]$. So164$\Th{Q} \Proves \eq[(\num{n} + \num{m}')][\num{n+m}']$.165\end{proof}166\begin{proof}[Proof of \olref{prop:rep-add}]168The !!{formula}~$!A_\Add(x_0, x_1, y)$ representing $\Add$ is169$\eq[y][(x_0 + x_1)]$. First we show that if $\Add(n, m) = k$, then170$\Th{Q} \Proves !A_\Add(\num{n}, \num{m}, \num{k})$, i.e., $\Th{Q}171\Proves \eq[\num{k}][(\num{n} + \num{m})]$. But since $k = n + m$,172$\num{k}$ just is $\num{n+m}$, and we've shown in173\olref{lem:q-proves-add} that $\Th{Q} \Proves \eq[(\num{n} +174 \num{m})][\num{n+m}]$.175We also have to show that if $\Add(n, m) = k$, then177\[178\Th{Q} \Proves \lforall[y][(!A_\Add(\num{n}, \num{m}, y) \lif179 \eq[y][\num{k}])].180\]181Suppose we have $\eq[(\num{n} + \num{m})][y]$. Since182\[183\Th{Q} \Proves \eq[(\num{n}+\num{m})][\num{n+m}],184\]185we can replace the left side with $\num{n+m}$ and get186$\eq[\num{n+m}][y]$, for arbitrary~$y$.187\end{proof}188\begin{prop}190\ollabel{prop:rep-mult}191The multiplication function $\Mult(x_0, x_1) = x_0 \cdot x_1$ is represented192in~$\Th{Q}$ by193\[194 !A_{\Mult}(x_0, x_1, y) \ident y = (x_0 \times x_1).195\]196\end{prop}197\begin{proof} Exercise. \end{proof}199\begin{lem}201\ollabel{lem:q-proves-mult}202$\Th{Q} \Proves \eq[(\num{n} \times \num{m})][\num{n \cdot m}]$203\end{lem}204\begin{proof} Exercise. \end{proof}206\begin{prob}208Prove \olref[inc][req][bre]{lem:q-proves-mult}.209\end{prob}210\begin{prob}212Use \olref[inc][req][bre]{lem:q-proves-mult} to prove213\olref[inc][req][bre]{prop:rep-mult}.214\end{prob}215\begin{explain}217 Recall that we use $\times$ for the function symbol of the language218 of arithmetic, and $\cdot$ for the ordinary multiplication operation219 on numbers. So $\cdot$ can appear between expressions for numbers220 (such as in $m \cdot n$) while $\times$ appears only between terms221 of the language of arithmetic (such as in $(\num{m} \times222 \num{n})$). Even more confusingly, $+$ is used for both the223 !!{function} and the addition operation. When it appears between224 terms---e.g., in $(\num{n} + \num{m})$---it is the $2$-place225 !!{function} of the language of arithmetic, and when it appears226 between numbers---e.g., in $n+m$---it is the addition operation.227 This includes the case $\num{n+m}$: this is the standard numeral228 corresponding to the number~$n+m$.229\end{explain}230\end{document}
content/incompleteness/representability-in-q/composition-representable.tex
1% Part: incompleteness2% Chapter: representability-in-q3% Section: composition-representable4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{inc}{req}{cmp}10\olsection{Composition is Representable in $\Th{Q}$}11Suppose $h$ is defined by13\[14h(x_0,\dots,x_{l-1}) = f(g_0(x_0,\dots,x_{l-1}), \dots,15g_{k-1}(x_0,\dots,x_{l-1})).16\]17where we have already found !!{formula}s $!A_f, !A_{g_0}, \dots,18!A_{g_{k-1}}$ representing the functions $f$, and $g_0$,19\dots,~$g_{k-1}$, respectively. We have to find !!a{formula}~$!A_h$20representing $h$.21Let's start with a simple case, where all functions are $1$-place,23i.e., consider $h(x) = f(g(x))$. If $!A_f(y, z)$ represents~$f$, and24$!A_g(x, y)$ represents~$g$, we need !!a{formula}~$!A_h(x, z)$ that25represents~$h$. Note that $h(x) = z$ iff there is a~$y$ such that26both $z = f(y)$ and $y = g(x)$. (If $h(x) = z$, then $g(x)$ is such27a~$y$; if such a $y$ exists, then since $y = g(x)$ and $z = f(y)$, $z28= f(g(x))$.) This suggests that $\lexists[y][(!A_g(x, y) \land !A_f(y,29 z))]$ is a good candidate for~$!A_h(x, z)$. We just have to verify30that $\Th{Q}$ proves the relevant !!{formula}s.31\begin{prop}33\ollabel{prop:rep1}34If $h(n) = m$, then $\Th{Q} \Proves !A_h(\num{n}, \num{m})$.35\end{prop}36\begin{proof}38Suppose $h(n) = m$, i.e., $f(g(n)) = m$. Let $k = g(n)$. Then39\begin{align*}40 \Th{Q} & \Proves !A_g(\num{n}, \num{k})41 \intertext{since $!A_g$ represents~$g$, and}42 \Th{Q} & \Proves !A_f(\num{k}, \num{m})43 \intertext{since $!A_f$ represents~$f$. Thus,}44 \Th{Q} & \Proves !A_g(\num{n}, \num{k}) \land !A_f(\num{k}, \num{m})45 \intertext{and consequently also}46 \Th{Q} & \Proves \lexists[y][(!A_g(\num{n}, y) \land !A_f(y, \num{m}))],47\end{align*}48i.e., $\Th{Q} \Proves !A_h(\num{n}, \num{m})$.49\end{proof}50\begin{prop}52\ollabel{prop:rep2}53If $h(n) = m$, then $\Th{Q} \Proves \lforall[z][(!A_h(\num{n}, z) \lif54 z = \num{m})]$.55\end{prop}56\begin{proof}58Suppose $h(n) = m$, i.e., $f(g(n)) = m$. Let $k = g(n)$. Then59\begin{align*}60 \Th{Q} & \Proves \lforall[y][(!A_g(\num{n}, y) \lif \eq[y][\num{k}])]61 \intertext{since $!A_g$ represents~$g$, and}62 \Th{Q} & \Proves \lforall[z][(!A_f(\num{k}, z) \lif \eq[z][\num{m}])]63 \intertext{since $!A_f$ represents~$f$. Using just a little bit of64 logic, we can show that also}65 \Th{Q} & \Proves \lforall[z][(\lexists[y][(!A_g(\num{n}, y) \land66 !A_f(y, z))] \lif \eq[z][\num{m}])].67\end{align*}68i.e., $\Th{Q} \Proves \lforall[y][(!A_h(\num n, y) \lif \eq[y][\num m])]$.69\end{proof}70The same idea works in the more complex case where $f$ and~$g_i$ have72arity greater than~$1$.73\begin{prop}75\ollabel{prop:rep-composition}76If $!A_f(y_0, \dots, y_{k-1}, z)$ represents $f(y_0, \dots, y_{k-1})$77in~$\Th{Q}$, and $!A_{g_i}(x_0, \dots, x_{l-1}, y)$ represents78$g_i(x_0, \dots, x_{l-1})$ in~$\Th{Q}$, then79\begin{multline*}80 \lexists[y_0\dots][\lexists[y_{k-1}][(!A_{g_0}(x_0,\dots,x_{l-1},y_0) \land81 \dots \land {}]]\\82 !A_{g_{k-1}}(x_0,\dots,x_{l-1},y_{k-1}) \land !A_f(y_0,\dots,y_{k-1},z))83\end{multline*}84represents85\[86h(x_0, \dots, x_{l-1}) = f(g_0(x_0, \dots, x_{l-1}), \dots, g_{k-1}(x_0,87\dots, x_{l-1})).88\]89\end{prop}90\begin{proof}92Exercise.93\end{proof}94\begin{prob}96Using the proofs of \olref[inc][req][cmp]{prop:rep2} and97\olref[inc][req][cmp]{prop:rep2} as a guide, carry out the proof of98\olref[inc][req][cmp]{prop:rep-composition} in detail.99\end{prob}100\end{document}
content/incompleteness/representability-in-q/minimization-representable.tex
1% Part: incompleteness2% Chapter: representability-in-q3% Section: minimization-representable4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{inc}{req}{min}10\olsection{Regular Minimization is Representable in $\Th{Q}$}11Let's consider unbounded search. Suppose $g(x, z)$ is regular and13representable in $\Th{Q}$, say by the !!{formula}~$!A_g(x, z, y)$. Let14$f$ be defined by $f(z) = \umin{x}{[g(x, z) = 0]}$. We would like to find15!!a{formula}~$!A_f(z, y)$ representing~$f$. The value of~$f(z)$ is16that number~$x$ which (a) satisfies $g(x, z) = 0$ and (b) is the least17such, i.e., for any $w < x$, $g(w, z) \neq 0$. So the following is a18natural choice:19\[20!A_f(z,y) \ident !A_g(y, z, \Obj 0) \land \lforall[w][(w < y \lif \lnot21 !A_g(w, z, \Obj 0))].22\]23In the general case, of course, we would have to replace $z$ with24$z_0$, \dots, $z_k$.25The proof, again, will involve some lemmas about things $\Th{Q}$ is27strong enough to prove.28\begin{lem}30\ollabel{lem:succ} For every !!{constant}~$a$ and every natural31number~$n$,32\[33\Th{Q} \Proves \eq[(a' + \num n)][(a + \num n)'].34\]35\end{lem}36\begin{proof}38The proof is, as usual, by induction on $n$. In the base case, $n =390$, we need to show that $\Th{Q}$ proves $\eq[(a' + \Obj 0)][(a + \Obj400)']$. But we have:41\begin{align}42 \Th{Q} & \Proves \eq[(a' + \Obj 0)][a'] \quad \text{by axiom $Q_4$}43 \ollabel{step1}\\44 \Th{Q} & \Proves \eq[(a + \Obj 0)][a] \quad \text{by axiom $Q_4$}45 \ollabel{step2} \\46 \Th{Q} & \Proves \eq[(a + \Obj 0)'][a'] \quad \text{by \olref{step2}}47 \ollabel{step3} \\48 \Th{Q} & \Proves \eq[(a' + \Obj 0)][(a + \Obj 0)'] \quad49 \text{by \olref{step1} and \olref{step3}}\notag50\end{align}51In the induction step, we can assume that we have shown that $\Th{Q}52\Proves \eq[(a' + \num n)][(a + \num n)']$. Since53$\num{n+1}$ is $\num{n}'$, we need to show that $\Th{Q}$ proves54$\eq[(a' + \num{n}')][(a + \num{n}')']$. We have:55\begin{align}56 \Th{Q} & \Proves \eq[(a' + \num n')][(a' + \num n)'] \quad57 \text{by axiom $!Q_5$} \ollabel{step5}\\58 \Th{Q} & \Proves \eq[(a' + \num n')][(a + \num n')'] \quad59 \text{inductive hypothesis} \ollabel{step6}\\60 \Th{Q} & \Proves \eq[(a' + \num n)'][(a + \num n')'] \quad61 \text{by \olref{step5} and \olref{step6}.} \notag62\end{align}63\end{proof}64It is again worth mentioning that this is weaker than saying that66$\Th{Q}$ proves $\lforall[x][\lforall[y][(x' + y) = (x + y)']]$.67Although this !!{sentence} is true in~$\Struct{N}$, $\Th{Q}$ does not68prove it.69\begin{lem}71\ollabel{lem:less-zero}72$\Th{Q} \Proves \lforall[x][\lnot x < \Obj 0]$.73\end{lem}74\begin{proof}76We give the proof informally (i.e., only giving hints as to77how to construct the formal !!{derivation}).78We have to prove $\lnot a < \Obj 0$ for an arbitrary~$a$. By the80definition of $<$, we need to prove $\lnot81\lexists[y][\eq[(y'+a)][\Obj 0]]$ in $\Th{Q}$. We'll assume82$\lexists[y][\eq[(y'+a)][\Obj 0]]$ and prove a contradiction. Suppose83$\eq[(b'+a)][\Obj 0]$. Using $!Q_3$, we84have that $\eq[a][\Obj 0] \lor \lexists[y][\eq[a][y']]$. We85distinguish cases. 86Case 1: $\eq[a][\Obj 0]$ holds. From $\eq[(b'+a)][\Obj 0]$, we have88$\eq[(b' + \Obj 0)][\Obj 0]$. By axiom~$!Q_4$ of $\Th{Q}$, we have89$\eq[(b' + \Obj 0)][b']$, and hence $\eq[b'][\Obj 0]$. But by90axiom~$!Q_2$ we also have $\eq/[b'][\Obj 0]$, a contradiction. 91Case 2: For some $c$, $\eq[a][c']$. But then we have $\eq[(b' +93c')][\Obj 0]$. By axiom~$!Q_5$, we have $\eq[(b' + c)'][\Obj 0]$, again94contradicting axiom~$Q_2$.95\end{proof}96\begin{lem}98\ollabel{lem:less-nsucc}99For every natural number~$n$, 100 \[101 \Th{Q} \Proves102 \lforall[x][(x < \num {n+1} \lif (\eq[x][\Obj 0] \lor \dots \lor103 \eq[x][\num n]))].104 \]105\end{lem}106\begin{proof}108We use induction on~$n$. Let us consider the base case, when $n = 0$.109In that case, we need to show $a < \num 1 \lif \eq[a][\Obj 0]$, for110arbitrary~$a$. Suppose $a < \num 1$. Then by the defining axiom for111$<$, we have $\lexists[y][\eq[(y'+a)][\Obj 0']]$ (since $\num 1 \ident112\Obj 0'$).113Suppose $b$ has that property, i.e., we have $\eq[(b'+a)][\Obj 0']$.115We need to show $\eq[a][\Obj 0]$. By axiom~$!Q_3$, we have either116$\eq[a][\Obj 0]$ or that there is a $c$ such that $\eq[a][c']$. In the117former case, there is nothing to show. So suppose $\eq[a][c']$. Then118we have $\eq[(b' + c')][\Obj 0']$. By axiom~$!Q_5$ of $\Th{Q}$, we have119$\eq[(b'+c)'][\Obj 0']$. By axiom~$!Q_1$, we have $\eq[(b' + c)][\Obj1200]$. But this means, by axiom~$!Q_8$, that $c < \Obj 0$, contradicting121\olref{lem:less-zero}.122Now for the inductive step. We prove the case for $n+1$, assuming the124case for~$n$. So suppose $a < \num {n+2}$. Again using $!Q_3$ we can125distinguish two cases: $\eq[a][\Obj 0]$ and for some $b$,126$\eq[a][b']$. In the first case, $\eq[a][\Obj 0] \lor \dots \lor127\eq[a][\num{n+1}]$ follows trivially. In the second case, we have $b'128< \num {n+2}$, i.e., $b' < \num{n+1}'$. By axiom~$!Q_8$, for some $c$,129$\eq[(c'+b')][\num{n+1}']$. By axiom $!Q_5$,130$\eq[(c'+b)'][\num{n+1}']$. By axiom~$!Q_1$, $\eq[(c'+b)][\num{n+1}]$,131and so $b < \num{n+1}$ by axiom~$!Q_8$. By inductive hypothesis,132$\eq[b][\Obj 0] \lor \dots \lor \eq[b][\num{n}]$. From this, we get133$\eq[b'][\Obj 0'] \lor \dots \lor \eq[b'][\num{n}']$ by logic, and so134$\eq[a][\num{1}] \lor \dots \lor \eq[a][\num{n+1}]$ since135$\eq[a][b']$.136\end{proof}137\begin{lem}139 \ollabel{lem:trichotomy} For every natural number~$m$,140 \[141 \Th{Q} \Proves142 \lforall[y][((y < \num{m} \lor \num{m} < y) \lor \eq[y][\num{m}])].143 \]144\end{lem}145\begin{proof}147By induction on~$m$. First, consider the case $m=0$. $\Th{Q} \Proves148\lforall[y][(\eq[y][\Obj 0] \lor \lexists[z][\eq[y][z']])]$ by~$!Q_3$.149Let $a$ be arbitrary. Then either $\eq[a][\Obj 0]$ or for some~$b$,150$\eq[a][b']$. In the former case, we also have $(a < \Obj 0 \lor \Obj1510 < a) \lor \eq[a][\Obj 0]$. But if $\eq[a][b']$, then $\eq[(b' +152\Obj 0)][(a + \Obj 0)]$ by the logic of~$\eq$. By $!Q_4$, $\eq[(a +153\Obj 0)][a]$, so we have $\eq[(b' + \Obj 0)][a]$, and hence154$\lexists[z][\eq[(z' + \Obj 0)][a]]$. By the definition of $<$ in155$!Q_8$, $\Obj 0 < a$. If $\Obj 0 < a$, then also $(\Obj 0 < a \lor a156< \Obj 0) \lor \eq[a][\Obj 0]$. 157Now suppose we have159\begin{align*}160 \Th{Q} & \Proves \lforall[y][((y < \num{m} \lor \num{m} < y) \lor161 \eq[y][\num{m}])]162 \intertext{and we want to show}163 \Th{Q} & \Proves \lforall[y][((y < \num{m+1} \lor \num{m+1} < y) \lor164 \eq[y][\num{m+1}])]165\end{align*}166Let $a$ be arbitrary. By $!Q_3$, either $\eq[a][\Obj 0]$ or for167some~$b$, $\eq[a][b']$. In the first case, we have $\eq[\num{m}' +168a][\num{m+1}]$ by $!Q_4$, and so $a < \num{m+1}$ by $!Q_8$.169Now consider the second case, $\eq[a][b']$. By the induction171hypothesis, $(b < \num{m} \lor \num{m} < b) \lor172 \eq[b][\num{m}]$.173The first disjunct $b < \num{m}$ is equivalent (by $!Q_8$) to175$\lexists[z][\eq[(z' + b)][\num{m}]]$. Suppose $c$ has this property.176If $\eq[(c' + b)][\num{m}]$, then also $\eq[(c' + b)'][\num{m}']$. By177$!Q_5$, $\eq[(c' + b)'][(c' + b')]$. Hence, $\eq[(c' +178b')][\num{m}']$. We get $\lexists[u][\eq[(u' + b')][\num{m+1}]]$ by179existentially generalizing on~$c'$ and keeping in mind that $\num{m}'180\ident \num{m+1}$. Hence, if $b < \num{m}$ then $b' < \num{m+1}$ and181so $a < \num{m+1}$.182Now suppose $\num{m} < b$, i.e., $\lexists[z][\eq[(z' +184\num{m})][b]]$. Suppose $c$ is such a~$z$, i.e., $\eq[(c' +185\num{m})][b]$. By logic, $\eq[(c' + \num{m})'][b']$. By $!Q_5$,186$\eq[(c' + \num{m}')][b']$. Since $\eq[a][b']$ and $\num{m}' \ident187\num{m+1}$, $\eq[(c' + \num{m+1})][a]$. By $!Q_8$, $\num{m+1} < a$.188Finally, assume $\eq[b][\num{m}]$. Then, by logic,190$\eq[b'][\num{m}']$, and so $\eq[a][\num{m+1}]$.191Hence, from each disjunct of the case for~$m$ and~$b$, we can obtain193the corresponding disjunct for~$m+1$ and~$a$.194\end{proof}195 196\begin{prop}197\ollabel{prop:rep-minimization}198If $!A_g(x, z, y)$ represents $g(x, z)$ in~$\Th{Q}$, then199\[200!A_f(z,y) \ident !A_g(y, z, \Obj 0) \land \lforall[w][(w < y \lif \lnot201 !A_g(w, z, \Obj 0))]202\]203represents $f(z) = \umin{x}{[g(x, z) = 0]}$.204\end{prop}205\begin{proof}207First we show that if $f(n) = m$, then $\Th{Q} \Proves !A_f(\num n, \num m)$,208i.e., 209\begin{align}210 \Th{Q} & \Proves !A_g(\num{m}, \num{n}, \Obj 0) \land \lforall[w][(w <211 \num{m} \lif \lnot !A_g(w, \num{n}, \Obj 0))]. \notag212 \intertext{Since $!A_g(x, z, y)$ represents $g(x, z)$ and $g(m, n) =213 0$ if $f(n) = m$, we have}214\Th{Q} & \Proves !A_g(\num{m}, \num{n}, \Obj 0). \notag215\intertext{If $f(n) = m$, then for every $k < m$, $g(k, n) \neq 0$. So}216\Th{Q} & \Proves \lnot !A_g(\num{k}, \num{n}, \Obj 0). \notag217\intertext{We get that}218\Th{Q} & \Proves \lforall[w][(w < \num{m} \lif \lnot219 !A_g(w, \num{n}, \Obj 0))]. \ollabel{rep-less}220\end{align}221by \olref{lem:less-zero} in case $m = 0$ and by \olref{lem:less-nsucc} otherwise.222Now let's show that if $f(n) = m$, then $\Th{Q} \Proves224\lforall[y][(!A_f(\num{n}, y) \lif \eq[y][\num{m}])]$. We again225sketch the argument informally, leaving the formalization to the226reader.227Suppose $!A_f(\num{n}, b)$. From this we get (a) $!A_g(b, \num{n},229\Obj 0)$ and (b) $\lforall[w][(w < b \lif \lnot !A_g(w, \num{n}, \Obj230 0))]$. By \olref{lem:trichotomy}, $(b < \num{m} \lor \num{m} < b)231\lor \eq[b][\num{m}]$. We'll show that both $b < \num{m}$ and $\num{m}232< b$ leads to a contradiction.233If $\num{m} < b$, then $\lnot !A_g(\num{m}, \num{n}, \Obj 0)$235from~(b). But $m = f(n)$, so $g(m, n) = 0$, and so $\Th{Q} \Proves236!A_g(\num{m}, \num{n}, \Obj 0)$ since $!A_g$ represents~$g$. So we237have a contradiction.238Now suppose $b < \num{m}$. Then since $\Th{Q} \Proves \lforall[w][(w <240 \num{m} \lif \lnot !A_g(w, \num{n}, \Obj 0))]$ by \olref{rep-less}, we241get $\lnot !A_g(b, \num{n}, \Obj 0)$. This again contradicts~(a).242\end{proof}243\end{document}
content/incompleteness/representability-in-q/comp-representable.tex
1% Part: incompleteness2% Chapter: representability-in-q3% Section: comp-representable4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{inc}{req}{crq}10\olsection{Computable Functions are Representable in $\Th{Q}$}11\begin{thm}13Every computable function is representable in~$\Th{Q}$.14\end{thm}15\begin{proof}17For definiteness, and using the Church--Turing Thesis, let's say that a18function is computable iff it is general recursive. The general19recursive functions are those which can be defined from the zero20function~$\Zero$, the successor function~$\Succ$, and the projection21function~$\Proj{n}{i}$ using composition, primitive recursion, and22regular minimization. By \olref[pri]{lem:prim-rec}, any function~$h$23that can be defined from $f$ and~$g$ can also be defined using24composition and regular minimization from $f$, $g$, and $\Zero$,25$\Succ$, $\Proj{n}{i}$, $\Add$, $\Mult$, $\Char{=}$. Consequently, a26function is general recursive iff it can be defined from $\Zero$,27$\Succ$, $\Proj{n}{i}$, $\Add$, $\Mult$, $\Char{=}$ using composition28and regular minimization.29We've furthermore shown that the basic functions in question are31representable in~$\Th{Q}$32(\cref{inc:req:bre:prop:rep-zero,inc:req:bre:prop:rep-succ,inc:req:bre:prop:rep-proj,inc:req:bre:prop:rep-id,inc:req:bre:prop:rep-add,inc:req:bre:prop:rep-mult}),33and that any function defined from representable functions by34composition or regular minimization35(\olref[cmp]{prop:rep-composition},36\olref[min]{prop:rep-minimization}) is also representable. Thus every37general recursive function is representable in~$\Th{Q}$.38\end{proof}39\begin{explain}41We have shown that the set of computable functions can be42characterized as the set of functions representable in $\Th{Q}$. In43fact, the proof is more general. From the definition of44representability, it is not hard to see that any theory extending45$\Th{Q}$ (or in which one can interpret $\Th{Q}$) can represent the46computable functions. But, conversely, in any !!{derivation} system in47which the notion of !!{derivation} is computable, every representable48function is computable. So, for example, the set of computable49functions can be characterized as the set of functions representable50in Peano arithmetic, or even Zermelo--Fraenkel set theory. As G\"odel51noted, this is somewhat surprising. We will see that when it comes to52provability, questions are very sensitive to which theory you53consider; roughly, the stronger the axioms, the more you can prove.54But across a wide range of axiomatic theories, the representable55functions are exactly the computable ones; stronger theories do not56represent more functions as long as they are axiomatizable.57\end{explain}58\end{document}
content/incompleteness/representability-in-q/representing-relations.tex
1% Part: incompleteness2% Chapter: representability-in-q3% Section: representing-relations4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{inc}{req}{rel}10\olsection{Representing Relations}12Let us say what it means for a \emph{relation} to be representable.14\begin{defn}16\ollabel{defn:representing-relations} A relation $R(x_0,\dots,x_k)$ on17the natural numbers is {\em representable in $\Th{Q}$} if there is a18formula $!A_R(x_0,\dots,x_k)$ such that whenever $R(n_0,\dots,n_k)$ is19true, $\Th{Q}$ proves $!A_R(\num{n_0},\dots,\num{n_k})$, and whenever20$R(n_0,\dots,n_k)$ is false, $\Th{Q}$ proves $\lnot !A_R(\num{n_0},21\dots, \num{n_k})$.22\end{defn}23\begin{thm}25\ollabel{thm:representing-rels} A relation is representable in26$\Th{Q}$ if and only if it is computable.27\end{thm}28\begin{proof}30For the forwards direction, suppose $R(x_0,\dots,x_k)$ is31represented by the formula $!A_R(x_0,\dots,x_k)$. Here is an32algorithm for computing $R$: on input $n_0$, \dots,~$n_k$, simultaneously33search for a proof of $!A_R(\num{n_0}, \dots, \num{n_k})$ and a proof of34$\lnot !A_R(\num{n_0}, \dots, \num{n_k})$. By our hypothesis, the search35is bound to find one or the other; if it is the first, report ``yes,''36and otherwise, report ``no.''37In the other direction, suppose $R(x_0, \dots, x_k)$ is computable. By39definition, this means that the function $\Char{R}(x_0, \dots, x_k)$40is computable. By \olref[int]{thm:representable-iff-comp}, $\Char{R}$41is represented by a formula, say $!A_{\Char{R}}(x_0, \dots, x_k,42y)$. Let $!A_R(x_0, \dots, x_k)$ be the formula $!A_{\Char{R}}(x_0,43\dots, x_k, \num{1})$. Then for any $n_0$, \dots,~$n_k$, if $R(n_0,44\dots, n_k)$ is true, then $\Char{R}(n_0, \dots, n_k) = 1$, in which45case $\Th{Q}$ proves $!A_{\Char{R}}(\num{n_0}, \dots, \num{n_k},46\num{1})$, and so $\Th{Q}$ proves $!A_R(\num{n_0}, \dots,47\num{n_k})$. On the other hand, if $R(n_0, \dots, n_k)$ is false, then48$\Char{R}(n_0, \dots, n_k) = 0$. This means that $\Th{Q}$ proves49\[50\lforall[y][(!A_{\Char{R}}(\num{n_0}, \dots, \num{n_k}, y) \lif y =51 \num{0})].52\]53Since $\Th{Q}$ proves $\eq/[\num{0}][\num{1}]$, $\Th{Q}$ proves54$\lnot !A_{\Char{R}}(\num{n_0}, \dots, \num{n_k}, \num{1})$, and so it55proves $\lnot !A_R(\num{n_0}, \dots, \num{n_k})$.56\end{proof}57\begin{prob}59Show that if $R$ is representable in~$\Th{Q}$, so is~$\Char{R}$.60\end{prob}61\end{document}
content/incompleteness/representability-in-q/undecidability.tex
1% Part: incompleteness2% Chapter: representability-in-q3% Section: undecidability4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{inc}{req}{und}10\olsection{Undecidability}11We call a theory $\Th{T}$ \emph{undecidable} if there is no13computational procedure which, after finitely many steps and14unfailingly, provides a correct answer to the question ``does $\Th{T}$15prove~$!A$?'' for any sentence~$!A$ in the language of~$\Th{T}$. So16$\Th{Q}$ would be decidable iff there were a computational procedure17which decides, given a sentence~$!A$ in the language of arithmetic,18whether $\Th{Q} \Proves !A$ or not. We can make this more precise by19asking: Is the relation~$\Prov[\Th{Q}](y)$, which holds of~$y$20iff $y$ is the G\"odel number of a sentence provable in~$\Th{Q}$,21recursive? The answer is: no.22\begin{thm}24$\Th{Q}$ is undecidable, i.e., the relation25\[26\Prov[\Th{Q}](y) \defiff \fn{Sent}(y) \land27\lexists[x][\Prf[\Th{Q}](x, y)]28\]29is not recursive.30\end{thm}31\begin{proof}33Suppose it were. Then we could solve the halting problem as follows:34Given $e$ and $n$, we know that $\cfind{e}(n) \fdefined$ iff there is35an~$s$ such that $T(e, n, s)$, where $T$ is Kleene's predicate from36\olref[cmp][rec][nft]{thm:kleene-nf}. Since $T$ is primitive recursive37it is representable in~$\Th{Q}$ by a formula $!B_T$, that is, $\Th{Q}38\Proves !B_T(\num{e}, \num{n}, \num{s})$ iff $T(e, n, s)$. If $\Th{Q}39\Proves !B_T(\num{e}, \num{n}, \num{s})$ then also $ \Th{Q} \Proves40\lexists[y][!B_T(\num{e}, \num{n}, y)]$. If no such $s$ exists, then41$\Th{Q} \Proves \lnot !B_T(\num{e}, \num{n}, \num{s})$ for42every~$s$. But $\Th{Q}$ is $\omega$-consistent, i.e., if $\Th{Q}43\Proves \lnot !A(\num{n})$ for every~$n \in \Nat$, then $\Th{Q}44\Proves/ \lexists[y][!A(y)]$. We know this because the axioms of45$\Th{Q}$ are true in the standard model~$\Struct{N}$. So, $\Th{Q}46\Proves/ \lexists[y][!B_T(\num{e}, \num{n}, y)]$. In other words,47$\Th{Q} \Proves \lexists[y][!B_T(\num{e}, \num{n}, y)]$ iff there is48an $s$ such that $T(e, n, s)$, i.e., iff $\cfind{e}(n) \fdefined$.49From $e$ and~$n$ we can compute $\Gn{\lexists[y][!B_T(\num{e},50 \num{n}, y)]}$, let $g(e, n)$ be the primitive recursive function51which does that. So52\[53h(e, n) =54\begin{cases}551 & \text{if $\Prov[\Th{Q}](g(e, n))$}\\560 & \text{otherwise}.57\end{cases}58\]59This would show that $h$ is recursive if $\Prov[\Th{Q}]$ is. But~$h$60is not recursive, by \olref[cmp][rec][hlt]{thm:halting-problem}, so61$\Prov[\Th{Q}]$ cannot be either.62\end{proof}63\begin{cor}65First-order logic is undecidable.66\end{cor}67\begin{proof}69If first-order logic were decidable, provability in~$\Th{Q}$ would be70as well, since $\Th{Q} \Proves !A$ iff $\Proves !T \lif !A$, where71$!T$ is the conjunction of the axioms of~$\Th{Q}$.72\end{proof}73\end{document}
content/incompleteness/representability-in-q/sigma1-completeness.tex
1% Part: incompleteness2% Chapter: representability-in-q3% Section: sigma1-completeness4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{inc}{inp}{s1c}10\olsection{\texorpdfstring{$\Sigma_1$}{Sigma-1} completeness}11Despite the incompleteness of $\Th{Q}$ and its consistent, axiomatizable13extensions, we have seen that $\Th{Q}$ does prove many basic facts about14numerals. In fact, this can be extended quite considerably. To understand15the scope of what can be proved in~$\Th{Q}$, we introduce the notions of16$\Delta_0$, $\Sigma_1$, and $\Pi_1$ !!{formula}s. Roughly speaking, a17$\Sigma_1$ !!{formula} is one of the form $\lexists[x][!B(x)]$, where $!B$18is constructed using only propositional connectives and bounded19quantifiers. We shall show that if $!A$ is a $\Sigma_1$ !!{sentence}20which is true in $\Struct{N}$, then $\Th{Q} \Proves !A$21(\olref{thm:sigma1-completeness}).22\begin{defn}24\ollabel{defn:bd-quant}25A \emph{bounded existential !!{formula}} is one of the form26$\lexists[x][(x < t \land !A(x))]$ where $t$ is any term, which we27conventionally write as $\bexists{x < t}{!A(x)}$.28%29A \emph{bounded universal !!{formula}} is one of the form30$\lforall[x][(x < t \lif !A(x))]$ where $t$ is any term, which we31conventionally write as $\bforall{x < t}{!A(x)}$.32\end{defn}33\begin{defn}35\ollabel{defn:delta0-sigma1-pi1-frm}36A !!{formula} $!B$ is $\Delta_0$ if it is built up from atomic37!!{formula}s using only propositional connectives and bounded38quantification.39%40A !!{formula} $!A$ is $\Sigma_1$ if $!A \ident \lexists[x][!B(x)]$41where $!B$ is $\Delta_0$.42%43A !!{formula} $!A$ is $\Pi_1$ if $!A \ident \lforall[x][!B(x)]$44where $!B$ is $\Delta_0$.45\end{defn}46\begin{lem}48\ollabel{lem:q-proves-clterm-id} Suppose $t$ is a closed term such that49$\Value{t}{N} = n$. Then $\Th{Q} \Proves \eq[t][\num n]$.50\end{lem}51\begin{proof}53We prove this by induction on the complexity of~$t$. For the base case,54$\Value{\Obj 0}{N} = 0$, and $\Th{Q} \Proves \eq[\Obj 0][\num 0]$55since $\num 0 \ident \Obj 0$.56%57For the inductive case, let $t_1$ and $t_2$ be terms such that58$\Value{t_1}{N} = n_1$, $\Value{t_2}{N} = n_2$,59$\Th{Q} \Proves \eq[t_1][\num n_1]$, and60$\Th{Q} \Proves \eq[t_2][\num n_2]$.61Then $\Value{(t_1')}{N} = n_1 + 1$, and we have that $\Th{Q} \Proves63\eq[t_1'][{\num n_1}']$ by the first-order rules for identity applied64to the induction hypothesis and the !!{formula}65$\eq[\num{n_1}'][\num{n_1}']$,66so we have $\Th{Q} \Proves \eq[t_1'][\num{n_1 + 1}]$67by the definition of numerals.68For sums we have70\[71 \Value{(t_1 + t_2)}{N}72 = \Value{t_1}{N} + \Value{t_2}{N}73 = n_1 + n_2.74\]75By the induction hypothesis and the rules for identity,76$\Th{Q} \Proves \eq[t_1 + t_2][\num{n_1} + t_2]$, and then77$\Th{Q} \Proves \eq[t_1 + t_2][\num{n_1} + \num{n_2}]$78by a second application of the rules for identity.79By \olref[inc][req][bre]{lem:q-proves-add},80$\Th{Q} \Proves \eq[\num{n_1} + \num{n_2}][\num{n_1 + n_2}]$,81so $\Th{Q} \Proves \eq[t_1 + t_2][\num{n_1 + n_2}]$.82Similar reasoning also works for~$\times$, using84\olref[inc][req][bre]{lem:q-proves-mult}.85%86Since this exhausts the closed terms of arithmetic, we have that87$\Th{Q} \Proves \eq[t][\num n]$ for all closed terms~$t$ such that88$\Value{t}{N} = n$.89\end{proof}90\begin{prob}92Prove in detail the part of \olref{lem:q-proves-clterm-id}93involving~$\times$.94\end{prob}95\begin{lem}97\ollabel{lem:atomic-completeness}98Suppose $t_1$ and $t_2$ are closed terms. Then99\begin{enumerate}100\item If $\Value{t_1}{N} = \Value{t_2}{N}$,101 then $\Th{Q} \Proves \eq[t_1][t_2]$.102\item If $\Value{t_1}{N} \neq \Value{t_2}{N}$,103 then $\Th{Q} \Proves \eq/[t_1][t_2]$.104\item If $\Value{t_1}{N} < \Value{t_2}{N}$,105 then $\Th{Q} \Proves t_1 < t_2$.106\item If $\Value{t_2}{N} \leq \Value{t_1}{N}$,107 then $\Th{Q} \Proves \lnot(t_1 < t_2)$.108\end{enumerate}109\end{lem}110\begin{proof}112Given terms $t_1$ and $t_2$, we fix $n = \Value{t_1}{N}$ and113$m = \Value{t_2}{N}$.114Suppose $!A \ident t_1 = t_2$. By \olref{lem:q-proves-clterm-id},116$\Th{Q} \Proves \eq[t_1][\num n]$ and $\Th{Q} \Proves \eq[t_2][\num n]$.117If $n = m$, then $\Th{Q} \Proves \eq[\num n][\num m]$ and hence118$\Th{Q} \Proves \eq[t_1][t_2]$ by the transitivity of identity.119If $n \neq m$ then $\Th{Q} \Proves \eq/[\num n][\num m]$,120and by the transitivity of identity again,121$\Th{Q} \Proves \eq/[t_1][t_2]$.122Now let $!A \ident t_1 < t_2$. For both cases, we rely on axiom~$!Q_8$,124which states that $x < y \liff \lexists[z][\eq[z' + x][y]]$125for all $x,y$.126Suppose $\Sat{N}{t_1 < t_2}$. Then there exists some $k \in \Nat$128such that $n + k + 1 = m$. By \olref{lem:q-proves-clterm-id},129$\Th{Q} \Proves \eq[t_1][\num n]$ and $\Th{Q} \Proves \eq[t_2][\num m]$,130and by the first part of this lemma,131$\Th{Q} \Proves \eq[\num n + {\num k}'][\num m]$.132By the transitivity of identity it follows that133$\Th{Q} \Proves \eq[{\num k}' + t_1][t_2]$,134so $\Th{Q} \Proves \lexists[z][\eq[z' + t_1][t_2]]$.135By the right-to-left direction of~$!Q_8$, $\Th{Q} \Proves t_1 < t_2$.136Suppose instead that $\Sat/{N}{t_1 < t_2}$, i.e., $m \leq n$.138%139We work in~$\Th{Q}$ and assume that $t_1 < t_2$. By the left-to-right140direction of~$!Q_8$, there is some~$z$ such that $\eq[z' + t_1][t_2]$.141Since $\Th{Q} \Proves \eq[t_1][\num n]$ and142$\Th{Q} \Proves \eq[t_2][\num m]$, $\eq[z' + \num n][\num m]$.143%144By an external induction on~$m$ using~$!Q_5$,145$\eq[z' + \num{n - m}][\Obj 0]$.146If $m = n$ then $\eq/[z'][\Obj 0]$, giving a contradiction via~$!Q_3$.147If $m < n$ then $\eq[(z' + \num{n - m - 1})'][\Obj 0]$ by~$!Q_5$ again,148giving a contradiction via~$!Q_3$.149So $\Th{Q} \Proves \lnot(t_1 < t_2)$.150\end{proof}151\begin{lem}153\ollabel{lem:bounded-quant-equiv}154Suppose $!A$ is !!a{formula}, $t$ a closed term, and $k=\Value{t}{N}$. Then155\begin{enumerate}156\item $\Th{Q} \Proves \bforall{x<t}{!A(x)}$ iff $\Th{Q} \Proves157 !A(\num 0) \land \dots \land !A(\num{k-1})$.158\item $\Th{Q} \Proves \bexists{x<t}{!A(x)}$ iff $\Th{Q} \Proves159 !A(\num 0) \lor \dots \lor !A(\num{k-1})$.160\end{enumerate}161\end{lem}162\begin{proof}164 We prove the case for the bounded universal quantifier.165 If $\Value{t}{N} = 0$ then the left-hand side of the166 equivalence is provable in~$\Th{Q}$, because there is no167 $x<\num 0$ by \olref[inc][req][min]{lem:less-zero}.168 Similarly, we can take an empty disjunction to be simply169 $\ltrue$, which is also provable in~$\Th{Q}$.170 %171 We therefore suppose that $\Value{t}{N} = k+1$ for some172 natural number~$k$. By \olref{lem:q-proves-clterm-id} we173 can assume that we are working with !!a{formula} of the174 form $\bforall{x<\num{k+1}}{!A(x)}$.175 176 Suppose that $\Th{Q} \Proves \bforall{x<\num{k+1}}{!A(x)}$,177 and let $n \leq k$. Since $\Th{Q} \Proves \num n < \num{k+1}$178 by \olref{lem:atomic-completeness}, it follows by logic that179 $\Th{Q} \Proves !A(\num n)$. Applying this fact $k+1$ times180 for each $n \leq k$, we get that $\Th{Q} \Proves !A(\num 0)181 \land \dots \land !A(\num k)$ as desired.182 183 For the other direction, suppose that $\Th{Q} \Proves184 !A(\num 0) \land \dots \land !A(\num k)$. Working in185 $\Th{Q}$, suppose that $x < \num{k+1}$.186 By \olref[inc][req][min]{lem:less-nsucc} we have that187 $x = \num 0 \lor \dots \lor x = \num k$, so by logic it188 follows that~$!A(x)$, and hence the universal claim189 $\bforall{x<\num{k+1}}{!A(x)}$ follows.190 191 The proof of the equivalence for bounded existentially192 quantified !!{formula}s is similar.193\end{proof}194\begin{prob}196Give a detailed proof of the existential case in197\olref{lem:bounded-quant-equiv}.198\end{prob}199\begin{lem}201\ollabel{lem:delta0-completeness}202If $!A$ is a $\Delta_0$ !!{sentence} which is true in203$\Struct{N}$, then $\Th{Q} \Proves !A$.204\end{lem}205\begin{proof}207We prove this by induction on !!{formula} complexity.208%209The base case is given by \olref{lem:atomic-completeness},210so we move to the induction step. For simplicity we split211the case of negation into subcases depending on the212structure of the !!{formula} to which the negation is213applied.214\begin{enumerate}216\item Suppose $(!A \land !B)$ is true in $\Struct{N}$,217so $!A$ and $!B$ are true in~$\Struct{N}$.218By the induction hypothesis, $\Th{Q} \Proves !A$ and219$\Th{Q} \Proves !B$,220so $\Th{Q} \Proves (!A \land !B)$ by logic.221%222\item Suppose $\lnot (!A \land !B)$ is true in $\Struct{N}$,223so either $\lnot !A$ or $\lnot !B$ is true in $\Struct{N}$.224Without loss of generality, suppose the former. By the225induction hypothesis $\Th{Q} \Proves \lnot !A$, and hence226$\Th{Q} \Proves \lnot (!A \land !B)$ by logic.227%228\item Suppose $(!A \lor !B)$ is true in $\Struct{N}$, so229either $!A$ is true in $\Struct{N}$ or $!B$ is true in230$\Struct{N}$. Without loss of generality, suppose the former231holds. By the induction hypothesis $\Th{Q} \Proves !A$, and232hence $\Th{Q} \Proves (!A \lor !B)$ by logic.233%234\item Suppose $\lnot(!A \lor !B)$ is true in $\Struct{N}$,235so $\lnot !A$ and $\lnot !B$ are true in $\Struct{N}$.236Then $\Th{Q} \Proves \lnot !A$ and $\Th{Q} \Proves \lnot !B$237by the induction hypothesis. Consequently,238$\Th{Q} \Proves \lnot(!A \lor !B)$ by logic.239%240\item Suppose that $\bforall{x<t}{!A(x)}$ is true 241in~$\Struct{N}$, where $t$ is a closed term and $k=\Value{t}{N}$. By the induction242hypothesis and logic, if $!A(\num n)$ is true in~$\Struct{N}$243for all $n < \Value{t}{N}$ then $\Th{Q} \Proves244!A(\num 0) \land \dots \land !A(\num{k-1})$.245By \olref{lem:bounded-quant-equiv} it follows that246$\Th{Q} \Proves \bforall{x<t}{!A(x)}$.247%248\item The case for the bounded existential quantifier, where249we have !!a{sentence} of the form $\bexists{x < t}{!A(x)}$,250is similar to that for the bounded universal quantifier.251%252\item Suppose that $\lnot \bforall{x<t}{!A(x)}$ is true 253in~$\Struct{N}$, where $t$ is a closed term. This !!{sentence}254is equivalent to the !!{sentence} $\bexists{x<t}{\lnot !A(x)}$,255with the equivalence derivable in~$\Th{Q}$, so we may apply256the reasoning for bounded existential quantifiers.257%258\item Similarly, suppose that $\lnot \bexists{x<t}!A(x)$ is259true in $\Struct{N}$, where $t$ is a closed term. This260!!{sentence} is equivalent in $\Th{Q}$ to261$\bforall{x<t}{\lnot!A(x)}$, and so we may apply the reasoning262for bounded universal quantifiers.263%264\item Finally, suppose $\lnot !A$ is true in $\Struct{N}$.265The only cases remaining are when $!A$ is atomic and when266$\lnot !A \ident \lnot\lnot !B$ for some $\Delta_0$267!!{sentence} $!B$. If $!A$ is atomic then by268\olref{lem:atomic-completeness}, $\Th{Q} \Proves \lnot !A$.269If $\lnot !A \ident \lnot\lnot !B$, then by logic it is270provably equivalent in~$\Th{Q}$ to~$!B$, which is true 271in~$\Struct{N}$ since $\lnot !A$ is true in~$\Struct{N}$.272By the induction hypothesis we therefore have that273$\Th{Q} \Proves \lnot !A$.274\end{enumerate}275\end{proof}276\begin{prob}278Give a detailed proof of the existential case in279\olref{lem:delta0-completeness}.280\end{prob}281\begin{thm}283\ollabel{thm:sigma1-completeness}284If $!A$ is a $\Sigma_1$ !!{sentence} which is true285in~$\Struct{N}$, then $\Th{Q} \Proves !A$.286\end{thm}287\begin{proof}289If $\lexists{x}!A(x)$ is a $\Sigma_1$ !!{sentence} which290is true in~$\Struct{N}$, then there exists a natural291number~$n$ and a variable assignment~$s$ such that $s(x) = n$ and292$\Sat{N}{!A(x)}[s]$. By standard facts about293the satisfaction relation it follows that294$\Sat{N}{!A(\num n)}$. But $!A(\num n)$ is a295$\Delta_0$ !!{formula}, so by \olref{lem:delta0-completeness}296we have that $\Th{Q} \Proves !A(\num n)$, and hence by297logic we also have that $\Th{Q} \Proves \lexists[x][!A(x)]$.298\end{proof}299\end{document}