Incompleteness

Theories and Computability

content/incompleteness/theories-computability/theories-computability.tex

% Part: incompleteness% Chapter: theories-computability\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\begin{editorial}  This chapter depends on material in the chapter on computability  theory, but can be left out if that hasn't been covered.  It's  currently a basic conversion of Jeremy Avigad's notes, has not been  revised, and is missing exercises.\end{editorial}\olchapter{inc}{tcp}{Theories and Computability}\olimport{introduction}\olimport{q-is-ce}\olimport{oconsis-ext-of-q-undec}\olimport{extensions-of-q-not-decidable}\olimport{computably-axiomatizable}\olimport{complete-decidable}\olimport{first-incompleteness}\olimport{inseparability}\olimport{consis-with-q}\olimport{interpretability}\OLEndChapterHook\end{document}

content/incompleteness/theories-computability/introduction.tex

% Part: incompleteness% Chapter: theories-computability% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{tcp}{int}\olsection{Introduction}\begin{editorial}This section should be rewritten.  \end{editorial}We have the following:\begin{enumerate}\item A definition of what it means for a function to be representable  in $\Th{Q}$ (\olref[req][int]{defn:representable-fn})\item a definition of what it means for a relation to be representable  in $\Th{Q}$ (\olref[req][rel]{defn:representing-relations})\item a theorem asserting that the representable functions of $\Th{Q}$  are exactly the computable ones  (\olref[req][int]{thm:representable-iff-comp})\item a theorem asserting that the representable relations of $\Th{Q}$  are exactly the computable ones  \olref[req][rel]{thm:representing-rels})\end{enumerate}A {\em theory} is a set of sentences that is deductively closed, thatis, with the property that whenever $T$ proves $!A$ then $!A$ is in$T$. It is probably best to think of a theory as being a collection ofsentences, together with all the things that these sentences imply.From now on, we will use $\Th{Q}$ to refer to the {\em theory}consisting of the set of sentences derivable from the eight axioms in\olref[req][int]{sec}.  Remember that we can code formula of $\Th{Q}$as numbers; if $!A$ is such a formula, let $\Gn{!A}$ denote the numbercoding $!A$. Modulo this coding, we can now ask whether various setsof formulas are computable or not.\end{document}

content/incompleteness/theories-computability/q-is-ce.tex

% Part: incompleteness% Chapter: theories-computability% Section: q-is-ce\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{tcp}{qce}\olsection{$\Th{Q}$ is \printtoken{S}{c.e.}-Complete}\begin{thm}$\Th{Q}$ is !!{c.e.} but not decidable. In fact, it is a complete  !!{c.e.} set.\end{thm}\begin{proof}It is not hard to see that $\Th{Q}$ is !!{c.e.}, since it is the set of(codes for) sentences $y$ such that there is a proof $x$ of $y$ in$\Th{Q}$:\[Q = \Setabs{y}{\lexists[x][\Prf[\Th{Q}](x,y)]}.\]But we know that $\Prf[\Th{Q}](x,y)$ is computable (in fact, primitiverecursive), and any set that can be written in the above form is c.e.Saying that it is a complete c.e.\ set is equivalent to saying that $K\leq_m Q$, where $K = \Setabs{x}{!A_x(x) \downarrow}$. So let us showthat $K$ is reducible to $\Th{Q}$. Since Kleene's predicate $T(e,x,s)$ isprimitive recursive, it is representable in $\Th{Q}$, say, by $!A_T$. Thenfor every $x$, we have\begin{align*}x \in K & \lif \lexists[s][T(x,x,s)] \\& \lif \lexists[s][(\Th{Q} \Proves !A_T(\num x,\num x, \num s))]  \\& \lif \Th{Q} \Proves \lexists[s][!A_T(\num x, \num x, s)].\end{align*}Conversely, if $\Th{Q} \Proves \lexists[s][!A_T(\num x, \num x, s)]$,then, in fact, for some natural number $n$ the formula $!A_T(\num x,\num x, \num n)$ must be true.  Now, if $T(x,x,n)$ were false,$\Th{Q}$ would prove $\lnot !A_T(\num x, \num x, \num n)$, since$!A_T$ represents $T$.  But then $\Th{Q}$ proves a false formula,which is a contradiction. So $T(x,x,n)$ must be true, which implies$!A_x(x) \downarrow$.In short, we have that for every $x$, $x$ is in $K$ if and only if$\Th{Q}$ proves $\lexists[s][T(\num x,\num x,s)]$. So the function $f$which takes $x$ to (a code for) the sentence $\lexists[s][T(\num x,  \num x, s)]$ is a reduction of $K$ to $\Th{Q}$.\end{proof}\end{document}

