Whitehead and Russell

ch-newton found that this series borrows a title and none of its apparatus. The other Principia is worse, because the corpus does not merely borrow the name — it runs on the mathematics. Measured at HEAD, entity-aware, this page and its Book 13 companion classified out:

The corpus discusses the phenomenon at length — paradox 27 chapters, self-reference 9, incompleteness 39 — and holds none of the machinery built for it. Lean's kernel is a dependent type theory; types were invented in this book, to block a paradox. Part IV is the part that made this page necessary rather than decorative.

The 1925 second edition opens by giving away a piece of its own machinery. Where the first edition took not-p and p or q as indefinables, the second takes Sheffer's single one — p|q, “p is incompatible with q” — and defines the rest:

Block [2] does not take the sufficiency of the stroke on authority. It enumerates every expression in p and q reachable from the stroke and collects the truth function each realises: 16 of 16, with ~p coming out as the shortest, (p|p). And block [3] takes a formula printed in the Introduction — Nicod's single primitive proposition, which replaces the five of ∗1 —

and evaluates it on all 32 rows: true on every one. A source checked against itself, which is the strongest kind of block this corpus writes. The rule of inference — given p and p|(q|r), infer r — is sound on all eight rows, with no row making both premises true and the conclusion false.

And ∗54.43, the proposition Volume I is famous for, in the only sense it claims: for unit classes α and β, α ∩ β = Λ if and only if α ∪ β ∈ 2. Checked in every finite universe from 2 to 6 elements, no mismatch. It is not a proof that one plus one is two; it is the statement of what that sentence means once classes and cardinals have been defined, which is the point of taking 360 pages to reach it.

Block [5] runs Russell's paradox in the form that survives — no map from a set onto its power set — by enumerating every map and looking for the diagonal set D = {x : x ∉ f(x)} in its image:

Exhaustive, not sampled. But the caveat belongs to the authors, and it is the most self-aware sentence in either Principia. Of the Axiom of Reducibility they write that it has “a purely pragmatic justification” and that “clearly it is not the sort of axiom with which we can rest content”, and they record that without it “Cantor's proof that 2ⁿ > n breaks down unless n is finite”. Block [5] is entirely inside the case they say survives — finite n — and says so. An ASSUME tag, declared by the authors, in their own introduction, about their own axiom.

Introduction ch. II states the rule the whole book is arranged around: no object may be defined in terms of a totality that includes itself. The theory of logical types enforces it, and it enforces it in a specific way — by stratifying the range of a variable. That last clause is the operative one, and it is what tools/self_reference.py was written to test: not whether a script mentions a word, but whether the set it counts over contains the script.

The remedy is Russell's: stratify the range. Both columns now exclude the ruler, and at 654fb06 that changes nothing — which is how the exclusion is known to be the right one rather than a convenient one. Stratified, rung 28 goes 2 → 17 and rung 33 goes 31 → 56, and the inversion the paper reported narrows to 3.3 : 1 rather than 3.0 : 1. The finding survives and the numbers moved, which is the ordinary outcome of measuring the same thing twice.

The instrument and what it means for the rest of the repository are in Book 13 · The Range of a Variable, which is where the type theory belongs, because that is where this corpus's Lean work lives.