Birkhoff completeness in institutions (Q1001374)

This paper belongs to a series of model-theoretic studies at the level of the categorical form of abstract model theory known as `institution theory', that has been introduced by Goguen and Burstall. The Birkhoff form of completeness is developed at the generic level of abstract institutions by a technique originally developed by Borzyszkowski, and which consists of separating the proof rules and the completeness phenomenon on several layers. In this approach, the base layer consists of an institution with a given sound and complete proof system. Since this base layer refers usually to the `atomic' sentences, its completeness is rather easy to establish in each particular case. The other layers are built on top of the base layer successively by considering more complex sentences and consequently adding new proof rules and meta-rules. This layered construction is done fully abstractly and the respective completeness result is proved fully generally relative to the completeness of the predecessor level, thus leading to a multitude of concrete complete proof calculi for various logics, some of them rather unconventional. Many of these complete proof calculi are new, and quite surprising in that they appear rather remote from the original Birkhoff completeness.