Principia Mathematica is modern and insightful

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/>

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.

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 ∫abφ(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.