Introduction to Incompleteness

Source file content/incompleteness/introduction/introduction.tex

Source file content/incompleteness/introduction/historical-background.tex

Historical Background

In this section, we will briefly discuss historical developments that will help put the incompleteness theorems in context. In particular, we will give a very sketchy overview of the history of mathematical logic; and then say a few words about the history of the foundations of mathematics.

The study of logic began, essentially, with Aristotle, who lived approximately 384--322 textscbce. His Categories, Prior analytics, and Posterior analytics include systematic studies of the principles of scientific reasoning, including a thorough and systematic study of the syllogism.

Aristotle's logic dominated scholastic philosophy through the middle ages; indeed, as late as the eighteenth century, Kant maintained that Aristotle's logic was perfect and in no need of revision. But the theory of the syllogism is far too limited to model anything but the most superficial aspects of mathematical reasoning. A century earlier, Leibniz, a contemporary of Newton's, imagined a complete “calculus” for logical reasoning, and made some rudimentary steps towards designing such a calculus, essentially describing a version of propositional logic.

The nineteenth century was a watershed for logic. In 1854 George Boole wrote The Laws of Thought, with a thorough algebraic study of propositional logic that is not far from modern presentations. In 1879 Gottlob Frege published his Begriffsschrift (Concept writing) which extends propositional logic with quantifiers and relations, and thus includes first-order logic. In fact, Frege's logical systems included higher-order logic as well, and more. In his Basic Laws of Arithmetic, Frege set out to show that all of arithmetic could be derived in his Begriffsschrift from purely logical assumptions. Unfortunately, these assumptions turned out to be inconsistent, as Russell showed in 1902. But setting aside the inconsistent axiom, Frege more or less invented modern logic singlehandedly, a startling achievement. Quantificational logic was also developed independently by algebraically-minded thinkers after Boole, including Peirce and Schröder.

Let us now turn to developments in the foundations of mathematics. Of course, since logic plays an important role in mathematics, there is a good deal of interaction with the developments just described. For example, Frege developed his logic with the explicit purpose of showing that all of mathematics could be based solely on his logical framework; in particular, he wished to show that mathematics consists of a priori analytic truths instead of, as Kant had maintained, a priori synthetic ones.

Many take the birth of mathematics proper to have occurred with the Greeks. Euclid's Elements, written around 300 B.C., is already a mature representative of Greek mathematics, with its emphasis on rigor and precision. The definitions and proofs in Euclid's Elements survive more or less intact in high school geometry textbooks today (to the extent that geometry is still taught in high schools). This model of mathematical reasoning has been held to be a paradigm for rigorous argumentation not only in mathematics but in branches of philosophy as well. (Spinoza even presented moral and religious arguments in the Euclidean style, which is strange to see!)

Calculus was invented by Newton and Leibniz in the seventeenth century. (A fierce priority dispute raged for centuries, but most scholars today hold that the two developments were for the most part independent.) Calculus involves reasoning about, for example, infinite sums of infinitely small quantities; these features fueled criticism by Bishop Berkeley, who argued that belief in God was no less rational than the mathematics of his time. The methods of calculus were widely used in the eighteenth century, for example by Leonhard Euler, who used calculations involving infinite sums with dramatic results.

In the nineteenth century, mathematicians tried to address Berkeley's criticisms by putting calculus on a firmer foundation. Efforts by Cauchy, Weierstrass, Bolzano, and others led to our contemporary definitions of limits, continuity, differentiation, and integration in terms of “epsilons and deltas,” in other words, devoid of any reference to infinitesimals. Later in the century, mathematicians tried to push further, and explain all aspects of calculus, including the real numbers themselves, in terms of the natural numbers. (Kronecker: “God created the whole numbers, all else is the work of man.”) In 1872, Dedekind wrote “Continuity and the irrational numbers,” where he showed how to “construct” the real numbers as sets of rational numbers (which, as you know, can be viewed as pairs of natural numbers); in 1888 he wrote “Was sind und was sollen die Zahlen” (roughly, “What are the natural numbers, and what should they be?”) which aimed to explain the natural numbers in purely “logical” terms. In 1887 Kronecker wrote “Über den Zahlbegriff” (“On the concept of number”) where he spoke of representing all mathematical objects in terms of the integers; in 1889 Giuseppe Peano gave formal, symbolic axioms for the natural numbers.

