Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- It blows my mind that Russell invented (formalized) types. Such an elemental concept, but so useful.by lordleft
- Russell’s types aren’t really the same notion as types in programming: https://planetmath.org/russellstheoryoftypesby layer8
- 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.by scoofy
- This book is an interesting approach to The Principia:
Magnificent Principia (2013), by Colin Pask
https://devontrevarrowflaherty.com/2014/08/26/book-review-pr...
by sergius - The article is about Russell and Whitehead’s Principia, not Newton’s.by layer8
- 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
by jonjacky - 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).
- > 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.
by fn-mote - 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.
by js8 - 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.by nitsuaeekcm
- The foundation of math is (mostly) ZFC.by emil-lp
- 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.by voidhorse
- 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.by cubefox
- 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
by igravious - 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,
meansa$b .$: x$y .$. p$q
At least, that's my recollection. It's been over fifty years since I read (significant parts of) it...(a$b) $ ((x$y) $ (p$q))by radford-neal - In what way do you think this is useful over parentheses?by layer8
- 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.by glimshe
- 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.
by keltor - 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?by kjellsbells
- 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 sketchesby sergevar
- 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.
by gumby - 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.
by pngwen - > 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...
by lioeters - 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:
by WillAdams - similarly the work itself is available here: https://people.umass.edu/klement/pom/by zote
- 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).by hasley
- "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)
by tristramb - This was my first thought when I saw the article.by danilafe
- Have someone refactored it into a more concise and modern version?by bazoom42