6.1.4 Extensions

      EXTENSION ::= extension SPEC+

An extension is written:

SP₁ then...then SP_n

When the current local environment is empty, SP₁ must determine a complete signature Sigma₁; otherwise, it must determine an extension from the local environment to a complete signature Sigma₁. For i=2,...,n each SP_i must determine an extension from Sigma_i-1 to a complete signature Sigma_i. The signature determined by the entire extension is then Sigma_n.

Similarly, SP₁ determines a class of models M₁ over Sigma₁. For i=2,...,n each SP_i determines the class M_i of those models over Sigma_i whose reducts to Sigma_i-1 are in M_i-1. The class of models determined by the entire extension is then M_n.

An annotation is to be provided for indicating that a series of extensions is conservative, i.e., every model in M_i-1 is the reduct of some model in M_i, for i=2,...,n.