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{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 ∫_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/>