Part III — Making Reasoning Checkable

Institutions, Part III — Witnesses, the Missing Substrate, and Eigenius

30 July 2026 · Eigenius · Part III of III in Institutions

The final part of a three-part introduction to the theory of institutions. Part I disassembled a single logic; Part II connected logics by morphisms and comorphisms and used them to borrow theorem provers. Here we make the whole edifice checkable*: by moving institutions inside a constructive proof assistant, satisfaction stops being a bare yes-or-no and starts carrying evidence a machine can inspect. That upgrade, this part argues, is the missing foundation for reproducible, AI-assisted science — and it is what the Eigenius project is building.*

Recap: where Parts I and II leave us

An institution is a logic reduced to four moving parts — signatures, sentences, models, satisfaction — obeying one law, that truth is invariant under change of notation (Part I). Logics connect by morphisms (forgetful projections) and comorphisms (encodings), and those connections let one logic borrow another’s theorem prover, or let many logics share a single joint semantics as a graph of logics (Part II). One phrase from Part II carried an assumption we deferred: borrowing lets you trust the verdict of a foreign prover. This part is about no longer having to.

10. The constructive turn

Everything so far has treated satisfaction as a yes-or-no affair: a model either satisfies a sentence or it does not. Now the pivot. The proof-assistant revolution that reshaped mathematics rests on constructive type theory — the foundation of Lean 4 and Rocq (formerly Coq) — in which a proposition is a type and a proof is a concrete object inhabiting it. That is what let mathematics become checkable rather than merely reviewable: a Lean proof is an object the kernel inspects, not an argument a referee trusts. Mathlib, Lean’s library, has grown into a shared, kernel-checked corpus that thousands of mathematicians build on. Viewing institution theory through the same lens does not merely re-verify it; it changes what several of its core notions are, and in doing so it turns institutions into the scientific analogue of what type theory gave mathematics.

Satisfaction becomes a type of witnesses. In type theory, “M satisfies φ” is not a bare fact but a type whose elements are the reasons: proof objects, checkable evidence. The examples from Part I make this concrete. A witness that a trajectory satisfies a differential equation is the verifying computation; a witness that a machine satisfies “every request is eventually acknowledged” is a strategy or a checked exploration of its states; a witness of statistical fit is a likelihood computation over the data. There is a pleasing historical footnote here: Goguen and Roșu’s own categorical machinery naturally produces multi-relations, in which a model and a sentence can be related in many different ways, and they remark that they know of no application for the extra structure — so they flatten it away. The constructive reading is that application. The many “ways” are exactly the witnesses, and flattening is the deliberate act of forgetting evidence.

The one law becomes two transport maps. Classically, the satisfaction condition is a biconditional: truth is invariant under change of notation. Constructively, “if and only if” decomposes into a pair of functions that carry witnesses forward along the sentence translation and backward along the reduct. The slogan sharpens accordingly: change of notation loses no evidence. This is a stronger demand than the classical one, and it generates new proof obligations — the transport maps must respect composition of vocabulary changes — turning what was a property into a structure with coherence laws.

Where the formalization actually stands. Honesty requires a two-stage picture. Stage one is done: Reynolds and Monahan have formalized a fragment of institution theory in Coq/Rocq, machine-checking the satisfaction conditions for first-order predicate logic and for an institution capturing the industrial Event-B specification language, along with institution morphisms, comorphisms, and entailment systems. Their motivation is squarely practical: satisfaction-condition proofs had been expert folklore, tedious enough to block adoption, and a formalized framework turns “is this really a logic?” into a machine-checked certificate. But — instructively — their development suppresses proof relevance, assuming classical-flavored axioms so that Goguen and Burstall’s original definitions go through verbatim. Stage two, natively proof-relevant institutions in which satisfaction is a witness type and the satisfaction condition is coherent witness transport, remains open territory, with homotopy type theory the natural setting.

Borrowing becomes a compiler of proofs. The classical borrowing theorem of Part II lets you trust a foreign prover’s verdict. The constructive upgrade translates the foreign proof itself back into a native, kernel-checked certificate — which is precisely what “hammer” tools in the proof-assistant world already do when they reconstruct an external prover’s output rather than merely believing it. Two classical hypotheses change character along the way. Existence assumptions become data: where the classical theorem asks that every model on one side be hit by the model translation, the constructive version asks for an explicit procedure producing the preimage. And the payoff route is concrete: Event-B proof obligations are today shipped to first-order provers through translations that are trusted rather than verified; a formalized comorphism is exactly the missing correctness certificate for that pipeline.