The end of the nineteenth century also brought a new boldness in dealing with the infinite. Before then, infinitary objects and structures (like the set of natural numbers) were treated gingerly; “infinitely many” was understood as “as many as you want,” and “approaches in the limit” was understood as “gets as close as you want.” But Georg Cantor showed that it was possible to take the infinite at face value. Work by Cantor, Dedekind, and others helped to introduce the general 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. In 1904 Zermelo proved Cantor's well-ordering principle, using the so-called “axiom of choice”; the legitimacy of this axiom prompted a good deal of debate. Between 1910 and 1913 the three volumes of Russell and Whitehead's Principia Mathematica appeared, extending the Fregean program of establishing mathematics on logical grounds. Unfortunately, Russell and Whitehead were forced to adopt two principles that seemed hard to justify as purely logical: an axiom of infinity and an axiom of “reducibility.” In the 1900's Poincaré criticized the use of “impredicative definitions” in mathematics, and in the 1910's Brouwer began proposing to refound all of mathematics on an “intuitionistic” basis, which avoided the use of the law of the excluded middle ($!A \lor \lnot !A$source).

Strange days indeed! The program of reducing all of mathematics to logic is now referred to as “logicism,” and is commonly viewed as having failed, due to the difficulties mentioned above. The program of developing mathematics in terms of intuitionistic mental constructions is called “intuitionism,” and is viewed as posing overly severe restrictions 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 by Cantor and Dedekind: “no one will drive us from the paradise that Cantor has created for us.” At the same time, he was sensitive to foundational criticisms of these new methods (oddly enough, now called “classical”). He proposed a way of having one's cake and eating it too:

1. Represent classical methods with formal axioms and rules; represent mathematical questions as formulas in an axiomatic system.

2. Use safe, “finitary” methods to prove that these formal deductive systems are consistent.

Hilbert's work went a long way toward accomplishing the first goal. In 1899, he had done this for geometry in his celebrated book Foundations of geometry. In subsequent years, he and a number of his students and collaborators worked on other areas of mathematics to do what Hilbert had done for geometry. Hilbert himself gave axiom systems for arithmetic and analysis. Zermelo gave an axiomatization of set theory, which was expanded on by Fraenkel, Skolem, von Neumann, and others. By the mid-1920s, there were two approaches that laid claim to the title of an axiomatization of “all” of mathematics, the Principia mathematica of Russell and Whitehead, and what came to be known as Zermelo--Fraenkel set theory.

In 1921, Hilbert set out on a research project to establish the goal of proving these systems to be consistent. He was aided in this project by several of his students, in particular Bernays, Ackermann, and later Gentzen. The basic idea for accomplishing this goal was to cast the question of the possibility of a derivation of an inconsistency in mathematics as a combinatorial problem about possible sequences of symbols, namely possible sequences of sentences which meet the criterion of being a correct derivation of, say, $!A \land \lnot !A$source from the axioms of an axiom system for arithmetic, analysis, or set theory. A proof of the impossibility of such a sequence of symbols would---since it is itself a mathematical proof---be formalizable in these axiomatic systems. In other words, there would be some sentence $\OCon$source which states that, say, arithmetic is consistent. Moreover, this sentence should be provable in the systems in question, especially if its proof requires only very restricted, “finitary” means.

The second aim, that the axiom systems developed would settle every mathematical question, can be made precise in two ways. In one way, we can formulate it as follows: For any sentence $!A$source in the language of an axiom system for mathematics, either $!A$source or $\lnot !A$source is provable from the axioms. If this were true, then there would be no sentences which can neither be proved nor refuted on the basis of the axioms, no questions which the axioms do not settle. An axiom system with this property is called complete. Of course, for any given sentence it might still be a difficult task to determine which of the two alternatives holds. But in principle there should be a method to do so. In fact, for the axiom and derivation systems considered by Hilbert, completeness would imply that such a method exists---although Hilbert did not realize this. The second way to interpret the question would be this stronger requirement: that there be a mechanical, computational method which would determine, for a given sentence $!A$source, whether it is derivable from the axioms or not.

In 1931, Godel proved the two incompleteness theorems, which showed that Hilbert's program could not succeed: no consistent, effectively axiomatized system strong enough for the intended mathematics is complete. A Godel sentence is undecidable under the first theorem's hypotheses, while the second theorem says that a suitably strong consistent system cannot prove its own formal consistency statement.

