nucleation

LIT-1661: Institutions: abstract model theory for specification and programming

2 min read

Properties5
StatusActive — read in full 2026-10-29 (NOTE-1348) from a copy of the published article supplied by the owner; worth reading as the source of the Satisfaction Condition, the one axiom that makes truth invariant under change of notation, and of what follows from it for every logic at once: theories glue wherever signatures do (Theorem 11), constraints for abstract data types glue too, and a translation between logics that meets the condition and reaches every model lets one logic's prover decide another's entailments (Proposition 35). For this record it gives a precise standard of correct translation, relative to a translation of models, distinct from structural resemblance and from route agreement. Proofs are omitted for the Satisfaction Condition of its own examples; natural language is named as an application and not developed. Source of THEORY-1150 and THEORY-1142.
Version3
Tagslogic, mathematics
Cited as “paper” byNOTE-1348 — Goguen & Burstall — Institutions
Cited as “source” byTHEORY-1142 — A translation between two logics presented as institutions is correct, in the Satisfaction Condition's sense, when a translated sentence holds in a model exactly when the original holds in the model's translation; given the model translation this fixes the sentence translation up to semantic equivalence, and when every model of the target is reached it preserves and reflects entailment, so one logic's prover can decide the other's; but the condition alone admits collapsing translations and is relative to a model translation it does not supply, THEORY-1150 — In any logical system presented as an institution, theories can be glued wherever their vocabularies can: if the category of signatures has colimits, so does the category of theories, the glued theory being the semantic closure of the union of the parts' translated sentences; and because constraints requiring free or initial interpretation also obey the Satisfaction Condition, theories carrying them glue the same way

Graph View

Goguen, J. A., & Burstall, R. M. (1992). Institutions: Abstract model theory for specification and programming. Journal of the ACM, 39(1), 95–146. doi:10.1145/147508.147524.

Read in full in NOTE-1348, from a copy of the published article supplied by the owner.

Why this is here

A9 §7 offered it as the formal frame for the owner’s specification–realization analogy, and for comparing record migrations when the specification language itself changes: renaming, conservative refinement, splitting or promoting a type, changing governing rules. A9’s correction stands with it: theory and realization “can be mathematically related without either being ontologically prior”, and satisfaction is not production. It bears on CLAIM-477 and CLAIM-476.

The paper bears out A9’s correction: a specification denotes a class of models that “Programmers construct” (p. 98), and closed theories and closed model classes determine each other without either being defined from the other (Proposition 3). It narrows the frame in two ways. Both sentences and models are indexed by signatures, so the symmetry holds over a fixed notation, not between notation and what it describes. And of the migrations A9 listed, renaming and enrichment are signature morphisms, while splitting a type is not a morphism from the old signature to the new one, and changing the governing rules changes the institution (NOTE-1348). It also bears on CLAIM-469, CLAIM-470, QUESTION-130 and CLAIM-496.

Key takeaways

  • The Satisfaction Condition, m′ ⊨ φe iff φm′ ⊨ e, is the whole axiom; sentences move with a change of notation and models move against it.
  • If signatures can be glued by colimits, so can theories (Theorem 11), including theories with data constraints (Theorem 24).
  • A translation between logics is correct when it meets the same condition with a model translation; given that model translation it is fixed up to equivalence, and with every model reached it preserves and reflects entailment (Propositions 33 and 35).
  • The condition alone admits a translation that collapses everything to one model; it is relative to a model translation it does not supply, and it covers truth conditions only.

Backlinks