3 ms·

Erm, the linked metamath page asks what's the longest path one can take. Well, geez, it's long. Proving that 2+2=4 from the usual Peano axioms isn't that hard o

by chx 11y ago

Erm, the linked metamath page asks what's the longest path one can take. Well, geez, it's long. Proving that 2+2=4 from the usual Peano axioms isn't that hard or long. We define addition by a+0=a,a+S(b)=S(a+b). Now what we mean by a positive integer number is just a shorthand for that number of successive S(). So 2+2=4 is just S(S(0)) + S(S(0)) = S(S(S(S(0)))). To prove this, let's apply the second part of the addition to S(S(0)) + S(S(0)) we get S(S(S(0)) + S(0)). Let's repeat this "move the S() from the second to the outside" and you will get S(S(S(S(0)) + 0)). Now we can use our first half of definition where +0 can be left out: S(S(S(S(0)))). Now, that wasn't that long, was it?

lokedhs 11y ago
I'm not a mathematician, so please bear with me. I'm trying to understand your definition of addition. Surely that can't be enough? At the very least a+b=0 satisfies your formulas (should I use the word axiom there?). What I'm trying to understand is how I am supposed to think in order to prove/disprove my statement above. Disproving something by contradiction is easy enough, if you can find a contradiction but what if you can't? How can you be sure that you've covered all variations? This is something one struggles with as a developer too. There are cases where you think that a fundamental function does the right thing for all inputs but then you discover an edge case where that isn't true. The number of cases where this has been the case even in high profile libraries suggests that I'm not alone in this.
- gizmo686 11y ago
  What is missing from chx's description is the definition of the natural numbers (and the S (successor) function). The standard definition is: 0 is a natural number S(n) is a natural number, if and only if n is a natural number x=y if and only if S(x)=S(y) for all x, S(x)!=0 These axioms are sufficient to show that the natural numbers form a line. At this point, we can use the definition of addition that chx provided: a+0=a a+S(b)=S(a+b) It is true that, without the restrictions on S, than defining a+b=0 would satisfy these. However, because of the restrictions on S from our definition of the natural numbers, it is impossible for S(a+b)=0.
Natsu 11y ago
In this case, both of the twos are actually complex numbers (2+0i) so they have to construct complex arithmetic from bare axioms.

by chx 11y ago

lokedhs 11y ago

I'm not a mathematician, so please bear with me. I'm trying to understand your definition of addition. Surely that can't be enough? At the very least a+b=0 satisfies your formulas (should I use the word axiom there?). What I'm trying to understand is how I am supposed to think in order to prove/disprove my statement above. Disproving something by contradiction is easy enough, if you can find a contradiction but what if you can't? How can you be sure that you've covered all variations? This is something one struggles with as a developer too. There are cases where you think that a fundamental function does the right thing for all inputs but then you discover an edge case where that isn't true. The number of cases where this has been the case even in high profile libraries suggests that I'm not alone in this.

gizmo686 11y ago
What is missing from chx's description is the definition of the natural numbers (and the S (successor) function). The standard definition is: 0 is a natural number S(n) is a natural number, if and only if n is a natural number x=y if and only if S(x)=S(y) for all x, S(x)!=0 These axioms are sufficient to show that the natural numbers form a line. At this point, we can use the definition of addition that chx provided: a+0=a a+S(b)=S(a+b) It is true that, without the restrictions on S, than defining a+b=0 would satisfy these. However, because of the restrictions on S from our definition of the natural numbers, it is impossible for S(a+b)=0.

Natsu 11y ago

In this case, both of the twos are actually complex numbers (2+0i) so they have to construct complex arithmetic from bare axioms.