This struck a lethal blow to Hilbert's original program. However, as is so often the case in mathematics, it also opened up exciting new avenues for research. If there is no one, all-encompassing formal system of mathematics, it makes sense to develop more circumscribed systems and investigate what can be proved in them. It also makes sense to develop less restricted methods of proof for establishing the consistency of these systems, and to find ways to measure how hard it is to prove their consistency. Since Gödel showed that (almost) every formal system has questions it cannot settle, it makes sense to look for “interesting” questions a given formal system cannot settle, and to figure out how strong a formal system has to be to settle them. To the present day, logicians have been pursuing these questions in a new mathematical discipline, the theory of proofs.

Source file content/incompleteness/introduction/definitions.tex

Definitions

In order to carry out Hilbert's project of formalizing mathematics and showing that such a formalization is consistent and complete, the first order of business would be that of picking a language, logical framework, and a system of axioms. For our purposes, let us suppose that mathematics can be formalized in a first-order language, i.e., that there is some set of constant symbols, function symbols, and predicate symbols which, together with the connectives and quantifiers of first-order logic, allow us to express the claims of mathematics. Most people agree that such a language exists: the language of set theory, in which $\in$source is the only non-logical symbol. That such a simple language is so expressive is of course a very implausible claim at first sight, and it took a lot of work to establish that practically all of mathematics can be expressed in this very austere vocabulary. To keep things simple, for now, let's restrict our discussion to arithmetic, so the part of mathematics that just deals with the natural numbers $\Nat$source. The natural language in which to express facts of arithmetic is $\Lang L_A$source. $\Lang L_A$source contains a single two-place predicate symbol $<$source, a single constant symbol $\Obj 0$source, one one-place function symbol $\prime$source, and two two-place function symbols $+$source and $\times$source.

There are two easy ways to specify theories. One is as the set of sentences true in some structure. For instance, consider the structure for $\Lang L_A$source in which the domain is $\Nat$source and all non-logical symbols are interpreted as you would expect.

Note the difference between `$\times$source' and `$\cdot$source': $\times$source is a symbol in the language of arithmetic. Of course, we've chosen it to remind us of multiplication, but $\times$source is not the multiplication operation but a two-place function symbol (officially, $\Obj f^2_1$source). By contrast, $\cdot$source is the ordinary multiplication function. When you see something like $n \cdot m$source, we mean the product of the numbers $n$source and $m$source; when you see something like $x \times y$source we are talking about a term in the language of arithmetic. In the standard model, the function symbol $\times$source is interpreted as the function $\cdot$source on the natural numbers. For addition, we use $+$source as both the function symbol of the language of arithmetic, and the addition function on the natural numbers. Here you have to use the context to determine what is meant.

$\Th{TA}$source is a theory, for whenever $\Th{TA} \Entails !A$source, $!A$source is satisfied in every structure which satisfies $\Th{TA}$source. Since $\Sat{N}{\Th{TA}}$source, we have that $\Sat{N}{!A}$source, and so $!A \in \Th{TA}$source.

The other way to specify a theory $\Gamma$source is as the set of sentences entailed by some set of sentences $\Gamma_0$source. In that case, $\Gamma$source is the “closure” of $\Gamma_0$source under entailment. Specifying a theory this way is only interesting if $\Gamma_0$source is explicitly specified, e.g., if the elements of $\Gamma_0$source are listed. At the very least, $\Gamma_0$source has to be decidable, i.e., there has to be a computable test for when a sentence counts as an element of $\Gamma_0$source or not. We call the sentences in $\Gamma_0$source axioms for $\Gamma$source, and $\Gamma$source axiomatized by $\Gamma_0$source.

Both $\Th{Q}$source and $\Th{PA}$source are axiomatized theories. The big question is, how strong are they? For instance, can $\Th{PA}$source prove all the truths about $\Nat$source that can be expressed in $\Lang L_A$source? Specifically, do the axioms of $\Th{PA}$source settle all the questions that can be formulated in $\Lang L_A$source?

Another way to put this is to ask: Is $\Th{PA} = \Th{TA}$source? $\Th{TA}$source obviously does prove (i.e., it includes) all the truths about $\Nat$source, and it settles all the questions that can be formulated in $\Lang L_A$source, since if $!A$source is a sentence in $\Lang L_A$source, then either $\Sat{N}{!A}$source or $\Sat{N}{\lnot !A}$source, and so either $\Th{TA} \Entails !A$source or $\Th{TA} \Entails \lnot !A$source. Call such a theory complete.

