Amusing fact is it didn't take long at all, compared to some later approaches ;) 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-foun...

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?

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!

Check out the axioms of Peano 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.

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?

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

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.