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.
The current version is 1.3, August 2026
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/>
Page 8 of Principia has perhaps the first mention in mathematical
literature of intensions and extensions, and what is now called
`referential transparency': ``if p≡q we shall have f(p)≡f(q)''.
Here f(p) is a proposition that includes another proposition p. In
modern terms, we would call f a context and denote by C[], and say
that if p≡q then C[p]≡C[q], which is the familiar statement of
a referential transparent context. The page then shows an
example of a non-referentially transparent context ``A believes p'': a
proposition whose meaning varies when p is substituted with
equivalent propositions. The example betrays the origin of this
concept, from linguistics, specifically, from the work of Frege (who
is mentioned in a footnote). The book states that ``mathematics is
always concerned with extensions rather than intensions.'' (again
borrowing Frege terms, but in English translation.)
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.
Page 15 introduces ``propositional functions'', what is now known as lambda-terms. See for yourself, from the running example on the page.
"
xis hurt" [called ambiguous] really makes no assertion at all, till we have settled whoxis. Yet owing to the individuality retained by the ambiguous variablex, it is an ambiguous example from the collection of propositions arrived at by giving all possible determinations toxin "xis hurt" which yield a proposition, true or false.
The authors
then introduce the notation for that ``propositional function'':
"\hat{x} is hurt". Although "x is hurt" and "y is hurt"
occurring in the same context can be distinguished, ``"\hat{x} is
hurt" and "\hat{y} is hurt" convey no distinction of meaning at
all.'' The paragraph concludes: ``More generally, φx is an ambiguous
value of the propositional function φ\hat{x}, 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 ∫abφ(x) dxsince in neither case is the expression a function ofx. … Thexwhich 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 = xwe 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=xin 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 = xwe 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 = 1does not assert this or that particular case of the formula, nor does it assert that the formula holds for all possible values ofx, although this is equivalent to this latter assertion; it simply asserts that the formula holds, leavingxwholly undetermined; and it is able to do this legitimately, because howeverxis 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
yfor whichφyholds, 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.
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.
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.)
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.''
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/>