The higher-order logic community extensively uses syntactical schemes for extensions that guarantee conservativeness of the extension, see [GM93]. Of course, since conservativeness is undecidable, one cannot expect to be able to recognize all conservativeness syntactically. But by restricting oneself to the syntactical schemes, one can be sure that the extension is conservative - the corresponding proof obligation can be automatically discharged by an appropriate tool in this case. Similarly, there are syntactical schemes for definitional extensions (c.f also the informal guidelines for definitional extensions in [RM99]).