content/incompleteness/theories-computability/oconsis-ext-of-q-undec.tex

% Part: incompleteness% Chapter: theories-computability% Section: oconsis-ext-of-q-undec\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{tcp}{oqn}\olsection{$\omega$-Consistent Extensions of $\Th{Q}$ are Undecidable}\begin{explain}The proof that $\Th{Q}$ is c.e.-complete relied on the fact that anysentence provable in $\Th{Q}$ is ``true'' of the natural numbers. Thenext definition and theorem strengthen this theorem, by pinpointingjust those aspects of ``truth'' that were needed in the proofabove. Don't dwell on this theorem too long, though, because we willsoon strengthen it even further. We include it mainly forhistorical purposes: G\"odel's original paper used the notion of$\omega$-consistency, but his result was strengthened by replacing$\omega$-consistency with ordinary consistency soon after.\end{explain}\begin{defn}\ollabel{thm:oconsis-q}A theory $\Th{T}$ is $\omega$-consistent if the following holds: if$\lexists[x][!A(x)]$ is any sentence and $\Th{T}$ proves $\lnot!A(\num 0)$, $\lnot !A(\num 1)$, $\lnot !A(\num 2)$, \dots then $\Th{T}$does not prove $\lexists[x][!A(x)]$.\end{defn}\begin{thm}  Let $\Th{T}$ be any $\omega$-consistent theory that includes $\Th{Q}$. Then  $\Th{T}$ is not decidable.\end{thm}\begin{proof}If $\Th{T}$ includes $\Th{Q}$, then $\Th{T}$ represents the computablefunctions and relations. We need only modify the previous proof. Asabove, if $x \in K$, then $\Th{T}$ proves $\lexists[s][!A_T(\num  x,\num x, s)]$. Conversely, suppose $\Th{T}$ proves$\lexists[s][!A_T(\num x, \num x, s)]$. Then $x$ must be in $K$:otherwise, there is no halting computation of machine $x$ on input$x$; since $!A_T$ represents Kleene's $T$ relation, $\Th{T}$proves $\lnot !A_T(\num x, \num x, \num 0)$, $\lnot !A_T(\num x, \numx, \num 1)$, \dots, making $\Th{T}$ $\omega$-inconsistent. \end{proof}\end{document}

content/incompleteness/theories-computability/extensions-of-q-not-decidable.tex

% Part: incompleteness% Chapter: theories-computability% Section: extensions-of-q-not-decidable\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{tcp}{cqn}\olsection{Consistent Extensions of $\Th{Q}$ are Undecidable}\begin{explain}Remember that a theory is \emph{consistent} if it does not prove both$!A$ and $\lnot !A$ for any formula~$!A$. Since anything follows froma contradiction, an inconsistent theory is trivial: every sentence isprovable. Clearly, if a theory if $\omega$-consistent, then it isconsistent. But being consistent is a weaker requirement (i.e., thereare theories that are consistent but not $\omega$-consistent.). We canweaken the assumption in \olref[oqn]{thm:oconsis-q} to simpleconsistency to obtain a stronger theorem.\end{explain}\begin{lem}There is no ``universal computable relation.'' That is, there is nobinary computable relation $R(x,y)$, with the following property:whenever $S(y)$ is a unary computable relation, there is some $k$ suchthat for every $y$, $S(y)$ is true if and only if $R(k,y)$ is true.\end{lem}\begin{proof}Suppose $R(x,y)$ is a universal computable relation. Let $S(y)$be the relation $\lnot R(y,y)$. Since $S(y)$ is computable, for some$k$, $S(y)$ is equivalent to $R(k,y)$. But then we have that $S(k)$ isequivalent to both $R(k,k)$ and $\lnot R(k,k)$, which is acontradiction.\end{proof}\begin{thm}Let $\Th{T}$ be any consistent theory that includes $\Th{Q}$. Then$\Th{T}$ is not decidable.\end{thm}\begin{proof}Suppose $\Th{T}$ is a consistent, decidableextension of $\Th{Q}$. We will obtain a contradiction by using $\Th{T}$ todefine a universal computable relation.Let $R(x,y)$ hold if and only if\begin{quote}$x$ codes a formula $!D(u)$, and $\Th{T}$ proves $!D(\num y)$.\end{quote}Since we are assuming that $\Th{T}$ is decidable, $R$ is computable. Let usshow that $R$ is universal. If $S(y)$ is any computable relation, thenit is representable in $\Th{Q}$ (and hence $\Th{T}$) by a formula$!D_S(u)$. Then for every $n$, we have\begin{eqnarray*}S(\num n) & \lif & T \vdash !D_S(\num n) \\& \lif & R(\Gn{!D_S(u)}, n)\end{eqnarray*}and\begin{eqnarray*}\lnot S(\num n) & \lif & T \vdash \lnot !D_S(\num n) \\& \lif & T \not\vdash !D_S(\num n) \quad \text{(since $\Th{T}$ is  consistent)} \\& \lif & \lnot R(\Gn{!D_S(u)}, n).\end{eqnarray*}That is, for every $y$, $S(y)$ is true if and only if$R(\Gn{!D_S(u)}, y)$ is. So $R$ is universal, and we have thecontradiction we were looking for.\end{proof}Let ``true arithmetic'' be the theory $\Setabs{!A}{ \Sat{\Nat}{!A}}$,that is, the set of sentences in the language of arithmetic that aretrue in the standard interpretation.\begin{cor}True arithmetic is not decidable.\end{cor}%In Section~\olref{undefinability:truth:section} we will state a stronger%result, due to Tarski.\end{document}

