conservative extensions in higher-order logic

Hi,

the definition of "conservative extension" in higher-order logic, as found in

Michael J. C. Gordon and Tom F. Melham,
Introduction to HOL
Cambridge University Press, 1993

requires that a new constant c should be defined by an equation
c=t, where t should be a CLOSED term, i.e., it should not contain any free variables.

While this seems rather intuitive, I am wondering: why exactly is this restriction necessary? What would go wrong if we allowed free variables in t?

Thanks for any help,

Jan
.

Quantcast