Birkhoff completeness in institutions (Q1001374): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 02:52, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Birkhoff completeness in institutions |
scientific article |
Statements
Birkhoff completeness in institutions (English)
0 references
17 February 2009
0 references
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.
0 references
proof theory
0 references
institutional model theory
0 references
Horn sentences
0 references
Birkhoff completeness
0 references
abstract substitutions
0 references