content/incompleteness/theories-computability/computably-axiomatizable.tex

% Part: incompleteness% Chapter: theories-computability% Section: computably-axiomatizable\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{tcp}{cax}\olsection{\printtoken{S}{axiomatizable} Theories}A theory $\Th{T}$ is said to be \emph{!!{axiomatizable}} if it has acomputable set of axioms~$A$. (Saying that $A$ is a set of axioms for$\Th{T}$ means $T = \Setabs{!A}{A \Proves !A}$.) Any ``reasonable''axiomatization of the natural numbers will have this property. Inparticular, any theory with a finite set of axioms is!!{axiomatizable}.\begin{lem}Suppose $\Th{T}$ is !!{axiomatizable}. Then $\Th{T}$ is !!{computablyenumerable}.\end{lem}\begin{proof}Suppose $A$ is a computable set of axioms for $\Th{T}$. To determineif $!A \in T$, just search for !!a{derivation} of $!A$ from the axioms.Put slightly differently, $!A$ is in $\Th{T}$ if and only if there isa finite list of axioms $!B_1$, \dots, $!B_k$ in $A$ and !!a{derivation} of$(!B_1 \land \dots \land !B_k) \lif !A$ in first-order logic.  Butwe already know that any set with a definition of the form ``thereexists \dots such that \dots'' is !!{c.e.}, provided the second ``\dots''is computable.\end{proof}\end{document}

content/incompleteness/theories-computability/complete-decidable.tex

% Part: incompleteness% Chapter: theories-computability% Section: complete-decidable\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{tcp}{cdc}\olsection{\printtoken{S}{axiomatizable} Complete Theories are Decidable}A theory is said to be {\em complete} if for every sentence $!A$,either $!A$ or $\lnot !A$ is provable.\begin{lem}Suppose a theory $\Th{T}$ is complete and !!{axiomatizable}. Then$\Th{T}$ is decidable.\end{lem}\begin{proof}Suppose $\Th{T}$ is complete and $A$ is a computable set of axioms.If $\Th{T}$ is inconsistent, it is clearly computable. (Algorithm: ``justsay yes.'') So we can assume that $\Th{T}$ is also consistent.To decide whether or not a sentence $!A$ is in~$\Th{T}$,simultaneously search for !!a{derivation} of~$!A$ from~$\Th{T}$ and!!a{derivation} of~$\lnot !A$. Since $\Th{T}$ is complete, you arebound to find one or the other; and since $\Th{T}$ is consistent, if youfind !!a{derivation} of~$\lnot !A$, there is no !!{derivation} of~$!A$.Put in different terms, we already know that $\Th{T}$ is !!{c.e.}; soby a theorem we proved before, it suffices to show that the complementof~$\Th{T}$ is !!{c.e.} also. But !!a{formula}~$!A$ is in~$\Th{\barT}$ if and only if $\lnot !A$ is in~$\Th{T}$; so $\Th{\bar T} \leq_m\Th{T}$.\end{proof}\end{document}

content/incompleteness/theories-computability/first-incompleteness.tex

