Has Anyone Else Proven 1 + 1 = 2 Besides Russell?

[robertjford80]

Has anyone else tried to prove that 1 + 1 = 2 besides Russell?

 

[micromass]

I consider $1+1=2$ to be basically a definition.

Anyway, see here: http://us.metamath.org/mpegif/mmset.html#trivia

 

[robertjford80]

Wow! Amazingly useful! Very good webpage. I didn't know that they had it that well organized.

 

[.Scott]

Has anyone else tried to prove that 1 + 1 = 2 besides Russell?

Wasn't Bertrand's proof thorough enough? He went 100+ pages before he finally laid down enough groundwork to define 1+1. Then another 20+ pages before he defined 1+1=2. Then it was close to the end of the book before he finally proved it.
Even if you think there's something deficient about his attempt, most people are willing to treat it as proof enough.

 

[robertjford80]

Wasn't Bertrand's proof thorough enough? He went 100+ pages before he finally laid down enough groundwork to define 1+1. Then another 20+ pages before he defined 1+1=2. Then it was close to the end of the book before he finally proved it.
Even if you think there's something deficient about his attempt, most people are willing to treat it as proof enough.

It's not that it's enough, but it's too much. Our proofs should be as simple as possible but not simpler. (I forget who said that). I'm working on a proof that has maybe 10 steps but it won't be ready until I can get a computer to output the proof using the same algorithm that outputs the proof to similar sentence. I'm trying to build an automated theorem prover that works for a variety of sentences. However, my ambition exceeds my knowledge. I don't know enough about the foundations of math to really prove this and I don't even know set theory. I'm working on correcting that lack of knowledge now.

 

[Tobias Funke]

I'd imagine that 99% of mathematicians either treat this as a definition or simply don't care about slogging through a "rigorous" proof from set theory of the fact. Which provides a great response anytime someone complains about a beautiful, intuitive proof that's not totally rigorous: "you haven't even done a computer-verifiable proof that 1+1=2, so...shut up."

I'm only about half serious, I don't want any angry logicians or set theorists to yell at me.

 

[robertjford80]

I'd imagine that 99% of mathematicians either treat this as a definition or simply don't care about slogging through a "rigorous" proof from set theory of the fact.

It's interesting to note that mathematicians are not too interested in the foundations of mathematics. Some speculate that that is why no one read Frege's work.

 

[robertjford80]

"you haven't even done a computer-verifiable proof that 1+1=2, so...shut up."

I'm new to mathematics. I'm a philosopher that sees in mathematics a guide. I really like the idea of computer-verifiable proofs. The reason why I like them is because computers help us keep track of whether or not we've obeyed all of our rules. Back when I used to try to make philosophical arguments using logic I deluded myself into believing that all of my steps inevitably followed from the previous line. With computers I now know how easy it is to delude yourself into believing that you've proved something when you really haven't. I'm wondering how popular this idea of computer-verifiable proofs is in math today.

 

[micromass]

It's interesting to note that mathematicians are not too interested in the foundations of mathematics.

There are many mathematicians interested in the foundations of mathematics.

Some speculate that that is why no one read Frege's work.

Nobody reads Frege because Frege is wrong. It's also outdated and difficult to read.

 

[.Scott]

It's not that it's enough, but it's too much. Our proofs should be as simple as possible but not simpler..

What Bertrand Russell did was to first define all of the arithmetic operations in terms of sets - and from there proved that addition worked.
The whole trick was "how to do it". Now that it's been explained in detail, it's kind of pointless for someone to restate it - except for translation. Which is kindof what you're doing.

There's only about 4 pages of "The Principles of Mathematics" that you need to understand what has to be done to get a computer "proof" engine to perform the proof.

For example, §113 and §114 provide a definition of addition based on set theory. Here's how §114 ends:

This point may be made clearer by considering a special case, such as 1+1. It is plain that we cannot take the number 1 itself twice over, for there is one number 1, and there are not two instances of it. And if the logical addition of 1 to itself were in question, we should find that 1 and 1 is 1, according to the general principle of Symbolic Logic. Nor can we define 1+1 as the arithmetical sum of a certain class of numbers. This method can be employed as regards 1+2, or any sum in which no number is repeated; but as regards 1+1, the only class of numbers involved is the class whose only member is 1, and since this class has one member, not two, we cannot define 1+1 by its means. Thus the full definition of 1+1 is as follows: 1+1 is the number of a class w which is the logical sum of two classes u and v which have no common term and have each only one term. The chief point to be observed is, that logical addition of classes is the fundamental notion, while the arithmetical addition of numbers is wholly subsequent.

As you can see, it's only long because he's being very careful and explicit with both the logic and the way it is presented. He wants to be clearly understood.
You can then skip to §131 where he takes on the defintion of the result of an addition:

Addition, it should be carefully observed, is not primarily a method of forming numbers, but of forming classes or collections. If we add B to A, we do not obtain the number 2, but we obtain A and B, which is a collection of two terms, or a couple. And a couple is defined as follows: u is a couple if u has terms, and if, if x be a term of u, there is a term different from x, but if x, y be different terms of u, and z differs from x and from y, then every class to which z belongs differs from u. In this definition, only diversity occurs, together with the notion of a class having terms. It might no doubt be objected that we have to take just two terms x, y in the above definition: but as a matter of fact any finite number can be defined by induction without introducing more than one term. For, if n has been defined, a class u has n+1 terms, if a term x be a term of u the number of terms of u which differ from x is n. And the notion of the arithmetical sum n+1 is obtained from that of the logical sum of a class of n terms and a class of one term. When we say 1+1=2, it is not possible that we should mean 1 and 1, since there is only one 1: if we take 1 as an individual, 1 and 1 is nonsense, while if we take it as a class, the rule of Symbolic Logic applies, according to which 1 and 1 is 1. Thus in the corresponding logical proposition, we have on the left-hand side terms of which 1 can be asserted, and on the right-hand side we have a couple. That is, 1+1=2 means "one term and one term are two terms," or, stating the proposition in terms of variables, "if u has one term and v has one term, and u differs from v, their logical sum has two terms." It is to be observed that on the left-hand side we have a numerical conjunction of propositions, while on the right-hand side we have a proposition concerning a numerical conjunction of terms. But the true premiss, in the above proposition, is not the conjunction of the three propositions, but their logical product. This point, however, has little importance in the present connection.

As you can see, this is important information if you're looking to have a computer prove 1+1=2. It provides a basic definition that is provable in set theory.

As I recall, the actual proof is about 80% of the way through the book. If I find it in the next 5 or 10 minutes, I post it.

 

[Mark44]

This is a good place to close this thread. The OP is no longer a member of this forum.