Apoth3osis

Mathematical Engineering · Institution Theory

The institution system — and how the Atlas uses it

The Visual Atlas is governed by Grothendieck institution theory (Goguen–Burstall; Diaconescu). An institution is a model-theory-independent notion of “a logic”; the Grothendieck construction flattens many logics into one. This page explains the framework and shows exactly how our system instantiates it — with the proofs that back each claim living in HeytingLean.Institution.

← Back to the Visual Atlas

What an institution is

An institution is a tuple (Sig, Sen, Mod, ⊨): Sig a category of signatures (vocabularies) and signature morphisms; Sen : Sig → Set a functor giving sentences (translated forward along morphisms); Mod : Sig → Cat^op a contravariant functor giving models (reduced backward along morphisms); and for each signature a satisfaction relation between models and sentences. The single defining axiom is the satisfaction condition — truth is invariant under change of notation:

Mod(σ)(M′) ⊨Σ ρ  ⟺  M′ ⊨Σ′ Sen(σ)(ρ)

This condition is the proof obligation behind every relationship the Atlas draws. A relationship that type-checks without discharging it is vacuous — which is why each Atlas edge is held to a satisfaction-condition proof, not a label.

The relationship taxonomy (Logic by Translation)

Institution morphism

μ : I′ → I, a projection (complex → simpler): a functor on signatures, a sentence map, and a model reduct, natural, with the translation condition. E.g. first-order → propositional.

Institution comorphism

ρ : I → I′, an encoding (simpler → complex): the direction the Atlas spine arrows take. E.g. propositional → first-order; Kolmogorov classical → intuitionistic.

Conservative comorphism

A comorphism whose model reduct is surjective: every model lifts. This is the borrowing criterion — prove a hard fact in a tool-rich logic and reflect it back (Cerioli–Meseguer, “May I borrow your logic?”).

Equivalence of institutions

A comorphism that is a categorical equivalence at every level. The identity of a logic = an equivalence class of institutions under this relation (Mossakowski–Goguen–Diaconescu–Tarlecki, “What is a logic?”).

The Grothendieck institution

Given a diagram of institutions linked by comorphisms (a heterogeneous environment), the Grothendieck construction (Diaconescu 2002; Mossakowski 2002) flattens it into a single institution that retains all the data. A signature is a pair (i, Σ) — a diagram node plus a signature there; a signature morphism is a pair (u, φ) of a diagram edge and a signature morphism. Sentences, models, and satisfaction are inherited fibrewise. This is the backbone of heterogeneous specification (Hets, CafeOBJ, the OMG OntoIOp standard): “classify X against Y” becomes “find the morphism (u, φ) in the flattened institution.”

Heterogeneous specification

Many logics, one framework — without forcing them into a single syntax.

Borrowing / proof transport

A conservative comorphism transports a theorem from a tool-rich logic back to the logic of interest.

One identity for a logic

An equivalence class under equivalence of institutions.

How our system instantiates it

The Atlas is not described by institution theory loosely — it is a Grothendieck institution, and the structural claims are proven in Lean and checked in CI.

The nine registers = one institution

proven in main

Each step’s registers (Logic, Geometry, Matrix, Dynamics, Computation, Topos/Lawvere, Polynomial, Polygraphic) are pairwise institution equivalent, via a satisfaction-preserving bijection — and the equivalence is operator-preserving on the re-entry involution (“one operator, many faces”), not a bare relabel.

HeytingLean.Institution.atlas_registers_pairwise_equivalent
HeytingLean.Institution.atlas_registers_share_reentry

The spine 1→8 = forcing comorphisms

proven in main

Each level forces the next. Because the levels have genuinely different carriers, these are directed encodings (forcings), not equalities — the eight node theorems are bundled into one certificate.

HeytingLean.Ontology.GenerativeTopos.theForcingSpine

The reusable machinery

Institution.Basic (the Core spine, satisfaction condition as a field), HetComorphism / Equivalence (refl/symm/trans), and AtlasDistinction.ofPresentationIso — the lego block that turns any “same object, different presentation” edge into a proof.

The whole grid, flattened

The 8 × 9 grid of objects-in-registers, plus the spine comorphisms, flattened by the Grothendieck construction, is a single institution — the floor the Atlas descends to.

Key sources

  • Goguen & Burstall, “Institutions: Abstract model theory for specification and programming”, JACM 39(1) 1992.
  • Diaconescu, “Grothendieck institutions”, Applied Categorical Structures 10(4) 2002.
  • Mossakowski, “Comorphism-based Grothendieck logics”, MFCS 2002.
  • Mossakowski, Goguen, Diaconescu, Tarlecki, “What is a logic?”, Logica Universalis 2005.
  • Cerioli & Meseguer, “May I borrow your logic?”, TCS 173 1997.
  • Diaconescu, Institution-independent Model Theory, Birkhäuser 2008.