Shingai Thornton · Binghamton University · 2026
Lean 4 formalization · ~4,700 lines · zero sorrys (no unfinished proofs)
Co-authored with Claude Opus 4.6 via Claude Code.
Human editorial judgment; LLM Lean fluency; compiler final authority.
Repository
Seven systems science traditions, developed independently across six decades, encoded as formal definitions in the Lean 4 proof assistant. The compiler verifies their shared categorical structure; the encodings are editorial choices, but every claim about those encodings is machine-checked. This is a companion to the interactive Verso document, which presents the full narrative with hoverable Lean proofs. This page summarizes the key results with diagrams.
I am a systems scientist, not a mathematician or computer scientist. I have no formal training in category theory, type theory, or proof assistants. What I do have is a decade of practice thinking in systems, access to foundational texts that much of the field has moved past without fully absorbing, and a willingness to use new tools at the boundary of what they can do.
This document is the result of pairing that background with two things that did not exist five years ago: a large language model (Claude) fluent in Lean 4 syntax and Mathlib's API, and a proof assistant that does not care about credentials. The human contribution is editorial: which definitions to encode, how to interpret ambiguous source texts, and when the LLM's output is type-correct but conceptually wrong. The LLM contribution is mechanical fluency: tactic generation, library navigation, and the stamina to formalize seven traditions without cutting corners. The compiler's contribution is final authority. It accepted or rejected every claim. There are zero sorrys (unfinished proofs).
The foundational systems science texts formalized here — Klir (1964–2001), Bunge (1979), Mesarovic (1975), Joslyn (1995), Mobus (2022) — are not obscure, but they are underutilized. Most working systems scientists cite them without comparing them formally. Most category theorists building new frameworks (lenses, polynomial functors, operads) do not engage with them at all. This work sits in the gap: it takes the old definitions seriously enough to type-check them, and discovers that they agree on more than anyone knew.
The results should be read with that context. The category theory is real but elementary. The proofs are machine-checked but the encodings are mine. A trained category theorist would likely formalize differently and perhaps find more. What I can offer is the domain judgment to know which seven definitions matter, the editorial sense to encode them faithfully, and the honesty to say where the formalization reaches its limits.
We write 2 for the walking-arrow category: two objects 0 and 1 with a single non-identity morphism f : 0 → 1. Throughout this document, 2 always denotes this category (bold to distinguish from the numeral).
Each tradition defines "system" as a tuple with structural dependencies. We encode these as shape categories (free categories on dependency quivers) to make the relationships between traditions visible and comparable.
The Seven-Tradition Landscape. Gold edges within each panel mark the image of the walking arrow under faithful embedding. Dashed gold lines trace the embedding direction: from K ≅ 2 outward into each tradition.
Three orientations emerge from the encoding. Structural traditions (Klir, Bunge, Mobus) point arrows inward, converging toward components. Operational traditions (Myers, Wymore, Mesarovic) point arrows outward, radiating from state. Joslyn is the only cyclic tradition: feedback generates infinitely many morphisms in the free category. Same arrow, three orientations. The divergence is the history of systems science.
Findings the formalization produced, not claims from the source texts.
The two paths from Mobus to Klir (direct, and via Bunge) produce definitionally identical results. The proof is rfl: the two functor-composites reduce to the same normal form, so the diagram commutes on the nose (definitional equality, not merely up to natural isomorphism). Neither Bunge nor Mobus knew their frameworks were this compatible.
The Commuting Triangle. Both paths reduce to the same normal form. Proof: rfl (definitional equality).
Definition 1.6 in Treatise on Basic Philosophy, Vol. 4, Ch. 1 (1979) states the subsystem relation is "reflexive, asymmetric, and transitive." Reflexive + asymmetric is a contradiction (any inhabited element witnesses reflexivity and irreflexivity simultaneously). The compiler rejected it. Correct property: antisymmetric.
Two readings of Bunge's structure — flat (single relation) and family (set of relations) — both support the commuting triangle. The flat encoding is a faithful quotient. Bonus: Mobus's N/G separation is the natural 2-element structure family. Three distinct subsystem orderings satisfy strict containment: family ⊊ refinement ⊊ flat.
"All interaction is mediated by the boundary" is not assumed. It follows from the bipartite constraint on external flows (the requirement that every flow edge connects an internal component to an external entity, never two internals or two externals). The boundary completeness property is derived, not axiomatized.
Seven traditions, encoded as shape categories, all faithfully embed the walking arrow 2. The common core is maximal: any shape category embedding faithfully into Klir's quiver (two objects, one non-identity arrow) has at most two objects and at most one non-identity arrow, hence is a quotient of 2; faithfulness forces it to be 2 itself. The irreducible content of "system" is a single morphism: relations depend on things.
Each row is a faithful functor EX : 2 → IX. The gold edges in the landscape diagram above mark the image of each embedding. Diagram labels are expanded here to their semantic names:
| Tradition | 0 (things) ↦ | 1 (relation) ↦ | Arrow (f) ↦ | Orientation |
|---|---|---|---|---|
| Klir | things | relation | rel_on_things |
is the core |
| Bunge | composition (Comp) | structure (Struct) | struct_on_comp |
inward |
| Mobus | components (Comp) | internalNetwork (Net) | network_on_components |
inward |
| Myers | output (Out) | state (State) | expose |
outward |
| Wymore | output (Out) | state (State) | readout |
outward |
| Mesarovic | output (Out) | globalState (GlobalState) | response_output |
outward |
| Joslyn | controlled (Controlled) | effector (Effector) | efferent |
cyclic |
Structural traditions say: relations are defined over things. Operational traditions say: state determines observables. Joslyn says: the regulator constrains what it controls. The embedding picks the efferent arc (Effector → Sensor in the diagram); the afferent return has no counterpart in the walking arrow.
Beyond the common core, functors between traditions reveal where the frameworks genuinely diverge:
| Functor | Property | What it reveals |
|---|---|---|
| Mobus → Bunge | Faithful, not full | 6 categories of divergence (boundary, milieu, capacity, transforms, history, timescale). The formal content of "engineering elaboration." |
| Mobus → Myers | Statics vs dynamics | All structural constraints map to expose. Myers's update has no preimage. Mobus captures what systems are; Myers captures how they behave. |
| Wymore → Mobus | Injective on objects, not full | stateOnTime requires length-2 path through boundary. Mobus mediates time through interface structure. |
| Joslyn → any acyclic | Not formalized | Joslyn's cyclic shape generates infinite hom-sets. A faithful functor preserves distinct morphisms, so no faithful functor from Joslyn to a finite acyclic target can exist: the target has only finitely many morphisms to receive infinitely many distinct ones. The open problem. |
Structure formalizes cleanly. Dynamics and semantics do not. These are the open problems:
Unit. No formal theory of what systems do. Mobus's transforms are where engineering content lives; the formalization treats them as opaque.
ActsOn : α → α → Prop is opaque. Cannot distinguish a thermostat's bang-bang control (a chosen rule) from Newton's law of cooling (a physical law). This is Joslyn's central concern.
Spivak, Fong, and Myers build new categorical frameworks from scratch: polynomial functors, lenses, operads. They capture compositionality beautifully. Note: David Jaz Myers appears in both roles here. His 2023 Categorical Systems Theory is one of the seven traditions encoded (IMyers), and he is also one of the researchers building the compositional future. The encoding treats his framework as a peer alongside Klir (1964) and Mesarovic (1975); the positioning places his broader program alongside Spivak's.
This work is comparative: seven existing definitions as written, encoded faithfully, the encodings themselves editorial choices, the compatibility results verified by the compiler. The common core theorem is a finding about those particular encodings, not a design choice.
They build the future of systems theory. This audits its past. The audit reveals the past already agrees on more than anyone knew.
Ashby, W.R. (1956). An Introduction to Cybernetics. London: Chapman & Hall.
Bunge, M. (1979). Treatise on Basic Philosophy, Vol. 4: Ontology II: A World of Systems. Dordrecht: D. Reidel Publishing.
Bunge, M. (2000). Systemism: The Alternative to Individualism and Holism. Journal of Socio-Economics, 29(2), 147–157.
Klir, G.J. (2001). Facets of Systems Science (2nd ed.). New York: Springer.
Klir, G.J. & Valach, M. (1967). Cybernetic Modelling. London: Iliffe Books.
Klir, G.J. & Rogers, G.S. (1977). Basic and Applied General Systems Research: A Bibliography. In G.J. Klir (Ed.), Applied General Systems Research. New York: Plenum.
Mesarovic, M.D. & Takahara, Y. (1975). General Systems Theory: Mathematical Foundations. New York: Academic Press.
Mobus, G.E. (2022). Systems Science: Theory, Analysis, Modeling, and Design. Cham: Springer.
Myers, D.J. (2021). Categorical Systems Theory. Topos Institute Blog, November 4, 2021. topos.institute/blog.
Myers, D.J. (2023). Categorical Systems Theory. Manuscript, Topos Institute.
Topos Institute (2021–). Fundamental Research: Pioneering a Mathematical Systems Science. topos.institute/work.
Wymore, A.W. (1993). Model-Based Systems Engineering. Boca Raton: CRC Press.
Goguen, J.A. (1978). General Systems Theory and the Chomsky Hierarchy. In B.P. Zeigler et al. (Eds.), Methodology in Systems Modelling and Simulation (pp. 321–333). Amsterdam: North-Holland.
Takahara, Y. & Takai, M. (1985). Category Theoretical Framework of General Systems Theory. International Journal of General Systems, 11(3), 233–246.
Wach, L., Joslyn, C., Purvine, E., & Jensen, S.A. (2021). Conjoining Wymore's Systems Theoretic Framework and the DEVS Modeling Formalism. Systems Engineering, 24(5), 271–290.
Joslyn, C. (1995/2000). Semantic Control Systems. World Futures: The Journal of General Evolution, 45(1-4), 87–123.
Joslyn, C. & Purvine, E. (2018). Hypergraph Theory for the Analysis of Complex Social Systems. SIAM Workshop on Network Science.
Pattee, H.H. (1995). Evolving Self-Reference: Matter, Symbols, and Semantic Closure. Communication and Cognition — Artificial Intelligence, 12(1-2), 9–28.
Rosen, R. (1991). Life Itself: A Comprehensive Inquiry into the Nature, Origin, and Fabrication of Life. New York: Columbia University Press.