2 What are the consequences for CASL?

The question arises which definition of conservative extension should be chosen to allow for optimal tool support. Initially I thought that the proof theoretical definition would allow for more proof support and thus would be more suitable than the model-based definition. While writing this note, my opinion has changed in favour to the model-theoretic definition. But it's like curing one evil with an even worse evil. In the following I have listed some pro's and cons'es of mt-conservative extension:

+

The definition of mt-conservative extensions is independent of the underlying logic. This seems to me an important point as translations of CASL aim at different logics.

-

There is no uniform way (to be honest, I don't know of any) to prove the property of being a mt-conservative extension in a logical (proof theoretical) way. In general it is impossible to characterize a single infinite model (like natural numbers) inside any logic usable for automated theorem proving.

+/-

Switching to pt-conservative extensions would not be of any practical help as the definition postulates a property of all (usually infinitely many) sentences of a theory. As illustrated in the footnote, we cannot rephrase this property to a simple property of the given axioms.

+

There are subclasses of extensions for which we know how to prove that they are mt-conservative. Examples for this are constructive specifications. We can, for instance, provide definition principles how to define new functions based on given datatypes (like algorithms in INKA or the definition principle in NQTHM). In these cases the problem of being a mt-extension can be reduced to proving a first-order theorem (with induction).

Summing up, I have no clue how to tackle either notion of conservative extension in a CASL-verification tool. Is there a way to use Ehrenfeucht-Fraisse games for such purposes? From a more general point of view, the notion of mt-conservative extension captures the underlying idea more closer than the proof theoretical version and does not implicitely incorporate the weakness of logics into such a definition. Also, there are some special cases in which we can support the notion of mt-conservative extension, e.g. when using "algorithms" or special definition principles to extend a given theory.