▲ 278 points
back
155 comments
"Principia Mathematica is an odd book, worth looking into from a historical point of view as well as a mathematical one. It was written around 1910, and mathematical logic was still then in its infancy, fresh from the transformation worked on it by Peano and Frege. The notation is somewhat obscure, because mathematical notation has evolved substantially since then. And many of the simple techniques that we now take for granted are absent. Like a poorly-written computer program, a lot of Principia Mathematica's bulk is repeated code, separate sections that say essentially the same things, because the authors haven't yet learned the techniques that would allow the sections to be combined into one."
- Mark Dominus (https://blog.plover.com/math/PM.html)
Have someone refactored it into a more concise and modern version?
Possibly pertinent: Principia Mathematica Maps and Table Site (PM-MATS):
https://principia.lib.uiowa.edu/about.html - more description in my top-level
comment in this page.
It seems like a frontier model LLM could probably do it in day, probably less. Someone would have to read and correct it, though
This was my first thought when I saw the article.
For an accessible introduction before beginning this, consider his _Introduction to Mathematical Philosophy_:
https://en.wikipedia.org/wiki/Introduction_to_Mathematical_P...
and for ease of reading see the various PDF versions at:
Of you prefer an even more entertaining approach and a very gentle introduction into the topic, I recommend the comic "Logicomix" which tells Russel's journey (though not historically correct all the time for story telling reasons).
Just got this from the library, it's a real page turner. Heard about it in this excellent interview: https://www.typetheoryforall.com/episodes/goedel-s-incomplet...
Logicomix is novel, and done well, but flawed … it's deficiencies lie in what it leaves out which may come across as an unfair charge but in this case the charge is warranted. There is a more historically correct and less orthodox work waiting in the wings for whosoever should attempt it.
new comics recommendation! thanks!
similarly the work itself is available here: https://people.umass.edu/klement/pom/
You might be interested in Kurt Goedel’s extended book review wherein he proves that Principia cannot do what it sets out to do, nor can any such system.
I do teach PM when I teach theory of computation, but largely to tell the story of how we discovered the limits to computation.
> Goedel’s extended book review wherein he proves that Principia cannot do what it sets out to do
Perhaps it's this one:
On Formally Undecidable Propositions of Principia Mathematica and Related Systems
https://en.wikipedia.org/wiki/On_Formally_Undecidable_Propos... - PDF: https://monoskop.org/images/9/93/Kurt_G%C3%B6del_On_Formally...
If you can read this book cover-to-cover, you're an absolute hero. Sometimes I wonder if they inserted a big logical error in the middle just to troll people under the assumption nobody would bother to read it.
You mean you don’t have a framed, signed, bug-bounty cheque from Alfred North Whitehead on your wall??
More seriously, there is indeed a huge logical error at the heart of the whole enterprise but it was not discovered until much later by Kurt Gödel.
This is commonly believed, but Gödel didn't identify a logical error at the heart of the whole enterprise, he proved astonishing theorems revealing limitations of any sufficiently powerful formal system. One can kind of think of the Principia as a science experiment to find the extent to which known mathematics could be proven from foundational axioms that could be thought of as "laws of logic". To make their system work, Russell and Whitehead themselves had to add extralogical axioms, such as their Axiom of Reducibility [0] and the Axiom of Infinity, giving empirical evidence (but not a proof) that "laws of logic" alone were not enough. They were also aware of limitations in their own system, such as the inability to define the cardinal $\aleph_\omega$ [1].
Like the article says, what they did was ahead-of-its-time, and a monumental influence on all subsequent work on formal systems, including Gödel's work, regardless of whether Russell and Whitehead achieved their initial aims.
[0] https://en.wikipedia.org/wiki/Axiom_of_reducibility [1] https://www.gutenberg.org/files/78255/78255-h/78255-h.htm#Pa...
Interestingly, there was a Show HN last year formalizing PM in Lean (https://news.ycombinator.com/item?id=43797256), and the Principia Rewrite project (https://www.principiarewrite.com) verified all 189 propositional logic theorems (sections 1-5) in Coq against the original proof sketches
I used to wonder how likely it was that the printers made some typesetting errors. Who among us could, say, type a thousand pages of APL symbols without introducing a bug?
It was required reading for my Logics class in undergrad. Pretty sure it was also on the optionals (aka required) for my Set Theory class as well.
It's also pretty typically a part of History Of Mathematics and Philosophy of Mathematics courses.
The notation for avoiding parentheses is interesting, and I've thought that it might be useful in programming languages.
To illustrate, suppose you have a non-associative operator $. Rather than write a$(b$c), you can write a$.b$c - the . makes the $ before it be lower precedence on the right side. More dots make things be even lower precedence.
So, for example,
a$b .$: x$y .$. p$q
(a$b) $ ((x$y) $ (p$q))
In what way do you think this is useful over parentheses?
It's better visually. No dot, ., :, :., ::, ::., :::, etc. have increasing visual weight, which shows which are the more top-level operators without having to match up parentheses.
I have a copy and like it much. However, i was always partial to Frege's Begriffschrift. His notation was really creative. It's a shame Russel's deflation of that project has sentenced it to the rubbish heap of history.
The Begriffschrift has in no way been consigned to the rubbish heap of history. What gave you that impression? It is seminal. That it had one unresolved paradox in its set-theoretic foundations does not scupper the philosophical insights, nor the creative notation, nor the more-or-less novel approach of conjoining mathematical functions and logic to give us predicate logic (apologies for this brutally simplified sketch)
i like to think of Frege and the Begriffschrift like this
Boole: logic + algebra = algebraic logic
Frege: logic + functions = predicate logic
ergo, if Boole is rightly deified then so should Frege regardless of minor infelicities (which prompted type theory anyhow) -- again, apologies if this is totally misleading
You are confusing his book Begriffsschrift ("concept notation"), where he invented what became modern predicate logic, and his later work "Grundgesetze der Arithmetik" (I/II) which (unsuccessfully) tried to derive arithmetic from purely logical notions, and which made heavy use of the Begriffsschrift.
For those who aren't familiar with the great but tragic story of Principia and Russell's quest for the foundation of math (spoiler: there is none), there's a really great graphic novel called Logicomix https://en.wikipedia.org/wiki/Logicomix
I haven't read it in probably ten years, but it's one of those books and stories I spend an inordinate amount of time thinking about, for whatever reason.
The foundation of math is (mostly) ZFC.
Instead of spending time beating one’s head against Russell and Whitehead, I would advise reading Homotopy Type Theory (aka the HoTT Book). Dependent types are cool and mind-expanding, but higher inductive types are downright mind-altering.
The Little Schemer/Typer could be used as a preparatory text to gear one up for HoTT.
It also has the advantage of being a bit more applicable to functional programming languages, maybe even more so than Mac Lane’s Categories for the Working Mathematician (which I sometimes see suggested to mathematically-inclined Haskell novices).
I tried to read HoTT. First chapter on type theory is great and pretty easy to follow. The second chapter, I got completely lost. I don't remember why, maybe they fixed it since.
But I find univalence axiom intriguing. I am interested in different approach to types, using triage calculus, which is more "materialist" than "structuralist" - type is given by the structure of the (quoted) term in normal form (unlike lambda calculus, triage calculus makes quoting easy). And I feel like univalence is related to quoting, something like if the two quoted terms are equal under "standard self-interpreter", then they are equal.
> maybe even more so than Mac Lane’s Categories for the Working Mathematician (which I sometimes see suggested […])
FWIW, I am very against this recommendation. That book is needlessly opaque. I don’t know a good recommendation for category theory, but that isn’t it.
Principia Mathematica Maps and Table Site (PM-MATS):
https://principia.lib.uiowa.edu/about.html
"The goal of this project is to make clear structural connections between different parts of Principia and to make analyzable data about the theorems, definitions, and primitive postulates in its text. We do this by providing three digital tools ..."
For example here is their take on the celebrated proof in PM that 1 + 1 = 2
This book is an interesting approach to The Principia:
Magnificent Principia (2013), by Colin Pask
https://devontrevarrowflaherty.com/2014/08/26/book-review-pr...
The article is about Russell and Whitehead’s Principia, not Newton’s.
As a former analytic philosophy student, it's always a bit strange and encouraging for me to see stuff like this show up in CS/Tech forums. We need more philosophy now that we are dealing with the implication of "intelligent" machines.
It blows my mind that Russell invented (formalized) types. Such an elemental concept, but so useful.
Russell’s types aren’t really the same notion as types in programming: https://planetmath.org/russellstheoryoftypes
Domainname optional
Tangential but for those who don't know it, Whitehead's Science and the Modern World (1925) is a fascinating read.
I miss modernism!
it seems that someone wants to traduce the PM in lean here : https://github.com/l-pommeret/Principia-Mathematica (probably with the use of llms)
"traduce" doesn't have the same meaning in English as it does in Spanish. The translation of "traducir" is "to translate".
An interesting fact I learned while reading The Dream Machine[1], is that Principia was the basis of Newell, Simon and Shaw’s Logic Theorist (1956), considered to be the “first AI program”. Amusing and amazing to see this in the context of today’s Erdos-slaying LLMs.
Quoting from Wikipedia:
https://en.wikipedia.org/wiki/Logic_Theorist
Logic Theorist is a computer program completed in 1956 by Allen Newell, Herbert A. Simon, and Cliff Shaw.[1] It was the first program deliberately engineered to perform automated reasoning, and has been described as "the first artificial intelligence program".[1][a] Logic Theorist proved 38 of the first 52 theorems in chapter two of Whitehead and Bertrand Russell's Principia Mathematica, and found a new and shorter proof for Theorem 2.85.[3]
It always amazes me how a random dump of someone who read the first 40 pages of PM attracts dozens comments on HN.
This really must be a very math-starved community of people who wanted to learn math but never quite could.
Two thoughts on someone who went out of their way to learn math:
1. If you can already program, the worst thing you can do is think of mathematics as learning a programming language. It is not, and you will waste your time being frustrated with things like syntax and notation. You get “used to” mathematics by doing it, and it’s something on its own. Just go with it. It’s ok to be confused.
2. Do the exercises, and stop asking for “solution manuals”, the point is to get you thinking and the struggle is most important part, not whether you got it “right”. Again, I think this is a programmer centric way of looking at things: “how do I know it’s right if I can’t compile it”.
Maybe that’s why programmers like the foundations of mathematics. Like if somehow they could just go to the bottom of things, the assembler/machine code of sorts, the whole enterprise would make sense. Counterintuitively, the really great mathematicians of yore, did mathematics before it was anywhere close to formalized.
So... the ancient childish attempt to prove mathematics using mathematics (Gödel's Incompleteness slew the challenger) can be used to help me be a better TypeScript programmer? I learned something new today.
Why the belittling language? You actually can prove the completeness and consistency of portions of mathematics.
While axioms were known in ancient times, only Hilbert started the whole "prove Mathematics" thing.
How else would you prove mathematics and why would that be childish to use math? The limitations discovered were quite surprising back then.