Abstract Beth definability in institutions (abstract)
- This paper studies definability within the theory of institutions, a
version of abstract model theory that emerged in computing science
studies of software specification and semantics.
We generalise the concept of definability to arbitrary logics,
formalised as institutions, and we develop three general definability
results.
One generalises the classical Beth theorem by relying on the
interpolation properties of the institution.
Another relies on a meta Birkhoff axiomatizability property of the
institution and constitutes a source for many new actual definability
results, including definability in (fragments of) classical model
theory.
The third one gives a set of sufficient conditions for `borrowing'
definability properties from another institution via an `adequate'
encoding between institutions.
- The power of our general definability results is illustrated with
several applications to (many-sorted) classical model theory and
partial algebra, leading for example to definability results for
(quasi-)varieties of models or partial algebras.
Many other applications are expected for the multitude of logical
systems formalised as institutions from computing science and logic.
-
back to Selected Publications