Principia Mathematica

Principia Mathematica by Whitehead and Russell was published
back in 1910 — and yet it reads like a modern text on programming
languages. I have found Principia quite engaging and 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 insightfully observes that the notions of free
and bound variables, substitution, abstraction, and application all
come 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).

The whole Principia is very large: It is said that the book is famous
for taking a thousand pages to prove that 1+1=2. As the preface
stresses, the 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.
If Principia were to be published today, all the proofs would be
relegated to a Supplement (or a theorem prover). What important are
the basic notions and the set up — most of which is explained in the
Preface and Chapter 1.

These following are a few notes taken while reading Chapter 1 of
Principia, with several comments very kindly given by Jacques Carette.

Version

The current version is 1.3, August 2026

References

Principia Mathematica by Alfred North Whitehead and Bertrand Russell.
Cambridge: University Press, 1910-
<http://name.umdl.umich.edu/AAT3201.0001.001>
The full scanned text, many thanks to The University of Michigan
Historical Mathematics Collection

Linsky, Bernard. The Notation in Principia Mathematica
The Stanford
Encyclopedia of Philosophy (Summer 2026 Edition), Edward N. Zalta & Uri
Nodelman (eds.)
<https://plato.stanford.edu/archives/sum2026/entries/pm-notation/>

On p12, the book states that definitions are merely typographic
conveniences. On the other hand, definitions are of most importance,
because they show the intent.

…the definitions are not part of our subject, but are, strictly
speaking, mere typographical conveniences.… In spite of the
fact that definitions are theoretically superfluous, it is
nevertheless true that they often convey more important information
than is contained in the propositions in which they are used. …
The collection of definitions embodies our choice of subjects and
our judgement as to what is most important. Secondly, … the
definition contains an analysis of a common idea, and may therefore
express a notable advance.

Propositional functions: anticipation of lambda-calculus

Page 15 introduces “propositional functions”, what is now known as
lambda-terms. See for yourself, from the running example on the page.

“x is hurt” [called ambiguous]
really makes no assertion at all, till we have settled who x is.
Yet owing to the individuality retained by the
ambiguous variable x, it is an ambiguous example from the collection
of propositions arrived at by giving all possible determinations to
x in “x is hurt” which yield a proposition, true or false.

The authors
then introduce the notation for that “propositional function”:
“\hat💬 is hurt”. Although “x is hurt” and “y is hurt”
occurring in the same context can be distinguished, “”\hat🔥 is
hurt” and “\hat⚡ is hurt” convey no distinction of meaning at
all.” The paragraph concludes: “More generally, φx is an ambiguous
value of the propositional function φ\hat🔥, and when a definite
signification a is substituted for x, φa is an unambiguous value
of φ\hat{x}.” Here we have it: free variables, bound variables,
substitution and alpha-equivalence.

The topic of variables comes up again, on p17, in the discussion of
quantified formulas:

The symbol “(x).φx” [in modern notation, ∀x.φ(x)]
denotes one definite proposition, and there is
no distinction in meaning between “(x).φx” and “(y).φy” when
they occur in the same context.
…
The symbol “(x).φx” has some analogy to the symbol
∫_a^bφ(x) dx since in neither case is the expression a
function of x. … The x which occurs in “(x).φx”
or “(∃x).φx” is called (following Peano) an “apparent variable”.

The page then goes on to introduce the notion of a variable scope.

What Principia calls `apparent variable’ is bound variable in
modern terminology; `real variable’ is now called free variable.
The example of a definite integral to illustrate bound variables and
alpha-equivalence is striking. It also shows that lambda calculus
has a long pedigree. I couldn’t help but admire the Leibniz insight.

p18 and p19 of Principia deals with what we now call
schematic variables and schematic assertions, of the form
⊢ f x.

When we assert something containing a real variable, as in e.g.
⊢ x = x
we are asserting any value of the propositional function.
When we assert something containing an apparent variable, as in
⊢ (x).x = x [which is ⊢ ∀ x. x=x in modern notation]
we are asserting … all values of the proposition function in question.
It is plain that
we can only assert “any value” if all values are true;
for otherwise, since the value of the variable remains to be determined,
it might be so determined as to give a false proposition.
Thus in the above instance, since we have
⊢ x = x
we may infer
⊢ (x).x = x

The authors then go on to introduce what we now call generalization,
of ∀-introduction. (Page 20 introduces the inverse, ∀-elimination,
or, as Principia puts it, “what holds for all, holds for any”.)

Although a schematic formula (for any) is equivalent to the corresponding
universally
quantified formula in Principia’s logic [which was later distilled to
is now called First-Order Logic], the authors still wish to keep
the two notions distinct.

The ordinary formulae of mathematics contain such [real-variable]
assertions; for example
sin² x + cos² x = 1
does not assert this or that particular case of the formula, nor does it
assert that the formula holds for all possible values of x,
although this is equivalent to this latter assertion; it simply asserts
that the formula holds, leaving x wholly undetermined; and it is able
to do this legitimately, because however x is determined, a true
proposition results.

On page 20, Principia says, after describing ∃-introduction:
⊢ φy ⊂ (∃x).φx:

The above proposition gives what is in practice the only way of proving
existence theorems: we always have to find some particular y for which
φy holds, and hence to infer (∃x).φx.
If we were to assume what is called the multiplicative axiom, or the
equivalent axiom enunciated by Zermello, that would, in an important class
of cases, give an existence-theorem where no particular instance of
truth can be found.

Thus, for Russell and Whitehead, “the only way in practice” of proving
existence theorems was to exhibit a witness. They have, perhaps
unconsciously, took up intuitionistic, or even constructivist view.
And this was published in 1910…

Jacques Carette noted that Brouwer was also publishing around that
time. (Although it has to be said that Brouwer writings of that time
were hardly
comprehensible to a mathematician. The intuitionistic vs. classical
controversy has really started with Hermann Weyl.)
Jacques has further noted that
some aspects of that constructivism can be traced back
Kronecker 30 years earlier.

Types

On p21, after asserting a proposition (in modern notation)

    ⊢ ∀x. φ(x) ∧ ∀x. ψ(x)   ⇒   ∀x. φ(x) ∧ ψ(x)

the authors write “this requires φ and ψ should be functions which take
arguments of the same type. (We shall explain this requirement at a
later stage).”
How contemporary! That was perhaps the
first use of the word `type’ in the sense now so common in programming.

Origin of set-membership

On p26, the authors note that
the symbol for set membership is actually the Greek epsilon,
the first letter of the word ἐστί — which, by a Russian analogue, I
assume means “to be”. So x ∈ man literally means “x is a man”.
(I don’t mean that Principia first proposed that notation. It was
already established.)

Descriptive functions

Page 33 is probably the first modern definition of a function as a
particular form of a binary relation: any binary relation R induces
a function R'y as the unique x such that xRy holds. No
restriction on R is imposed; however, later `domain’ is introduced
as a class of those y for which there exists only one x so that
xRy holds. A one-to-many relation hence does define a function, with
the empty domain.

Principia calls such binary-relation–induced functions `descriptive
functions’ (now often called “definite descriptions’).
The name and the exposition follows the theory of
descriptions in natural languages that Russell developed five years
prior (in his famous paper “On denoting”, Mind 14(4), 1905).

Jacques Carette noted that Principia 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.”

References

Ludlow, Peter. Descriptions
The Stanford Encyclopedia of Philosophy
(Winter 2023 Edition), Edward N. Zalta & Uri Nodelman (eds.)
<https://plato.stanford.edu/archives/win2023/entries/descriptions/>