"Meta-Theory a la Carte" (MTC) uses a model of language extension where modules build on a shared set of declarations of syntax categories and relations, declaring new syntax constructors and rules defining the relations. This model is also used by other works, such as "Proof Weaving".
The set of shared declarations MTC uses is sort of a degenerate host language, so we model it as such. The shared declarations form a module introducing the syntax categories and relations, but not rules for them. Each other module adds new syntax constructors and rules to the language.
The drawback of this approach compared to the one Sterling takes is that new relations cannot be added by extensions. Anything not introduced by the host language is not allowed in the language, so extensions are only able to add new syntax and extend the existing semantics to the new syntax.
z or s(N) for
some N