add section incompleteness/representability-in-q/undecidability

Author: rzach

computability/recursive-functions/halting-problem.tex

@@ -18,8 +18,8 @@
 \[
 h(e, n) = 
 \begin{cases}
-1 & \text{if computation $e$ halts on input $n$}
-0 & otherwise
+1 & \text{if computation $e$ halts on input $n$}\\
+0 & \text{otherwise,}
 \end{cases}
 \]
 is not computable.
@@ -40,8 +40,8 @@
 \[
 h(e, x) = 
 \begin{cases}
-1 & \text{if $\cfind{e}(x) \defined$}
-0 & otherwise.
+1 & \text{if $\cfind{e}(x) \defined$}\\
+0 & \text{otherwise.}
 \end{cases}
 \]
 Note that $h(e, x) = 0$ if $\cfind{e}(x) \undefined$, but also
@@ -58,7 +58,7 @@
 \[
 d(y) = 
 \begin{cases}
-1 & \text{if $h(y, y) = 0$}
+1 & \text{if $h(y, y) = 0$}\\
 \umin{x}{x \neq x} & \text{otherwise.}
 \end{cases}
 \]

computability/recursive-functions/normal-form.tex

@@ -10,29 +10,35 @@
 \olsection{The Normal Form Theorem}
 
 \begin{thm}[Kleene's Normal Form Theorem]
+\ollabel{thm:kleene-nf}
 There are a primitive recursive relation $T(e, x, s)$ and a primitive
 recursive function $U(s)$, with the following property: if $f$ is any
 partial recursive function, then for some~$e$,
 \[
-f(x) \simeq U(\mu s \; T(e, x, s))
+f(x) \simeq U(\umin{s}{T(e, x, s)})
 \]
-for every $x$.
+for every $x$. 
 \end{thm}
 
 \begin{explain}
-The proof of the norm is involved, but the basic idea is simple.
-Every partial recursive function has an \emph{index}~$e$, intuitively,
-a number coding its program or definition.  If $f(x) \defined$, the
-computation can be recorded systematically and coded by some
-number~$s$, and that $s$ codes the computation of $f$ on input $x$ can
-be checked primitive recursively using only $x$ and the
+The proof of the normal form theorem is involved, but the basic idea
+is simple.  Every partial recursive function has an \emph{index}~$e$,
+intuitively, a number coding its program or definition.  If $f(x)
+\defined$, the computation can be recorded systematically and coded by
+some number~$s$, and that $s$ codes the computation of $f$ on input
+$x$ can be checked primitive recursively using only $x$ and the
 definition~$e$.  This means that $T$ is primitive recursive.  Given
 the full record of the computation~$s$, the ``upshot'' of~$s$ is the
 value of~$f(x)$, and it can be obtained from~$s$ primitive recursively
-as well.  The normal form theorem shows that only a single unbounded
-search is required for the definition of any partial recursive
-function.
-\end{explain}
+as well.
 
+The normal form theorem shows that only a single unbounded search is
+required for the definition of any partial recursive function.  We can
+use the numbers $e$ as ``names'' of partial recursive functions, and
+write $\cfind{e}$ for the function $f$ defined by the equation in the
+theorem.  Note that any partial recursive function can have more than
+one index---in fact, every partial recursive function has infinitely
+many indices.  
+\end{explain}
 \end{document}
 

computability/recursive-functions/recursive-functions.tex

@@ -29,6 +29,8 @@ \chapter{Recursive Functions}
 
 \olimport{normal-form}
 
+\olimport{halting-problem}
+
 \olimport{general-recursive-functions}
 
 \OLEndChapterHook

incompleteness/arithmetization-syntax/proofs-in-lk.tex

@@ -154,7 +154,7 @@
 to express that every sentence in it is in~$\Gamma$.  Thus we can
 define $\fn{Pr}_\Gamma(x, y)$ by
 \begin{align*}
-\Prov_\Gamma(x, y) \defiff {}&
+\fn{Pr}_\Gamma(x, y) \defiff {}&
 \fn{Sent}(x) \land \fn{Deriv}(y) \land {} \\
 & \lforall[i <
   \len{((y)_1)_0}][(((y)_1)_0)_i \in \Gamma] \land {}\\

incompleteness/representability-in-q/representability-in-q.tex

@@ -23,6 +23,8 @@ \chapter{Representability in $\Th{Q}$}
 
 \olimport{representing-relations}
 
+\olimport{undecidability}
+
 \OLEndChapterHook
 
 \end{document}

incompleteness/representability-in-q/undecidability.tex

@@ -0,0 +1,72 @@
+% Part: incompleteness
+% Chapter: representability-in-q
+% Section: undecidability
+
+\documentclass[../../include/open-logic-section]{subfiles}
+
+\begin{document}
+
+\olfileid{inc}{req}{und}
+\olsection{Undecidability}
+
+We call a theory $\Th{T}$ \emph{undecidable} if there is no
+computational procedure which, after finitely many steps and
+unfailingly, provides a correct answer to the question ``does $\Th{T}$
+prove~$!A$'' for any sentence~$!A$ in the language of~$\Th{T}$.  So
+$\Th{Q}$ would be decidable iff there were a computational procedure
+which decides, given a sentence~$A$ in the language of arithmetic,
+whether $\Th{Q} \Proves !A$ or not.  We can make this more precise by
+asking: Is the relation~$\fn{Prov}_{\Th{Q}}(x)$, which holds of~$x$
+iff $x$ is the G\"odel number of a sentence provable in~$\Th{Q}$,
+recursive?  The answer is: no. 
+
+\begin{thm}
+$\Th{Q}$ is undecidable, i.e., the relation 
+\[
+\fn{Prov}_{\Th{Q}}(x) \defiff \fn{Sent}(x) \land
+\lexists[y][\fn{Pr}_{\Th{Q}}(x, y)]
+\]
+is not recursive.
+\end{thm}
+
+\begin{proof}
+Suppose it were.  Then we could solve the halting problem as follows:
+Given $e$ and $n$, we know that $\cfind{e}(n) \defined$ iff there is
+an~$s$ such that $T(e, x, s)$, where $T$ is Kleene's predicate from
+\olref[cmp][rec][nft]{thm:kleene-nf}. Since $\Char{T}$ is primitive
+recursive it is representable in~$\Th{Q}$ by a formula
+$!B_T(e,x,s,y)$, that is, $\Th{Q} \Proves !B_T(\num{e}, \num{x},
+\num{s}, \num{1})$ iff $T(e, x, s)$.  If $\Th{Q} \Proves !B_T(\num{e},
+\num{x}, \num{s}, \num{1})$ then also $\Th{Q} \Proves \Th{Q} \Proves
+\lexists[y][!B_T(\num{e}, \num{x}, y, \num{1})]$. If no such $s$
+exists, then $\Th{Q} \Proves \lnot !B_T(\num{e}, \num{x}, \num{s},
+\num{1})$ for every~$s$. Since $\Th{Q}$ is $\omega$-consistent,
+$\Th{Q} \Proves/ \lexists[y][!B_T(\num{e}, \num{x}, y, \num{1})]$.  In
+other words, $\Th{Q} \Proves \lexists[y][!B_T(\num{e}, \num{x}, y,
+  \num{1})]$ iff there is an $s$ such that $T(e, n, s)$, i.e., iff
+$\cfind{e}(n) \defined$.  From $e$ and~$n$ we can compute
+$\Gn{\lexists[y][!B_T(\num{e}, \num{n}, y, \num{1})]}$, let $g(e, n)$
+  be the primitive recursive function which does that. So
+\[
+h(e, n) = 
+\begin{cases}
+1 & \text{if $\fn{Pr}_{\Th{Q}}(g(e, n))$}\\
+0 & \text{otherwise}.
+\end{cases}
+\]
+This would show that $h$ is recursive if $\fn{Pr}_{\Th{Q}}$ is. But $h$ is not
+recursive, by \olref[cmp][rec][hlt]{thm:halting-problem}, so $\fn{Pr}_{\Th{Q}}$
+cannot be either.
+\end{proof}
+
+\begin{cor}
+First-order logic is undecidable.
+\end{cor}
+
+\begin{proof}
+If first-order logic were decidable, provability in~$\Th{Q}$ would be
+as well, since $\Th{Q} \Proves !A$ iff $\Proves !O \lif !A$, where
+$!O$ is the conjunction of the axioms of~$\Th{Q}$.
+\end{proof}
+
+\end{document}

sty/open-logic-formulas.sty

@@ -28,10 +28,10 @@
 % Provides !A, !B etc in math mode to produce \phi, \psi etc.
 
 \def\olgreekformulas
-{\gdef\formula{\lookup{A/\varphi,B/\psi,C/\chi,D/\theta,E/\alpha,F/\beta,G/\gamma,H/\delta,K/\xi,L/\zeta,R/\rho,T/\tau}}}
+{\gdef\formula{\lookup{A/\varphi,B/\psi,C/\chi,D/\theta,E/\alpha,F/\beta,G/\gamma,H/\delta,K/\xi,L/\zeta,O/\omega,R/\rho,T/\tau}}}
 
 \def\olalphagreekformulas
-{\gdef\formula{\lookup{A/\alpha,B/\beta,C/\gamma,D/\delta,E/\phi,F/\psi,G/\chi,H/\sigma,K/\xi,L/\zeta,R/\rho,T/\tau}}}
+{\gdef\formula{\lookup{A/\alpha,B/\beta,C/\gamma,D/\delta,E/\phi,F/\psi,G/\chi,H/\sigma,K/\xi,L/\zeta,O/\omega,R/\rho,T/\tau}}}
 
 % args -- format a list of arguments separated by commas without commas