# Thread: 1+1=2, Axiom or Proof

1. ## 1+1=2, Axiom or Proof

Hello,

1+1-2

Is this an axiom or a proof?

2. ## Re: 1+1=2, Axiom or 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.

3. ## Re: 1+1=2, Axiom or Proof

Originally Posted by emakarov
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.
May be I am wrong. Did Russell proved 1+1=2 in Principia Mathematica?

4. ## Re: 1+1=2, Axiom or Proof

What does 1+1=2 have to do with 1+1-2 from the original post?

5. ## Re: 1+1=2, Axiom or Proof

Originally Posted by shounakbhatta
Did Russell proved 1+1=2 in Principia Mathematica?
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.

6. ## Re: 1+1=2, Axiom or Proof

Originally Posted by emakarov
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.
Thank you.

7. ## Re: 1+1=2, Axiom or Proof

Originally Posted by emakarov
E.g., in Peano Arithmetic, it is a theorem [...]
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$
?

8. ## Re: 1+1=2, Axiom or Proof

Yes, plus the axioms of equality that would allow replacing S0 + 0 with S0 under S and would justify SS0 = SS0.

9. ## Re: 1+1=2, Axiom or Proof

Thanks

(Yes of course for the equality axioms, but as the equality is always on the language [at least in the class I followed] and that the axioms do not depend of the language, I consider them implicitly.)

10. ## Re: 1+1=2, Axiom or Proof

Originally Posted by emakarov
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.
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".

11. ## Re: 1+1=2, Axiom or Proof

Originally Posted by bryangoodrich
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".
Thank you very much. This seems to be clearing my concepts more clearly.