> How can you prove that 1+1 is really 2?

Worse, we're often tripped up figuring out if 1 + 1 is the correct expression in the first place. A lot of science and technology is bottlenecked on getting accurate and useful inputs.

I did not know about that aspect of the problem. What do you mean, that "we're often tripped up figuring out if 1 + 1 is the correct expression in the first place"? That we might be using the wrong paradigm for mathematic formulations?

In real life, there are problems like classification and precision that cause problems in making broader conclusions. If you are measuring poverty rates, for instance, you could be basing your decisions on several different benchmarks. The statistics, math, machine learning, etc., are all downstream from what we're even measuring and counting in the first place.

In a more elementary formulation, we could say one bag of rice plus one bag of rice is two bags of rice. But one bag of rice is underfilled and the other is contaminated with pests. So you don't really have two bags of rice after all. So maybe 8/10 + 0 is the correct expression in that case.

isnt 1+1=2 true in the same way that 0=0 is true, namely by definition? its proven analytically, 2 is defined as 1 greater than 1, 1 less than 3, 1/2 of 4, etc, all of which derive from 0=0, which is a tautology. I really don't understand the difficulty in proving something that is true by definition, it's like saying "prove all white swans are white." To me, it seems a harder thing to prove would be something empirical such as "prove the moon and stars exist during the daytime"

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

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.

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

This idea "... all of which derive from 0=0" is kind of interesting. I've got a fuzzy recollection of a terrific book about the number zero ("History of a Dangerous Idea", IIRC), and thought that historically, a surprising amount of math was developed prior to 0 being recognized as a number per se.

Anything you can prove is tautological, by definition.

Empirical statements cannot be proved; the best you can do is provide evidence for belief.

Right. So is 1+1=2 not a tautology then? Mrlieter seemed to be implying it could not be proven.

Bertrand Russell proved it via set theory [1]. Which is again based on the axioms of set theory, so as repsilat said above, you end up in one of the Münchhausen trilemmae, in this case you end up in some mix of regressive and axiomatic argument: there's an axiom, you cannot prove it within itself, but with another axiom and so forth.

It's a difficult subject and I am by no means an expert in it.

[1] https://blog.plover.com/math/PM.html

PS: You are correct, 1+1=2 is not a tautology. With a tautology, both the statement and the negation of the statement are true. In this case either 1+1=2 or 1+1=!2 - but never both, if you get what I mean?

PPS: And sorry for all those downvotes - don't understand why. Your questions are perfectly fine.