and square 144 will never have any perfect-power mates in Leonardo di Pisa’s recursive sequence (except for 1). Though extremely recondite, the reason behind the infinite mutual-avoidance dance had been found. This is just one more triumph of the Mathematician’s Credo — one more reason to buy a lot of stock in the idea that in mathematics, where there’s a pattern, there’s a reason.
A Tiny Spark in Godel’s Brain
We now return to the story of Kurt Godel and his encounter with the powerful idea that all sorts of infinite classes of numbers can be defined through various kinds of recursive rules. The image of the organic growth of an infinite structure or pattern, all springing out of a finite set of initial seeds, struck Godel as much more than a mere curiosity; in fact, it reminded him of the fact that theorems in PM (like theorems in Euclid’s Elements) always spring (by formal rules of inference) from earlier theorems in PM, with the exception of the first few theorems, which are declared by fiat to be theorems, and thus are called “axioms” (analogues to the seeds).
In other words, in the careful analogy sparked in Godel’s mind by this initially vague connection, the axioms of PM would play the role of Fibonacci’s seeds 1 and 2, and the rules of inference of PM would play the role of adding the two most recent numbers. The main difference is that in PM there are several rules of inference, not just one, so at any stage you have a choice of what to do, and moreover, you don’t have to apply your chosen rule to the most recently generated theorem(s), so that gives you even more choice. But aside from these extra degrees of freedom, Godel’s analogy was very tight, and it turned out to be immensely fruitful.
Clever Rules Imbue Inert Symbols with Meaning
I must stress here that each rule of inference in a formal system like PM not only leads from one or more input formulas to an output formula, but it does so by purely typographical means — that is, via purely mechanical symbol-shunting that doesn’t require any thought about the meanings of symbols. From the viewpoint of a person (or machine) following the rules to produce theorems, the symbols might as well be totally devoid of meaning.
On the other hand, each rule has to be very carefully designed so that, given input formulas that express truths, the output formula will also express a truth. The rule’s designer (Russell and Whitehead, in this case) therefore has to think about the symbols’ intended meanings in order to be sure that the rule will work exactly right for a manipulator (human or otherwise) who is not thinking about the symbols’ intended meanings.
To give a trivial example, suppose the symbol “?” were intended to stand for the concept “or”. Then a possible rule of inference would be:
From any formula “P ? Q” one can derive the reversed formula “Q ? P”.
This rule of inference is reasonable because whenever an or-statement (such as “You’re crazy or I’m crazy”) is true, then so is the flipped-around or-statement (“I’m crazy or you’re crazy”).
This particular ?-flipping rule happens not to be one of PM’s rules of inference, but it could have been one. The point is just that this rule shows how one can mechanically shunt symbols and ignore their meanings, and yet preserve truth while doing so. This rule is rather trivial, but there are subtler ones that do real work. That, indeed, is the whole idea of symbolic logic, first suggested by Aristotle and then developed piecemeal over many centuries by such thinkers as Blaise Pascal, Gottfried Wilhelm von Leibniz, George Boole, Augustus De Morgan, Gottlob Frege, Giuseppe Peano, David Hilbert, and many others. Russell and Whitehead were simply developing the ancient dream of totally mechanizing reasoning in a more ambitious fashion than any of their predecessors had.
Mechanizing the Mathematician’s Credo
If you apply PM’s rules of inference to its axioms (the seeds that constitute the “zeroth generation” of theorems), you will produce some “progeny” — theorems of the “first generation”. Then apply the rules once again to the first-generation theorems (as well as to the axioms) in all the different ways you can; you will thereby produce a new batch of theorems — the second generation. Then from that whole brew comes a third batch of theorems, and so on, ad infinitum, constantly snowballing. The infinite body of theorems of PM is fully determined by the initial seeds and by the typographical “growth rules” that allow one to make new theorems out of old ones.
Needless to say, the hope here is that all of these mechanically generated theorems of PM are true statements of number theory (i.e., no false statement is ever generated), and conversely, it is hoped that all true statements of number theory are mechanically generated as theorems of PM (i.e., no true statement is left ungenerated forever). The first of these hopes is called consistency, and the second one is called completeness.
In a nutshell, we want the entire infinite body of theorems of PM to coincide exactly with the infinite body of true statements in number theory — we want perfect, flawless alignment. At least that’s what Russell and Whitehead wanted, and they believed that with PM they had attained this goal (after all, “s0 + s0 = ss0” was a theorem, wasn’t it?).
Let us recall the Mathematician’s Credo, which in some form or other had existed for many centuries before Russell and Whitehead came along:
X is true because there is a proof of X;
X is true and so there is a proof of X.
The first line expresses the first hope expressed above — consistency. The second line expresses the second hope expressed above — completeness. We thus see that the Mathematician’s Credo is very closely related to what Russell and Whitehead were aiming for. Their goal, however, was to set the Credo on a new and rigorous basis, with PM serving as its pedestal. In other words, where the Mathematician’s Credo merely speaks of “a proof ” without saying what is meant by the term, Russell and Whitehead wanted people to think of it as meaning a proof within PM.
Godel himself had great respect for the power of PM, as is shown by the opening sentences of his 1931 article:
The development of mathematics in the direction of greater exactness has — as is well known — led to large tracts of it becoming formalized, so that proofs can be carried out according to a few mechanical rules. The most comprehensive formal systems yet set up are, on the one hand, the system of Principia Mathematica (PM) and, on the other, the axiom system for set theory of Zermelo-Fraenkel (later extended by J. v. Neumann). These two systems are so extensive that all methods of proof used in mathematics today have been formalized in them, i. e., reduced to a few axioms and rules of inference.
And yet, despite his generous hat-tip to Russell and Whitehead’s opus, Godel did not actually believe that a perfect alignment between truths and PM theorems had been attained, nor indeed that such a thing could ever be attained, and his deep skepticism came from having smelled an extremely strange loop lurking inside the labyrinthine palace of mindless, mechanical, symbol-churning, meaning-lacking mathematical reasoning.
Miraculous Lockstep Synchrony
The conceptual parallel between recursively defined sequences of integers and the leapfrogging set of theorems of PM (or, for that matter, of any formal system whatever, as long as it had axioms acting as seeds and rules of inference acting as growth mechanisms) suggested to Godel that the typographical patterns of symbols on the pages of Principia Mathematica — that is, the
