4 ms·

> isnt 1+1=2 true in the same way that 0=0 is true, namely by definition? In the "traditional" formalism, it matters exactly what you mean by "+1" :-). People

> isnt 1+1=2 true in the same way that 0=0 is true, namely by definition? In the "traditional" formalism, it matters exactly what you mean by "+1" :-). People normally define a binary addition relation (two operands -> sum) using a "more fundamental" unary successor relation (one operand -> successor). Zero is just a constant, and numbers are defined in terms of it and the successor relation: one is "S(0)", two is "S(S(0))" and so on. So if the "+1" in your post is an invocation of the successor function, it certainly is axiomatic (from the axioms of equality): S(S(0)) = S(S(0)) On the other hand, if we're using actual addition, it might take another step or two, using axioms of addition, like: X + 0 = X, and S(X + Y) = X + S(Y) So the proof might go something like S(S(0)) = S(S(0)), by axioms of equality, S(S(0)) = S(S(0) + 0), by the first axiom above, then S(S(0)) = S(0) + S(0), by the second axiom above. And I guess I got lucky that the second axiom was not written S(X + Y) = S(X) + Y or I'd have been stuck for a day trying to prove that addition is commutative :-).

mike741 8y ago
That makes sense, thank you. However, at what point is the symbol "2" introduced in such a scheme? Is it before addition, or after? At some point it is given a definition, like S(S(0)) where S(0)=1 and S(X)=X+1, at which point isnt it easy to substitute 2 = S(S(0))= S(0)+1 = 1+1 is this simple equivalence really not provable with sufficient axioms? Obviously from the downvotes I am missing something fundamental, I would very much like to know what that is but am at a loss. Perhaps I am just missing mrleiter's original point.
- repsilat 8y ago
  Normally it's defined exactly as S(S(0)) like you said, so the above should constitute a proof that 1+1=2. Anyone disputing that sort of proof normally needs to take issue with one or more of, - The axioms, - The rules of inference. So someone might say, "In step one, you used an axiom of the form X=X. What basis do you have for assuming it's true?" It's worth looking up the Munchausen trilemma for a little more on that sort of thing, but I'm not sure how many people would seriously argue against the validity of that proof (or one just like it if I've made a mistake :-) As for why you've been downvoted, I have no idea. I think your question was perfectly fine, asked politely enough, and there are no doubt many perfectly reasonable logical systems in which 1+1=2 is trivially true (and not just "a short proof away.")

mike741 8y ago

That makes sense, thank you. However, at what point is the symbol "2" introduced in such a scheme? Is it before addition, or after? At some point it is given a definition, like S(S(0)) where S(0)=1 and S(X)=X+1, at which point isnt it easy to substitute 2 = S(S(0))= S(0)+1 = 1+1 is this simple equivalence really not provable with sufficient axioms? Obviously from the downvotes I am missing something fundamental, I would very much like to know what that is but am at a loss. Perhaps I am just missing mrleiter's original point.

repsilat 8y ago
Normally it's defined exactly as S(S(0)) like you said, so the above should constitute a proof that 1+1=2. Anyone disputing that sort of proof normally needs to take issue with one or more of, - The axioms, - The rules of inference. So someone might say, "In step one, you used an axiom of the form X=X. What basis do you have for assuming it's true?" It's worth looking up the Munchausen trilemma for a little more on that sort of thing, but I'm not sure how many people would seriously argue against the validity of that proof (or one just like it if I've made a mistake :-) As for why you've been downvoted, I have no idea. I think your question was perfectly fine, asked politely enough, and there are no doubt many perfectly reasonable logical systems in which 1+1=2 is trivially true (and not just "a short proof away.")