I wonder how can we formalize in logic the fact that we sometimes add additional constants for the sake of readability.
Consider, for example, that in some formal system we prove that if $a,i$ are variables that:
$$\exists !i (\forall a( ai=a)).$$
Then, one says something like "we have shown that there is a unique right identity (or any other funny name) and let us from now on denote it by $1$". I guess what is actually happening is that we construct a new formal system where we redefine things like terms and formulas as necessary to include $1$ and we add new formal symbol $1$. But that means that it is not the same formal system anymore. But we are still interested in the one before adding $1$.
Question 1: Are there some standard procedures or ways to deal with adding constants to formal system in a way that we can reason about the theory which is obtained before adding new constants?
Question 2: Kleene in "Mathematical Logic" states that we can add $1$ in such case to our list of formal symbols and also add a new axiom "$\forall a(a1=a)$". Why would we want to add this axiom? On one hand, this gives some rules about constant $1$ without which we do not know how to apply it in our reasoning. On the other hand, we are adding a new axiom - how do we know it doesn't lead to a contradiction? For example, how do we know that we do not get more results from it than if we had only original axioms?
Ideally, I would want some procedure of adding constants in a way that new formal theory has some way of translating all of the sentences of new constants in terms of old formal theory, and that it does not introduce any new results - it can prove only those theorems that could be proven without adding those constants.
I hope my question is clear and if not please let me know and I will try to improve it, thanks!
Okay, let's consider the case of $1,$ added to some reasonable arithmetic system via the axiom that it is the multiplicative identity $$ \forall y(y\cdot1=y)$$ and we'll assume the system is strong enough to prove the sentence $$ \exists x \forall y(y\cdot x=y)\land \forall x \forall z(\forall y(y\cdot x = y)\land\forall y(y\cdot z=y)\to x=z)$$ that $1$ exists and is uniquely defined by this axiom.
Now let's write a true statement about $1$ (more-or less chosen randomly): $$ \forall x \exists y(y=x+1).$$ We can write an equivalent statement in the language without $1$ as follows: $$ \exists z (\forall w(w\cdot z=w) \land \forall x\exists y(y=x+z)).$$ To prove the abbreviated statement implies this, take the conjunction of it and the axiom and use existential generalization. To prove this implies the abbreviated statement, instantiate $z$, then use the left conjunct and the uniqueness statement to prove $z=1,$ then substitute $1$ in for $z$ in the right conjunct.
This is quite general. If we have a defining formula $\phi(x)$ where we can prove $\exists! x\phi(x)$ and we extend the language with the constant $c$ and the theory with the axiom $\phi(c),$ then we can translate any sentence $\psi(c)$ in the extended language back into the initial language as $$ \exists x(\phi(x)\land\psi(x)).$$ Similar things can be said about defined functions. Defined relations are easier since you can literally just replace an instance like $R(x,y)$ with its defining formula $\phi_R(x,y).$
This process is called definitional extension, and hopefully this makes it clearer than these extensions are always conservative.