An algebra for witnesses. Once witnesses are first-class, they want operations: ways to combine, apply, and check evidence. That is what Artemov’s justification logic provides — a calculus of terms t in assertions “t justifies F,” with an application operation, a combination operation, and a proof-checker. Two connections stand out, though the reader should know that wiring justification logic to institutions is synthesis rather than settled literature. First, justification logic’s forgetful projection — collapsing “t justifies F” to the mere modality “F is justified” — is, in institutional terms, a forgetful morphism from a proof-relevant logic to its truncated shadow, confirming once more the proverb of Part II that the trustworthy direction is the forgetting one; the celebrated Realization Theorem is the hard, choice-laden journey back. Second, justification terms were designed to accommodate evidence more general than mathematical proof — and that is exactly the door left ajar in Part I, where statistical satisfaction wanted degrees of fit. Generalized institutions gave graded satisfaction a home; justification-style witness calculi could give it a syntax and a composition theory.

A reflexive twist. Once institution theory itself lives inside Lean or Rocq, the host type theory becomes the meta-language, and every formalized logic is an institution internal to one particular logic — the map of all territories, drawn inside one territory. Far from betraying the framework’s ecumenical spirit, this is the architecture the field was groping toward: a single kernel-checked hub, encodings of each logic verified as morphisms into it, and borrowing implemented as certified proof translation through it. The open problems that close Goguen and Roșu’s paper — which morphisms support borrowing, which categories of institutions behave well — stop being pen-and-paper questions and become formalization targets: you answer them by writing them down and letting the kernel object.

11. The substrate that science is missing

Put the pieces together and a thesis comes due. Proof assistants gave mathematics a shared, machine-checked corpus — Mathlib — in which a result is not a claim to be believed but an object to be inspected. The reason mathematics could have this and science could not is that mathematics works in essentially one logic, while science is irreducibly plural: the immunologist’s statistics, the control engineer’s differential equations, the protocol designer’s temporal logic, the chemist’s reaction rules. A single-logic substrate cannot hold science. Institution theory is precisely the mathematics of many logics held together coherently (Parts I and II), and its constructive form is precisely the version in which “held together” means “with checkable evidence transported across the seams.” That is the missing foundation: a Mathlib-for-science would not be one giant logic but a graph of institutions — each scientific logic formalized, each connected to its neighbors by verified (co)morphisms, each claim carrying a witness that survives translation between them.

This is where the current wave of AI scientists meets a real limitation, and a real opportunity. Tools like Anthropic’s Claude Science, OpenAI’s Rosalind, and DeepMind’s science platforms are genuinely careful: they produce reproducible code, trace every citation, and run reviewer agents that flag numbers they cannot source. But inspect what the reasoning ultimately is, and it is prose and code — artifacts that a human, or another pass of the same model, must read and judge. Even the reviewer agent typically checks the work using the same kind of model that produced it. This is auditability in the sense of a well-kept lab notebook, not in the sense of a kernel-checked proof. The distinction matters most exactly where these systems are most valuable and most fallible: a multi-step argument that starts in a statistical model, passes through a differential-equation model of a mechanism, and ends in a discrete claim about a pathway is today a chain of prose whose weakest link is invisible.

An institutional substrate changes the unit of trust. A scientific argument becomes a term in a graph of institutions: the statistical inference carries its witness, the translation into the mechanistic model is a verified comorphism that transports that witness, and the final claim inherits a certificate traceable — by a kernel, not a model — back through every logic it crossed. An AI scientist emitting reasoning in this substrate would produce not an essay to be reviewed but an object to be checked; its errors would surface as failures to typecheck rather than as plausible-sounding paragraphs; and its results would compose, accumulating into a shared corpus the way formalized mathematics does, instead of remaining a pile of individually-plausible reports. The AI need not itself work only in the substrate — natural-language exploration remains where discovery happens — but it would have somewhere to land its arguments where landing them means making them checkable.

12. Eigenius: the substrate under construction

This is precisely the project of Eigenius, which bills itself as “a compiler for AI thought” — and once the vocabulary of these articles is in hand, the description is close to literal. Eigenius is a typed knowledge graph in which every scientific claim, whether authored by a human or an AI agent, must record how it was justified. Its architecture is a modular arrangement of what it calls institutions connected by cross-vocabulary bridges; a kernel refuses to commit ill-typed reasoning; layers are content-addressed and deterministic. Translate the marketing into the terms built up here and it reads as a direct instantiation: the institutions are institutions, the bridges are comorphisms, the kernel is the type-checking core of a proof assistant, and “recording how a claim was justified” is proof-relevant satisfaction — a claim carrying not just a truth value but a witness.

