Notes on Principia Mathematica by Alfred North Whitehead and Bertrand Russell Cambridge: University Press, 1910- http://www.hti.umich.edu/cgi/t/text/text-idx?c=umhistmath;idno=AAT3201.0001.001 http://name.umdl.umich.edu/AAT3201.0001.001 It is said that the book is famous for taking a thousand pages to prove that 1+1=2. That view of course misses the point emphasized in the preface of Principia. Its proofs are excruciatingly detailed so to remove the chance of an unstated premise being used in a proof. The goal of Principia was to put forward a set of very basic notions, and show that they and they alone are sufficient for the whole Mathematics. I have found Principia quite engaging, hard to put away. Principia discusses, with great insight, such modern topics as extensionality/intensionality, referential transparency, type. It contains perhaps the first mentioning of `domain', `alpha renaming' and `type' in the modern sense. Its `incomplete symbols' -- the ones that only make sense in a context -- anticipate continuations and control operators. It is insightful to observe that the notions of a free and bound variable, substitution, abstraction, and application came from linguistics. I could not help but feel that Principia already contained lambda-calculus. It also seems that Russell and Whitehead anticipated intuitionism, for example, when insisting on separate notations for 'any' vs. `all' (although admitting the equivalence of these notions in their theory). These following are a few notes taken while reading Chapter 1 of Principia, with several comments very kindly given by Jacques Carette. Page 8 of the book has perhaps the first mentioning of referential transparency (although it is not called by this name). It is remarkable that Russell uses "A believes p" as an example of a non-referentially transparent function, whose meaning varies when p is substituted with equivalent propositions. He then states that mathematics is always concerned with extensions rather than intentions. On p12, the book states that definitions are merely typographic conveniences. On the other hand, definitions are of most importance, because they show the intentions of the author. Page 15 draws the distinction between a functional notation and denotation. "\overbar(x) is hurt" is a notation for a propositional function. OTH, "x is hurt" is the denotation. The notation is a closed term; the denotation is an open term, and 'x' is free there. Thus "\overbar(x) is hurt" and "\overbar(y) is hurt" are the same functions; OTH, "x is hurt" and "y is hurt" are distinct. Thus, they introduce alpha-equivalence. They come back to that topic on p 17, after considering quantifiers. What they call `apparent variable' is a bound variable in current terminology; their `real variable' is a free variable. I was particularly amazed at the example they chose to illustrate bound variables and alpha-equivalence: Integral{ f(x) dx where x from a to b} I was quite taken by the following definition: ``The proposition forall x. f x is the total variation of the function \overbar(x).fx'' It seems Russell already anticipated second-order lambda-calculus, where \x.f x indeed has the type Pi x.B? On p18 they introduce what we now call `schematic variables' and assertions of the form |- f x where x is free. This is equivalent to the assertion |- (x) f x (or |- forall x. f x in modern notation) -- which they take as a primitive notion (primitive rule of inference). Still, they want to keep the distinction between asserting the truth for any x vs asserting the truth for all x. They say that many formulas in Math are actually stated in this, schematic way: e.g., in sin^x + cos^2 x = 1, x is free. On page 20, the book says that the only practical way of proving the existence theorems is to find the witness. That is again intuitionism, even more, constructivism. And this was published in 1910... [Jacques noted that Brouwer was also publishing around that time. Some aspects of that constructivism can be traced back Kronecker 30 years earlier.] On p21, after asserting a proposition |- forall x. phi(x) ^ forall x. pwi(x) => forall x. phi(x) ^ psi(x) they write ``this requires phi and psi should be functions which take arguments of the same type. We shall explain this requirement at a later stage).'' I like that remark about types. How contemporary! That was perhaps the first use of the word `type' in the sense now so common in programming. Page 26: the symbol for set membership is actually the Greek epsilon, the first letter of the word `esti' (which, by a Russian analogue), I assume means "to be". So "x \in man" literally means "x is a man" [I don't mean that Principia first proposed that notation. It was already established.] Page 28: ``Negation of a class alpha consists of terms of suitable type for which "x \in alpha" can be _significantly_ and _truly_ denied.'' Again, intuitionism! [Jacques noted that Principia may also be talking about relative complement. ``You need to have a universe of things you can name, in which alpha belongs, to be able to name those things outside alpha.''] Page 33 is probably the first modern definition of a function, which they call `descriptive functions' (they borrow the term from `THE' descriptions). They define a descriptive function from a binary relation: any binary relation R induces a function R'y as the unique x such that xRy holds. They don't impose any restriction on R; however, later, they define `domain' as a class of those y for which there exists only one x so that xRy holds. A one-to-many relation does define a function, with the empty domain. [Jacques commented that logicians call the descriptive functions "definite descriptions" these days. ``The nice thing is that they have to be functional (by definition), but do not have to be constructive! Hilbert is usually credited with its invention.''] They note already in the beginning the difference between these `descriptive functions' (which are most functions in mathematics) and propositional functions. The latter are purely substitution-based, and for them, applying the function to logically equivalent arguments yields equivalent results. That is not generally so for descriptive functions. Thus propositional functions are so defined to satisfy the substitution Lemma. So, Whitehead and Russell have anticipated higher-order abstract syntax back in 1910? [Jacques noted that they anticipated the difference between "definite description" and "explicit function" back in 1910, because there were already examples in mathematics of these. ``Analytic continuation is one of those processes in mathematics which is 'functional' but not a _function_, as it involves a certain amount of choice.'']