% Part: incompleteness% Chapter: theories-computability% Section: first-incompleteness\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{tcp}{inc}\olsection{$\Th{Q}$ has no Complete, Consistent, !!^{axiomatizable}  Extensions}\begin{thm}\ollabel{thm:first-incompleteness}There is no complete, consistent, !!{axiomatizable} extension of$\Th{Q}$.\end{thm}\begin{proof}We already know that there is no consistent, decidable extension of$\Th{Q}$. But if $\Th{T}$ is complete and !!{axiomatized}, thenit is decidable. \end{proof}\begin{explain}This theorems is not that far from G\"odel's original 1931 formulationof the First Incompleteness Theorem. Aside from the more modernterminology, the key differences are this: G\"odel has``$\omega$-consistent'' instead of ``consistent''; and he could notsay ``!!{axiomatizable}'' in full generality, since the formalnotion of computability was not in place yet. (The formal models ofcomputability were developed over the following decade, including byG\"odel, and in large part to be able to characterize the kinds oftheories that are susceptible to the G\"odel phenomenon.)The theorem says you can't have it all, namely, completeness,consistency, and !!{axiomatizability}. If you give up any one ofthese, though, you can have the other two: $\Th{Q}$ is consistent andcomputably axiomatized, but not complete; the inconsistent theory iscomplete, and computably axiomatized (say, by $\{ \eq/[0][0] \}$), butnot consistent; and the set of true sentence of arithmetic is completeand consistent, but it is not computably axiomatized.\end{explain}\end{document}

content/incompleteness/theories-computability/inseparability.tex

