\doc{Conservative extension}
\ref{conservative-extension}

One system is a \def{conservative extension} of another if any consequence of
that system is also a consequence of the other or contains a function symbol
that does not occur in the other.  Thus, conservative extensions can be used to
define properties of new symbols, but do not introduce inconsistencies or
additional properties of existing symbols.