Another question we are led to ask is this: Is there a computational procedure we can use to test if a sentence is in $\Th{TA}$source, in $\Th{PA}$source, or even just in $\Th{Q}$source? We can make this more precise by defining when a set (e.g., a set of sentences) is decidable.

So our question becomes: Is $\Th{TA}$source ($\Th{PA}$source, $\Th{Q}$source) decidable?

The answer to all these questions will be: no. None of these theories are decidable. However, this phenomenon is not specific to these particular theories. In fact, any theory that satisfies certain conditions is subject to the same results. One of these conditions, which $\Th{Q}$source and $\Th{PA}$source satisfy, is that they are axiomatized by a decidable set of axioms.

In answering this question---and the more general question of which theories are complete or decidable---it will be useful to consider also the following definition. Recall that a set $X$source is enumerable iff it is empty or if there is a surjective function $f \colon \Nat \to X$source. Such a function is called an enumeration of $X$source.

In addition to axiomatizability, another condition on theories to which the incompleteness theorems apply will be that they are strong enough to prove basic facts about computable functions and decidable relations. By “basic facts,” we mean sentences which express what the values of computable functions are for each of their arguments. And by “strong enough” we mean that the theories in question count these sentences among their theorems. For instance, consider a prototypical computable function: addition. The value of $+$source for arguments $2$source and $3$source is $5$source, i.e., $2+3 = 5$source. A sentence in the language of arithmetic that expresses that the value of $+$source for arguments $2$source and $3$source is $5$source is: $(\num{2} + \num{3}) = \num{5}$source. And, e.g., $\Th{Q}$source proves this sentence. More generally, we would like there to be, for each computable function $f(x_1, x_2)$source a formula $!A_f(x_1, x_2, y)$source in $\Lang{L_A}$source such that $\Th{Q} \Proves !A_f(\num{n_1}, \num{n_2}, \num{m})$source whenever $f(n_1, n_2) = m$source. In this way, $\Th{Q}$source proves that the value of $f$source for arguments $n_1$source, $n_2$source is $m$source. In fact, we require that it proves a bit more, namely that no other number is the value of $f$source for arguments $n_1$source, $n_2$source. And the same goes for decidable relations. This is made precise in the following two definitions.

A theory is “strong enough” for the incompleteness theorems to apply if it represents all computable functions and all decidable relations. $\Th{Q}$source and its extensions satisfy this condition, but it will take us a while to establish this---it's a non-trivial fact about the kinds of things $\Th{Q}$source can prove, and it's hard to show because $\Th{Q}$source has only a few axioms from which we'll have to prove all these facts. However, $\Th{Q}$source is a very weak theory. So although it's hard to prove that $\Th{Q}$source represents all computable functions, most interesting theories are stronger than $\Th{Q}$source, i.e., prove more than $\Th{Q}$source does. And if $\Th{Q}$source proves something, any stronger theory does; since $\Th{Q}$source represents all computable functions, every stronger theory does. This means that many interesting theories meet this condition of the incompleteness theorems. So our hard work will pay off, since it shows that the incompleteness theorems apply to a wide range of theories. Certainly, any theory aiming to formalize “all of mathematics” must prove everything that $\Th{Q}$source proves, since it should at the very least be able to capture the results of elementary computations. So any theory that is a candidate for a theory of “all of mathematics” will be one to which the incompleteness theorems apply.

Source file content/incompleteness/introduction/overview.tex

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 the consistency of this theory with very weak, “finitary,” means, which would defend classical mathematics against the challenges of intuitionism. Gödel's incompleteness theorems showed that these goals cannot be achieved.

Gödel's first incompleteness theorem showed that a version of Russell and Whitehead's Principia Mathematica is not complete. But the proof was actually very general and applies to a wide variety of theories. This means that it wasn't just that Principia Mathematica did not manage to completely capture mathematics, but that no acceptable theory does. It took a while to isolate the features of theories that suffice for the incompleteness theorems to apply, and to generalize Gödel's proof to make it depend only on these features. But we are now in a position to state a very general version of the first incompleteness theorem for theories in the language $\Lang L_A$source of arithmetic.

To say that $\Gamma$source is not complete is to say that for at least one sentence $!A$source, $\Gamma \Proves/ !A$source and $\Gamma \Proves/ \lnot !A$source. Such a sentence is called independent (of $\Gamma$source). We can in fact relatively quickly prove that there must be independent sentences. But the power of Gödel's proof of the theorem lies in the fact that it exhibits a specific example of such an independent sentence. The intriguing construction produces a sentence $!G_\Gamma$source, called a Gödel sentence for $\Gamma$source, which is unprovable because in $\Gamma$source, $!G_\Gamma$source is equivalent to the claim that $!G_\Gamma$source is unprovable in $\Gamma$source. It does so constructively, i.e., given an axiomatization of $\Gamma$source and a description of the derivation system, the proof gives a method for actually writing down $!G_\Gamma$source.

The construction in Gödel's proof requires that we find a way to express in $\Lang L_A$source the properties of and operations on terms and formulas of $\Lang L_A$source itself. These include properties such as “$!A$source is a sentence,” “$\delta$source is a derivation of $!A$source,” and operations such as $\Subst{!A}{t}{x}$source. This way must (a) express these properties and relations via a “coding” of symbols and sequences thereof (which is what terms, formulas, derivations, etc. are) as natural numbers (which is what $\Lang L_A$source can talk about). It must (b) do this in such a way that $\Gamma$source will prove the relevant facts, so we must show that these properties are coded by decidable properties of natural numbers and the operations correspond to computable functions on natural numbers. This is called “arithmetization of syntax.”

Before we investigate how syntax can be arithmetized, however, we will consider the condition that $\Gamma$source 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 Turing machines, or as those functions computable by programs in some general-purpose programming language. Since our aim is to represent these functions and relations in a theory in the language $\Lang L_A$source, however, it is best to pick a simple definition of computability of just numerical functions. This is the notion of recursive function. So we will first discuss the recursive functions. We will then show that $\Th{Q}$source already represents all recursive functions and relations. This will allow us to apply the incompleteness theorem to specific theories such as $\Th{Q}$source and $\Th{PA}$source, since we will have established that these are examples of theories that are “strong enough.”

The end result of the arithmetization of syntax is a formula $\OProv[\Gamma](x)$source which, via the coding of formulas as numbers, expresses provability from the axioms of $\Gamma$source. Specifically, if $!A$source is coded by the number $n$source, and $\Gamma \Proves !A$source, then $\Gamma \Proves \Prov[\Gamma](\num{n})$source. This “provability predicate” for $\Gamma$source allows us also to express, in a certain sense, the consistency of $\Gamma$source as a sentence of $\Lang L_A$source: let the “consistency statement” for $\Gamma$source be the sentence $\lnot \Prov[\Gamma](\num{n})$source, where we take $n$source to be the code of a contradiction, e.g., of $\lfalse$source. The second incompleteness theorem states that suitably strong, consistent axiomatizable theories also do not prove their own consistency statements. The conditions required for this theorem to apply are a bit more stringent than just that the theory represents all computable functions and decidable relations, but we will show that $\Th{PA}$source satisfies them.

Source file content/incompleteness/introduction/undecidability.tex

Undecidability and Incompleteness

Gödel's proof of the incompleteness theorems requires arithmetization of syntax. But even without that we can obtain some nice results just on the assumption that a theory represents all decidable relations. The proof is a diagonal argument similar to the proof of the undecidability of the halting problem.

Once we have established that, e.g., $\Th{Q}$source, represents all decidable properties, the corollary tells us that $\Th{Q}$source must be incomplete. However, its proof does not provide an example of an independent sentence; it merely shows that such a sentence must exist. For this, we have to arithmetize syntax and follow Gödel's original proof idea. And of course, we still have to show the first claim, namely that $\Th{Q}$source does, in fact, represent all decidable properties.

It should be noted that not every interesting theory is incomplete or undecidable. There are many theories that are sufficiently strong to describe interesting mathematical facts that do not satisfy the conditions of Gödel's result. For instance, $\Th{Pres} = \Setabs{!A \in \Lang{L_{A^+}}}{\Sat{N}{!A}}$source, the set of sentences of the language of arithmetic without $\times$source true in the standard model, is both complete and decidable. This theory is called Presburger arithmetic, and proves all the truths about natural numbers that can be formulated just with $\Obj{0}$source, $\prime$source, and $+$source.