Birkhoff completeness in institutions (Q1001374): Difference between revisions
From MaRDI portal
Created a new Item |
Set OpenAlex properties. |
||
(2 intermediate revisions by 2 users not shown) | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/s11787-008-0035-1 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2078682546 / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 21:55, 19 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