Gödel's Theorem: An Incomplete Guide to Its Use and Abuse 1st Edition

In glancing over everyone else's reviews I noticed that no one wants to actually describe the situations where Godel's theorem is wrongly used.

And I guess I can't blame them because the last thing you'd want to do in a review talking about the wrongful use of Godel's theorem is to wrongfully use it yourself!

That being said, I'll cast aside caution and just say that chapters 4 and 6 in regards to Rucker and Penrose are helpful reading along with the book's cautionary message to be mindful in invoking theorem, well, only where it actually applies.

Because the book is so short (just 170 pages), it's a pretty quick read. Reader's new to Godel's theorem may wish to read the excellent Ernest Nagel book entitled simply "Godel's Theorem."

This is a book I bought a few years ago and started reading immediately but put aside and only this summer read it fully from cover to cover. In order to appreciate its content you need some degree of mathematical and computer science maturity. For example, if you have never heard of his theorems and only read Incompleteness: The Proof and Paradox of Kurt Godel or similar popular book then you would have difficulty going through the book and it would appear boring. It is not an entertaining or bedside reading. This is why I put it aside on the first reading although I knew about this theorem since I read Mathematics: The Loss of Certainty more than 25 years ago being a schoolboy (in Russian translation). Just before writing this review I ordered There's Something About Godel: The Complete Guide to the Incompleteness Theorem and the latter looks like less heavy reading judged from excerpts from its publisher website. Putting all these reminiscences aside I really enjoyed second reading of "Godel's Theorem". It really clarified some points from ¬B->¬A or PA & ¬Con(PA) perspectives and made me curious about fixpoints. I even borrowed the latter term and introduced them for crash dump analysis and debugging: "a dereference fixpoint". I also liked chapters 4 and 6 about using Godel's theorems outside mathematics and clarifying misconceptions in Rucker's and Penrose's books. However, after a few months I cannot recall anything definite what I read from that book although I felt good that I understood everything while reading so perhaps the book requires the 3rd reading for me I'm going to give it another try after "There's Something About Godel" and update this review.

Thanks,
Dmitry Vostokov
Founder of Literate Scientist Blog

A lot of new-age drivel has been written about Gödel's theorem. Franzén's goal is to explain its true meaning, which is a marvel unto itself, with no post-Modern overtones. Of course, if you have mush for brains, as is the case for most post-Moderns, you will not be able to sit still long enough to get through this slim book. For those with inquiring minds, however, Franzén offers an exhilarating read.

However important Gödel's theorem in its own right, I found the book interesting as a review of the basics of the foundations of mathematics. Without introducing any equations, Franzén manages to do a very serious job of explaining the issues. The math is needed to verify the validity of some key assertions made in the book, but there is nothing very enlightening about the math itself, so one gets a good feel for the subject just through a mostly-verbal overview.

Franzén deals with "formal systems," which have enough logic and arithmetic to state and prove theorems. Franzén's basic formal systems are the "basic arithmetic" embodied in the Peano Axioms for the natural numbers, including enough propositional and first-order predicate logic to permit proving propositions about numbers (PA), and the Zermelo-Fraenkel axioms of set theory, including the Axiom of Choice (ZFC).

