UNION ::= union SPEC+
A union is written:
SP1 and...and SPn
When the current local environment is empty, each SPi must determine a complete signature Sigmai. The signature of the union is obtained by the ordinary union of the Sigmai (not their disjoint union). Thus all (non-localized) occurrences of a symbol in the SPi are interpreted uniformly (rather than being regarded as homonyms for potentially different entities).
The models are those models of the union signature for which the reduct along the signature inclusion morphism from SPi is a model of SPi, for each i=1,...,n.
When the current local environment is non-empty, each SPi must determine an extension from it to a complete signature Sigmai; then the resulting signature is determined as above. Similarly, models of the local environment are extended to models of the SPi; then the resulting models are determined as above. This provides the required partial functions from signatures to signatures, and from model classes to model classes.