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.