Incompleteness

Introduction to Incompleteness

content/incompleteness/introduction/introduction.tex

% Part: incompleteness% Chapter: first-incompleteness\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{inc}{int}{Introduction to Incompleteness}\olimport{historical-background}\olimport{definitions}\olimport{overview}\olimport{undecidability}\OLEndChapterHook\end{document}

content/incompleteness/introduction/historical-background.tex

% Part: incompleteness% Chapter: introduction% Section: historical-background\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{int}{bgr}\olsection{Historical Background}In this section, we will briefly discuss historical developments thatwill help put the incompleteness theorems in context. In particular,we will give a very sketchy overview of the history of mathematicallogic; and then say a few words about the history of the foundationsof mathematics.\begin{digress}  The phrase ``mathematical logic'' is ambiguous. One can interpret theword ``mathematical'' as describing the subject matter, as in, ``thelogic of mathematics,'' denoting the principles of mathematicalreasoning; or as describing the methods, as in ``the mathematics oflogic,'' denoting a mathematical study of the principles of reasoning.The account that follows involves mathematical logic in both senses,often at the same time.\end{digress}The study of logic began, essentially, with Aristotle, who livedapproximately 384--322 \textsc{bce}. His \emph{Categories}, \emph{Prior  analytics}, and \emph{Posterior analytics} include systematicstudies of the principles of scientific reasoning, including athorough and systematic study of the syllogism.Aristotle's logic dominated scholastic philosophy through the middleages; indeed, as late as the eighteenth century, Kant maintained thatAristotle's logic was perfect and in no need of revision. But thetheory of the syllogism is far too limited to model anything butthe most superficial aspects of mathematical reasoning. A centuryearlier, Leibniz, a contemporary of Newton's, imagined a complete``calculus'' for logical reasoning, and made some rudimentary stepstowards designing such a calculus, essentially describing a version ofpropositional logic.The nineteenth century was a watershed for logic. In 1854 George Boolewrote \emph{The Laws of Thought}, with a thorough algebraic study ofpropositional logic that is not far from modern presentations. In 1879Gottlob Frege published his \emph{Begriffsschrift} (Concept writing)which extends propositional logic with quantifiers and relations, andthus includes first-order logic. In fact, Frege's logical systemsincluded higher-order logic as well, and more. In his \emph{Basic Laws  of Arithmetic}, Frege set out to show that all of arithmetic couldbe derived in his Begriffsschrift from purely logicalassumption. Unfortunately, these assumptions turned out to beinconsistent, as Russell showed in 1902. But setting aside theinconsistent axiom, Frege more or less invented modern logicsinglehandedly, a startling achievement. Quantificational logic wasalso developed independently by algebraically-minded thinkers afterBoole, including Peirce and Schr\"oder.Let us now turn to developments in the foundations of mathematics. Ofcourse, since logic plays an important role in mathematics, there is agood deal of interaction with the developments just described. Forexample, Frege developed his logic with the explicit purpose ofshowing that all of mathematics could be based solely on his logicalframework; in particular, he wished to show that mathematics consistsof a priori \emph{analytic} truths instead of, as Kant had maintained,a priori \emph{synthetic} ones.Many take the birth of mathematics proper to have occurred with theGreeks. Euclid's \emph{Elements}, written around 300 B.C., is alreadya mature representative of Greek mathematics, with its emphasis onrigor and precision. The definitions and proofs in Euclid's\emph{Elements} survive more or less intact in high school geometrytextbooks today (to the extent that geometry is still taught in highschools). This model of mathematical reasoning has been held to be aparadigm for rigorous argumentation not only in mathematics but inbranches of philosophy as well. (Spinoza even presented moral andreligious arguments in the Euclidean style, which is strange to see!)Calculus was invented by Newton and Leibniz in the seventeenthcentury. (A fierce priority dispute raged for centuries, but mostscholars today hold that the two developments were for the most partindependent.)  Calculus involves reasoning about, for example,infinite sums of infinitely small quantities; these features fueledcriticism by Bishop Berkeley, who argued that belief in God was noless rational than the mathematics of his time. The methods ofcalculus were widely used in the eighteenth century, for example byLeonhard Euler, who used calculations involving infinite sums withdramatic results.In the nineteenth century, mathematicians tried to address Berkeley'scriticisms by putting calculus on a firmer foundation. Efforts byCauchy, Weierstrass, Bolzano, and others led to our contemporarydefinitions of limits, continuity, differentiation, and integration interms of ``epsilons and deltas,'' in other words, devoid of anyreference to infinitesimals. Later in the century, mathematicianstried to push further, and explain all aspects of calculus, includingthe real numbers themselves, in terms of the natural numbers.(Kronecker: ``God created the whole numbers, all else is the work ofman.'') In 1872, Dedekind wrote ``Continuity and the irrationalnumbers,'' where he showed how to ``construct'' the real numbers assets of rational numbers (which, as you know, can be viewed as pairsof natural numbers); in 1888 he wrote ``Was sind und was sollen dieZahlen'' (roughly, ``What are the natural numbers, and what shouldthey be?'') which aimed to explain the natural numbers in purely``logical'' terms. In 1887 Kronecker wrote ``\"Uber den Zahlbegriff''(``On the concept of number'') where he spoke of representing allmathematical object in terms of the integers; in 1889 Giuseppe Peanogave formal, symbolic axioms for the natural numbers.The end of the nineteenth century also brought a new boldness in dealingwith the infinite. Before then, infinitary objects and structures(like the set of natural numbers) were treated gingerly; ``infinitelymany'' was understood as ``as many as you want,'' and ``approaches inthe limit'' was understood as ``gets as close as you want.'' But GeorgCantor showed that it was possible to take the infinite at facevalue. Work by Cantor, Dedekind, and others help to introduce thegeneral set-theoretic understanding of mathematics that is now widely accepted.This brings us to twentieth century developments in logic and foundations.In 1902 Russell discovered the paradox in Frege's logical system. In1904 Zermelo proved Cantor's well-ordering principle, using theso-called ``axiom of choice''; the legitimacy of this axiom prompted agood deal of debate. Between 1910 and 1913 the three volumes ofRussell and Whitehead's \emph{Principia Mathematica} appeared,extending the Fregean program of establishing mathematics on logicalgrounds. Unfortunately, Russell and Whitehead were forced to adopt twoprinciples that seemed hard to justify as purely logical: an axiom ofinfinity and an axiom of ``reducibility.'' In the 1900's Poincar\'ecriticized the use of ``impredicative definitions'' in mathematics,and in the 1910's Brouwer began proposing to refound all ofmathematics in an ``intuitionistic'' basis, which avoided the use ofthe law of the excluded middle ($!A \lor \lnot !A$).Strange days indeed!{} The program of reducing all of mathematics tologic is now referred to as ``logicism,'' and is commonly viewed ashaving failed, due to the difficulties mentioned above. The program ofdeveloping mathematics in terms of intuitionistic mental constructionsis called ``intuitionism,'' and is viewed as posing overly severerestrictions on everyday mathematics. Around the turn of the century,David Hilbert, one of the most influential mathematicians of all time,was a strong supporter of the new, abstract methods introduced byCantor and Dedekind: ``no one will drive us from the paradise thatCantor has created for us.'' At the same time, he was sensitive tofoundational criticisms of these new methods (oddly enough, now called``classical''). He proposed a way of having one's cake and eating ittoo:\begin{enumerate}\item Represent classical methods with formal axioms and rules;  represent mathematical questions as !!{formula}s in an axiomatic  system.\item Use safe, ``finitary'' methods to prove that these formal  deductive systems are consistent.\end{enumerate}Hilbert's work went a long way toward accomplishing the first goal.In 1899, he had done this for geometry in his celebrated book\emph{Foundations of geometry}. In subsequent years, he and a numberof his students and collaborators worked on other areas of mathematicsto do what Hilbert had done for geometry.  Hilbert himself gave axiomsystems for arithmetic and analysis. Zermelo gave an axiomatization ofset theory, which was expanded on by Fraenkel, Skolem, von Neumann,and others.  By the mid-1920s, there were two approaches that laidclaim to the title of an axiomatization of ``all'' of mathematics, the\emph{Principia mathematica} of Russell and Whitehead, and what came tobe known as Zermelo--Fraenkel set theory.In 1921, Hilbert set out on a research project to establish the goalof proving these systems to be consistent.  He was aided in thisproject by several of his students, in particular Bernays, Ackermann,and later Gentzen. The basic idea for accomplishing this goal was tocast the question of the possibility of !!{derivation} of aninconsistency in mathematics as a combinatorial problem about possiblesequences of symbols, namely possible sequences of sentences whichmeet the criterion of being a correct !!{derivation} of, say, $!A \land\lnot !A$ from the axioms of an axiom system for arithmetic, analysis,or set theory.  A proof of the impossibility of such a sequence ofsymbols would---since it is itself a mathematical proof---beformalizable in these axiomatic systems.  In other words, there wouldbe some sentence $\OCon$ which states that, say, arithmetic isconsistent.  Moreover, this sentence should be provable in the systemsin question, especially if its proof requires only very restricted,``finitary'' means.The second aim, that the axiom systems developed would settle everymathematical question, can be made precise in two ways. In one way, wecan formulate it as follows: For any sentence~$!A$ in the language ofan axiom system for mathematics, either $!A$ or $\lnot !A$ is provablefrom the axioms.  If this were true, then there would be no sentenceswhich can neither be proved nor refuted on the basis of the axioms, noquestions which the axioms do not settle.  An axiom system with thisproperty is called \emph{complete}. Of course, for any given sentenceit might still be a difficult task to determine which of the twoalternatives holds.  But in principle there should be a method to doso.  In fact, for the axiom and !!{derivation} systems considered byHilbert, completeness would imply that such a method exists---althoughHilbert did not realize this.  The second way to interpret thequestion would be this stronger requirement: that there be amechanical, computational method which would determine, for a givensentence~$!A$, whether it is derivable from the axioms or not.In 1931, G\"odel proved the two ``incompleteness theorems,'' whichshowed that this program could not succeed. There is no axiom systemfor mathematics which is complete, specifically, the sentence thatexpresses the consistency of the axioms is a sentence which canneither be proved nor refuted.This struck a lethal blow to Hilbert's original program. However, asis so often the case in mathematics, it also opened up exciting newavenues for research. If there is no one, all-encompassing formalsystem of mathematics, it makes sense to develop more circumscribedsystems and investigate what can be proved in them. It also makessense to develop less restricted methods of proof for establishing theconsistency of these systems, and to find ways to measure how hard itis to prove their consistency.  Since G\"odel showed that (almost)every formal system has questions it cannot settle, it makes sense tolook for ``interesting'' questions a given formal system cannotsettle, and to figure out how strong a formal system has to be tosettle them. To the present day, logicians have been pursuing thesequestions in a new mathematical discipline, the theory of proofs.\end{document}

