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
Sign	—	Signatures	Category
Sen	—	Sentences	Functor
Mod	—	Models	Functor
⊨	U+22A8	Satisfaction	Relation
Σ	U+03A3	Signature	Vocabulary
σ	U+03C3	Morphism	Translation
^op	—	Opposite	Contravariant

Metatheory. Satisfaction condition is key property. Institutions form a 2-category. Model theory generalizes (ultraproducts, compactness). Specification refinement across logics. Liberality: free models. Exactness: logic combinations.

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

Limitations. Highly abstract. Requires category theory. Far from practice. Limited tool support. Learning curve steep. Specification languages complex.