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