Proper extension

In mathematical logic, a conservative extension is a supertheory of a theory which is often convenient for proving theorems, but proves no new theorems about the language of the original theory.

More formally stated, a theory ${\displaystyle T_{2}}$ is a (proof theoretic) conservative extension of a theory ${\displaystyle T_{1}}$ if the language of ${\displaystyle T_{2}}$ extends the language of ${\displaystyle T_{1}}$; that is, every theorem of ${\displaystyle T_{1}}$ is a theorem of ${\displaystyle T_{2}}$, and any theorem of ${\displaystyle T_{2}}$ in the language of ${\displaystyle T_{1}}$ is already a theorem of ${\displaystyle T_{1}}$.

...
Wikipedia