% Part: incompleteness% Chapter: theories-computability% Section: inseparability\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{tcp}{ins}\olsection{Sentences Provable and Refutable in $\Th{Q}$ are Computably  Inseparable}Let $\Th{\bar Q}$ be the set of sentences whose {\em negations} areprovable in $\Th{Q}$, i.e., $\Th{\bar Q} = \Setabs{!A}{\Th{Q} \Proves  \lnot !A}$. Remember that disjoint sets $A$ and $B$ are said to becomputably inseparable if there is no computable set $C$ such that $A\subseteq C$ and $B \subseteq \Complement{C}$.\begin{lem}$\Th{Q}$ and $\Th{\bar Q}$ are computably inseparable. \end{lem}\begin{proof}Suppose $C$ is a computable set such that $\Th{Q} \subseteq C$ and$\Th{\bar Q} \subseteq \Complement{C}$. Let $R(x,y)$ be the relation\begin{quote}$x$ codes a formula $!D(u)$ and $!D(\num y)$ is in $C$.\end{quote}We will show that $R(x,y)$ is a universal computable relation, yieldinga contradiction.Suppose $S(y)$ is computable, represented by $!D_S(u)$ in $\Th{Q}$. Then\begin{eqnarray*}S(\num n) & \lif & \Th{Q} \Proves !D_S(\num n) \\& \lif & !D_S(\num n) \in C\end{eqnarray*}and \begin{eqnarray*}\lnot S(\num n) & \lif & \Th{Q} \Proves \lnot !D_S(\num n) \\& \lif & !D_S(\num n) \in \Th{\bar Q} \\& \lif & !D_S(\num n) \not\in C\end{eqnarray*}So $S(y)$ is equivalent to $R(\#(!D_S(\num u)),y)$. \end{proof}\end{document}

content/incompleteness/theories-computability/consis-with-q.tex

% Part: incompleteness% Chapter: theories-computability% Section: consis-with-q\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{tcp}{con}\olsection{Theories Consistent with $\Th{Q}$ are Undecidable}The following theorem says that not only is $\Th{Q}$ undecidable, but, infact, any theory that does not disagree with $\Th{Q}$ is undecidable.\begin{thm}Let $\Th{T}$ be any theory in the language of arithmetic that isconsistent with $\Th{Q}$ (i.e., $\Th{T} \cup \Th{Q}$ isconsistent). Then $\Th{T}$ is undecidable.\end{thm}\begin{proof}Remember that $\Th{Q}$ has a finite set of axioms, $!Q_1$, \dots,$!Q_8$. We can even replace these by a single axiom, $!E = !Q_1 \land\dots \land !Q_8$.Suppose $\Th{T}$ is a decidable theory consistent with~$\Th{Q}$. Let\[C = \Setabs{!A}{\Th{T} \Proves !E \lif !A}.\]We show that $C$ would be a computable separation of $\Th{Q}$ and$\Th{\bar Q}$, a contradiction. First, if $!A$ is in $\Th{Q}$, then$!A$ is provable from the axioms of $\Th{Q}$; by the deductiontheorem, there is !!a{derivation} of $!E \lif !A$ in first-order logic. So$!A$ is in~$C$.On the other hand, if $!A$ is in $\Th{\bar Q}$, then there is a proofof $!E \lif \lnot !A$ in first-order logic. If $\Th{T}$ also proves$!E \lif !A$, then $\Th{T}$ proves $\lnot !E$, in which case $\Th{T}\cup \Th{Q}$ is inconsistent. But we are assuming $\Th{T} \cup \Th{Q}$is consistent, so $\Th{T}$ does not prove $!E \lif !A$, and so $!A$is not in~$C$.We've shown that if $!A$ is in $\Th{Q}$, then it is in $C$, and if$!A$ is in $\Th{\bar Q}$, then it is in $\Complement{C}$. So $C$ is acomputable separation, which is the contradiction we were looking for.\end{proof}This theorem is very powerful. For example, it implies:\begin{cor}  First-order logic for the language of arithmetic (that is, the set  $\Setabs{!A}{\text{$!A$ is provable in first-order logic}}$) is  undecidable.\end{cor}\begin{proof}First-order logic is the set of consequences of $\emptyset$,which is consistent with~$\Th{Q}$.\end{proof}\end{document}

content/incompleteness/theories-computability/interpretability.tex

% Part: incompleteness% Chapter: theories-computability% Section: intepretability\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{tcp}{itp}\olsection{Theories in which $\Th{Q}$ is Interpretable are Undecidable}We can strengthen these results even more. Informally, aninterpretation of a language $\Lang{L_1}$ in another language$\Lang{L_2}$ involves defining the universe, relation symbols, andfunction symbols of $\Lang{L_1}$ with !!{formula}s in$\Lang{L_2}$. Though we won't take the time to do this, one can makethis definition precise.\begin{thm}  Suppose $\Th{T}$ is a theory in a language in which one can  interpret the language of arithmetic, in such a way that $\Th{T}$ is  consistent with the interpretation of $\Th{Q}$. Then $\Th{T}$ is  undecidable. If $\Th{T}$ proves the interpretation of the axioms of  $\Th{Q}$, then no consistent extension of $\Th{T}$ is decidable.\end{thm}The proof is just a small modification of the proof of the lasttheorem; one could use a counterexample to get a separation of $\Th{Q}$ and$\Th{\bar Q}$. One can take $\Th{ZFC}$, Zermelo--Fraenkel set theory with theaxiom of choice, to be an axiomatic foundation that is powerful enoughto carry out a good deal of ordinary mathematics. In $\Th{ZFC}$ onecan define the natural numbers, and via this interpretation, theaxioms of $\Th{Q}$ are true. So we have\begin{cor}There is no decidable extension of $\Th{ZFC}$.\end{cor}\begin{cor}There is no complete, consistent, computably !!{axiomatizable} extension of$\Th{ZFC}$. \end{cor}The language of $\Th{ZFC}$ has only a single binary relation,$\in$. (In fact, you don't even need equality.) So we have\begin{cor}First-order logic for any language with a binary relation symbol isundecidable.\end{cor}This result extends to any language with two unary function symbols,since one can use these to simulate a binary relation symbol. Theresults just cited are tight: it turns out that first-order logic fora language with only \emph{unary} relation symbols and at most one\emph{unary} function symbol is decidable.One more bit of trivia. We know that the set of sentences in thelanguage $\Obj 0$, $'$, $+$, $\times$, $<$ true in the standard modelis undecidable. In fact, one can define $<$ in terms of the othersymbols, and then one can define $+$ in terms of $\times$ and $'$. Sothe set of true sentences in the language $\Obj 0$, $'$, $\times$ isundecidable. On the other hand, Presburger has shown that the set ofsentences in the language $\Obj 0$, $'$, $+$ true in the language ofarithmetic is decidable. The procedure is computationally infeasible,however.\end{document}

Source-census fragment evidence

The complete original formula is shown in Read and Explore. These immutable census fragments are retained for traceability.

Census fragment projected-formula-0020053 — source evidence only
<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" data-expression-id="expr-ad21ff31eb419ada" data-source-fragment="incomplete_source_fragment" data-fragment-kind="nested_inline_math_census_prefix"><semantics><mrow><merror><mtext>Source fragment ends inside the set condition text.</mtext></merror><mrow><mo>{</mo><mi>A</mi><mo>:</mo></mrow></mrow><annotation encoding="application/x-tex">\Setabs{!A}{\text{</annotation></semantics></math>
Census fragment projected-formula-0020054 — source evidence only
<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" data-expression-id="expr-342e35c540e50532" data-source-fragment="incomplete_source_fragment" data-fragment-kind="nested_inline_math_census_suffix"><semantics><mrow><merror><mtext>Source fragment continues the preceding set condition text.</mtext></merror><mrow><mtext>is provable in first-order logic</mtext><mo>}</mo></mrow></mrow><annotation encoding="application/x-tex">is provable in first-order logic}}</annotation></semantics></math>