111–120 of 175 posts
Earlier quoted context omitted.
How is it dated?
A large chunk of the book is philosophizing about AI and the nature of the mind and intelligence. And when it's betting on the AI that existed pre-AI winter... yeah, that part is quite dated.
Earlier quoted context omitted.
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 d…
I heard about St. John's from a twitter thread and find it deeply baffling. 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 classic…
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.
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?
apocryphally a typesetter saw "make x as small as possible" at the end of a math problem to be typeset, and did exactly that
[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.
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 […]) 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.
Earlier quoted context omitted.
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.
Yikes, guys/girls. I got downvoted to -4 points for a misunderstanding or something. Because the author of the website would probably agree with 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 for serious students of computer science. Wow. Yeah. You guys ironically didn't just throw out the baby with the b…
> 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.
"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 f…
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.
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
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…
Interesting, dropping this link here for others: https://treecalcul.us/
Earlier quoted context omitted.
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…
HoTT distinguishes equality from equivalence. 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…
(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.