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 :-). 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.
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.")
Empirical statements cannot be proved; the best you can do is provide evidence for belief.
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.