Publikation

What is a Logic? (revised version)

Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki

In: Jean-Yves Béziau (Hrsg.). Logica Universalis. Seiten 111-133 second edition Birkhäuser 2007.

Abstrakt

This paper builds on the theory of institutions, a version of abstract model theory that emerged in computer science studies of software specification and semantics. To handle proof theory, our institutions use an extension of traditional categorical logic with sets of sentences as objects instead of single sentences, and with morphisms representing proofs as usual. A natural equivalence relation on institutions is defined such that its equivalence classes are logics. Several invariants are defined for this equivalence, including a Lindenbaum algebra construction, its generalization to a Lindenbaum category construction that includes proofs, and model cardinality spectra; these are used in some examples to show logics inequivalent. Generalizations of familiar results from first order to arbitrary logics are also discussed, including Craig interpolation and Beth definability.

Weitere Links

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence