Principia Mathematica is modern and insightful

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. Principia Mathematica by Alfred North Whitehead and Bertrand Russell. Cambridge: University Press, 1910- 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.) 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.) …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. The authors then introduce the notation for that ``propositional function'': ""x is hurt" [called ambiguous] really makes no assertion at all, till we have settled whox is. 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 tox in "x is hurt" which yield a proposition, true or false. \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 page then goes on to introduce the notion of a variable scope.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 ofx . … Thex which occurs in "(x).φx " or "(∃x).φx " is called (following Peano) an "apparent variable". 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. ⊢ f 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''.)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 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 examplesin² 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 ofx , although this is equivalent to this latter assertion; it simply asserts that the formula holds, leavingx wholly undetermined; and it is able to do this legitimately, because howeverx is determined, a true proposition results. ⊢ φy ⊂ (∃x).φx : 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...The above proposition gives what is in practice the only way of proving existence theorems: we always have to find some particulary 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. 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. ⊢ ∀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. x ∈ man literally means "x is a man". (I don't mean that Principia first proposed that notation. It was already established.) 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.)