Seven Frameworks, Three Orientations
Each tradition defines "system" as a tuple whose components stand in structural dependencies. We encode each as a shape category, a small category whose objects are the tradition's named concepts and whose arrows are the dependency relations between them. Then we ask: what do all seven shapes have in common?
| Tradition | Orientation | The arrow reads as |
|---|---|---|
| Klir (1969) | Structural | Relations depend on things |
| Bunge (1979) | Structural | Structure depends on composition |
| Mobus (2022) | Structural | Network depends on components |
| Mesarović (1975) | Operational | Output depends on input |
| Wymore (1993) | Operational | State mediates I/O through time |
| Myers (2023) | Operational | Expose/update lens on state |
| Joslyn (1995) | Cybernetic | Feedback cycle on the arrow |
Three orientations: structural traditions point arrows inward, operational traditions point arrows outward, and the cybernetic tradition closes the loop. All seven embed the same irreducible content: 2, the category with two objects and one non-identity morphism.
Each embedding is a faithful functor from 2 into the tradition's shape category. The functor sends the two objects (things, relation) and the single arrow (relation_on_things) to their tradition-specific counterparts:
| Target | things ↦ | relation ↦ | arrow ↦ |
|---|---|---|---|
| Klir | things | relation | relation_on_things |
| Bunge | composition | structure' | struct_on_comp |
| Mobus | components | internalNetwork | network_on_components |
| Mesarović | output | globalState | response_output |
| Wymore | output | state | readout |
| Myers | output | state | expose |
| Joslyn | controlled | effector | efferent |
The compiler caught a forty-seven-year-old error.
Definition 1.6 in Mario Bunge's Treatise on Basic Philosophy, Vol. 4 (1979), states that the subsystem relation is "reflexive, asymmetric, and transitive." Reflexivity and asymmetry contradict. Any reflexive relation contains (x, x); asymmetry forbids it. The Lean 4 compiler rejected the conjunction on the first attempt. The correct property is antisymmetric: if x ≤ y and y ≤ x, then x = y.
Bunge's text has been cited for over four decades. No reviewer caught it. The compiler did, in seconds.
What the Compiler Found
Four results that were not known before the formalization. Each is machine-verified. The Lean 4 compiler is the final authority, not the author.
rfl: the compiler confirms the two compositions are the same function.theorem klir_has_two_elements :
∀ (f : Fin 3 → KlirPosition), ¬ Function.Injective f := by
intro f hinj
have h : f 0 = f 1 ∨ f 0 = f 2 ∨ f 1 = f 2 := by
cases (f 0) <;> cases (f 1) <;> cases (f 2) <;> simp
rcases h with h | h | h
· exact absurd (hinj h) (by decide)
· exact absurd (hinj h) (by decide)
· exact absurd (hinj h) (by decide)
Where It Fails
Honest about the boundaries. Four things the current formalization cannot reach:
- TransformsWhat systems do (transformation functions, mechanisms, dynamics) is encoded as opaque. The formalization captures structure, not behavior.
- Rule vs. LawThe distinction between chosen rules and physical laws cannot be expressed in the current type system.
- Active ControlMaintaining dynamic equilibrium against disturbance requires temporal reasoning beyond the snapshot model.
- Variety MeasuresJoslyn's dimensional and cardinal variety lack formalization. Constraint analysis requires a quantitative layer.
One Open Question
Joslyn's cybernetic tradition generates a cyclic shape category. The cycle produces infinitely many morphisms. No faithful functor to a finite acyclic target can exist. What categorical structure enables comparison? The six acyclic traditions converge cleanly. The seventh demands categorical machinery that does not yet exist for systems science.
~6,265 lines · zero sorrys · 39 files · Lean 4 + Mathlib