At the limit

I reread my copy of Gödel's Proof, by Ernest Nagel and James R. Newman. It's a compact outline (102 pages, not counting the back matter) of the work published by Kurt Gödel in the 1930s on the limitations of formal, deductive methods of proof in mathematics. I recommend it to anyone, mathematician or humanist, who is interested in the idea of what it means to say we have proved something mathematically.

In high school, we're introduced to the axiomatic method, usually through a class in geometry. Given the ground rules: definitions of mathematical objects (points, lines), axioms (also called postulates: these are statements to be accepted without proof, like "any two points can be joined with a line"), and a few rules of logic, the student learns to prove more complex statements about the objects. The most interesting, general-purpose of these statements we call theorems, like that of Pythagoras concerning the sides of a right triangle.

While definitions and rules of logic seem to be given to us a priori, our choice of axioms seems to offer some conceptual leeway. Euclid did a lot of good geometry with his five axioms, but mathematicians wondered whether they were the "right" axioms. In particular, would it be possible, given a set of axioms, to prove every true thing that could be said in geometry, or algebra, or arithmetic? In other words, would there be "nothing you can see that isn't shown?"

Gödel answered this question decisively with a No. For a field as seemingly simple as the arithmetic of the integers, no matter what axioms we choose, there will be true statements that can't be proved from those axioms. There will always be a place where "you can't get there from here."

Well, then, we'd at least like to know that the axioms are consistent, that is, that they can't be used to prove contradictory statements. But to know something, to a mathematician, is to prove it. Without, of course, making inferences that assume that it's true already, or using logic more complicated than the original ground rules. And Gödel established that, again for a simple field like arithmetic, its axioms cannot be proved to be consistent using arithmetic's own ground rules.

Nagel and Newman walk the reader through the proof, illustrating some points in detail, skimming over others. In particular, they explain Gödel's clever way of using primes to assign a unique number to every statement in arithmetic. In this way, every logical relationship among theorems and axioms can be represented by a numerical relationship among their corresponding numbers. Their treatment is easy to follow, although the sailing gets a little rough on p. 89, at the crux of Gödel's proof. (My copy includes some loose sheets of notes from my last reading, about 20 years ago, in which I invented some new notation to help me wrap my head around the argument.)

So how does this work apply to software development? Well, for one thing, it establishes an upper bound, perhaps only in theoretical space, on the effectiveness of formal methods of proving program correctness. (Since I've never written avionics software, this isn't a field I spend too much time in.)

Today's calculating machines have a fixed set of directives built into them; these directives correspond to the fixed rules of inference of formalized axiomatic procedure. The machines thus supply answers to problems by operating in a step-by-step manner, each step being controlled by the built-in directives. But, as Gödel showed in his incompleteness theorem, there are innumerable problems in elementary number theory that fall outside the scope of a fixed axiomatic method, and that such engines are incapable of answering, however intricate and ingenious their built-in mechanisms may be and however rapid their operations. Given a definite problem, a machine of this type might be built for solving it; but no one such machine can be built for solving every problem.

Gödel's Proof has recently been reissued in a new edition, edited by Douglas Hofstadter. Andrew Hodges wrote an appraisal of the original 1958 edition, pointing out the proof's direct influence on Alan Turing and computability theory.