LP, the Larch Prover -- Conservative extension
One system is a 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.