Stephan Wolfram: 100 Years Since Principia Mathematica
blog.stephenwolfram.com
blog.stephenwolfram.com
The creation of Mathematica counts as squandering?
Especially to the extent he's putting resources into this instead of Mathematica.
(Note: the above is from the author's (and others) point of view; I've not read the book and have no first hand opinion on it or Wolfram, besides the law-suit happy thing and such, e.g. I don't use Wolfram Alpha because they own whatever is the output of it, I don't and am restricted in how I can use it.)
That's the whole point. If you read it without thinking "Wolfram wrote this therefore it will be self-centered", then it sounds perfectly fine. The GP's snark was merely appealing to people's confirmation bias. It's a high-level version of that high-school classic: "I'll pick on that kid to show I'm part of the group".
Besides, it's depressingly ironic that a community producing a deluge of "How my startup achieved X in Y months" complains about this post being self-centered.
Read it! It's a good essay!
Your analogy works, except its Wolfram who does the bullying, not the other way around.
But Wolfram seems incapable of talking about any subject without shoehorning in some reference to his own works. Even when expected, it's a jarring, unnecessary interruption; a wild swing from a reasonably interesting article on mathematical history to unabashed self-promotion.
The snark wasn't intended as an offering to Hacker New group-think, but rather borne out of a genuine frustration at Wolfram's style of writing. I find it very difficult to read anything he says, because I'm continually awaiting that moment when he will pause, smile cheesily at the proverbial camera, and explain how amazing his products are.
"To resolve this, Russell introduced what is often viewed as his most original contribution to mathematical logic: his theory of types—which in essence tries to distinguish between sets, sets of sets, etc. by considering them to be of different “types”, and then restricts how they can be combined. I must say that I consider types to be something of a hack. And indeed I have always felt that the related idea of “data types” has very much served to hold up the long-term development of programming languages. (Mathematica, for example, gets great flexibility precisely from avoiding the use of types.)"
No one uses ramified type theory these days, at least not that I am aware, although Russell's predicativism lives on in e.g. Feferman's programme [1] (there are some interesting results in reverse mathematics relating to this; see Simpson's book [2]).
Anyone missing the background I and the parent comment allude to might want to take a look at Thierry Coquand's article on type theory in the SEP [3]. Coquand is the originator of many ideas in this area, including the calculus of constructions [4] and the proof assistant Coq based on it.
[1] http://math.stanford.edu/~feferman/papers/predicativity.pdf
[2] http://www.math.psu.edu/simpson/sosoa/
I also like this page as a more basic introduction to type systems: http://blogs.perl.org/users/ovid/2010/08/what-to-know-before...
In the 1920s Frank Ramsey proved that the theory of ramified types + "The Axiom of Reducibility" is equivalent to the theory of simple types: http://en.wikipedia.org/wiki/Type_theory#Simple_theory_of_ty...
The history I've heard is that ramified types were abandoned after this, since simple type theory is easier and has the same expressive power.
José Ferreirós in The Princeton Companion to Mathematics mentions his name as well, albeit without much detail. Chwistek seems a fascinating character: like his contemporary Witkacy, he was an artist as well as a logician, and according to the biography of Alfred Tarski by the Fefermans [2], was appointed to a professorship at Lvov in 1930 which Tarski was also in the running for; apparently a letter of recommendation from Russell was the decisive factor (see p. 67 of the aforementioned).
Bernard Linsky seems to have written a chapter on Chwistek and type theory in The Golden Age of Polish Philosophy. You can read the first page [3] but I haven't been able to find the entire thing online.
[1] http://en.wikipedia.org/wiki/Leon_Chwistek
[2] http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=052...
Try gigapedia.com ;-D
I'll try to write about it later when I get a bit more time.
And a twist you might find worthy a mention in your forthcoming essay, http://mathoverflow.net/questions/40920/what-if-current-foun...
This presumes, of course, that one can tell interesting from uninteresting by examining result statements. I am not certain that this is in fact the case. Our appreciation of the importance of a result stems from our ability to connect it to others; for example, König's lemma allows us to prove completeness and compactness (amongst many other things). If we simply saw it stated in symbolic form, amongst millions of others, would we recognise its importance?
In my freshman year of college, I asked my real analysis professor why 1+1=2 and he failed to provide an edifying explanation. He did, however, commend me for asking -- I think it earned me some brownie points, which I redeemed by asking for extra clarification on more course-related topics later in the quarter.
Anyway, it's always bothered me so if I can learn something about it then I would love to!
If we use Dedekind's recursive definition of addition, and the definitions 1=S(0) and 2=S(S(0)), then:
S(0) + S(0) = S(S(0)+0) = S(S(0))
I know the computer proof assistant Isabelle/HOL, inspired by the Principia Mathematica, can prove simple theorems about arithmetic using a "rewrite" system similar to what I've done above.
I have no idea what "why does 1+1=2?" is trying to find out.
What do you mean by "2"?
What do you mean by "1"?
What do you mean by "+"?
What do you mean by "="?
There's more than one way to get to the number 7. You can start at 0 and count upwards, or you can "add" the numbers "3" and "4". Why should it be that you end up in the same place?
Slightly more complex/general ...
Consider the number line, and divide the stretch between 0 and 1 into 9 equal pieces. Start from 0 and move along two of these pieces. Call the place you get to "T".
Now consider the stretch from 0 to 2, and divide that into 9 equal sized pieces. Take just the first one, and call where that gets to "S".
Why are they the same point?
This seems to me like it's simply rephrasing the question why does 1+1=2. Or, at least, I can't answer it without invoking the field axioms, or perhaps only the ring axioms. Please forgive me if my terminology is awkward.
The story is well-written, it's fascinating. Here the link: http://www.logicomix.com/
Is there some book that proves this?
I see this almost happening daily on HN with the huge interest in new languages especially functional languages. By almost I mean these are mostly descendants of either Lisp or ML and they are based on the same logic. I'm not sure if you would gain anything by hard-wiring a language into one of the other multitude of axiomatic systems. It would be an intellectual challenge to first select an appropriate system, and then construct a useful language. And it would be hard to recruit people to use it enough to provide useful feedback.
In 1903, he published The Principles of Mathematics: Volume 1 (no volume 2 was ever published) [...]
[...] it did not hurt the whole impression that it took until more than 80 pages into volume 2 [...]