Decompositions of Stratified Institutions

TL;DR

This paper advances the theory of stratified institutions by introducing a projection-based representation technique, enabling general results on model amalgamation and existence diagrams applicable to various state-based model theories.

Contribution

It presents a novel projection technique for stratified institutions, facilitating broader applicability and new model theory developments.

Findings

Developed a projection-based representation method.

Established general results on model amalgamation.

Analyzed existence diagrams for stratified institutions.

Abstract

The theory of stratified institutions is a general axiomatic approach to model theories where the satisfaction is parameterised by states of the models. In this paper we further develop this theory by introducing a new technique for representing stratified institutions which is based on projecting to such simpler structures. On the one hand this can be used for developing general results applicable to a wide variety of already existing model theories with states, such as those based on some form of Kripke semantics. On the other hand this may serve as a template for defining new such model theories. In this paper we emphasise on the former application of this technique by developing general results on model amalgamation and on existence diagrams for stratified institutions. These are two most useful properties to have in institution theoretic model theory.