Live data from Hacker News

Stephan Wolfram: 100 Years Since Principia Mathematica

blog.stephenwolfram.com

11–20 of 38 posts

Re: Stephan Wolfram: 100 Years Since Principia Mathematica

#12

It's interesting that Wolfram makes a quick foray into computer science to bash type systems. (I think he couldn't be more wrong) "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 c…

It is a strange comment. The type theories used in programming languages, certainly in those based on the λ-cube, descend from simple type theory (via the simply-typed λ-calculus), which Russell discarded in favour of his ramified theory of types. I also wonder why Wolfram, originally a mathematician, doesn't even mention the Curry-Howard correspondence, which seems to me a fairly important result linking mathematics and computation.

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/

[3] http://plato.stanford.edu/entries/type-theory/

[4] http://en.wikipedia.org/wiki/Calculus_of_constructions

Re: Stephan Wolfram: 100 Years Since Principia Mathematica

#13
post #5

Earlier quoted context omitted.

An interesting project that is developing an updated version of this idea is Metamath: http://us.metamath.org/index.html

That is interesting - I think the idea that looms over the whole essay is that we have computers that do logic and can fit those logical operations together, we should be able to give a computer some basic axioms and see what theorems it can construct. Et voila! , there it is. Mention of such a project would have fit the essay well.

Well, the problem is that first-order theories have an infinite number of theorems, so while one can prove as many theorems using a computer as one likes, there is still nothing to say whether they are of any interest or not. Most results are trivial, and in order to find the interesting ones we would have to go digging through a heap mainly composed of uninteresting ones.

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?

Re: Stephan Wolfram: 100 Years Since Principia Mathematica

#14

In case you're interested, about halfway down is the usually quoted result (*110.643) that 1+1=2. I'm often asked why it took so long (it's over 80 pages into volume 2) to prove something so trivially, and obviously true, and recently I've come up with an example that demonstrates the idea. I'll try to write about it later when I get a bit more time.

Please do...

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!

Re: Stephan Wolfram: 100 Years Since Principia Mathematica

#15

I'm impressed it took Wolfram until the third paragraph to mention A New Kind of Science .

Whenever anyone mentions NKS I'm always reminded of Cosma Shalizi's brilliant and hilarious review, 'A Rare Blend of Monster Raving Egomania and Utter Batshit Insanity'.

http://www.cscs.umich.edu/~crshalizi/reviews/wolfram/

Re: Stephan Wolfram: 100 Years Since Principia Mathematica

#16

I'm impressed it took Wolfram until the third paragraph to mention A New Kind of Science .

I also thought it was kind of a dick move to wait until the end to admit that he didn't understand the symbols in principia_1b1.jpg. This is actually a pet peeve of mine in mathematics writing in general, introducing ambiguity and not resolving it until several pages or paragraphs later. It's really alienating. =(

Re: Stephan Wolfram: 100 Years Since Principia Mathematica

#18
post #9
post #4

There's a Principia Mathematica anniversary symposium at Trinity College, Cambridge this weekend. http://www.srcf.ucam.org/principia/

Sorry I miss clicked and downvoted you instead of upvoting; the interface prevents me from rectifying this error.

So does -1 + 1 = 0 here?

Is there some book that proves this?

Re: Stephan Wolfram: 100 Years Since Principia Mathematica

#19
post #6

First: In 1903, he published The Principles of Mathematics: Volume 1 (no volume 2 was ever published) [...] Later: [...] it did not hurt the whole impression that it took until more than 80 pages into volume 2 [...]

Volume 2 of Principia Mathematica, not Principles of Mathematics.

Sharp reading... sorry!

Re: Stephan Wolfram: 100 Years Since Principia Mathematica

#20

I'm impressed it took Wolfram until the third paragraph to mention A New Kind of Science .

The post by Wolfram is a great discussion of logic and the philosophy of mathematics throughout the 20th century. Yet the top comment on HN is a snark, tribal bashing of the author.
Post reply on HN