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.'']