Birkhoff completeness in institutions

DOI10.1007/S11787-008-0035-1MaRDI QIDQ1001374zbMATH OpenOpenAlexFDO

Authors Mihai Codescu, Daniel Găină

Publication date 17 February 2009

Published in Logica Universalis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11787-008-0035-1

zbMATH Keywords

abstract substitutionsBirkhoff completenessHorn sentencesinstitutional model theoryproof theory

Mathematics Subject Classification ID

Abstract deductive systems (03B22) Abstract model theory (03C95) Proof theory in general (including proof-theoretic semantics) (03F03) Categorical logic, topoi (03G30)

Review text

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.

Recommendations

• Birkhoff style calculi for hybrid logics
• An Institutional Version of Gödel’s Completeness Theorem
• Proof Systems for Institutional Logic
• Completeness Theorems for Universal and Implicational Logics of Algebras Via Congruences
• An institution-independent proof of Craig interpolation theorem

Cited in

(13)

• Birkhoff style calculi for hybrid logics
• Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally
• Foundations of logic programming in hybrid logics with user-defined sharing
• Constructor-based institutions
• Abstract Beth definability in institutions
• An Institutional Version of Gödel’s Completeness Theorem
• scientific article; zbMATH DE number 621854 (Why is no real title available?)
• Revisiting the Institutional Approach to Herbrand’s Theorem
• Abstract categorical logic
• Institution morphisms
• Non-deterministic algebraic rewriting as adjunction
• An encoding of partial algebras as total algebras
• Saturated models in institutions

This page was built for publication: Birkhoff completeness in institutions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1001374)