>>10570952It not an assumption, its a result of set theory. Although if it were an assumption, it indeed wouldnt be provable.
>>10570922Generally people assume conventional axioms and definitions, provided they exist, and x+y=x+y is certainly not a standard axiom of integer arithmetic. Of course it could be - although its not really necessary. Perhaps you're thinking of the communtativity of addition, which states that x+y=y+x? In that case it could be a proof, but usually we'd be looking for something a more so implicit in the definition and axioms. Basically, you take the definition and axioms for additive identity, the definition and axioms for addition operator, and a set of constant terms (numerals) that denote ordinal positions of numbers in the integer sequence, and from that you can prove that by the definition and axioms of the + operator (which is a function taking two arguments) and the values of the constants 1, 2 you can prove that 1+1=2 without assumimg by definition that the formulae "1+1" and "2" mean the same thing in your model.
