Conservative extension is frequently used in formal specifications for stepwise refinement and implementation of abstract datatypes. Basically we like to extend a given specification by new function or predicate definitions but without changing the intended meaning of the original parts of the specifications. E.g. we like to extend the definition of natural numbers by a recursive definition of addition but without changing the "meaning" of the specificaton of natural numbers.
A theory T' is an extension of a theory T (denoted T c T') if T' can be obtained from T by adding additional symbols and axioms.
There are two ways to define conservative extensions formally, either in terms of the theories (proof theoretical, pt) or in terms of their models (model theoretical, mt):
T c T' is a mt-conservative extension iff every model of T can be expanded to a model of T'.
T c T' is a pt-conservative extension iff the restriction of T' to sentences of the language of T consists only of consequences of T. 2
It is well-known that mt-conservativeness implies pt-conservativeness but not vice versa [BP90]. The following example from [Veloso92] illustrates the differences:
Consider a specification of natural numbers with constructors 0 and s and a binary relation < in the following (first order) way:
This theory is complete and maximally consistent; i.e. for every closed formula Phi in the given language either Phi or ¬Phi holds. This might be surprising knowing Goedels results about arithmetic, but the reason is that the given language (using only s, 0 and < ) is so poor that you cannot specify any "interesting" property. Obviously, the axiomatization does not characterize natural numbers up to isomorphism. Non-standard models are the natural numbers plus additional copies of the integers. Especially the natural numbers plus one copy of the integers is a model of the presented theory.
forall y : y = 0 \/ exist x : y = s(x) forall x,y : x < s(y) -> (x < y \/ x = y) forall x : ¬x < 0 forall x,y : (x < y \/ x = y \/ y < x) forall x,y : x < y -> ¬y < x forall x,y,z : (x < y /\ y < z) -> x < z
Figure 1: Various models of the given specification
We now extend this theory T to T' by a recursive definition of +.
The first two axioms coincide with the standard recursive definition of +. If our specification of natural numbers would contain an induction axiom then the third axiom would be derivable from all the others. But in this case it is not.
0 + y = y s(x) + y = s(x + y) s(x) + y > y
Since T is maximally consistent, T' is a pt-conservative extension iff it is consistent, i.e. there is a model of T'. Obviously, the natural numbers is a model of T' and thus, T' is a pt-conservative extension of T.
From a model-theoretical view T' is no mt-conservative extension because we cannot extent the model of T consisting of natural numbers plus one copy of integers to T' (cf. [Enderton72]). In [Veloso92] you can find a refutation proof of this showing that in this model any attempt to interpret + will result in a contradiction.
The reason for this phenomenon is related to the weakness of logics. The language of T is too poor to formulate a property which allows us to distinguish, for instance, between the standard model "natural numbers" and the non-standard model mentioned above. All properties which can be formulated in the languange of T, behave in both models in the same way. The situation changes once we add a recursively defined function like + to the theory, then we have means to distinguish between some of the non-standard models. In practice we fail to rule out all non-standard models:
It is well-known that for many inductively defined structures like for instance natural numbers there is no categorial first-order theory. In case of natural numbers for instance, each first-order axiomatisation has also so-called non-standard models like those mentioned above. Changing to higher-order logics we have to adapt the semantics to obtain a calculus suitable for machines. This ends up in the use of Henkin-semantics which allow for complete calculi. But using Henkin-semantics we also fail to characterize natural numbers up to isomorphism (or more general, to characterize some notion of initiality (cf. [Andrews86] pp. 199)). Roughly speaking, the price for being complete is some kind of blurring the interpretation of given axiomizations.
