The paired entries on capitalism and socialism rest on a small set of categorization rules: a three-condition test for when a formation counts as substantially organized around accumulation, a layered rule separating socialist projects (identified by genealogy) from socialist institutions and formations (identified by the productive powers actually socialized, and their extent), and the claim that the two categories genuinely overlap rather than partitioning the space. Rules of that shape can harbour quiet contradictions – two locally plausible boundary claims that no possible formation could satisfy together. That class of defect is mechanically detectable, so it has been mechanically checked.
The rules are formalized in Alloy, a relational modelling language whose analyzer searches exhaustively for models and counterexamples within a bounded scope. Each boundary claim the entries make became a named predicate; the analyzer then confirmed a witness for every claim and the validity of every definitional check. One check was written to fail: an earlier draft assumed that satisfying the capitalist test excludes being a socialist formation, an external review caught the contradiction with the entries’ own hybrid space, and the corrected position – the categories overlap – is now guarded by a counterexample the analyzer must find.
Results
Alloy 6.2.0, all commands, August 13, 2026. A witness row asks whether a described formation can exist under the rules (SAT means yes); a check row asks whether a universal claim holds in every model within scope (valid means no counterexample exists).
| Command | Kind | Result | Reading |
|---|---|---|---|
marketSocialismOverlap | witness | SAT | Market socialism can satisfy both the capitalist structural test and the socialist-formation threshold: the overlap between the categories is real. |
merchantQualifying | witness | SAT | Merchant capital that reorganized production and finance around itself qualifies as capitalist. |
merchantFailing | witness | SAT | Merchant commerce that skims an unchanged base does not. |
householdBelowBoundary | witness | SAT | Household commercial production with markets but no structured domains is not capitalist: markets do not suffice, witnessed. |
plantationCapitalism | witness | SAT | Coerced labour is compatible with the capitalist test; the labour-regime orthogonality claim has a model. |
stateCapitalismStructural | witness | SAT | A formation can sit in the structural overlap with no socialist programme: formation-level categorization is structural, genealogy separate. |
socialDemocracyProjectOnly | witness | SAT | A socialist project can govern a capitalist, non-socialist formation. |
nepRecruitment | witness | SAT | A socialist project can deliberately recruit markets without dissolving. |
plannedSocialismNoMarkets | witness | SAT | Comprehensive planning without markets remains categorizable as a socialist formation, and is not capitalist. |
enclaveNeverFormation | check | valid | Enclave socialization never makes a socialist formation: the threshold does its job. |
marketsDoNotSuffice | check | valid | No structured domains, no capitalism, however commercial the society. |
formationRequiresPowers | check | valid | The socialist-formation label follows the powers. |
twoDomainsInsufficient | check | valid | The three conditions are genuinely joint: two of three domains never suffice. |
capitalistExcludesSocialistFormation | check | counterexample | The assumption that capitalist excludes socialist formation is refuted, as intended: an earlier draft made this assumption, an external review caught it, and the check now guards it mechanically. |
What this does and does not show
A satisfiable witness certifies that a boundary claim is coherent under this formalization; a valid check certifies a definitional claim within the search scope. Neither certifies the prose itself: the mapping from prose to model is a judgment step, and threshold notions such as “materially structures” and “a substantial part of productive life” enter the model as primitives, which is faithful to the entries, where they are threshold judgments too. Nothing evidential is modelled: the entries’ five-step evidential test and bounded verdicts concern the force of evidence, which does not reduce to relational structure, and pretending otherwise would be the kind of false rigour the entries argue against.
Reproducing
Download the model source and the Alloy 6.2.0 dist jar, then run java -jar org.alloytools.alloy.dist.jar exec -c '*' -f institutional_categorization.als. The fourteen results above should reproduce exactly.