Principia Mathematica is modern and insightful (okmij.org)

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.

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:

https://people.umass.edu/klement/imp/

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.

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).

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.

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.

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.

I miss modernism!

"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)

[dead]

It blows my mind that Russell invented (formalized) types. Such an elemental concept, but so useful.

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]

[1] https://press.stripe.com/the-dream-machine

Tangential but for those who don't know it, Whitehead's Science and the Modern World (1925) is a fascinating read.

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.

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

means

    (a$b) $ ((x$y) $ (p$q))

At least, that's my recollection. It's been over fifty years since I read (significant parts of) it...

This book is an interesting approach to The Principia:

Magnificent Principia (2013), by Colin Pask

https://devontrevarrowflaherty.com/2014/08/26/book-review-pr...

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)

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

https://principia.lib.uiowa.edu/?n=110.643&n=110

Domainname optional

https://216.92.24.179/ftp/

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.

[dead]