Post

Ranked #5 on Hacker News with 61 points and 25 comments.

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

Referential transparency, extensionality

Definitions: a mere typographic convenience of most importance

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.

for any vs for all: a glimpse of Intuitionism

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.