Morphism axioms (Q2402279)

A model is an interpretation of the symbols of a theory which satisfies the axioms. This gives rise to the class of models for a theory which can be turned into a category with the associated model morphisms. But here may be some difficulties associated with this straightforward looking approach. Look at topological spaces, which may be specified among others through open sets, another specification comes through closed sets. The corresonding models have morphisms which map open sets to open sets and closed sets to closed sets, and none of these conditions makes sure that the morphisms are continuous. Thus models and their morphisms sometimes behave in a fashion which is not exactly intuitive. The paper under review deals with this observation and related ones by discussing syntactic concepts for specifying and reasoning about model morphisms, introducing concepts that correspond to formulas, axioms, proofs and theorems on the side of models (the counterpart, e.g., for a `formula' is called `mormula', which requires some getting used to). This permits to specify models, of course, but also to specify their morphisms (in the case of topological spaces it is shown that a simple family of maxioms suffices render morphisms continuous maps). One of the main result is that the corresponding calculus is sound, completeness, however, remains an open question. The paper is carefully written and takes the reader with great diligence through the pitfalls which open up on the road from axioms to models to their morphisms. The solutions offered by the author appear intuitively satisfying, and the examples make convincing cases.