8 ms·

Stephan Wolfram: 100 Years Since Principia Mathematica

RiderOfGiraffes 16y ago
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.
- slackenerny 16y ago
  Amusing fact is it didn't take long at all, compared to some later approaches ;) http://mathoverflow.net/questions/14356/bourbakis-epsilon-calculus-notation http://mathoverflow.net/questions/14356/bourbakis-epsilon-ca... And a twist you might find worthy a mention in your forthcoming essay, http://mathoverflow.net/questions/40920/what-if-current-foundations-of-mathematics-are-inconsistent/40928#40928 http://mathoverflow.net/questions/40920/what-if-current-foun...
- mchouza 16y ago
  An interesting project that is developing an updated version of this idea is Metamath: http://us.metamath.org/index.html http://us.metamath.org/index.html
  - pbhjpbhj 16y ago
    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.
    - ionfish 16y ago
      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?
- zackattack 16y ago
  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!
  - xcthulhu 16y ago
    Check out the axioms of Peano Arithmetic: http://en.wikipedia.org/wiki/Peano_axioms#Arithmetic http://en.wikipedia.org/wiki/Peano_axioms#Arithmetic 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.
  - jodrellblank 16y ago
    Can you rephrase that question without using the word "why"? I have no idea what "why does 1+1=2?" is trying to find out.
  - RiderOfGiraffes 16y ago
    As a taster ... 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?
    - zackattack 16y ago
      >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.
ionfish 16y ago
There's a Principia Mathematica anniversary symposium at Trinity College, Cambridge this weekend. http://www.srcf.ucam.org/principia/ http://www.srcf.ucam.org/principia/
- pbhjpbhj 16y ago
  Sorry I miss clicked and downvoted you instead of upvoting; the interface prevents me from rectifying this error.
  - oiuyhgfthyujik 16y ago
    So does -1 + 1 = 0 here? Is there some book that proves this?
ez77 16y ago
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 [...]
- joelburget 16y ago
  Volume 2 of Principia Mathematica, not Principles of Mathematics.
  - ez77 16y ago
    Sharp reading... sorry!
joelburget 16y ago
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 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.)"
- ionfish 16y ago
  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 http://math.stanford.edu/~feferman/papers/predicativity.pdf [2] http://www.math.psu.edu/simpson/sosoa/ http://www.math.psu.edu/simpson/sosoa/ [3] http://plato.stanford.edu/entries/type-theory/ http://plato.stanford.edu/entries/type-theory/ [4] http://en.wikipedia.org/wiki/Calculus_of_constructions http://en.wikipedia.org/wiki/Calculus_of_constructions
  - joelburget 16y ago
    Thanks for a better explanation than I could have written myself. 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-debating-type-systems.html http://blogs.perl.org/users/ovid/2010/08/what-to-know-before...
weavejester 16y ago
I'm impressed it took Wolfram until the third paragraph to mention A New Kind of Science.
- ionfish 16y ago
  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/ http://www.cscs.umich.edu/~crshalizi/reviews/wolfram/
  - zackattack 16y ago
    From the review: "[Wolfram] has talent, and once had some promise; he has squandered them". The creation of Mathematica counts as squandering?
    - hga 16y ago
      For "someone who was once a respectable physicist", yes. 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.)
- zackattack 16y ago
  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. =(
  - ionfish 16y ago
    Clearly he should have read the SEP entry on this very subject, 'The Notation in Principia Mathematica'. http://plato.stanford.edu/entries/pm-notation/ http://plato.stanford.edu/entries/pm-notation/
Kototama 16y ago
There is a nice comic book about the life of Bertrand Russell: Logicomix: An Epic Search for Truth The story is well-written, it's fascinating. Here the link: http://www.logicomix.com/ http://www.logicomix.com/
jackfoxy 16y ago
Wolfram ends the essay on a tantalizing note ...another level of automation.... [I]nventing and developing [systems using other axiomatic systems] to respond to some particular purpose. 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 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.

slackenerny 16y ago
Amusing fact is it didn't take long at all, compared to some later approaches ;) http://mathoverflow.net/questions/14356/bourbakis-epsilon-calculus-notation http://mathoverflow.net/questions/14356/bourbakis-epsilon-ca... And a twist you might find worthy a mention in your forthcoming essay, http://mathoverflow.net/questions/40920/what-if-current-foundations-of-mathematics-are-inconsistent/40928#40928 http://mathoverflow.net/questions/40920/what-if-current-foun...
mchouza 16y ago
An interesting project that is developing an updated version of this idea is Metamath: http://us.metamath.org/index.html http://us.metamath.org/index.html
- pbhjpbhj 16y ago
  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.
  - ionfish 16y ago
    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?
zackattack 16y ago
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!
- xcthulhu 16y ago
  Check out the axioms of Peano Arithmetic: http://en.wikipedia.org/wiki/Peano_axioms#Arithmetic http://en.wikipedia.org/wiki/Peano_axioms#Arithmetic 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.
- jodrellblank 16y ago
  Can you rephrase that question without using the word "why"? I have no idea what "why does 1+1=2?" is trying to find out.
- RiderOfGiraffes 16y ago
  As a taster ... 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?
  - zackattack 16y ago
    >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.

ionfish 16y ago

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

pbhjpbhj 16y ago
Sorry I miss clicked and downvoted you instead of upvoting; the interface prevents me from rectifying this error.
- oiuyhgfthyujik 16y ago
  So does -1 + 1 = 0 here? Is there some book that proves this?

ez77 16y ago

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

joelburget 16y ago
Volume 2 of Principia Mathematica, not Principles of Mathematics.
- ez77 16y ago
  Sharp reading... sorry!

joelburget 16y ago

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

ionfish 16y ago
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 http://math.stanford.edu/~feferman/papers/predicativity.pdf [2] http://www.math.psu.edu/simpson/sosoa/ http://www.math.psu.edu/simpson/sosoa/ [3] http://plato.stanford.edu/entries/type-theory/ http://plato.stanford.edu/entries/type-theory/ [4] http://en.wikipedia.org/wiki/Calculus_of_constructions http://en.wikipedia.org/wiki/Calculus_of_constructions
- joelburget 16y ago
  Thanks for a better explanation than I could have written myself. 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-debating-type-systems.html http://blogs.perl.org/users/ovid/2010/08/what-to-know-before...

weavejester 16y ago

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

ionfish 16y ago
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/ http://www.cscs.umich.edu/~crshalizi/reviews/wolfram/
- zackattack 16y ago
  From the review: "[Wolfram] has talent, and once had some promise; he has squandered them". The creation of Mathematica counts as squandering?
  - hga 16y ago
    For "someone who was once a respectable physicist", yes. 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.)
zackattack 16y ago
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. =(
- ionfish 16y ago
  Clearly he should have read the SEP entry on this very subject, 'The Notation in Principia Mathematica'. http://plato.stanford.edu/entries/pm-notation/ http://plato.stanford.edu/entries/pm-notation/

Kototama 16y ago

There is a nice comic book about the life of Bertrand Russell: Logicomix: An Epic Search for Truth The story is well-written, it's fascinating. Here the link: http://www.logicomix.com/ http://www.logicomix.com/

jackfoxy 16y ago

Wolfram ends the essay on a tantalizing note ...another level of automation.... [I]nventing and developing [systems using other axiomatic systems] to respond to some particular purpose. 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.