Institutions

Origin. Goguen and Burstall introduced institutions (1984, 1992). Category-theoretic framework for abstract model theory. Formalizes "what is a logic?" Signature, sentences, models, satisfaction. Foundation for heterogeneous specification.

Models. Abstract notion of logical system. Institution = signature category + sentences + models + satisfaction. Signature morphisms translate between vocabularies. Satisfaction invariant under translation. Unifies diverse logics abstractly.

Formalism.

Institution: I = (Sign, Sen, Mod, ⊨) where:

Sign: category of signatures
Sen: Sign → Set (sentences functor)
Mod: Sign^op → Cat (models functor)
⊨_Σ ⊆ |Mod(Σ)| × Sen(Σ) (satisfaction)

Satisfaction condition: For σ: Σ → Σ' signature morphism: M' ⊨_Σ' Sen(σ)(φ) iff Mod(σ)(M') ⊨_Σ φ

"Translation of sentence satisfied in translated model iff original sentence satisfied in reduct."

Examples:

FOL: signatures = (sorts, operations, predicates)
Equational logic: signatures = algebraic signatures
Modal logic: signatures + modalities
Temporal logic: signatures + temporal operators

Institution morphisms: Maps between institutions preserving structure. Encode one logic in another.

Heterogeneous specifications: Combine different logics via institution morphisms. CASL: Common Algebraic Specification Language.

Symbols.

Symbol	Unicode	Name	Meaning
×	U+00D7	Multiplication sign	Cartesian product forming the satisfaction relation
Σ	U+03A3	Sigma	A signature: an object of the category Sign
σ	U+03C3	Sigma, small	A signature morphism: a change of notation
φ	U+03C6	Phi	A sentence, an element of Sen(Σ)
→	U+2192	Rightwards arrow	A functor, or a morphism of signatures
⊆	U+2286	Subset of or equal to	Satisfaction as a subset of models × sentences
⊨	U+22A8	Satisfaction	⊨_Σ, the satisfaction relation at the signature Σ
I	—	Institution	The quadruple (Sign, Sen, Mod, ⊨)
Sign	—	Category of signatures	Objects are vocabularies, arrows are translations
Sen	—	Sentence functor	Sign → Set, covariant: translates sentences forward
Mod	—	Model functor	Sign^op → Cat, contravariant: takes reducts
^op	—	Opposite category	The contravariance of Mod
Set, Cat	—	Target categories	Sets, and categories, respectively
M	—	Model	An object of Mod(Σ)
Mod(σ)	—	Reduct functor	Forgets whatever σ did not name
comorphism	—	Institution comorphism	An encoding of one institution inside another
liberal	—	Liberality	Every reduct functor has a left adjoint: free models exist
semi-exact	—	Semi-exactness	Mod turns signature pushouts into model pullbacks
CASL	—	Common Algebraic Specification Language	A specification language defined over an institution
Hets	—	Heterogeneous Tool Set	Implements a graph of institutions and comorphisms

Metatheory. The satisfaction condition — that truth is invariant under change of notation — is the whole axiom, and a surprising amount of model theory follows from it alone. Diaconescu's Institution-independent Model Theory (2008) develops ultraproducts and Łoś's theorem, elementary diagrams, Craig interpolation, Beth definability, Robinson consistency, and Birkhoff-style axiomatizability at this level, so those results become theorems about the abstract structure rather than about first-order logic. Two derived conditions do the structural work. An institution is semi-exact when Mod carries pushouts of signatures to pullbacks of model categories; that is model amalgamation, and it is what makes structured specification and the institution-independent interpolation results go through. It is liberal when every reduct functor has a left adjoint, so free models exist — equational logic is liberal, first-order logic is not. Goguen and Roşu (2002) codified the distinction between institution morphisms and comorphisms, projection against encoding, and Diaconescu's Grothendieck construction (2002) flattens a diagram of institutions linked by comorphisms into a single institution, which is what heterogeneous specification and the Hets tool are built on.

Applies to. Formal specification (CASL, CafeOBJ). Software engineering. Combining logics. Database theory. Ontology integration. Heterogeneous systems.

Limitations. An institution says what sentences and models there are for each signature and nothing about what sentences are made of: Sen(Σ) is a bare set, so there is no induction on formula structure and no account of connectives, quantifiers, or compositionality at this level. Parchments were introduced to generate institutions from syntax precisely because the definition does not supply it. Proof is absent as well — satisfaction is primitive, entailment is derived from it, and a proof calculus must be added, as in Meseguer's general logics. Nor does the framework deliver metatheorems by itself: compactness, completeness, interpolation, and definability are hypotheses on a given institution rather than consequences of the axiom, and the institution-independent proofs of them carry substantial side conditions such as semi-exactness. The satisfaction condition itself excludes any logic whose truth is not preserved under translation.