Live data from Hacker News

Principia Mathematica is modern and insightful

okmij.org

51–60 of 175 posts

Re: Principia Mathematica is modern and insightful

#51

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,…

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.

Re: Principia Mathematica is modern and insightful

#52
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.

Re: Principia Mathematica is modern and insightful

#53

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.

Re: Principia Mathematica is modern and insightful

#55

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/

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

https://en.wikipedia.org/wiki/Logicomix

Re: Principia Mathematica is modern and insightful

#56

Earlier quoted context omitted.

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?

There's a reason mathematics was known as "penalty copy" and was notoriously difficult to typeset and even more difficult to turn a profit on. For a deep dive into both ends of that, see the history of publication of Knuth's TAoCP where the text was originally published traditionally by setting metal type on a composition machine (to the extent possible), then compositors would add the additional characters and spaci…

> the current version is 3.141592653

Another instance of a "clever" joke that becomes annoying very fast.

Re: Principia Mathematica is modern and insightful

#57
post #55

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/

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). https://en.wikipedia.org/wiki/Logicomix

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

Re: Principia Mathematica is modern and insightful

#58
post #12

Earlier quoted context omitted.

No it's not. No it wasn't. And you did not read it. EDIT: source: took logic as undergrad + wrote on the tractatus which required a lot of pre-reqs to understand. 0 chance a course at undergrad level ever assigns principia mathematica. I don't care if you went to yale or oxford or ecole normale ... 0 chance. Most charitable interepretation: some pages of it + was on a bibliography. not required reading. if feel embar…

Well said. Thanks for calling out these sort of posers and charlatans on HN. We should not tolerate these people if we are to discuss/argue/motivate interesting/hard subjects productively. I automatically discount anybody on HN (until i have looked at their profile/comment history/any personal bio websites etc.) who claim they have read/studied a) Euclid's Elements b) Newton's Principia c) Maxwell's Treatise on Elect…

I don't know the exact curriculum and I'm sure it's changed over the years, but one of my girlfriends from back in the day really did go to a school that had one like this. St. John's College, which has two campuses in Annapolis, MA and Santa Fe, NM. They had no majors and everyone learns by reading the classics directly. They also have to learn classical Latin and Greek and read many in their original languages. I don't know everything they assigned, but I remember at least they actually did learn geometry by reading Euclid and calculus by reading Newton.

Apparently, the history is that the school lost its accreditation and had to shut down during the Great Depression, so to attract investors and reopen, it adopted an extremely unique identity with no watering down of curriculum and commitment to western classics in an attempt to combat the rise of fascism.

Re: Principia Mathematica is modern and insightful

#59

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.

Re: Principia Mathematica is modern and insightful

#60
post #51

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,…

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 lamb…

I would highly recommend "PROGRAM = PROOF" by Samuel Mimram.

It covers everything from pure lambda calculus through dependent type theory up to homotopy type theory. In comparison to the HoTT book, the book "PROGRAM = PROOF" is oriented less towards mathematicians more towards programmers. It contains also a short introduction to OCaml and Agda.

The book can downloaded from the authors web page:

https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...

https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/publicat...

Post reply on HN