The sharpest point of contact is Eigenius’s treatment of evidence. Rather than one undifferentiated notion of proof, it sorts every warrant into four peer categories according to what kind of evidence it carries: Observed (raw instrument data with unbroken provenance), Derived (the output of a deterministic computation, re-runnable byte-for-byte), Verified (a claim discharged by a machine-checked formal proof — a Lean-checked result, say), and Declared (something asserted by a named human or policy document, with an examinable citation). The first three are mechanically re-executable; the fourth is authoritative but examinable. This is exactly the generalization of the witness type that Section 10 reached for and Artemov’s justification logic anticipated: satisfaction whose witnesses range over more than formal proofs — measurements, computations, and cited declarations included — each with its own algebra of what counts as re-checking it. Crucially, the categories are peers, not a hierarchy: the system does not pretend a measurement is a proof. What it enforces is that the kind of warrant is recorded and cannot be counterfeited — an AI may still declare something false, but it cannot pass a declaration off as a mechanical derivation. That is the institutional satisfaction condition doing its job at the level of an entire scientific record: truth (and the evidence for it) invariant under who is reading, and under translation across the graph.

Consider Eigenius’s own worked example, the sentence “EIG_0291 was identified as a strong CDK2 inhibitor (IC₅₀ = 85 ± 5 nM, n = 6).” In prose this is a single assertion; structurally it bundles at least five — a measurement with instrument provenance (Observed), a statistical summary (Derived, emitted by a statistics institution), a vocabulary translation between the assay’s terms and the pharmacology’s, a decision rule applying a “strong inhibitor” threshold cited from a methodology document (Declared), and a sample attribution. Each is load-bearing; each is a place a confident hallucination can hide while looking exactly like the correct article. In the substrate, each becomes a typed artifact on a chain, the threshold’s provenance is a Declared warrant rather than an invisible assumption, the vocabulary translation is a comorphism that must actually typecheck, and auditing the headline claim becomes a walk back down the chain — a tree-walk, in Eigenius’s phrase, rather than a re-derivation from scratch. The weakest link stops being invisible.

None of the underpinnings are speculative in isolation. The theory is four decades old and unusually complete. The first machine-checked fragment exists — Reynolds and Monahan’s Coq development, with its handful of concrete logics, including one for an industrial specification language. The mathematical tools are mature enough to carry the rest: mathlib’s category theory, and homotopy type theory for the coherence laws that proof-relevance introduces. What Eigenius is attempting is to assemble these into working infrastructure and aim it at the trust gap that LLM-speed authoring has just blown open. The remaining program is legible in the vocabulary of these articles: formalize the workhorse scientific logics as institutions; verify the comorphisms that bridge them; keep satisfaction proof-relevant so witnesses, not just verdicts, cross the translations; and give those witnesses an algebra — Eigenius’s four warrant kinds are a first cut — general enough for the graded, measured, computed, and declared evidence that real science actually runs on.

That is the vision this series exists to motivate. Institutions began, in the 1970s, as an answer to a narrow question about specification languages: what do all logics have in common? The answer turned out to be a careful balance of syntax and semantics, held stable under change of notation. Four decades later, with mathematics already reaping what proof assistants sowed and AI systems drafting an ever-larger share of the scientific record, that same answer looks like something larger — the shape of a substrate in which a brilliant analysis and a confident hallucination can, at last, no longer look the same in prose.

Glossary for Part III

Constructive type theory. The foundation of Lean 4 and Rocq, in which a proposition is a type and a proof is an object inhabiting it; what makes mathematics machine-checkable rather than merely reviewable.

Proof-relevant satisfaction. The constructive reading in which “M satisfies φ” is a type of witnesses (evidence objects) rather than a bare true/false fact; the classical relation is recovered by forgetting the witnesses.

Witness transport. The constructive form of the satisfaction condition: explicit functions carrying witnesses across a change of notation in both directions, so that translation loses no evidence.

Certified borrowing. Borrowing upgraded from trusting a foreign prover’s verdict to translating its proof back into a native, kernel-checked certificate.

Justification logic. Artemov’s family of logics whose assertions “t justifies F” carry explicit evidence terms with an algebra of operations; a candidate syntax for generalized (graded, non-proof) witnesses in institutions.

Graph of institutions. The proposed substrate for machine-checkable science: each scientific logic formalized as an institution, connected to its neighbors by verified (co)morphisms, with every claim carrying a witness that survives translation.

Warrant (Observed / Derived / Verified / Declared). Eigenius’s four peer kinds of evidence a claim may carry; a concrete, engineered instance of generalized witnesses, in which the kind of warrant is recorded and cannot be counterfeited.

Recap: where Parts I and II leave us

10. The constructive turn

11. The substrate that science is missing

12. Eigenius: the substrate under construction

Glossary for Part III

Further reading