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