content/incompleteness/introduction/definitions.tex

% Part: incompleteness% Chapter: introduction% Section: definitions\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{int}{def}\olsection{Definitions}In order to carry out Hilbert's project of formalizing mathematics andshowing that such a formalization is consistent and complete, thefirst order of business would be that of picking a language, logicalframework, and a system of axioms.  For our purposes, let us supposethat mathematics can be formalized in a first-order language, i.e.,that there is some set of !!{constant}s, !!{function}s, and!!{predicate}s which, together with the connectives and quantifiers offirst-order logic, allow us to express the claims of mathematics.Most people agree that such a language exists: the language of settheory, in which $\in$ is the only non-logical symbol.  That such asimple language is so expressive is of course a very implausible claimat first sight, and it took a lot of work to establish thatpractically all of mathematics can be expressed in this very austerevocabulary.  To keep things simple, for now, let's restrict ourdiscussion to arithmetic, so the part of mathematics that just dealswith the natural numbers~$\Nat$.  The natural language in which toexpress facts of arithmetic is~$\Lang L_A$. $\Lang L_A$ contains asingle two-place !!{predicate}~$<$, a single !!{constant}~$\Obj 0$,one one-place !!{function}~$\prime$, and two two-place!!{function}s~$+$ and~$\times$.\begin{defn}A set of !!{sentence}s~$\Gamma$ is a \emph{theory} if it is closedunder entailment, i.e., if $\Gamma = \Setabs{!A}{\Gamma \Entails!A}$.\end{defn}There are two easy ways to specify theories. One is as the set of!!{sentence}s true in some !!{structure}.  For instance, consider the!!{structure} for $\Lang L_A$ in which the !!{domain} is~$\Nat$ andall non-logical symbols are interpreted as you would expect.\begin{defn}\ollabel{def:standard-model}The \emph{standard model of arithmetic} is the !!{structure}~$\StructN$ defined as follows:\begin{enumerate}\item $\Domain N = \Nat$\item $\Assign{\Obj 0}{N} = 0$\item $\Assign{\Obj \prime}{N}(n) = n + 1$ for all $n \in \Nat$\item $\Assign{\Obj +}{N}(n, m) = n + m$ for all $n, m \in \Nat$\item $\Assign{\Obj \times}{N}(n, m) = n\cdot m$ for all $n, m \in \Nat$\item $\Assign{\Obj <}{N} = \Setabs{\tuple{n, m}}{n \in \Nat, m \in  \Nat, n < m}$\end{enumerate}\end{defn}Note the difference between `$\times$' and `$\cdot$': $\times$ is asymbol in the language of arithmetic. Of course, we've chosen it toremind us of multiplication, but $\times$ is not the multiplicationoperation but a two-place function symbol (officially, $\Obj f^2_1$).By contrast, $\cdot$~\emph{is} the ordinary multiplication function.When you see something like $n \cdot m$, we mean the product of thenumbers $n$ and~$m$; when you see something like $x \times y$ we aretalking about a term in the language of arithmetic. In the standardmodel, the function symbol~$\times$ is interpreted as the function$\cdot$ on the natural numbers. For addition, we use $+$ as both thefunction symbol of the language of arithmetic, and the additionfunction on the natural numbers. Here you have to use the context todetermine what is meant.\begin{defn}The theory of \emph{true arithmetic} is the set of !!{sentence}ssatisfied in the standard model of arithmetic, i.e.,\[\Th{TA} = \Setabs{!A}{\Sat{N}{!A}}.\]\end{defn}$\Th{TA}$ is a theory, for whenever $\Th{TA} \Entails !A$, $!A$ issatisfied in every !!{structure} which satisfies~$\Th{TA}$. Since$\Sat{N}{\Th{TA}}$, we have that~$\Sat{N}{!A}$, and so $!A \in \Th{TA}$.The other way to specify a theory~$\Gamma$ is as the set of!!{sentence}s entailed by some set of sentences~$\Gamma_0$. In thatcase, $\Gamma$ is the ``closure'' of $\Gamma_0$ under entailment.Specifying a theory this way is only interesting if $\Gamma_0$ isexplicitly specified, e.g., if the !!{element}s of~$\Gamma_0$ arelisted. At the very least, $\Gamma_0$ has to be decidable, i.e., therehas to be a computable test for when !!a{sentence} counts as anelement of~$\Gamma_0$ or not. We call the !!{sentence}sin~$\Gamma_0$ \emph{axioms} for~$\Gamma$, and $\Gamma$\emph{axiomatized} by~$\Gamma_0$.\begin{defn}A theory~$\Gamma$ is \emph{axiomatized} by~$\Gamma_0$ iff\[\Gamma = \Setabs{!A}{\Gamma_0 \Entails !A}\]\end{defn}\begin{defn}The theory $\Th{Q}$ axiomatized by the following sentences is knownas ``Robinson's $\Th{Q}$'' and is a very simple theory of arithmetic.\begin{align*}& \lforall[x][\lforall[y][(\eq[x'][y'] \lif \eq[x][y])]] \tag{$!Q_1$}\\& \lforall[x][\eq/[\Obj 0][x']] \tag{$!Q_2$}\\& \lforall[x][(\eq[x][\Obj 0] \lor \lexists[y][\eq[x][y']])] \tag{$!Q_3$}\\& \lforall[x][\eq[(x + \Obj 0)][x]] \tag{$!Q_4$}\\& \lforall[x][\lforall[y][\eq[(x + y')][(x + y)']]] \tag{$!Q_5$}\\& \lforall[x][\eq[(x \times \Obj 0)][\Obj 0]] \tag{$!Q_6$}\\& \lforall[x][\lforall[y][\eq[(x \times y')][((x \times y) + x)]]] \tag{$!Q_7$}\\& \lforall[x][\lforall[y][(x < y \liff \lexists[z][\eq[(z' + x)][y]])]] \tag{$!Q_8$}\end{align*}The set of !!{sentence}s $\{!Q_1, \dots, !Q_8\}$ are the axioms of$\Th{Q}$, so $\Th{Q}$ consists of all !!{sentence}s entailed by them:\[\Th{Q} = \Setabs{!A}{\{!Q_1, \dots, !Q_8\} \Entails !A}.\]\end{defn}\begin{defn}Suppose $!A(x)$ is !!a{formula} in $\Lang L_A$ with free variables~$x$and $y_1$, \dots, $y_n$. Then any !!{sentence} of the form\[\lforall[y_1][\dots\lforall[y_n][((!A(\Obj 0) \land \lforall[x][(!A(x)\lif !A(x'))]) \lif \lforall[x][!A(x)])]]\]is an instance of the \emph{induction schema}.\emph{Peano arithmetic}~$\Th{PA}$ is the theory axiomatized by theaxioms of $\Th{Q}$ together with all instances of the inductionschema.\end{defn}\begin{explain}Every instance of the induction schema is true in~$\Struct{N}$. Thisis easiest to see if the !!{formula}~$!A$ only has one free!!{variable}~$x$.  Then $!A(x)$ defines a subset~$X_{!A}$ of~$\Nat$in~$\Struct{N}$.  $X_{!A}$ is the set of all~$n \in \Nat$ such that$\Sat{N}{!A(x)}[s]$ when $s(x) = n$.  The corresponding instance ofthe induction schema is\[((!A(\Obj 0) \land \lforall[x][(!A(x) \lif !A(x'))]) \lif   \lforall[x][!A(x)]).\]If its antecedent is true in~$\Struct{N}$, then $0 \in X_{!A}$ and,whenever $n \in X_{!A}$, so is $n+1$.  Since $0 \in X_{!A}$, we get$1 \in X_{!A}$. With $1 \in X_{!A}$ we get $2 \in X_{!A}$. And so on.So for every $n \in \Nat$, $n \in X_{!A}$. But this means that$\lforall[x][!A(x)]$ is satisfied in~$\Struct{N}$.\end{explain}Both $\Th{Q}$ and $\Th{PA}$ are axiomatized theories.  The bigquestion is, how strong are they? For instance, can $\Th{PA}$ proveall the truths about~$\Nat$ that can be expressed in~$\Lang L_A$?Specifically, do the axioms of $\Th{PA}$ settle all the questionsthat can be formulated in~$\Lang L_A$?Another way to put this is to ask: Is $\Th{PA} = \Th{TA}$?$\Th{TA}$ obviously does prove (i.e., it includes) all the truthsabout~$\Nat$, and it settles all the questions that can be formulatedin~$\Lang L_A$, since if $!A$ is !!a{sentence} in $\Lang L_A$, theneither $\Sat{N}{!A}$ or $\Sat{N}{\lnot !A}$, and so either $\Th{TA}\Entails !A$ or $\Th{TA} \Entails \lnot !A$.  Call such a theory\emph{!!{complete}}.\begin{defn}A theory $\Gamma$ is \emph{!!{complete}} iff for every!!{sentence}~$!A$ in its language, either $\Gamma \Entails !A$ or$\Gamma \Entails \lnot !A$.\end{defn}\begin{explain}By the Completeness Theorem, $\Gamma \Entails !A$ iff $\Gamma \Proves!A$, so $\Gamma$ is complete iff for every !!{sentence}~$!A$ in itslanguage, either $\Gamma \Proves !A$ or $\Gamma \Proves \lnot !A$.\end{explain}Another question we are led to ask is this: Is there a computationalprocedure we can use to test if !!a{sentence} is in~$\Th{TA}$, in$\Th{PA}$, or even just in~$\Th{Q}$?  We can make this more preciseby defining when a set (e.g., a set of !!{sentence}s) is!!{decidable}.\begin{defn}A set $X$ is \emph{!!{decidable}} iff there is a computational procedurewhich on input~$x$ returns~$1$ if $x \in X$ and $0$ otherwise.\end{defn}So our question becomes: Is $\Th{TA}$ ($\Th{PA}$, $\Th{Q}$) !!{decidable}?The answer to all these questions will be: no. None of these theoriesare decidable. However, this phenomenon is not specific to theseparticular theories. In fact, \emph{any} theory that satisfies certainconditions is subject to the same results. One of these conditions,which $\Th{Q}$ and $\Th{PA}$ satisfy, is that they are axiomatized by!!a{decidable} set of axioms.\begin{defn}A theory is \emph{!!{axiomatizable}} if it is axiomatizedby !!a{decidable} set of axioms.\end{defn}\begin{ex}Any theory axiomatized by a finite set of !!{sentence}s is!!{axiomatizable}, since any finite set is !!{decidable}.Thus, $\Th{Q}$, for instance, is !!{axiomatizable}.Schematically axiomatized theories like~$\Th{PA}$ are also!!{axiomatizable}. For to test if $!B$ is among the axiomsof~$\Th{PA}$, i.e., to compute the function $\Char{X}$ where$\Char{X}(!B) = 1$ if $!B$ is an axiom of~$\Th{PA}$ and $= 0$otherwise, we can do the following: First, check if $!B$ is one of theaxioms of~$\Th{Q}$. If it is, the answer is ``yes'' and the value of$\Char{X}(!B) = 1$. If not, test if it is an instance of the inductionschema.  This can be done systematically; in this case, perhaps it'seasiest to see that it can be done as follows: Any instance of theinduction schema begins with a number of universal quantifiers, andthen a sub-!!{formula} that is a conditional. The consequent of thatconditional is $\lforall[x][!A(x, y_1, \dots, y_n)]$ where $x$ and$y_1$, \dots, $y_n$ are all the free variables of~$!A$ and the initialquantifiers of~$!B$ bind the variables~$y_1$, \dots,~$y_n$.  Once wehave extracted this~$!A$ and checked that its free variables match thevariables bound by the universal quantifiers at the frontand~$\lforall[x]$, we go on to check that the antecedent of theconditional matches\[!A(\Obj 0, y_1, \dots, y_n) \land \lforall[x][(!A(x, y_1, \dots, y_n)\lif !A(x', y_1, \dots, y_n))]\]Again, if it does, $!B$ is an instance of the induction schema, and ifit doesn't, $!B$ isn't.\end{ex}In answering this question---and the more general question of whichtheories are complete or decidable---it will be useful to consideralso the following definition. Recall that a set $X$ is !!{enumerable}iff it is empty or if there is !!a{surjective} function~$f \colon \Nat\to X$. Such a function is called an enumeration of~$X$.\begin{defn}A set $X$ is called \emph{!!{computably enumerable}} (!!{c.e.} forshort) iff it is empty or it has a computable enumeration.\end{defn}In addition to !!{axiomatizability}, another condition on theories towhich the incompleteness theorems apply will be that they are strongenough to prove basic facts about computable functions and!!{decidable} relations. By ``basic facts,'' we mean !!{sentence}swhich express what the values of computable functions are for each oftheir arguments.  And by ``strong enough'' we mean that the theoriesin question count these sentences among its theorems. For instance,consider a prototypical computable function: addition.  The value of$+$ for arguments $2$ and $3$ is~$5$, i.e., $2+3 = 5$. A sentence inthe language of arithmetic that expresses that the value of $+$ forarguments $2$ and $3$ is~$5$ is: $(\num{2} + \num{3}) = \num{5}$.And, e.g., $\Th{Q}$ proves this sentence.  More generally, we wouldlike there to be, for each computable function $f(x_1, x_2)$!!a{formula}~$!A_f(x_1, x_2, y)$ in~$\Lang{L_A}$ such that $\Th{Q}\Proves !A_f(\num{n_1}, \num{n_2}, \num{m})$ whenever $f(n_1, n_2) =m$. In this way, $\Th{Q}$ proves that the value of~$f$ for arguments$n_1$, $n_2$ is~$m$. In fact, we require that it proves a bit more,namely that no other number is the value of~$f$ for arguments$n_1$,~$n_2$. And the same goes for !!{decidable} relations. This ismade precise in the following two definitions.\begin{defn}A !!{formula}~$!A(x_1, \dots, x_k, y)$ \emph{!!{represents}} thefunction $f\colon \Nat^k \to \Nat$ in~$\Gamma$ iff whenever $f(n_1,\dots, n_k) = m$, then\begin{enumerate}\item $\Gamma \Proves !A(\num{n_1}, \dots, \num{n_k}, \num{m})$, and\item $\Gamma \Proves \lforall[y](!A(\num{n_1}, \dots, \num{n_k},y) \lif y = \num{m})$.\end{enumerate}\end{defn}\begin{defn}A !!{formula}~$!A(x_1, \dots, x_k)$ \emph{!!{represents}} therelation $R \subseteq \Nat^k$ iff,\begin{enumerate}\item whenever $R(n_1, \dots, n_k)$, $\Gamma \Proves !A(\num{n_1},\dots, \num{n_k})$, and\item whenever not $R(n_1, \dots, n_k)$, $\Gamma \Proves \lnot!A(\num{n_1}, \dots, \num{n_k})$.\end{enumerate}\end{defn}A theory is ``strong enough'' for the incompleteness theorems toapply if it !!{represents} all computable functions and all!!{decidable} relations. $\Th{Q}$~and its extensions satisfy thiscondition, but it will take us a while to establish this---it's anon-trivial fact about the kinds of things $\Th{Q}$ can prove, andit's hard to show because $\Th{Q}$ has only a few axioms from whichwe'll have to prove all these facts. However, $\Th{Q}$ is a very weaktheory. So although it's hard to prove that $\Th{Q}$ represents allcomputable functions, most interesting theories are strongerthan~$\Th{Q}$, i.e., prove more than $\Th{Q}$ does. And if $\Th{Q}$proves something, any stronger theory does; since $\Th{Q}$ representsall computable functions, every stronger theory does. This means thatmany interesting theories meet this condition of the incompletenesstheorems. So our hard work will pay off, since it shows that theincompleteness theorems apply to a wide range of theories. Certainly,any theory aiming to formalize ``all of mathematics'' must proveeverything that $\Th{Q}$ proves, since it should at the very least beable to capture the results of elementary computations.  So any theorythat is a candidate for a theory of ``all of mathematics'' will be oneto which the incompleteness theorems apply.\end{document}

content/incompleteness/introduction/overview.tex

% Part: incompleteness% Chapter: introduction% Section: overview\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{int}{ovr}\olsection{Overview of Incompleteness Results}Hilbert expected that mathematics could be formalized in an!!{axiomatizable} theory which it would be possible to prove!!{complete} and !!{decidable}. Moreover, he aimed to prove theconsistency of this theory with very weak, ``finitary,'' means, whichwould defend classical mathematics against the challenges ofintuitionism.  G\"odel's incompleteness theorems showed that thesegoals cannot be achieved.G\"odel's first incompleteness theorem showed that a version ofRussell and Whitehead's \emph{Principia Mathematica} is not!!{complete}.  But the proof was actually very general and applies toa wide variety of theories.  This means that it wasn't just that\emph{Principia Mathematica} did not manage to completely capturemathematics, but that \emph{no} acceptable theory does.  It took awhile to isolate the features of theories that suffice for theincompleteness theorems to apply, and to generalize G\"odel's proof toapply make it depend only on these features.  But we are now in aposition to state a very general version of the first incompletenesstheorem for theories in the language $\Lang L_A$ of arithmetic.\begin{thm}If $\Gamma$ is a consistent and !!{axiomatizable} theory in~$\LangL_A$ which !!{represents} all computable functions and !!{decidable}relations, then $\Gamma$ is not !!{complete}.\end{thm}To say that $\Gamma$ is not !!{complete} is to say that for at leastone !!{sentence}~$!A$, $\Gamma \Proves/ !A$ and $\Gamma \Proves/ \lnot!A$.  Such !!a{sentence} is called \emph{independent} (of~$\Gamma)$.We can in fact relatively quickly prove that there must be independentsentences. But the power of G\"odel's proof of the theorem lies in thefact that it exhibits a \emph{specific example} of such an independent!!{sentence}. The intriguing construction produces!!a{sentence}~$!G_\Gamma$, called a \emph{G\"odel sentence}for~$\Gamma$, which is unprovable because in $\Gamma$, $!G_\Gamma$ isequivalent to the claim that $!G_\Gamma$ is unprovable in~$\Gamma$.  Itdoes so \emph{constructively}, i.e., given an axiomatizationof~$\Gamma$ and a description of the !!{derivation} system, the proof gives amethod for actually writing down~$!G_\Gamma$.The construction in G\"odel's proof requires that we find a way toexpress in $\Lang L_A$ the properties of and operations on terms and!!{formula}s of $\Lang L_A$ itself. These include properties such as``$!A$ is !!a{sentence},'' ``$\delta$ is !!a{derivation} of~$!A$,''and operations such as $\Subst{!A}{t}{x}$.  This way must (a) expressthese properties and relations via a ``coding'' of symbols andsequences thereof (which is what terms, !!{formula}s, !!{derivation}s,etc. are) as natural numbers (which is what $\Lang L_A$ can talkabout). It must (b) do this in such a way that $\Gamma$ will prove therelevant facts, so we must show that these properties are coded by!!{decidable} properties of natural numbers and the operationscorrespond to computable functions on natural numbers. This is called``arithmetization of syntax.''Before we investigate how syntax can be arithmetized, however, we willconsider the condition that~$\Gamma$ is ``strong enough,'' i.e.,!!{represents} all computable functions and !!{decidable} relations.This requires that we give a precise definition of ``computable.''This can be done in a number of ways, e.g., via the model of Turingmachines, or as those functions computable by programs in somegeneral-purpose programming language.  Since our aim is to!!{represents}s these functions and relations in a theory in thelanguage~$\Lang L_A$, however, it is best to pick a simple definitionof computability of just numerical functions.  This is the notion of\emph{recursive function}.  So we will first discuss the recursivefunctions. We will then show that $\Th{Q}$ already !!{represents} allrecursive functions and relations.  This will allow us to apply theincompleteness theorem to specific theories such as $\Th{Q}$ and$\Th{PA}$, since we will have established that these are examples oftheories that are ``strong enough.''The end result of the arithmetization of syntax is!!a{formula} $\OProv[\Gamma](x)$ which, via the coding of !!{formula}sas numbers, expresses provability from the axioms of~$\Gamma$.Specifically, if $!A$ is coded by the number~$n$, and $\Gamma \Proves!A$, then $\Gamma \Proves \Prov[\Gamma](\num{n})$.  This ``provabilitypredicate'' for $\Gamma$ allows us also to express, in a certainsense, the consistency of $\Gamma$ as !!a{sentence} of~$\Lang L_A$:let the ``consistency statement'' for~$\Gamma$ be the !!{sentence}$\lnot \Prov[\Gamma](\num{n})$, where we take $n$ to be the code of acontradiction, e.g., of~$\lfalse$.  The second incompleteness theoremstates that consistent !!{axiomatizable} theories also do not provetheir own consistency statements.  The conditions required for thistheorem to apply are a bit more stringent than just that the theoryrepresents all computable functions and !!{decidable} relations, butwe will show that $\Th{PA}$ satisfies them.\end{document}

content/incompleteness/introduction/undecidability.tex

% Part: incompleteness% Chapter: introduction% Section: decidability\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{int}{dec}\olsection{Undecidability and Incompleteness}G\"odel's proof of the incompleteness theorems require arithmetizationof syntax. But even without that we can obtain some nice results juston the assumption that a theory !!{represents} all !!{decidable}relations.  The proof is a diagonal argument similar to the proof ofthe undecidability of the halting problem.\begin{thm}If $\Gamma$ is a consistent theory that !!{represents} every!!{decidable} relation, then $\Gamma$ is not !!{decidable}.\end{thm}\begin{proof}Suppose $\Gamma$ were !!{decidable}. We show that if $\Gamma$!!{represents} every !!{decidable} relation, it must be inconsistent.!!^{decidable} properties (one-place relations) are represented by!!{formula}s with one free variable. Let $!A_0(x)$, $!A_1(x)$, \dots,be a computable enumeration of all such !!{formula}s.  Now considerthe following set $D \subseteq \Nat$:\[D = \Setabs{n}{\Gamma \Proves \lnot !A_n(\num{n})}\]The set $D$ is !!{decidable}, since we can test if $n \in D$ by firstcomputing $!A_n(x)$, and from this $\lnot !A_n(\num{n})$. Obviously,substituting the term $\num{n}$ for every free occurrence of $x$ in$!A_n(x)$ and prefixing $!A(\num{n})$ by $\lnot$ is a mechanicalmatter.  By assumption, $\Gamma$ is !!{decidable}, so we can test if$\lnot !A(\num{n}) \in \Gamma$. If it is, $n \in D$, and if it isn't,$n \notin D$. So $D$ is likewise !!{decidable}.Since $\Gamma$ !!{represents} all !!{decidable} properties, it!!{represents}~$D$.  And the !!{formula}s which !!{represents}s $D$in~$\Gamma$ are all among $!A_0(x)$, $!A_1(x)$, \dots. So let $d$ be anumber such that $!A_d(x)$ !!{represents} $D$ in~$\Gamma$.  If $d\notin D$, then, since $!A_d(x)$ !!{represents}~$D$, $\Gamma \Proves\lnot !A_d(\num{d})$. But that means that $d$ meets the definingcondition of~$D$, and so $d \in D$. This contradicts $d \notin D$. Soby indirect proof, $d \in D$.Since $d \in D$, by the definition of~$D$, $\Gamma \Proves \lnot!A_d(\num{d})$. On the other hand, since $!A_d(x)$ !!{represents}~$D$in $\Gamma$, $\Gamma \Proves !A_d(\num{d})$. Hence, $\Gamma$ isinconsistent.\end{proof}\begin{explain}The preceding theorem shows that no consistent theory that!!{represents} all !!{decidable} relations can be !!{decidable}. Wewill show that $\Th{Q}$ does !!{represents}s all !!{decidable}relations; this means that all theories that include $\Th{Q}$, such as$\Th{PA}$ and $\Th{TA}$, also do, and hence also are not!!{decidable}. (Since all these theories are true in the standardmodel, they are all consistent.)We can also use this result to obtain a weak version of the firstincompleteness theorem.  Any theory that is !!{axiomatizable} and!!{complete} is !!{decidable}.  Consistent theories that are!!{axiomatizable} and !!{represents}s all !!{decidable} propertiesthen cannot be !!{complete}.\end{explain}\begin{thm}If $\Gamma$ is !!{axiomatizable} and !!{complete} it is !!{decidable}.\end{thm}\begin{proof}Any inconsistent theory is !!{decidable}, since inconsistent theoriescontain all !!{sentence}s, so the answer to the question ``is $!A \in\Gamma$'' is always ``yes,'' i.e., can be decided.So suppose $\Gamma$ is consistent, and furthermore is!!{axiomatizable}, and !!{complete}. Since $\Gamma$ is!!{axiomatizable}, it is !!{computably enumerable}. For we canenumerate all the correct !!{derivation}s from the axioms of~$\Gamma$by a computable function. From a correct !!{derivation} we can computethe !!{sentence} it !!{derive}s, and so together there is a computablefunction that enumerates all theorems of~$\Gamma$.  A !!{sentence} isa theorem of~$\Gamma$ iff $\lnot !A$ is not a theorem, since $\Gamma$is consistent and !!{complete}.  We can therefore decide if $!A \in\Gamma$ as follows. Enumerate all theorems of $\Gamma$. When $!A$appears on this list, we know that $\Gamma \Proves !A$. When $\lnot!A$ appears on this list, we know that $\Gamma \Proves/ !A$.  Since$\Gamma$ is !!{complete}, one of these cases eventually obtains, sothe procedure eventually produces an answer.\end{proof}\begin{cor}\ollabel{cor:incompleteness}If $\Gamma$ is consistent, !!{axiomatizable}, and !!{represents} every!!{decidable} property, it is not !!{complete}.\end{cor}\begin{proof}If $\Gamma$ were !!{complete}, it would be !!{decidable} by theprevious theorem (since it is !!{axiomatizable} and consistent). Butsince $\Gamma$ !!{represents} every !!{decidable} property, it is not!!{decidable}, by the first theorem.\end{proof}\begin{prob}Show that $\Th{TA} = \Setabs{!A}{\Sat{N}{!A}}$ is not!!{axiomatizable}. You may assume that $\Th{TA}$ represents alldecidable properties.\end{prob}Once we have established that, e.g., $\Th{Q}$, !!{represents} all!!{decidable} properties, the corollary tells us that $\Th{Q}$ must beincomplete. However, its proof does not provide an example of anindependent !!{sentence}; it merely shows that such !!a{sentence}must exist. For this, we have to arithmetize syntax and followG\"odel's original proof idea.  And of course, we still have to showthe first claim, namely that $\Th{Q}$ does, in fact, !!{represents}sall !!{decidable} properties.It should be noted that not every \emph{interesting} theory isincomplete or undecidable. There are many theories that aresufficiently strong to describe interesting mathematical facts that donot satisify the conditions of G\"odel's result. For instance,$\Th{Pres} = \Setabs{!A \in \Lang{L_{A^+}}}{\Sat{N}{!A}}$, the set of!!{sentence}s of the language of arithmetic without~$\times$ true inthe standard model, is both complete and decidable. This theory iscalled Presburger arithmetic, and proves all the truths about naturalnumbers that can be formulated just with $\Obj{0}$, $\prime$, and~$+$.\end{document}

Source and provenance notes