- Mark Dominus (https://blog.plover.com/math/PM.html)
https://en.wikipedia.org/wiki/Introduction_to_Mathematical_P...
and for ease of reading see the various PDF versions at:
I do teach PM when I teach theory of computation, but largely to tell the story of how we discovered the limits to computation.
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
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.
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...
OTOH, Russell found a logical error at the heart of Frege's work, and PM fixed it by introducing the theory of types.
Which leads us to our next borderline impenetrable book, Gödel, Escher, Bach by Douglas Hofstadter.
It is a popular science book which catches the vibe of mathematical logic in an excellent way. It is not a textbook, nor a piece of research. It's all vibes, but high-quality vibes. If you are in the right headspace it can be really inspiring!
If they do and enjoy it, good for them! But many parts haven't aged all that well.
However, I can still very warmly recommend 'The Pleasures of Counting' to this very day.
https://www.amazon.com/Godels-Theorem-Simplified-Harry-Gensl...
Hofstadter wrote a followup book: I am a strange loop.
He has another book about the beauty and challenges of translating poetry, but it’s actually about the sudden death of his wife and it's been too sad for me to finish.
I gave that book to my mathematician grandma, and she found it so boring she couldn’t finish it - “All this stuff was known for decades”. True anecdote.
However, it is pretty dated these days.
Why, yes, he works as a compiler engineer.
After a few attempts where I eventually tried "goddle s-chair batch" we found it.
It was under Western Philosophy.
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 spacing material necessary to compose the equations and so forth so as to lay out a galley (which would then be proofed/corrected) --- a successive edition was then typeset using an early imagesetter, which looked so ghastly that DEK considered giving up, but when informed that the imagesetter was controlled by a computer declared, "I am a computer scientist, I can fix that." and expected to knock out a typesetting system over his next sabbatical....
Roughly a decade later, TeX 1.0 was released.... the current version is 3.141592653 (with new versions adding another decimal place as the version tends towards \pi) --- while we're still waiting on the full publication of Vol. 4, it is widely considered that TeX was worth the delay.
Another instance of a "clever" joke that becomes annoying very fast.
[1] The more recent edition is titled "Littlewood's Miscellany"; I am fairly sure this story is in both the older and the newer version.
It's also pretty typically a part of History Of Mathematics and Philosophy of Mathematics courses.
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 embarrassed, that is the consequence for lieing. There is such a thing as intellectual honesty.
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 Electricity and Magnetism d) Einstein's 1905 Annus Mirabilis papers. e) Principia Mathematica by Russell/WhiteHead f) Godel's Theorem g) Bourbaki's mathematics books etc. etc. They might have browsed it out of curiosity but that is not the same as reading/studying it.
Actual conceptual mathematics/science is intrinsically hard even ignoring the archaic language/notations.
As a good example; the Nobel-prize winning physicist S.Chandrasekhar wrote Newton's Principia for the Common Reader where he explains a subset of the principia (only dealing with gravitation) using modern notation and language. He himself found it quite hard and thus the "common reader" in the title is somebody who has had a good course in calculus and has the motivation to put forth the effort in understanding it.
(Of course, if you don't read German, you should get yourself a translation.)
See https://myweb.rz.uni-augsburg.de/~eckern/adp/history/einstei...
I don't think I'm smart enough to casually read and understand original works on General relativity, but the Annus Mirabilis work seems much simpler. The famous E=MC2 paper is only three pages.
See https://myweb.rz.uni-augsburg.de/~eckern/adp/history/einstei...
About Gödel: if you are interested in the theorems, and not necessarily their original presentation, you can get plenty of rigorous modern treatments. It's very common for mathematicians to work out simpler proofs and more appealing presentations of famous results over time.
See https://dn721807.ca.archive.org/0/items/uber-formal-unentsch... if you want to give one of Gödel's work a go. It's only 26 pages. Footnote 48a is especially interesting. Overall the prose is crisp, but the notation is rather archaic to modern eyes.
I agree with your general sentiment, and your heuristic in general.
So what i do is try and find books which are written for the "educated common reader" by an expert who guides you through the original paper/book. It is still difficult to understand if you do not have the necessary background but at least you have a good starting point.
Some books in my collection;
1) Newton's Principia for the Common Reader by S.Chandrasekhar
2) Maxwell on the Electromagnetic Field: A Guided Study (Masterworks of Discovery) by Thomas Simpson
3) Einstein's Miraculous Year by John Stachel.
4) The Annotated Turing by Charles Petzold.
What we need is for a group of professors to get together and start writing a series on explaining the original papers to the "educated common reader" i.e. not too trivial nor too overwhelming. I think there is a huge market for this since it humanizes how science is done in real life which is fundamental for motivation.
We should read the original great works but with intellectual honesty to accept that some/most of it might be over our heads (depending on one's background) and not feel ashamed about it. The point is to not be completely clueless/ignorant but at least have some correct ideas even if it is a simplification/approximation. It is just one stage in the learning process and as we re-read little-by-little over time we begin to understand more and more. This is real education.
I must dissent. Einstein's Annus Mirabilis papers are really quite approachable. You don't need a book to guide you through.
Though if you are having fun with the book, more power to you! Enjoy!
For a general reader, even though they might not get the whole thing they can still get an appreciation for the whole from the commentary/details added by the editor.
The book contains the English translations of the 5 papers with Einstein's original introduction and a short discussion on each, a informative introduction and a foreword by Roger Penrose.
Of the lot, Elements feels misplaced.
Lots of people actually do read Elements as part of their course of study. It's niche but there's a whole cottage industry within academia for that sort of thing. There are probably over a dozen institutions that have either a degree program or a core curriculum that is organized around original texts, with Euclid usually serving as the math distribution of that sequence. So running into people who have read (big chunks of) Elements is not that uncommon. That's true even IRL outside of online discussions forums on thread topics that likely select for such people.
My impression is that this is not really true of the other examples. Except maybe Godel's proofs; I do think a sufficiently motivated instructor could pull a decent chunk of college students through the original text in a semester. Probably better ways to spend everyone's time, though.
... plus it's relatively approachable as such things go, and short enough that closely reading most or all of it isn't a crazy idea, and it was recently-enough widely used as an actual textbook that between that and ongoing modern interest in its use in that capacity, there are tons of study-oriented editions of it floating around and still being published. I mean hell "recreational mathematics" is a thing and lightly-annotated-and-updated Euclid's a pretty solid text for people with that kind of interest to noodle on, with bonus historical appeal since it's super-old and also is assumed background for all educated people into at least the early 20th century, so pops up all the time in historical writing and literature.
Now, Newton? That's more like it. Nobody reads a large amount of his mathematics unless they're some variety of mathematical historian.
I recently came to know of The Annotated Godel: A Reader's Guide to his Classic Paper on Logic and Incompleteness by Hal Prince which i think i need to sit with :-)
Hilbert's idea was that by completely formalizing mathematics on a axiomatic/deductive basis, one can mechanically derive proofs so that you don't run into paradoxes/contradictions.
But then Godel showed such a formal system applied to basic mathematics can never be complete (if consistent) and never prove its own consistency.
The work is in creating the theorem / contradiction from that point, but in the big picture, the approach doesn’t have to come from nowhere.
But the "why and what" must always be explained first even if it is incomplete; since that is the problem we are trying to solve. With logic it is even more important since you can follow a proof from one step to the next but by the time you reach the conclusion you have lost the connecting thread to the starting point (for most general folks) i.e. "you have missed the forest for the trees". This is why many folks feel lost when doing mathematics as mere symbol-pushing.
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.
Euclid isn’t surprising. School children used to learn plane geometry from Euclid until the 1950s or so. I learned geometry at school using a syllabus from Euclid and we learned the modern form of Euclid’s postulates etc but we didn’t study Euclid itself.
[1] Taylor series were developed in the modern form by James Gregory who was trying to reverse engineer how Newton had come up with his series expansions. I say rediscovered above because they were first written down by Madhava of Sangamagrama who gave Taylor series expansions for the trigonometric functions and natural logarithms/exponential function in the 14th century.
It's as if a group of monks wanted to keep the quadrivium and trivium but their clock stopped at the 16th century. One of their faculty proudly said they study analysis by reading Descartes! Which I thought was a highbrow joke but nope, dead serious.
There's a reason that 'standing on the shoulders of giants' is a thing. Dive into the classics after you have gained the maturity from modern texts.
Take one of the easier problems from Rudin. Prove that a continuous function from the unit interval [0,1] to itself has a fixed point. I wonder how a student immersed in the 'classics' would even begin to tackle this.
So, to be fair: most philosophy majors wouldn't have much luck with Rudin.
> Dive into the classics after you have gained the maturity from modern texts.
Diving into old texts is a skill unto itself. That's why a lot of institutions do the great books thing as a core curriculum (so, maybe 2-3 courses taught in this style, as an alternative to more conventional phil 101/history 101 style distribution requirements). Then a more conventional education from there onward. The theory is that this is a mid-point precisely because it provides lots of transferable skills for diving into the classics in your chosen field, while avoiding the "let's learn analysis from descarte" excesses.
Some report it's pretty damn effective at that and leads to an impressive breadth of intellectual confidence in tackling material of almost any sort, but IDK. Anecdotes.
IIRC (it's been a while since I looked into their programs) they do a lot of supplemental reading of newer papers, articles, and book excerpts, and tend to used updated notation when it makes sense. Plus all their classes are heavily discussion-oriented so the reading is potentially enhanced and brought "forward" by whatever their instructors and peers bring to class in their heads.
> Take one of the easier problems from Rudin. Prove that a continuous function from the unit interval [0,1] to itself has a fixed point. I wonder how a student immersed in the 'classics' would even begin to tackle this.
I don't think they tend to train mathematicians, and I think for most students (graduating from any college or university) they never, ever, ever touch the specifics of their more-advanced e.g. math classes (I think this is true even for most programmers or engineers or what have you) any time in the entire rest of their lives, to the point that entirely forgetting most of that stuff by a decade or so later and suffering for that not at all is utterly typical. How much does it matter for students who aren't going into extremely narrow vocations that they come out of them unable to perform this specific task, without first needing to study further?
The usual defense of this fact is "well it's about learning how to learn, expecting the actual content to ever matter for any but a teensy tiny proportion of the students is unreasonable" in which case... see the rest of the post.
That said, even if the OP was assigned the text at some point as an undergraduate, I remain a bit doubtful it was actually read.
The textbooks they use in that course are written in modern notation and are accessible to a knowledgeable reader; neither can be said of the Principia Mathematica. The archaic syntax is a serious issue.
- “effort to refute bullshit is order of magnitude more than to refute it”.
(p.s. this whole comment section is wild - the green & getting downvoted accounts? They said the most credible things of anyone )
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))
Magnificent Principia (2013), by Colin Pask
https://devontrevarrowflaherty.com/2014/08/26/book-review-pr...
This doesn't follow. The sense in which they are equivalent is that they are equifinal, which doesn't mean isomorphism or even homomorphism. It's a meaningful thing in theory, but not in reality. Otherwise, Turing tarpits wouldn't be a thing.
Every foundation occupies a unique region of proof space. Your foundation, and everything that goes into it, doesn't just affect the shape of what's accessible to you in native semantics, it also effects the way you move through this space. This means by changing foundation, not only can we prove things that we otherwise couldn't in theory (in native semantics), it also means we can prove things we otherwise couldn't in practice (what embedding other foundations as object languages doesn't get you). You can recognize a little bit of this in that it makes some things seem easy, but that's an extremely trivial case of what this relationship implies.
It's all just tools in a toolbelt. Treating them like immutable, universal truths is worth tolerating merely out of human limitation, because it's a lot of work to build intuition for a foundation. If we're talking about philosophy of mathematics though? No, it would be a mistake to pretend like choice isn't meaningful. It is extremely meaningful, and there's a lot to be gained out of realizing they're actually just highly specialized tools. Something to grab when it's useful, and throw away when it's not.
That's what I meant. I also tried to provide one justification (out of many) for why looking at other foundations is still useful.
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]
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
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).
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.
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...
It is possible it may get something wrong but as long as you keep beating on the wrongness you should eventually be able to work out what it is, and in its own way that would become possibly the best learning exercise there is. And of course, with the math proofs coming through from AIs lately, I wouldn't guarantee you'll see that much wrong stuff. I expect it would be at a low enough rate to keep you learning... after all, anyone who has had serious math education knows the human teachers aren't always completely correct either and there is the occasional impromptu exercise of everyone staring at the board and trying to figure out what went wrong with the demonstration.
Interesting, dropping this link here for others: https://treecalcul.us/
This means in triage calculus (unlike in lambda calculus, which lacks means to quote programs) you can include expected input data types in your programs.
You can also construct any type theory syntactically by putting together a set of terms in triage calculus which only normalize when composed with correct types.
In triage calculus, you can then study types and propositions as any other programs - using self-interpretation. But I believe, as I detail below, a univalence principle is needed, to postulate the equivalence of metalogical triage calculus and its representation within triage calculus.
Univalence says that equality is equivalent to equivalence, ie, formalizing the notion of when we can use equivalence rather than equality as a step in a proof. In practice, we often only care about proofs “up to equivalence”.
A way to think about this:
- equality is an identity map
- equivalence is an isomorphism
For example, 2 in Z and 2 in R do not have an identity map between them — but do have an isomorphism.
I think the key insight of univalence is not collapsing equivalence into equality — but allowing it to remain a second truth relation.
We don’t want 2 in Z to be equal to 2 in R (because we collapse type distinction), but we do want them to be equivalent — so we can do equivalent reasoning about arithmetic in R to reach conclusions about Z.
(I used equal to mean the latter, this is colloquial, so I should watch my language.)
And what I am saying in my version of univalence is not that these two are the same, but rather, we can simulate beta-reduction equivalence using self-interpretation.
My version of the axiom states, that two terms x, y are beta-equivalent iff the term interpret(quote(x)) is beta-equivalent to term interpret(quote(y)).
(Note that quote() is identity function in triage calculus, I only write it for clarity.)
So my axiom postulates that the metalogical notion of equivalence is equivalent to the one we can study using whatever interpret() - a self-interpreter - is.
Whether my axiom is related to univalence in HoTT, I am not sure. But it feels similar.
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.
He really likes working in informal categories (like his “ologs”) but I haven’t taught from it yet so I’m not sure if it is more or less confusing to introduce categories that way.
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.
Wow. Yeah. You guys ironically didn't just throw out the baby with the bath water thing. You burned me at the stake like a witch for heresy. Due to your cognitive biases and distortions.
You guys are Imperium of Mankind coded or something?
> You burned me at the stake like a witch for heresy.
I think you should try to get a better sense of proportion.
Also:
> my simple point that although the Principia Mathematica tried to do the impossible, there is still utility for its value as a programming self-teaching resource
I don't know what your original intention actually was, but your comment read to me very much as (1) implying that the OP was claiming that PM is useful for making people into better Typescript programmers (which OP very much does not claim) and (2) making fun of the OP for making such a claim while (3) calling the enterprise of which PM was a part "childish".
All of which seems to me like rather the sort of thing that does deserve downvoting to -4, though for what it's worth I didn't downvote you.
I'm guessing people downvoted you for snark.
This really must be a very math-starved community of people who wanted to learn math but never quite could.
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.
I would argue this would only be true for those without formal education. Writing your code on paper is very common in CS courses. You get used to not being able to compile it.