What is a Logic?
back to Selected Publications
- 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.