We say a proposition p about the natural number is true precisely if p. For instance, "every even natural number is the sum of two primes" is true if every even natural number is the sum of two primes (Goldbach's conjecture---still unproven). Note that the notion of "truth" is not formulated within PA or ZFC. What formal systems do is to turn axioms and inference rules into theorems. A theorem in a formal system is a sequence of symbols that can be proved within the system. A proof of a theorem is a sequence of statements, each of which is either an axiom or the result of applying the rules of inference to previous statements in the sequence. The theorem proved is simply the last statement of the proof. Thus, a proof can proceed without any concern with the "meanings" of the axioms and inference rules, whereas the concept of "truth" is inherently semantic: a true proposition means something, and what it means is in fact the case.

The foundations of mathematics revolve around assessing the plausibility and value of alternative axiomatic systems, and characterizing the relationship between theorems (strings of symbols legally derived from the axioms and other legally-derived strings of symbols) and the truth of what these theorems assert. We say a formal system S is "valid" if all of its theorems are true, and "complete" if all true statements that can be expressed in the system are theorems (i.e., can be proved). The best of all possible worlds for a formal system is that (a) has interesting theorems, and (b) is valid and complete. A minimum necessity for an acceptable formal system is that it be "consistent," meaning if p is a theorem, then not p is not a theorem. An inconsistent system that contains the propositional calculus (the logical symbols "and", "or", "not", and "implies," and the inference principle modus ponens, which says that "if you prove p, and if you prove p implies q, then you have proved q") can prove anything, so is useless. Consistency, however, is a very weak condition, because a consistent system need not be valid or complete; i.e., a consistent system can prove things that are false and can fail to prove things that are true. Note that a proposition p is provable in a system S if and only if the system S + not-p, gotten by adding non-p as an axiom, is inconsistent.

We say a proposition p is "decidable" in formal system S if it can be either proved or disproved in S. A proposition that can be neither proved nor disproved in S is called "undecidable." Note that p is undecidable in formal system S if and only if both S + p (adding p as an axiom to S) and S + not p (adding not p as an axiom) are consistent.

A Turing machine is basically a computer with a memory that can be expanded to be as large as we want. An "algorithm" is a program for a Turing machine that, given any number or finite sequence of numbers, terminates with an answer in a finite number of steps. Of course, a useful algorithm actually computes something useful. For instance, given two positive integers, there is a well-known algorithm for calculating their least common divisor. Similarly, given a polynomial function f(x,y,z) and a set of numerical inputs a, b, c, there is always an algorithm for calculating f(a,b,c).

We say a property P of numbers is "computable" if it can be checked by applying an algorithm. Consider, for instance, Goldbach's conjecture that every even natural number is the sum of two primes is computable, because given any even natural number k, we can simply run through the primes less than k until we find a pair that sums to k, or we run out of primes less than k. Franzén calls propositions that can be refuted by a computable process "Goldbach-like." A Goldbach-like proposition, if false, can always be proved false by a formal system that includes basic arithmetic, simply by running through all possibilities until a counter-example is found. If a Goldbach-like proposition is true, however, an algorithm for finding a counter-example will simply run forever. If a system is complete, then all its theorems are computable, because we can simultaneously check a statement and its negation, and by completeness, we will find one or the other true eventually, in finite amount of time.

An example of a non-Goldbach like proposition is "there are infinitely many primes p such that p+2 is also prime (we call these "prime pairs"). If this is false, a counterexample is a number k such that there are no prime pairs greater than k. Such a number may exist, but we cannot prove than any number k has this property by a finite algorithmic process.

This totally elementary analysis leads to one important conclusion. In a formal system that can do basic arithmetic, all propositions whose negation is Goldbach-like can be proved, and if the system is consistent, all propositions whose negation is Goldbach-like and can be proved, are true (the latter holds because if a Goldbach-like proposition is false, its negation can be proved, so a consistent system cannot also prove the proposition itself).

The connection between provability and truth is difficult only with respect to non-Goldbach propositions. The great mathematician David Hilbert, at the turn of the Twentieth Century, had the grand ambition to reduce all of mathematics to a finite algorithmic process, thus proving basic mathematical formal systems valid and complete. Kurt Gödel (with important additions provided later by Barkley Rosser, Sr.), in 1931 proved that in any consistent formal system with a certain amount of elementary arithmetic (e.g., PA), there statements of elementary arithmetic that can be neither proved nor disproved. Thus, if S is consistent, there are propositions about the natural numbers that are undecidable in S.

To understand why Gödel's theorem is true, as Franzén makes clear, we must understand the broad outlines of its proof. I confess that I found Franzén's explanation of Gödel numbering, fixpoint constructions, and self-reference statements inscrutable, so I will provide a really simple alternative (see Charlesworth, Mathematics Magazine 54,3 May 1981 for details).

Let us assume that our formal system S has a finite number of symbols, legal combinations of which we may call "formal statements," each of which is may be true or false. We think of a formal statement as containing no "free variables," whose value can affect the truth or falsity of the statement. We assume that given any sentence, there is a mechanical (algorithmic) process for determining whether or not it is a formal statement (i.e., it checks that the sentence is meaningful and does not have any "free variables.")
The system has axioms and rules of inference, so it produces theorems, which are the final lines of proofs, which in turn are sequences of axioms and the result of applying rules of inference to the axioms and other such products. Theorems are thus formal statements. Again, we can check mechanically to determine whether a sequence of sentences is or is not the proof of a theorem. We assume the system can perform negation (i.e. if f is a formal statement, then not-f is also a formal statement). Thus, we can say that the system is consistent if and only if does not prove both f and not-f for any formal statement f.

We assume that the system has a unique representation of each natural number k, and if one such representation is replaced by the representation of any other number in a formal statement, the result is another formal statement. We need a way of expressing functions f(x), where x is a "variable," in the system. We say that a sentence f is a "number predicate" if it is not a formal statement, but it has a recognizable segment that, when replaced by the systems representation for the number 1, becomes a formal statement (there is nothing special about 1, because above we have assumed any number can replace any other number in a formal expression). We write this expression as f(1), thereby defining f(n) for any natural number n.

Our final condition for the formal system is really the key assumption. It is not obviously true for such formal systems as PA and ZFC, but it is in fact true for these and many other systems, as Gödel showed. The assumption is that any computer program P that takes as input a single number and eventually stops, printing either "Yes" or "No" as its output, there is a number predicate fP in the system such that P prints "Yes" when given input n if and only if fP(n) is a theorem.

The rest is easy. With these assumptions, it is clear that a consistent system has a mechanical process (an algorithm) for generating all theorems. It does this by sifting through a list of all strings of the system, looking for proofs of theorems. For any formal statement, either it or its negation is a theorem, and since the system is consistent, eventually a mechanical process with find a proof of one or the other, and then stop. We say that the theorems of S are "computably enumerable." Similarly, there is an algorithm for generating a list of all number predicates f1, f2, f3, and so on. It follows that if the system is complete, there is an algorithm that determines whether any formal statement is a theorem.

We can now prove Gödel's theorem, which states that if our system has the above properties and is consistent, then it is incomplete; i.e., there is a formal statement that cannot be either proved or disproved. In other words, the set of non-theorems, while computable enumerable, is not computably decidable: given a sentence f that is not true but whose negation cannot be proved, we will search forever for a proof of f or not-f. To that when S is complete, there are meaningful sentences in S that are neither provable nor disprovable, assume the system is complete, so the algorithms described above actually exist. Consider a computer program P that, for input n, computes the number predicate fn, then computes whether or not fn(n) is a theorem using the above algorithms, and outputs "No" if fn(n) is a theorem, and "Yes" if fn(n) is not a theorem. By assumption, this program is has a corresponding number predicate. Say fm is the number predicate of P. Thus, by construction, P with input n prints "Yes" if and only if fm(n) is a theorem. It follows that P with input m prints "Yes" if and only if fm(m) is a theorem. But, we originally constructed P to say "No" when it sees input m if and only if its number predicate fm(m) is a theorem. Therefore, our original assumption that the system is complete is incorrect.

This proof makes it clear why the second Gödel theorem is true. This theorem, which Gödel proved informally shortly after his first proof, but was fully proved by Hilbert and Bernays some years after, is that in any consistent system with the above properties, the systems consistency cannot be proved within the system. Thus, if such a system proves its own consistency, then it must be inconsistent (and hence can prove anything). To see, the note that if there is a proof of consistency, this can be used to prove the existence of the algorithms described above, and hence the existence of the computer program P, which we have seen does not exist if the system is consistent.

The above argument seems to me extremely plausible, provided we are capable of showing that every computer program P that outputs "Yes" or "No" for all numerical inputs can be represented by a numerical predicate f(n) that is a theorem precisely when P prints "Yes." This seems quite provable.

Franzén's approach is closer to Gödel's, and less intuitive. First we give to each well-forms string of symbols in the formal system S a unique number, which we call the "Gödel number" of the string. We write the Gödel number of A as <A> (Franzén does not do this---he tries to avoid all mathematical notation). Suppose f is a numerical predicate, which is therefore either true or false when applied to any particular Gödel number. By a "fixpoint" numerical predicate for f we mean a sentence A such that "A if and only if f(<A>)" is a theorem of S. It is certainly not obvious that this construction is possible, but we'll take it on faith. Then, if f(n) asserts "n is not the Gödel number of a theorem of S," the fixpoint for f is denoted G, and is called a "Gödel sentence" for S. Thus, "G if and only if <G> is not the Gödel number of a theorem of S." However, if this sentence is a theorem, then it is provable that it is a theorem if S is consistent, since in this case we can go through all sentences looking for the proof of either G or not-G. This search necessarily halts, and if G is a theorem, it halts by proving this fact. Now, if G is a theorem, the <G> is not the Gödel number of a theorem of S, which is a contradiction.

Both Franzén's proof and the one I sketched use self-referencing sentences in a fundamental way. There is nothing wrong with this (unlike the supposed antinomies like Richard's Paradox, which involve inadmissible self-referencing), but Franzén show that there are computational proof that do not involve self-referencing at all.

Gödel's theorem proves that no consistent system that supports simple arithmetic can either prove its own consistency, or be a self-contained system of all mathematical truths. Some have claimed that this supports having a skeptical attitude towards mathematics, or even science. This is a mistake. One can have a skeptical attitude if one desires, but Gödel's theorem in no way supplies arguments in favor of skepticism. The fact that a formals system can prove its consistency is not a mark in favor of such a system, because an inconsistent system can always prove its consistency. Moreover, our confidence in the axioms of mathematical systems must ultimate come from an irreducible faith in them, based on evidence or reason. This remains true with or without Gödel's theorem.

The book is less than excellent in explaining what Gödel's theorem is all about. However, it is excellent in explaining what it is not! Including the absurd claims of some mathematicians that they know that a theorem that is not provable still is true (my position there is: prove it!).

The problem with Godel's theorems is that they are used as arguments for results in mathematics and philosophy of mathematics that go way beyond their scope - don't get me wrong - these are very significant and important theorems, both mathematically and philosophically, but most people draw a whole host of other (wrong) conclusions from them.

This book puts it all straight - 'nuff said ;-)