Hello,
1+1-2
Is this an axiom or a proof?
Neither. An axiom is in particular a proposition, i.e., something that is either true or false. Here, 1 + 1 - 2 is neither true nor false. Further, a proof is an expression that usually combines propositions according to specified inference rules. Therefore, this is not a proof, either.
Yes; see this post.
Whether 1 + 1 = 2 is considered an axioms or a theorem varies between formal systems. E.g., in Peano Arithmetic, it is a theorem and in the Calculus of Inductive Constructions it is an (instance of a universal) axiom.
Just to be sure to understand. $\displaystyle 2$ is syntaxic sugar for $\displaystyle SS0$ (with $\displaystyle S$ the symbol of the successor function).
So you say it's a theorem (result of a proof) and not an axiom because we have to invoque sequently :
(1) Axiom $\displaystyle \forall v_0\forall v_1 v_0+Sv_1 = S(v_0+v_1)$ on $\displaystyle S0$ and $\displaystyle 0$ :
$\displaystyle S0+S0 = S(S0+0)$
(2) Axiom $\displaystyle \forall v_0 v_0+0 = v_0$ on $\displaystyle S0$ :
$\displaystyle S0+S0 = SS0$
?
To further this point, any sentence s can be put into a formal system as an axiom. Therefore, the question is what system are we talking about and is the axiom redundant? By the latter question I mean can we take a formal system S and exclude the axiom s in it and still derive s. Then there was no need for s to be an axiom of S. As emakarov pointed out, in Peano Arithmetic, it would make no sense to have an axiom or axiom schema for "1 + 1 = 2," but in another system it can very well be an (instance of an) axiom. Of course, when we say something like Peano Arithmetic, it is so defined as to have certain axioms. If we had an axiom or schema for "1 + 1 = 2", it wouldn't actually be Peano Arithmetic anymore. It would be "PA + s".