Conservative Extension

An extension T' of a theory T is conservative if T' proves no new sentences in the language of T beyond those provable in T itself; equivalently, every sentence in the original language provable in the extension was already provable in the base theory.