Formalising Grassroots Social Contracts: From Legal Text to Grassroots Platforms

arXiv:2609.06231v1 [cs.CY] 5 Sep 2026

Formalising Grassroots Social Contracts: From Legal Text to Grassroots Platforms (Full Version) James GOLIKE a , Andy LEWIS-PYE a and Ehud SHAPIRO a,b a London School of Economics and Political Science b Weizmann Institute of Science Abstract. Almost two centuries ago Pierre-Joseph Proudhon envisioned a social contract that is (1) an agreement of man with man; (2) reciprocal; (3) imposing no obligation upon the parties except that which results from their personal promise; (4) subject to no external authority; (5) freely accepted and signed by all the participants; (6) of the nature of a contract of exchange; and a few other conditions. He also envisioned a property of social contracts, analogous to a property of digital platforms we term grassroots: that (i) one could “make a contract with all, as . . . with some”; digitally, that a grassroots platform can have multiple instances, and (ii) “each group of citizens . . . formed by a like contract . . . could thereafter, and always by a similar contract, agree with every and all other groups”; digitally, that independent platform instances may coalesce by mutual consent, possibly into a single global platform instance. We proposed grassroots platforms owned, operated and governed by their participants as a foundation for an equitable and democratic digital realm. Here we define grassroots social contracts as social contracts meeting Proudhon’s six conditions above and that (7) people are free to deal with each other; and (8) there is no external register of people, so people can come to know each other either directly or through people they already know. We show that a grassroots social contract can be transformed into a working smartphone-based grassroots platform through an abstraction cascade, starting from converting the social contract text to formal act schemas, verified syntactically to be grassroots, and then to volition-guarded multiagent atomic transactions, hitherto the most abstract formalism used to specify grassroots platforms. The abstraction cascade from there to a working app has been described elsewhere. Act schemas are a formal language for the acts the contract describes, each naming the parties’ roles, which of them must will the act, and its precondition and effect at each role, with contract parties determined upon signature. Any contract written in this language meets the eight conditions above, provided it is syntactically grassroots, satisfying : (i) Introduction, that some act can introduce any two willing parties, following which the state of each stores an identifier of the other; (ii) Provenance, that the state of a party stores an identifier of a person only by an act with that person, or with a party whose state stores that identifier; and (iii) Volition, that an act requires the consent of all its parties, unless the undirected graph formed by identifiers stored by the parties is connected. We prove that the protocol realising a syntactically grassroots contract is grassroots, and volitionally so. To do so, we first prove that politeness — any two parties can always come to interact, and no act joins two instances unless all its participants will it — is sufficient for the protocol over a set of volition-guarded multiagent atomic transactions to be grassroots, and volitionally so: two groups coalesce only when a member of each wills it. We then prove that a syntactically grassroots social contract compiles into a polite set of volition-guarded transactions. Clauses of a grassroots social contract are of three legal types: A breach of an enforced clause is impossible with a correct implementation of the contract; a breach of an attested or undertaken clause can be taken to court, with non-repudiably signed evidence of the breach in the case of an attested clause. We illustrate the three legal types with two grassroots social contracts, the grassroots social graph carrying signed items and grassroots currencies. Keywords. grassroots social contract, act schema, compilation, enforcement modalities, provenance, contract specification language, norm-governed systems, contract formation

1

1. Introduction Almost two centuries ago Pierre-Joseph Proudhon envisioned a social contract [1, Fourth Study] that is (1) an agreement of man with man; (2) reciprocal; (3) imposing no obligation upon the parties except that which results from their personal promise; (4) subject to no external authority; (5) freely accepted and signed by all the participants; (6) of the nature of a contract of exchange; and a few other conditions, among them that it include all citizens with their interests and that it increase the well-being and liberty of every citizen. In his words, the social contract is “an agreement of man with man”; “essentially reciprocal: it imposes no obligation upon the parties, except that which results from their personal promise of reciprocal delivery: it is not subject to any external authority: it alone forms the law between the parties: it awaits their initiative for its execution”; “freely discussed, individually accepted, signed with their own hands, by all the participants”; and “of the nature of a contract of exchange: not only does it leave the party free, it adds to his liberty; not only does it leave him all his goods, it adds to his property; it prescribes no labor; it bears only upon exchange”. He also envisioned a property of social contracts [1, Sixth Study], analogous to a property of digital platforms we term grassroots [2,3,4]: that (i) one could “make a contract with all, as . . . with some”; digitally, that a grassroots platform can have multiple instances, and (ii) “each group of citizens . . . formed by a like contract . . . could thereafter, and always by a similar contract, agree with every and all other groups”; digitally, that independent platform instances may coalesce by mutual consent, possibly into a single global platform instance. In full: “if I could make a contract with all, as I can with some; if all could renew it among themselves, if each group of citizens, as a town, county, province, corporation, company, &c., formed by a like contract, and considered as a moral person, could thereafter, and always by a similar contract, agree with every and all other groups, it would be the same as if my own will were multiplied to infinity. I should be sure that the law thus made on all questions in the Republic, from millions of different initiatives, would never be anything but my law; and if this new order of things were called government, it would be my government.” We proposed grassroots platforms owned, operated and governed by their participants as a foundation for an equitable and democratic digital realm [3]. A digital social contract is one realised by software the parties run [5]. We call the mathematical object a protocol and the software realising it a platform. We say a platform realises a contract, and reserve implements for the relation between two adjacent abstractions of the abstraction cascade [6]. A protocol is grassroots when its instances are independent of one another and of every global resource but the net, and can always coalesce, possibly into a single global instance [2,3,4], and a grassroots platform is the software realising a grassroots protocol. The grassroots notion is a formal property of a protocol, recalled in Section 4. Here we define grassroots social contracts as social contracts meeting Proudhon’s six conditions above and that (7) people are free to deal with each other; and (8) there is no external register of people, so people can come to know each other either directly or through people they already know. Our first theorem is that such a contract has the grassroots property: its acts — what clauses describe the parties doing — determine a grassroots platform, in which any two parties may come into relation without requiring anyone’s permission, two communities that adopted the contract independently coexist and may later merge, and every participant in any act is a party — no registry that issues identifiers, no log that orders acts, no authority that timestamps them.A social contract 2

is a contract among those who adopt it. Participating in a grassroots platform requires adopting the grassroots social contract that defines it, as participating in a global platform requires adopting an End-User Licence Agreement (EULA). A grassroots social contract is mutual and symmetric among all participants; an EULA is between each person and the platform operator. A friendship or a mutual credit line is an act under the contract between particular parties. We show contracts for a social network carrying signed speech acts [7,8] and for a currency of personal coins [9] that are grassroots. Not every social contract is. Examples that are not include a contract without coalescences, not allowing two strangers to come into relation; a contract with named third-party control, e.g. where introduction requires a token only a third party can make; and a contract with an act one party takes upon a stranger — an act that changes the stranger’s state without their will and requires no prior relation between the two; each fails one of the conditions. We show that a grassroots social contract can be transformed into a working smartphone-based grassroots platform through an abstraction cascade [6], starting from converting the social contract text to formal act schemas, verified syntactically to be grassroots, and then to volition-guarded multiagent atomic transactions [10], hitherto the most abstract formalism used to specify grassroots platforms. The abstraction cascade from there to a working app has been described elsewhere [6]. A grassroots social contract has two artefacts: a legal text, and a protocol realising it. A clause of the text describes an act, in the sense of a juridical act: a declaration by one or more parties intended to create a legal effect. Act schemas are a formal language for the acts the contract describes, each naming the parties’ roles, which of them must will the act, and its precondition and effect at each role, with contract parties determined upon signature. Any contract written in this language meets the eight conditions above, provided it is syntactically grassroots, satisfying : (i) Introduction, that some act can introduce any two willing parties, following which the state of each stores an identifier of the other — records the other, as we say, a friend, the issuer of a coin it holds, the author of an item it was sent; (ii) Provenance, that the state of a party stores an identifier of a person only by an act with that person, or with a party whose state stores that identifier; and (iii) Volition, that an act requires the consent of all its parties, unless the undirected graph formed by identifiers stored by the parties is connected. Conditions (1), (2) and (4) hold of every contract written as act schemas, since every participant in an act is a party and the schemas single out no one, and so does (5), since nobody is bound who has not adopted the contract (Section 3.5); (3) is Volition, (6) and (7) are Introduction, and (8) is Provenance (Section 3.6). The three are decidable, and a checker for them accompanies this paper, at https://github.com/EShapiro2/GLP/tree/main/programs/jurix; it certifies both of the contracts we carry through. The compilation into transactions is defined for contracts meeting them. We prove that the protocol realising a syntactically grassroots contract is grassroots, and volitionally so (Theorem 10). To do so, we first prove that politeness — any two parties can always come to interact, and no act joins two instances unless all its participants will it — is sufficient for the protocol over a set of volition-guarded multiagent atomic transactions to be grassroots, and volitionally so: two groups coalesce only when a member of each wills it (Theorem 24). We then prove that a syntactically grassroots social contract compiles into a polite set of volition-guarded transactions (Section 7).

3

Clauses of a grassroots social contract are of three legal types (Section 8), by whether a party can breach a clause and what record of it the contract leaves in another party’s state: a clause is enforced, if performing it is an act of the contract and no act of the contract can breach it; attested, if a party may breach it, with the contract recording the breach; or undertaken, if the contract records who gave the undertaking, but performing the undertaking is carried out outside the contract. A breach of an enforced clause is impossible with a correct implementation of the contract; a breach of an attested or undertaken clause can be taken to court, with non-repudiably signed evidence of the breach in the case of an attested clause. We illustrate the three legal types with two grassroots social contracts, the grassroots social graph carrying signed items [11,7,8] and grassroots currencies [9]. The compilation and the conditions are algorithmic, so the only informal step in the chain is the first: rendering a legal text as schemas. We carry two contracts through, a social graph carrying signed items and a currency of personal coins, and certify both from their schemas. A coin can be handed on, so a holding may record a person its holder has never transacted with; provenance carries the certification through, and conservation of money is its special case. Three languages. The paper employs three languages: natural language for the social contract; act schemas; and volition-guarded atomic transactions. Rendering the first as the second is by judgement; compiling the second into the third is algorithmic; and the conditions of the main theorem—that a syntactically grassroots social contract is grassroots—are verified in the second. Clause 1 of the social graph contract (Section 2.1) reads “Alice and Bob may jointly decide to become friends, if neither is the friend of the other”. Its schema (Section 3.3) names the act’s two roles, marks each with ? as having to will it, and at each role forbids the atom that role gains and adds it: befriend(Alice?, Bob?) : ¬friend(Bob), +friend(Bob) ¬friend(Alice), +friend(Alice). Compiling it (Section 5.2) gives the volition-guarded transaction (d → d ′ , {Alice, Bob}), ′ for every d with friend(Bob) ∈ / dAlice and friend(Alice) ∈ / dBob , where dAlice = dAlice ⊎ ′ {friend(Bob)} and dBob = dBob ⊎ {friend(Alice)}. The rest of the paper is read off the middle line. The abstraction cascade. The passage from a legal text to a running platform goes through the abstraction cascade [6] set out in Figure 1, from the legal text at the top to an app on each party’s own phone at the bottom. This paper provides (1)→(3). The steps below have been carried out by the Human–Science–AI methodology, in which AI derives code from a paper written for peer review and the paper is repaired wherever the code exposes a gap: the grassroots social graph [11], the grassroots social network [7] and grassroots currencies [12] are each a volition-guarded Grassroots Logic Program generated from its volition-guarded transactions, and one Dart bridge renders the three as panels of a single app, deployed on a physical smartphone [6]. A child-safe social network [13] is specified the same way. The Human–Science–AI methodology. The formal objects of the cascade are its abstractions and the implementations among them, each constructed, maintained, evolved and proved correct with AI, in tandem with the paper describing it. The methodology has two kinds of artefact: papers written for competitive peer review, and code. The papers serve as an evolving and cooperatively-constructed interface between us humans and AI, recording our shared understanding of the subject matter, and are the source of authority for coding. Papers are written by people and reviewed, revised and extended with the 4

help of AI; the code, with few exceptions, is written entirely by AI; and both evolve in the process of harmonising them. AI codes down the abstraction cascade, from a paper destined for peer review to tested code, and every gap the code exposes is repaired in the paper before it is repaired in the code. It is at the antipode of “vibe coding”, where a person describes the intended behaviour informally and AI guesses the rest [14]. Specdriven development makes the specification the primary artefact, maintained by people while the code is regenerated from it [15,16]; here that artefact is a scientific paper, and the feedback climbs all the way up to revise it. Nine components were carried to tested code in a single year, each in tandem with the paper describing it. Relation to contract specification languages. Formalising legal text has a large literature — contracts as automata, as defeasible deontic rules, as domain-specific languages, and statute as code — and Section 9 reviews it. Two languages formalise legal contracts in a way close enough to ours to say plainly how they differ. Symboleo [17,18] specifies a contract as obligations and powers with statechart lifetimes, for verification and for monitoring; Stipula [19] is a domain-specific language whose contracts are state machines over parties, fields and linear assets, with an agreement operator and a formal semantics. Both bind their parties at contract formation and both keep one global contract state. Our question is not about one contract instance among fixed parties: it is about the family of systems a contract induces over every finite set of people, and about what happens when two groups that formed independently meet. The question cannot be posed in either language, and each requires a global resource that closure forbids. Section 9 takes this up, together with the literature on norms and on contract languages more broadly. Structure. Section 2 gives the two contracts and Section 3 the syntax of act schemas, with the schemas of both. Section 4 recalls what is needed of [10] and Section 5 compiles the schemas into its transactions. Section 6 defines politeness and proves it sufficient for a protocol to be volitionally grassroots, and Section 7 gives the conditions on the schemas and certifies both contracts from them. Section 8 takes up the clauses and their modalities, and Section 9 places the work. Appendix A states the framework of [10] formally, citing its proofs. 2. Two Grassroots Social Contracts A grassroots social contract is a finite list of clauses its parties undertake towards one another. A party is a person, natural or legal, with the gender-neutral pronoun ‘they’; Alice and Bob are variables naming distinct parties. A clause either describes an act, which the protocol realising the contract carries out, or binds the parties without describing one. The two contracts are examples: the syntax of Section 3, the compilation of Section 5 and the conditions of Section 7 apply to any contract written the same way, and these two are the ones the paper certifies. Two contracts are carried through the paper: a social graph carrying signed items, and a currency of personal coins. Their clauses are given here as a contract has them. The sections that follow give the acts a formal syntax, compile the schemas into transactions, and certify both contracts from the schemas alone. 2.1. The Social Graph with Signed Items The parties to this contract are the members of a social network, and its clauses are five. The first two are the clauses of the grassroots social graph [11,7], the platform the rest 5

(1) The legal text. The clauses a grassroots social contract’s parties undertake towards one another, each describing an act or binding them without one. [informal]

(2) Act schemas. A formal language for those acts: a schema names an act’s roles, which of them must will it, and the precondition and effect at each role, the parties being filled in on signature. [this paper]

(3) Volition-guarded multiagent atomic transactions [10]. The primary vehicle for the concise and abstract specification of grassroots platforms. [6]

(4) Communicating volitional agents [6]. An implementation-ready restriction of the former in which the only non-unary transactions are discovery and message delivery. [6]

(5) Volition-guarded Grassroots Logic Programs [6], GLP (6) extended with volition guards, whose volition-guarded clauses determine the platform’s user interface. [6]

(6) Grassroots Logic Programs [20,21,22], a multiagent, concurrent, polymorphically typed logic programming language, designed for the implementation of grassroots platforms by AI. [21]

(7) Dart and Flutter [23], a programming language for smartphone applications, deployable on iPhone and Android, with Flutter for the user interface of both. [23]

(8) The grassroots app. One app on each person’s own phone, each platform it runs a panel of it. Figure 1. The abstraction cascade, from a legal text to a running platform. The framed (1)–(3) are this paper. Each arrow but the first is an implementation of the abstraction above it by the one below, carrying the reference in which that implementation is defined; the first, rendering a legal text as act schemas, is the one step left to judgement. A condition on the transactions of (3), politeness, is sufficient for the platform they specify to be a grassroots platform, and conditions on the schemas of (2) are sufficient in turn for politeness.

rests on: they say who may become whose friend. The next two carry signed items over it [8], and the fifth is added here as a clause that describes no act; Section 8 says what a realisation does with such a clause. 1. Friendship. Alice and Bob may jointly decide to become friends, if neither is the friend of the other. Each is thereafter a friend of the other. 2. Ending a friendship. Alice may decide to end their friendship with Bob, and it then ends for both. 3. Authorship. Alice may decide to sign an item of their own. 4. Forwarding. Alice may decide to forward an item they hold to their friend Bob, and warrants that they know personally the party they received the item from. 5. Confidence. Alice shall disclose an item they hold only by forwarding it. The first four clauses describe acts and determine the contract’s transactions. The warranty in the fourth describes no act of its own, and neither does the fifth; both bind the parties all the same.

6

2.2. Currencies A grassroots currencies contract [9] has five clauses. A coin is a unit of debt naming its issuer, and an Alice-coin is a coin issued by Alice. 1. Minting. Alice may decide to issue Alice-coins. 2. Swap. Alice and Bob may jointly decide to swap a coin Alice holds for a coin Bob holds. 3. Payment. Alice may decide to pay a Bob-coin they hold to Bob. 4. Redemption. Alice may decide to redeem a Bob-coin they hold against any coin Bob holds. 5. The issuer’s obligation. Alice accepts Alice-coins, at the prices they advertise, for the goods and services they offer. The first four determine the contract’s transactions. A swap in which Alice gives an Alice-coin and Bob gives a Bob-coin opens a mutual credit line between them, each thereafter holding a coin of the other. The fifth describes no act: it gives a coin its worth. 3. Act Schemas A clause of a contract describes an act, in the sense of a juridical act: a declaration by one or more parties intended to create a legal effect. This section gives those acts a formal syntax. A contract C is a finite set of act schemas over a set Σ of predicates, and SC is its set of states. A party’s state is a multiset of atoms; a schema names an act’s roles, which of them must will it, and the atoms it requires, forbids, adds and deletes at each role. 3.1. Atoms and States Write Π for a potentially infinite set of people, of which every contract and every run concerns a finite subset, and D for a set of speech acts disjoint from it: a speech act is a thing a party signs — a message, a post, an item — taken as an identity. Write Σ for a set of predicate symbols, predicates for short, and α : Σ → N for their arities; a predicate of arity n applied to n arguments is an atom, a syntactic object with no truth value. The arguments of an atom of a state are people and speech acts; those of an atom of a schema are roles and variables. Definition 1 (Atoms and states). For any set W of arguments put Σ[W ] = { e(u1 , . . . , uα(e) ) : e ∈ Σ, ui ∈ W }, call its members the atoms over W , and call u1 , . . . , uα(e) the arguments and e the predicate of e(u1 , . . . , uα(e) ). An atom over Π ∪ D is ground , a local state is a finite multiset of ground atoms, the initial state is s0 = 0, / and SC (P) = { s : s a finite multiset over Σ[P ∪ D] }

(P ⊂ Π).

Multiset operations are written ⊎, \, ∩ and ⊆: multiplicities are added, subtracted, minimised and compared. A set is a multiset in which every multiplicity is one. A state is local, so its holder is no argument of its atoms: friend(Bob) in the state of Alice says that Bob is a friend of Alice, and ¢(u) in the state of Alice is a coin issued by u and held by Alice; a friend set is a set of the former and a holding a multiset of the latter.

7

3.2. The Syntax of a Schema Fix disjoint sets R of roles and X of party variables, both disjoint from Π, and a set Y of speech-act variables disjoint from D. A schema is written over the atoms over R ∪ X ∪Y . A schema is a contract template: the role names are its parameters, and the identities of the parties assuming them are filled in on signature. The mark ? is a question the machine puts to the person in that role [5]. For example, take one predicate friend of arity one. The clause that Alice and Bob may jointly decide to become friends is the schema befriend(Alice?, Bob?) : ¬friend(Bob), +friend(Bob) ¬friend(Alice), +friend(Alice). Read it role by role. At Alice the atom friend(Bob) is forbidden, so Alice must not already have Bob as a friend, and the same atom is added — the effect of befriending; Bob is the mirror image. Both roles carry ?, so the act takes the will of both. Nothing is required and nothing deleted, and both parties change state, as every schema requires at every role. Definition 2 (Act schema). An act schema is written τ(π1 , . . . , πk ; x1 , . . . , xm ) :

E1

···

Ek

with τ its name, π1 , . . . , πk ∈ R distinct, k ≥ 1 its arity, x1 , . . . , xm ∈ X distinct, and each Ei a finite multiset of marked atoms, an atom over {π1 , . . . , πk , x1 , . . . , xm } ∪Y carrying at most one of the marks −, +, ¬. For each role πi the marks divide Ei into four finite multisets of atoms, +(i), −(i), ¬(i), =(i), its members marked +, marked −, marked ¬, and unmarked respectively; the atoms πi requires are =(i) ⊎ −(i). It is required that +(i) ∩ −(i) = 0/ and +(i) ⊎ −(i) ̸= 0. / A role may carry the mark ?; the guarding roles of τ are those that do. Definition 3 (Binding). A binding β for a schema τ maps its roles and party variables to Π, injectively on the roles, and Y to D, and is extended to atoms and to multisets of them componentwise. An act schema is a STRIPS operator [24] in multiagent form: what a role requires and forbids is a precondition, what it adds and deletes are an add list and a delete list, and a schema carries one of each per role, where STRIPS has one precondition and one pair of lists over a single global state. The marks are also the four kinds of arc of a contextual net transition [25]: an atom required and deleted is consumed, one required and kept is a positive context condition, one forbidden is a negative context condition, and one added is produced. We take no result from either theory. 3.3. The Schemas of the Social Graph Three predicates. friend, of arity one: friend(Bob) in the state of Alice says that Bob is a friend of Alice. item, of arity three: item(x, a, f ) in the state of Alice is the speech act x, authored by a and received from f ; a speech act a party signs is authored by it and received from it. And sent, of arity two: sent(x, Bob) says that its holder forwarded x to Bob. The roles are Alice and Bob, and the four clauses of Section 2.1 that describe acts become four schemas. Sign carries the speech-act variable x; forward carries x and two party variables, a for its author and f for the party it came from, neither of whom takes part in the act.

8

schema befriend(Alice?, Bob?) : unfriend(Alice?, Bob) : sign(Alice?; x) : forward(Alice?, Bob; x, a, f ) :

at Alice ¬friend(Bob), +friend(Bob) −friend(Bob) +item(x, Alice, Alice) item(x, a, f ), friend( f ), +sent(x, Bob)

at Bob ¬friend(Alice), +friend(Alice) −friend(Alice) friend(Alice), +item(x, a, Alice)

Nothing else is required, forbidden, added or deleted. “Alice and Bob may jointly decide” is the two guarding roles of befriend and “if neither is the friend of the other” its forbidden atom; “Alice may decide” is the single guarding role of unfriend, of sign and of forward; “it then ends for both” is that unfriend deletes in both roles. “An item they hold” is the item(x, a, f ) forward requires and “their friend Bob” is the friend(Alice) its recipient requires; friend( f ) is required of the forwarder because a party forwards only what came from a friend; only the forwarder guards, since only the forwarder decides; and forwarding keeps the item and adds the record of the forward, as every role must change state. The records. The schemas meet each of the five clauses differently. Befriend is the only schema adding a friend atom, that atom’s argument is a role, and befriend guards in both, so a party’s friends are only people who have willed the friendship, and no act of the contract can put one there against that person’s will. Unfriend is the only schema deleting a friend atom and it deletes in both roles, so a friendship never ends for one party without the other. A speech act a party signs sits in its own state and records nothing against it; the record appears when it is first forwarded, and it is the recipient’s item(x, a, Alice), naming the forwarder. Sign is the only schema adding an item atom whose author is not carried over from one it requires, and it names its own role there, so every speech act is authored by the party that signed it. A party may forward what it received from a friend it does not personally know, so the schemas cannot stop the warranty of clause 4 being false — holding a friend atom is not knowing a person. Instead they leave the false warranty on record against the party that gave it, in the hands of the party it was given to. Passing an item on outside the contract is no act of it, and forwarding, the one act that discloses an item, is permitted by clause 5, so no act can breach it; and a forward leaves item(x, a, Alice) in the recipient’s hands, naming the party that passed it on, so the party bound is on record. 3.4. The Schemas of the Currency One predicate, ¢, of arity one: ¢(u) in the state of Alice is a coin issued by u and held by Alice. The roles are Alice and Bob. schema mint(Alice?) : swap(Alice?, Bob?; u, v) : pay(Alice?, Bob) : redeem(Alice?, Bob; r) :

at Alice +¢(Alice) −¢(u), +¢(v) −¢(Bob) −¢(Bob), +¢(r)

at Bob −¢(v), +¢(u) +¢(Bob) −¢(r), +¢(Bob)

“Alice may decide” is the single guarding role of mint, of pay and of redeem; “Alice and Bob may jointly decide” is the two guarding roles of the swap; “a Bob-coin they hold” is that pay and redeem require of Alice a coin whose argument is Bob; “any coin Bob holds” is redeem’s party variable r. The mutual credit line of Section 2.2 is the swap at a binding sending u to Alice and v to Bob, where each gives a coin of its own issue. 9

The records. Selling at an advertised price is no act of the contract, so no act can breach clause 5 and no run shows whether the issuer honours it; but a mutual credit line leaves a coin of the issuer in another party’s holding, and that coin, naming the issuer, is the record of the undertaking. Minting records nothing against the issuer, putting the coin in its own holding; the undertaking becomes evidence only when the coin first passes to someone else, which is the moment a promissory note is handed over. A clause that a holding contains a coin only if its issuer willed the act that put it there would be met by nothing: pay adds ¢(Bob) at Bob and guards only at Alice, and the swap moves a coin between two parties by the will of the two. An issuer is not asked when its coin moves. A coin is therefore money rather than a promise between two people. 3.5. The Conditions Every Act-Schema Contract Meets Of the eight conditions of Section 1, (1), (2) and (4) are met by every contract written as act schemas, and so is (5), in that nobody is bound who has not adopted the contract, by two properties of the language. Both are about the protocol a contract realises, so both are stated and proved in Section 5, where that protocol is defined, and used here. Conditions (3), (6), (7) and (8) are those of Section 3.6. The first property is that nothing but a party bears an effect of an act: an agent’s state changes only under a schema of the contract and only in a role of it, which is Proposition 16. The second is that the language cannot name a person. The roles R, the party variables X and the speech-act variables Y are disjoint from Π, and a schema is written over the atoms over them, so no schema mentions a party; and by Definition 1 every agent begins in the same state s0 = 0. / Permuting the people therefore carries the system to itself, which is Proposition 17, and no party can reach a position another could not, which is Corollary 18. 1. (1) An agreement of man with man. Only people hold states, and by Proposition 16 an agent bears an effect of the contract only as a party and only in a role; by Corollary 18 no party can reach a position another could not. That an agent is a natural person is beyond any text, and is beyond this one. 2. (2) Reciprocal, (4) subject to no external authority. A party consents twice and both consents are its own: adopting the contract is consent to its schemas, and a guarding role is the consent an act asks again. By Proposition 16 nothing binds a party outside a role of a schema, so nothing binds it that its adoption did not, and every participant in an act is a party, so no registry, no log and no timing authority takes part in one; by Corollary 18 no party is privileged by the text. The model holds nothing else to be subject to. That a party is bound only by its own promise, condition (3), is Volition, Definition 8; Proudhon’s reciprocal delivery, that each party has value for value, is a condition on the contract’s content and is not carried over. 3. (5) Freely accepted and signed by all the participants. This is how a contract is entered into rather than what it says. It is a premise here: the people are the parties, each running the protocol because it adopted the contract; and by Proposition 16 nobody else is bound. The remaining conditions do not hold for every contract. A contract with no act by which two strangers can come into relation is written as act schemas as readily as one that has such an act, and fails Introduction. The rest of this paper takes them up. 10

3.6. What We Prove Conditions (3), (6), (7) and (8) of Section 1 become three conditions on a contract’s schemas, and the protocol realising a contract meeting them is grassroots. All three are properties of the text and are decidable, so whether a contract meets them is decided by a checker rather than left to its drafter. This section states them and the theorem; the sections that follow provide what is needed to prove it, and Section 7 proves it. A party’s state names people — its friends, the issuers of the coins it holds, the authors of the items it was sent. A state that names a person stores an identifier of them, in the words of Section 1, and every condition below turns on which people a state names. Definition 4 (Records). A local state records a person q if q is an argument of one of its atoms. A speech act is opaque. D is disjoint from Π, so a person named inside a signed item is not an argument of the atom carrying it and no state records them on its account. A contract records, and its schemas can require, only the arguments of atoms, and an atom has finitely many; a chain of signatures is carried inside a speech act rather than required of one. Introduction. Conditions (6) and (7): any two parties must be able to come into relation by an act of their own: some act of the contract, willed by both, that leaves each recording the other, e.g. befriending and a swap of coins issued by their givers. Definition 5 (Introductory act). A schema τ of C of arity two, guarded in both roles, is an introductory act if any two people p ̸= q have an introduction: a binding β of τ into {p, q} that sends π1 to p and π2 to q, under which some atom added at π1 names q and some atom added at π2 names p. Having such an act is not enough, because it may be out of reach: it may require an atom a party cannot obtain, or forbid one that somebody else can put there and leave. The condition is that neither happens. Definition 6 (Unobstructed). An introductory act τ of C is unobstructed if any two people p ̸= q have an introduction β such that, at each role πi of τ: 1. every atom τ requires at πi is, under β , added by some schema of C of arity one that is guarded in its role and requires and forbids nothing, at the binding that sends its role to β (πi ); 2. every schema of C that, at some binding, adds at β (πi ) an atom τ forbids at πi has, at that binding, the other of p and q in a role and adds at β (πi ) an atom naming them. The second clause exists against an atom somebody else can put in a party’s state and leave there. It excepts an act that puts it there while bringing the two parties together anyway: its binding gives the other party a role, and the atom it adds names that party, so every transaction it determines changes the state of both and leaves the first recording the second — an interaction between them. Befriending at the binding that swaps its two roles is one such act, and so is any more guarded act that specialises the introduction, such as a befriending that also takes the parents’ will. Provenance. Condition (8): a record may name a person its holder has never dealt with: a coin that changed hands, an item forwarded from a friend. Such a record must be

11

traceable to someone who was there — either the act that made it had that person as a party, or another party to the act already held a record naming them. Definition 7 (Traceable provenance). Write ΦE for the atoms over R ∪ X ∪ Y whose predicate is in E. A set E ⊆ Σ has traceable provenance in a contract C if for every schema τ of C with roles π1 , . . . , πk , every i, every ϕ ∈ +(i) ∩ ΦE and every argument u of ϕ in R ∪ X with u ̸= πi , u ∈ {π1 , . . . , πk }

or

u is an argument of some ψ ∈ (=( j) ⊎ −( j)) ∩ ΦE , some j.

A predicate has traceable provenance in C if it belongs to such a set, and an atom is said to have it when its predicate does. A predicate whose atoms are added only with roles among their arguments has traceable provenance. The condition is weaker: an act may give a party a record of someone it does not yet record, provided another party to that act records them already. Volition. Condition (3): an act that not all its parties are asked about must run only between parties that already record each other — unfriending and forwarding between friends, paying from a holder of the payee’s coins. Definition 8 (Volition). The role graph of a schema is the undirected graph on its roles with an edge between πi and π j when one of the two requires an atom of traceable provenance with the other among its arguments. A contract C satisfies volition if every schema of it of arity two or more is guarded in all its roles or has a connected role graph. The role graph is the undirected graph formed by the identifiers the parties store, of Section 1, taken on the roles of one schema. For a schema of arity two it is connected exactly when one of its two roles requires such an atom naming the other. Above that arity connectedness is weaker than asking it of every pair, and Proposition 29 uses it: lying in one instance is an equivalence, so a path through the roles puts all the participants there. Definition 9 (Syntactically grassroots). A contract is syntactically grassroots if it has an unobstructed introductory act and satisfies volition. A social contract written as act schemas is a grassroots social contract when it is syntactically grassroots, and the compilation of Section 5 is defined for such contracts. Theorem 10 (Grassroots realisation). The protocol realising a syntactically grassroots social contract is volitionally grassroots. The rest of the paper is dedicated to proving this theorem. Whether a contract is syntactically grassroots is decidable, and a checker deciding it accompanies this paper, at https://github.com/EShapiro2/GLP/tree/main/ programs/jurix. It certifies both contracts of Section 2, with the sets of predicates of traceable provenance that Section 7 states. Everything the three conditions quantify over is finite once the bindings are taken up to renaming: an introductory act is an assignment of a schema’s party variables to its two roles; unobstructed is the matching of one atom against those the finitely many schemas add; volition is a connectivity check on the roles. Traceable provenance is the one that is not a single pass — the largest set of predicates having it is reached by dropping any predicate that fails the condition and repeating, which ends because there are finitely many.

12

Section 4 recalls what grassroots means and Section 5 says what the protocol realising a contract is. Section 6 proves the theorem the proof rests on, and Section 7 proves this one. 4. Volition-Guarded Transactions and Grassroots Protocols This section recalls from [10] what the statements below use, in brief. Nothing in it is ours. Appendix A states the same notions formally, together with the results used in the proofs of Section 6, so that the paper is self-contained; the proofs of those results are in [10] and are not repeated. Throughout, Π is a potentially infinite set of agents, an agent being a person operating a machine, and P ⊂ Π ranges over its finite nonempty subsets. SP is the set of total functions from P to S, and c p is the value of c at p. A local-states function S maps every P ⊂ Π to a set S(P) of local machine states containing the initial state s0 , with P ⊂ P′ implying S(P) ⊂ S(P′ ). A machine transaction over participants Q is a pair d → d ′ ∈ (SQ )2 with d ̸= d ′ ; it is unary if |Q| = 1. A volitionguarded transaction is a pair (t, Q′ ) of a machine transaction t over Q with its guards Q′ ⊆ Q: the people in Q′ must be willing for it to be taken. A transaction equivalence ∼ relates transactions with the same participants and has countably many classes; a person wills a class, and taking one member of it fulfils that will. For a set R of volition-guarded transactions over S and P ⊂ Π, we write R(P) for those of them whose transactions are over S(P′ ) for some P′ ⊆ P. An agent state is a pair of a volitional state, a set of classes the person is willing their machine to take part in, and a machine state. A set of volition-guarded transactions over a local-states function induces, for each P, a transition system whose configurations are agent configurations over P and whose transitions are volition changes, by which a person by themselves alters their volitional state, and volitional machine transactions, each induced by a volition-guarded transaction whose guards all hold its class. A transaction is machine-enabled in a configuration whose machine states restrict on the participants to its source, and enabled if in addition every guard holds its class. The family of these systems, one per P, is the protocol F over the set, F (P) being its member at P; runs are safe when consecutive states form transitions, live when no class stays enabled forever without a member being taken, and correct when both. Definition 11 (Interaction, Interactive Run, First Interaction [10]). Let Q ⊂ Π. For a configuration c over Q and Q′ ⊆ Q, write c|Q′ for the restriction of c to Q′ . A transition e → e′ of F (Q) is an interaction between x ̸= y ∈ Q if e|{x} ̸= e′ |{x} and e|{y} ̸= e′ |{y} , and e|{x} → e′ |{x} is not a transition of F ({x}) or e|{y} → e′ |{y} is not a transition of F ({y}). It is an interaction between disjoint nonempty P, P′ ⊆ Q if it is an interaction between some x ∈ P and some y ∈ P′ . A run r̂ of F (Q) is interactive between P and P′ if some transition of r̂ is an interaction between them; the first interaction of P and P′ in r̂ is the first such transition. Definition 12 (Interaction Graph, Instance, Coalescence [10]). Let F be a protocol, Q ⊂ Π, and r a prefix of a run of F (Q). The interaction graph of r has vertices Q and an edge between a ̸= b ∈ Q whenever some transition of r is an interaction between a and b. A nonempty P ⊆ Q is an instance in r if it is a connected component of the interaction graph of r. Disjoint nonempty P, P′ ⊆ Q coalesce in a run r̂ of F (Q) if they are instances in some prefix of r̂ and lie in one component of the interaction graph of a longer prefix of r̂. 13

A protocol is oblivious if any interleaving of correct runs of two disjoint groups is a correct run of the two together, interactive if two groups that have not yet interacted can always still do so, and grassroots if it is both. It is volitionally grassroots if it is grassroots and the first interaction of two groups is induced by a transaction guarded by a member of each, so groups become connected only by mutual consent. In a grassroots protocol two instances can always coalesce. 5. Compiling Schemas into Transactions Act schemas have no operational semantics of their own: a schema of a syntactically grassroots contract means the volition-guarded transactions it compiles to, and those have the semantics of [10]. The compilation is defined for syntactically grassroots contracts, so a contract is checked before it is compiled. SC is a local-states function in the sense of Appendix A: s0 ∈ SC (P) for every P, and P ⊂ P′ implies SC (P) ⊂ SC (P′ ), strictly, provided some predicate has positive arity — for q ∈ P′ \ P and such a predicate, an atom with q among its arguments gives a state in SC (P′ ) and not in SC (P). 5.1. The Compilation Compilation maps an act schema of a syntactically grassroots contract to a volitionguarded multiagent atomic transaction [10]. Definition 13 (Compilation). Let τ be a schema with roles π1 , . . . , πk , β a binding for it, and pi := β (πi ). A machine transaction d → d ′ over {p1 , . . . , pk } is determined by τ at β if for every i β (=(i) ⊎ −(i)) ⊆ d pi , d ′pi =

β (¬(i)) ∩ d pi = 0, / β (+(i)) ∩ β (−(i)) = 0, /
d pi \ β (−(i)) ⊎ β (+(i)),

and the volition-guarded transaction it determines is the pair of it with {β (π) : π a guarding role of τ}. In the notation of [10], τ compiles to c′πi := (cπi \ −(i)) ⊎ +(i) (1 ≤ i ≤ k), provided =(i) ⊎ −(i) ⊆ cπi and ¬(i) ∩ cπi = 0/ (1 ≤ i ≤ k), guarded by the guarding roles of τ, which at a binding β denotes the volition-guarded transactions determined by τ at β . A contract compiles schema by schema. A schema with no guarding role compiles to transactions with an empty guard, which are enabled whenever they are machine-enabled and are then eventually taken: the act is the machines’. Definition 14 (Realisation of a contract). Let C be a syntactically grassroots contract. Its realisation RC is the set of volition-guarded transactions determined by the schemas of C at all bindings for them, with the equivalence ∼ relating two of them when one schema at one binding determines both. The protocol realising C is the volitional transactionsbased protocol over RC , SC and ∼. A set of volition-guarded transactions over SC with an equivalence ∼ is well formed if distinct machine transactions underlying it have disjoint P-closures for every P ⊂ Π, and ∼ is a transaction equivalence with finitely many classes over any P, which is what Definition 43 asks of it. 14

Lemma 15 (The translation is well defined). RC with ∼ is well formed. Proof. Let d → d ′ be determined by τ at β , with participants Q the people in its roles, and let P′ be Q together with the people β assigns to the party variables of τ and the arguments of the atoms of d. Every atom of every d ′p is an atom of d p or the image under β of an atom added in a role, so its arguments lie in P′ , as do those of every atom of d, and d → d ′ is a machine transaction over Q and SC (P′ ). By Definition 13 the state of every participant changes, so the participants of a machine transaction are exactly the agents that are not stationary in any transition of its Pclosure. A transition lying in the closures of two of them therefore forces the two to have the same participants and the same restriction to them, hence to be equal, and the closures of distinct machine transactions are disjoint — which is what Definition 43 requires of RC . Two transactions determined by one schema at one binding have the participants of that binding, so equivalent transactions have the same participants, and ∼ is an equivalence by construction. A contract has finitely many schemas and a schema admits finitely many bindings into a finite P, so the classes over P are finitely many, as the countability requirement on a transaction equivalence asks. 5.2. Two Examples With Alice and Bob standing for the parties in those roles, befriend (Section 3.3) compiles to c′Alice := cAlice ⊎ {friend(Bob)},

c′Bob := cBob ⊎ {friend(Alice)},

provided friend(Bob) ∈ / cAlice and friend(Alice) ∈ / cBob ,

guarded by {Alice, Bob},

and denotes, for every d with friend(Bob) ∈ / dAlice and friend(Alice) ∈ / dBob , the volition′ = dAlice ⊎ {friend(Bob)} and guarded transaction (d → d ′ , {Alice, Bob}) with dAlice ′ dBob = dBob ⊎ {friend(Alice)}. There is one for every admissible d, since the two may befriend whatever other friends each has, and ∼ relates them all: they are one act of befriending, available at different points of a run. The swap (Section 3.4) compiles to c′Alice := (cAlice \ {¢(u)}) ⊎ {¢(v)},

c′Bob := (cBob \ {¢(v)}) ⊎ {¢(u)},

provided ¢(u) ∈ cAlice and ¢(v) ∈ cBob ,

guarded by {Alice, Bob}.

The bindings with u = v determine nothing, by Definition 13: a swap of a coin for a coin of the same issue changes no state. The swap at u = Alice and v = Bob is the mutual credit line. 5.3. Every Participant Is a Party Throughout, C is a syntactically grassroots contract, F the protocol realising it and P ⊂ Π. No act reaches anyone who is not a party. Proposition 16 (Every participant is a party). Every agent whose machine state a transition of F (P) changes is assigned to a role of a schema of C by some binding. Proof. A volition change leaves every machine state unchanged (Definition 38), so a transition changing one is a volitional machine transaction induced by some (t, Q′ ) ∈ RC (P), and by that definition it leaves the machine state of every agent outside the participants of t unchanged. By Definition 14 t is determined by a schema τ of C at a binding β , and by Definition 13 the participants of t are the people β assigns to the roles of τ. 15

An agent therefore bears an effect of the contract only under a schema of it, and only in a role. The second property of Section 3.5 is that the schemas single out no agent. A permutation σ of Π extends to atoms, by permuting the arguments in Π and fixing those in D, and to states, configurations, transactions and runs componentwise. Proposition 17 (Anonymity). For every permutation σ of Π, σ (RC ) = RC , σ (c0 (P)) = c0 (σ (P)), and σ carries the runs of F (P) to the runs of F (σ (P)). Proof. σ maps Σ[P ∪ D] bijectively onto Σ[σ (P) ∪ D], hence SC (P) onto SC (σ (P)), and fixes s0 = 0; / so σ (c0 (P)) = c0 (σ (P)). Let t be determined by a schema τ at a binding β . Then σ ◦ β is again a binding for τ, being injective on the roles and leaving Y mapped into D. Each clause of Definition 13 is an inclusion, a disjointness or an identity between images under β and the local states of d and d ′ , and σ is a bijection on atoms, so applying it to both sides of each shows σ (t) determined by τ at σ ◦ β . The guarding roles of τ do not depend on the binding, so σ carries the volition-guarded transaction at β to the one at σ ◦ β ; by Definition 14 σ (RC ) ⊆ RC , and σ −1 gives the reverse inclusion. Two members of RC are ∼-related exactly when one schema at one binding determines both, a condition σ preserves, and RC (P) is carried to RC (σ (P)) because σ carries SC (P′ ) to SC (σ (P′ )) for every P′ ⊆ P. The volitional construction and the P-closure are defined from RC (P), ∼ and c0 (P) only, so σ carries F (P) to F (σ (P)) and runs to runs. Corollary 18 (No privileged party). If a configuration is reachable in a run over P, so is its image under every permutation of P. Proof. Extend the permutation of P by the identity on Π \ P and apply Proposition 17, which carries the run to a run over P ending in the image configuration. Conditions (1), (2), (4) and (5) of Section 1 follow from these two properties, as Section 3.5 sets out. What does not follow is that the protocol realising the contract is grassroots. 6. Polite Sets of Volition-Guarded Transactions Here we prove that the following condition on a set of volition-guarded transactions makes the protocol over it volitionally grassroots: (1) any two agents can always come to interact, and (2) no act joins two instances unless all its participants will it. Section 7 gives conditions on the acts of a contract sufficient for its compiled volition-guarded transactions to satisfy it, and both contracts of Section 2 satisfy it. Two graphs carry the argument: the interaction graph of Section 4, undirected, whose connected components are the instances; and the directed graph of who holds a record of whom, defined next. Throughout this section, S is a local-states function, R a set of volition-guarded transactions over S with equivalence ∼, and F the protocol over R, S and ∼. The proofs use three results of [10] recalled in Appendix A. Definition 19 (Records). A machine state s records an agent q ∈ Π if s ∈ / S(P) for every P ⊂ Π with q ∈ / P. Definition 20 (Recording graph). The recording graph of a machine configuration d is the directed graph on Π with an edge p → q whenever d p records q. The recording graph of an agent configuration is that of its machine states, and the recording graph of a run is the union of the recording graphs of its configurations. 16

Definition 21 (Mutual recording). A volition-guarded transaction (d → d ′ , {p, q}) over participants {p, q}, p ̸= q ∈ Π, is a mutual recording of p and q if it changes the state of each and the recording graph of d ′ has the edges p → q and q → p. A state records q when it could not have arisen among agents that leave q out: every set of agents whose states include it contains q. The recording graph of the initial configuration is empty, since s0 ∈ S(P) for every P. In the social graph of Section 3.3 the edges out of a party are its friends; in the currency of Section 3.4 they are the issuers of the coins it holds. A mutual recording is an act of two agents, willed by both, after which there is an edge each way between them: befriending is one, and a swap of coins the two have issued is another. An edge may point at an agent its source has never transacted with—a message signed by one friend and forwarded by another, a coin that has changed hands—and nothing below forbids it. The recording graph of a configuration is not monotone along a run, as an act may delete the atoms an edge rests on; the recording graph of a run and the interaction graph are monotone by construction. Let Q ⊂ Π. Lemma 22 (A Mutual Recording is an Interaction). Every transition of F (Q) induced by a mutual recording of p and q in R(Q) is an interaction between p and q. By Definition 11 it is then an interaction between any two disjoint sets of agents one of which holds p and the other q. Proof. The machine states of p and of q both change, by Definition 21. Since d ′p records q, d ′p ∈ / S(P) for every P with q ∈ / P, and in particular d ′p ∈ / S({p}); the machine states of every configuration of F ({p}) lie in S({p}) by Definition 50, so the restriction of the transition to p is no transition of F ({p}). By Definition 11 the transition is an interaction between p and q, hence between any two disjoint sets of agents one of which holds p and the other q. Definition 23 (Open, Closed, Polite). The set R is: 1. open if for any two agents p ̸= q in any Q ⊂ Π, every finite safe run of F (Q) with no interaction between p and q has a finite safe extension, by volition changes and unary transitions, at whose end some transaction of R(Q) whose induced transitions are interactions between p and q is machine-enabled; 2. closed if for every Q ⊂ Π, every transaction of R enabled at the end of a finite safe run of F (Q) is guarded by all its participants or has them all in one instance in that run; 3. polite if it is open and closed. Openness says that any two agents can always be brought, by zero or more acts each takes independently, to a configuration at which an act coupling the two can be taken if all whose will it asks are willing. It does not require that no one else take part in the act: a mutual recording is one, and so is any act that leaves one of them holding a record of the other, whoever else takes part. Two agents that have already taken part in one act are asked nothing: they have already met, and being interactive requires no more of them. Closure says that an act not willed by all its participants is enabled only where they already lie in one instance. Theorem 24 (Polite). The protocol over a polite set of volition-guarded transactions is volitionally grassroots. 17

Proof. Let R be polite. One fact is used throughout: an agent whose state a volitional machine transaction changes is a participant of the transaction inducing it, as only a participant changes machine state and only a participant holds its class in its volitional state (Definitions 37 and 38). Oblivious. Let P, P′ ⊂ Π be disjoint and nonempty, r a correct run of F (P), r′ a correct run of F (P′ ), and e = e0 , e1 , . . . an interleaving of r and r′ , with index sequences (ik ) and ( jk ). By Lemma 52, every finite prefix of e is a finite safe run of F (P ∪ P′ ). Every transition of e is a P-step or a P′ -step and so alters the state of agents of one group only, so no transition of e is an interaction between an agent of P and an agent of P′ , and no instance in a prefix of e holds agents of both. We verify the hypothesis of Proposition 53. Let [t] be a class of TR(P∪P′ ) /∼ whose transactions have participants Q meeting both P and P′ —the same Q for every member of the class, by Definition 36—let (t ′′ , Q′′ ) ∈ R with t ′′ ∈ [t], and take a ∈ Q ∩ P. Suppose (t ′′ , Q′′ ) is enabled at some ek . Its participants Q meet both groups and no instance in the prefix of e ending at ek holds agents of both, so they do not all lie in one instance in that prefix; by closure Q′′ = Q, and hence a ∈ Q′′ . Since Q meets P′ , t ′′ ∈ / R(P), so [t] ∈ / TR(P) /∼; and by Lemma 51 applied to r, ek va = (cik )va ⊆ TR(P) /∼. Hence [t] ∈ / ek va ′′ ′′ and the guard on a fails, so (t , Q ) is not enabled at ek —a contradiction. So no class whose transactions have participants in both groups is ever enabled in e, and by Proposition 53, F is oblivious. Interactive. Let Q ⊂ Π, let P, P′ ⊆ Q be disjoint and nonempty, let r̂ be a prefix of a correct run of F (Q) containing no interaction between P and P′ , and take p ∈ P and q ∈ P′ . An interaction between p and q is one between P and P′ by Definition 11, so r̂ contains none, and by openness some finite safe extension of r̂ by volition changes and unary transitions ends where some (t, Q′ ) ∈ R(Q) whose induced transitions are interactions between p and q is machine-enabled. A volition change and a unary transition each alter one agent only, and are therefore no interaction between P and P′ . Extend further by a volition change of each agent of Q′ , where needed, so that [t] lies in the volitional state of each; these leave every machine state unchanged, so (t, Q′ ) is now enabled. Extend by the volitional machine transaction it induces, an interaction between p and q and hence between P and P′ . The result is a finite safe run of F (Q) having r̂ as a prefix and containing an interaction between P and P′ , and by Lemma 40 it is a prefix of a correct run of F (Q). Hence F is interactive, and with obliviousness, grassroots. Volitionally grassroots. Let P, P′ ⊂ Π be disjoint and nonempty, let r̂ be a safe run of F (P ∪ P′ ) interactive between P and P′ , and let e → e′ be its first interaction. It changes the state of an agent of P and of an agent of P′ , and a volition change alters one agent only, so it is a volitional machine transaction induced by some (t, Q′ ) ∈ R(P ∪ P′ ) whose participants Q meet both groups; take a ∈ Q ∩ P and b ∈ Q ∩ P′ . The participants of t do not all lie in one instance in the prefix ρ of r̂ ending at e: were they, a and b would lie in one connected component of the interaction graph of ρ; every agent of ρ is in P ∪ P′ , so a path from a to b in that component has an edge between some x ∈ P and some y ∈ P′ , and the transition of ρ that puts that edge there is an interaction between x and y, hence between P and P′ , and it precedes e → e′ — contradicting that e → e′ is the first. As (t, Q′ ) is enabled at e, by closure Q′ = Q, which meets both P and P′ . Hence F is volitionally grassroots.

18

Politeness is a condition on the transactions of a protocol. Being grassroots is a property of its runs. The theorem states that the first is sufficient for the second. Section 7 takes the step before it, from the acts of a contract to the transactions realising them. 7. Conditions Sufficient for Openness and Closure We are now ready to prove Theorem 10, restated. Openness and closure are conditions on runs; the three conditions are on the schemas, and each half of the proof carries one across: openness comes from the unobstructed introductory act, and closure from volition. Throughout this section C is a syntactically grassroots contract and F the protocol realising it. Theorem 10 (Grassroots realisation). The protocol realising a syntactically grassroots social contract is volitionally grassroots. Lemma 25 (Records). On local states, Definitions 19 and 4 agree. Proof. Suppose q is an argument of an atom of s, as Definition 4 asks, and let P ⊂ Π with q ∈ / P. That atom has an argument outside P, so s ∈ / SC (P) by Definition 1. As P was arbitrary, s records q. Suppose q is an argument of no atom of s, and let P be the set of arguments of the atoms of s together with some person other than q, which exists as Π is infinite. Then P is nonempty, q ∈ / P and s ∈ SC (P), so s does not record q. The recording graph of a configuration of the protocol realising C therefore has an edge p → q exactly when some atom of the state of p has q among its arguments. Its edges divide by the predicate the atom carries. Definition 26 (E-recording graph). Let E be a set of predicates. The E-recording graph of a configuration is the spanning subgraph of its recording graph whose edges p → q are those for which the state of p contains an atom with predicate in E having q among its arguments; the E-recording graph of a run is the union of those of its configurations. Proposition 27 (Openness). RC is open. Proof. Let τ be one, let p ̸= q in Q, let r be a finite safe run of the protocol over Q containing no interaction between p and q, and let β be an introduction of p and q meeting Definition 6. Extend r, for each role πi of τ and each ϕ ∈ =(i) ⊎ −(i), by a volition change of β (πi ) and the unary transition adding β (ϕ) there, which that agent takes by itself and which is machine-enabled, its schema requiring and forbidding nothing. Such a schema deletes nothing, so the extension is finite and safe and every atom τ requires at β is present at its last configuration. Let ϕ ∈ ¬(i) and suppose the state of β (πi ) there contains β (ϕ). The initial state is empty, and the extension adds only the atoms τ requires at β , so some transition of r added it; that transition is induced by a transaction of RC determined by a schema τ ′ at a binding β ′ with β (ϕ) ∈ β ′ (+( j)) for a role sent to β (πi ). By Definition 6 β ′ sends a role of τ ′ to the other of p and q, and β ′ (+( j)) names that party. Both are then participants, so by Definition 13 the state of each changes, and the state of β (πi ) afterwards records the other, so it lies in no S(P) omitting them and the transition restricted to β (πi ) is no transition of that agent’s own transition system: the transition is an interaction between p and q, which r does not contain. So no forbidden atom is present, τ at β is machineenabled at the last configuration of the extension, and every transaction it determines

19

there leaves p holding an atom naming q and q one naming p, changing both states, and is guarded by both; by Lemma 25 each records the other, so it is a mutual recording of p and q in RC (Q), β mapping into {p, q} ⊆ Q, and by Lemma 22 the transitions it induces are interactions between p and q. Closure requires that the participants of an unguarded act already lie in one instance. Where an atom can be laid only by an act of the two people it relates, that follows directly. An edge may also arrive by transfer: a coin passes from hand to hand, and the person it points at is reached through the parties that carried it rather than by a single act. The condition below covers both and secures that no act ever leaves an edge whose ends lie in different instances. Let E have traceable provenance in C, Q ⊂ Π, and r a finite safe run of F (Q). Lemma 28 (No edge crosses instances). Every edge of the E-recording graph of r joins two agents that lie in one instance in r. Proof. The E-recording graph of r is the union of those of its configurations, and every configuration of r ends a prefix of r; the interaction graph of a prefix of r is a subgraph of that of r, so two agents in one instance in a prefix are in one instance in r. It suffices to treat an edge p → q of the E-recording graph of the last configuration. The claim is trivial for q = p, and we argue by induction on the length of r. The initial state is empty, so a run of one configuration holds it vacuously. Let r end with the transition e → c, and let the state of p at c contain an atom with predicate in E and q ̸= p among its arguments. If the state of p at e contains such an atom, the induction hypothesis applied to the prefix of r ending at e gives the claim. Otherwise e → c added it, so it is a volitional machine transaction induced by a transaction determined by a schema τ at a binding β , and the atom is β (ϕ) for an atom ϕ added at a role i, with predicate in E, where p = β (i), and q = β (s) for an argument s of ϕ; as β (s) ̸= β (i), s ̸= i. By Definition 13 the state of every participant changes, and by Lemma 25 the state of p at c records q, so it lies in no SC (P) with q ∈ / P and the restriction of the transition to p is no transition of F ({p}). By Definition 11 the transition is therefore an interaction between p and every other participant. By Definition 7 one of two cases holds. If s is a role of τ then q is a participant, so p and q are joined by an edge of the interaction graph of r. Otherwise s is an argument of an atom ψ required at some role j, with predicate in E; put p′ := β ( j). By Definition 13 β (ψ) is an atom of the state of p′ at e, its predicate is in E and it has q among its arguments, so by the induction hypothesis p′ and q lie in one instance in the prefix ending at e, hence in r. If p′ ̸= p then p′ is a participant, so p and p′ are joined by an edge of the interaction graph of r. Either way p and q lie in one instance in r. Proposition 29 (Closure). RC is closed. Proof. Let (t, Q′ ) of RC be enabled at the last configuration of a finite safe run r of the protocol, determined by a schema τ at a binding β . If τ is guarded in all its roles then (t, Q′ ) is guarded by all its participants. If τ has arity one, its single participant is a connected component of the interaction graph of r by itself or lies in one, so all participants of t lie in one instance in r. Otherwise take an edge of the role graph of τ, joining πi to π j , let πi be the one requiring an atom of traceable provenance with π j among its arguments, and put p := β (πi ) and q := β (π j ). As (t, Q′ ) is machine-enabled

20

at the last configuration of r, the state of p there contains the image under β of that atom, so the E-recording graph of r has the edge p → q for a set E of traceable provenance containing that atom’s predicate, and by Lemma 28 p and q lie in one instance in r. Instances are the connected components of the interaction graph of r, so lying in one instance is an equivalence; the role graph of τ is connected, and β carries a path in it to a chain of agents consecutive ones of which lie in one instance, so all participants of t lie in one instance in r. Proof of Theorem 10. Let C be syntactically grassroots. By Proposition 27 RC is open and by Proposition 29 it is closed, so it is polite, and by Theorem 24 the protocol over it is volitionally grassroots. Openness and closure. Openness lets any person start an instance, and without permission. A contract that gives one party of each instance a standing of its own is not open: two groups with no such party can never become connected. Federated architectures fail on this: each instance has its own server, and two instances remain two [10]. Closure leaves an instance requiring no global resource and no central authority: a registry that issues identifiers, a log that orders acts, or an authority that timestamps them takes part in a transaction without being a party to the contract. Every act of a grassroots social contract is between its parties, so no third party takes part in one. A smart contract that depends on a fact outside the blockchain obtains it from an oracle, a third party whose report the contract cannot check, and the trust the arrangement was built to remove returns at that point [26]; here a fact about the world enters as a party’s signed assertion instead. A smart contract requires a consensus protocol; a contract realised as volitionguarded transactions requires none where the parties transact between themselves [27, 28], and where a collective decision is called for it constitutes its own consensus among the parties [29]. 7.1. The Social Graph Certified Befriend is an introductory act: for any two parties, at the binding sending Alice and Bob to them, every transaction it determines adds friend(Bob) at Alice and friend(Alice) at Bob, changing both states, and it is guarded in both roles, so each is a mutual recording of the two. It is unobstructed: it requires nothing, and the only transactions adding friend(Bob) at Alice are those befriend determines at that binding. Befriend is also the only schema adding a friend atom and that atom’s argument is a role, so friend has traceable provenance. Volition holds, by Definition 8: befriend is guarded in all its roles, sign has arity one, and of the other two, unfriend’s role Alice requires friend(Bob) and forward’s role Bob requires friend(Alice), each an atom of traceable provenance naming the other role. The contract is therefore syntactically grassroots, and by Theorem 10 the protocol realising it is volitionally grassroots, so the platform realising the contract is a grassroots platform. The instances. The introductory act is befriending and the edge each lays to the other is the friend atom, so the friend-recording graph of a configuration is the friendship graph. The instances of a run are the connected components of its friend-recording graph, read undirected. Every interaction of this contract is a befriend, an unfriend or a forward, and each of the three leaves or requires a friend atom between its two participants at some configuration of the run. The other way round, every friend atom was laid by a befriend, which is a mutual recording and so an interaction by Lemma 22. Forwarding 21

lays an edge that is not one of those: it points at the author from the recipient, who has not transacted with them, as a coin does in Section 7.2. The author lies in the same instance nonetheless. The set {friend, item, sent} has traceable provenance: sign adds item(x, Alice, Alice), which names its own role, and forward adds sent(x, Bob) at Alice and item(x, a, Alice) at Bob, whose person arguments are the roles Alice and Bob and the party variable a, which the required item(x, a, f ) names; so Lemma 28 applies. 7.2. The Currency Certified The swap is an introductory act: at the binding sending u to Alice and v to Bob every transaction it determines leaves Alice holding a coin Bob issued and Bob a coin Alice issued, changing both states, and it is guarded in both roles, so each is a mutual recording of the two — the mutual credit line. It is unobstructed: it forbids nothing, and at that binding each role requires a coin of its own issue, which mint adds, mint being of arity one, guarded in its role, and requiring and forbidding nothing. ¢ has traceable provenance. Mint adds ¢(Alice) at Alice and pay adds ¢(Bob) at Bob, each naming the role that holds it; the swap adds in each role a coin the other role requires; and redeem adds ¢(r) at Alice, which role Bob requires, and ¢(Bob) at Bob, naming its own role. Volition holds, by Definition 8: mint has arity one, the swap is guarded in both its roles, and pay and redeem are guarded at Alice only and require there ¢(Bob), an atom of traceable provenance having Bob among its arguments. The contract is therefore syntactically grassroots, and by Theorem 10 the protocol realising it is volitionally grassroots, so the platform realising the contract is a grassroots platform. The origin of a record. A coin and an item are the same object: an atom naming a person who is not a participant, put in a state by an act of two parties. A friend edge can only have been laid by the two people it joins; a coin or an item can be handed on, so an edge may point at a person its source has never transacted with. Traceable provenance covers both. An edge is laid either to a party to the act that lays it or to a person another party to that act records already, so no act ever leaves an edge whose ends lie in different instances, which Lemma 28 proves by induction on the run. For coins the chain is the passage of the coin from its issuer, and conservation of money [10] is the special case: an invariant that here is read off the schemas rather than proved of the runs. Requiring an atom to carry the parties that passed it on is the same condition written as a clause of the contract rather than as one on the schemas [8]. The two differ in one respect: pay deletes the coin from the payer, and forward keeps the item. 8. Clauses and Their Modalities The schemas settle a second question: for each clause, whether a party can breach it, and what record of it the contract leaves in another party’s state. The two contracts already show it. A clause may be one no act of the contract can breach, one a party may breach with the contract recording the breach, or one whose performance lies outside the contract and of which it records only the undertaking. The question is about every clause, not only about those that describe no act. The three say what a realisation does with a clause, not what kind of obligation the clause is: a friendship kept on paper can be entered against a person’s will, and under the schemas of Section 3.3 it cannot. Throughout this section C is a syntactically grassroots contract.

22

Definition 30 (Clause). A clause of a contract C is a proposition about the conduct of its parties, and is kept or breached by that conduct; a party the clause names as answerable is its obligor. The runs of the protocol realising C determine the clause if whether it is kept is a function of the run. A transaction of RC may breach the clause if there are circumstances in which its occurrence puts a party in breach of it. Definition 31 (Witnessed). A volition-guarded transaction (d → d ′ , Q′ ) over participants Q is witnessed against a ∈ Π if the recording graph of d ′ has an edge b → a for some b ∈ Q with b ̸= a. A schema is witnessed against a role if every transaction it determines is witnessed against the person in that role. By Lemma 25 that edge is an atom naming a in the state of another party. A record serves as evidence when it names the party answerable and is held by someone else. Definition 32 (Enforced, Attested, Undertaken). Let ϕ be a clause of C, with obligor o where it has one. Then ϕ is 1. enforced by C if the runs of the protocol realising C determine it and no transaction of RC may breach it; 2. attested by C if some transaction of RC may breach it and every transaction that may is witnessed against o; 3. undertaken by C if no transaction of RC may breach it, the runs do not determine it, and some transaction of RC is witnessed against o. The three are exclusive, and they are not exhaustive. Two kinds of clause fall outside. One that some transaction may breach without witnessing against the obligor can be breached invisibly. One that the runs neither determine nor record is owed by no one identifiable. A contract carrying either has a clause its realisation does nothing with. A schema names its role π j at another role πi if an atom added at πi has π j among its arguments. Proposition 33 (Witnessing). A schema is witnessed against every role it names at another role. Proof. Let τ name π j at πi by an atom ϕ added at πi , let β be a binding for τ, and put a := β (π j ) and b := β (πi ), which differ as β is injective on roles. By Definition 13 every transaction determined by τ at β leaves b with β (+(i)) adjoined, so the state of b after it contains β (ϕ), an atom having a among its arguments, and the recording graph after it has the edge b → a by Lemma 25. A predicate e is guarded in C if whenever a schema of C adds an e-atom, the atom names only roles of that schema that will the act. The consent clause for e says that a party’s state holds an e-atom only if those the atom names willed the act that added it. Proposition 34 (Enforcement by guarding). If e is guarded in C, the consent clause for e is enforced by C. Proof. Let r be a finite safe run of the protocol realising C and let an e-atom occur in the state of a party at some configuration of r. The initial state is empty, so some transition of r added it, and by Definitions 14 and 13 that atom is β (ϕ) for a binding β of a schema τ of C and some ϕ ∈ +(i) with predicate e. By hypothesis every argument of that atom is a guarding role of τ, so every person among the atom’s arguments is β of a guarding

23

role and hence in the guard of the transaction taken; by Definition 44 each held its class in its volitional state at that point, which is to say willed the act. The clauses of the two contracts. Clauses 1 and 2 of Section 2.1 are enforced, by Proposition 34 and by unfriend deleting in both roles. Clause 5 of Section 2.1 is undertaken, forward adding item(x, a, Alice) at Bob and so being witnessed against the party that passed the item on; and so is clause 5 of Section 2.2, a mutual credit line adding ¢(Bob) at Alice and ¢(Alice) at Bob and so being witnessed against both of them. The clause that a coin enters a holding only by its issuer’s will is of no kind, being breachable by pay without pay naming the payer. The remaining clauses permit acts and oblige nothing, so no transaction may breach them and every run keeps them: they are enforced. Attestation and undertaking. The two require the same thing of the schemas — that the act naming the obligor leave the record in another party’s hands — and differ only in whether the breach is itself an act of the contract. The evidence depends on the schemas and the modality on the clause. A performance promised for later is never attested, because failing to perform is not an act; a warranty given in the course of an act is attested exactly when that act is witnessed against the party giving it. Witnessing therefore turns on whether an effect names the party performing the act and not only the parties the atom concerns. Unfriend adds no atom, so no clause against ending a friendship at will can be attested under the contract of Section 2.1; pay adds a coin naming its issuer and not its payer, so no clause against the payer can be attested under the contract of Section 2.2. A contract whose breaches are to be attested must have acts whose effects name their author. Signing provides it: an act taken as a digital speech act, an utterance signed with the key of the party taking it, leaves an atom naming that party, and the signed record is non-repudiable [5,8]. Performance outside the system. Clause 5 of Section 2.2 and the warranty in clause 4 of Section 2.1 are performed outside the schemas altogether — selling at an advertised price is no act of the contract, and neither is knowing a person — and they take different modalities. The first is undertaken: no transaction may breach it, no run determines whether the issuer honours it, and a mutual credit line is witnessed against the issuer, so the coin in another party’s holding is the record of the undertaking. The second is attested: forwarding is an act, a forward by a party that does not personally know the party it received the item from makes the warranty false, and every forward adds item(x, a, Alice) at Bob, so by Proposition 33 it is witnessed against Alice. The three modalities therefore do not divide by whether performance is digital. 9. Related Work Contracts as formal objects. The formal study of contracts in this field is dominated by the contract-as-automaton family. Contract automata [30] give the deontic modalities an operational semantics over the acts of named interactive parties; Flood and Goodenough [31] render a loan agreement as a deterministic finite automaton whose states are performing, delinquent and default and whose transitions are drawn from an alphabet of events; the L4 domain-specific language [32] gives an executable semantics in which deontic clauses with deadlines become states and transitions; and timed contract automata [33] add quantitative time to the same picture. Beside them run the rule-based encodings: contract clauses as defeasible deontic rules with violation and reparation 24

chains [34], and the comparison of imperative with declarative smart contracts running on a distributed ledger [35]. Three commitments are common to all of these, and this paper drops all three. The parties are fixed when the contract is formed, so the object of study is one instance among a known set of parties, where our conditions quantify over the family of systems a contract induces on every finite set of people. There is one contract state — the automaton’s state, the rule base’s facts, the ledger — where the definition of records, and therefore of what it is for two parties to be connected, needs a local state per party and a local-states function monotone in the set of people. And each requires something closure forbids: an alphabet of events every party is assumed to observe alike, a clock, or a ledger. Two languages outside this venue are the nearest neighbours of ours and worth stating exactly. Symboleo [17,18] specifies a legal contract as a set of obligations and powers over an ontology of roles, assets and events, with a semantics of logical axioms on statecharts, and properties verified in temporal logic; its purpose is monitoring, and roles are assigned to parties during each contract execution. Stipula [19] is a domain-specific language built on legal constructs — agreement, permissions, obligations, violations — whose contracts are state machines over parties, fields and linear assets; its agreement operator is the contract’s constructor, fixing the full list of parties, and thereafter each function is invoked by one named party. Catala [36] does the corresponding work for statute rather than contract, encoding the base-case and exception structure of legislation in default logic. Both contract languages make the three commitments above: a Stipula configuration carries a global clock, and Symboleo presupposes a monitor, which is a participant that is not a party. A concrete case makes the first point sharp. Befriending cannot be written in Stipula. It is an act that two parties must both will, available repeatedly between any two of them, and Stipula admits joint consent only in the constructor, so each befriending would be the formation of a new contract rather than a clause of a standing one. We claim no new language. The conditions of Section 7 are read off the four things a schema carries and nothing besides. Stipula’s function declarations name an invoking party and a precondition, and Symboleo attributes obligations to a debtor and a creditor, so the four could be extracted from either given a semantics in which each party holds its own state. The conditions transpose; the frame does not. Norms and normative systems. The formal study of what a contract obliges runs through deontic and defeasible logic, where contracts are represented as defeasible rules with deontic operators and compliance is checked against them [37]. Normative multi-agent systems ask how norms are operationalised, detected, and brought into conflict [38]. Volition-guarded transactions [10] stand beside this literature. A guard is a condition of enactment rather than a deontic operator: an act does not occur unless the people it obliges are willing. Where a clause of the contract describes no act the protocol carries out, Section 8 says what the realisation does with it instead — record its breach, or record the undertaking and the party who gave it — rather than leaving it outside the account. Juridical acts and declarative power. What we call an act is Sartor’s result-declaration, one of “acts intended to produce legal determinations” [39], and the fullest model of it is Hage’s [40], which analyses juridical acts as intentional changes in a world of law furnished with entities, facts and rules. Nor is a multi-party act willed by its parties new here. Declarative power is “the capacity of the power-holder of creating normative 25

positions, involving other agents, simply by ‘proclaiming’ such positions” [41], and its authors observe that a declarative power exercised jointly by several parties, with the consent of each, is a contract [42]. What we do not take from that tradition is where the effect comes from. There a proclamation has effect only if an institution provides for it — “when an agent j proclaims A, j brings it about that A only if the concerned institution s provides for this result” [42] — as in norm-governed institutions “designated agents are empowered to create particular kinds of states of affairs” [43], counts-as statements “hold only with respect to a context” [44], and an artificial institution “presupposes an agreement on an unambiguous definition of a set of concepts” [45]. A grassroots social contract has no such institution, being subject to no external authority, and there is nowhere above the parties to put one. The effect of an act is therefore the change it makes in the parties’ own states, and the condition of its effectiveness is their will and not a conferred power. An act schema is a result-declaration with the institution taken out: its precondition is on each participant’s own local state rather than on an institutionally conferred power, and its guard takes the place of authorisation. Standard-form contracting. A grassroots social contract changes the form. It has no drafting party among the parties, so there is no party whose terms are policed and no party from whom disclosure is required, and what the literature treats as a defect of the arrangement between a person and a proprietor is absent because the proprietor is absent. The End-User Licence Agreement is a contract of adhesion. Radin [46] treats massmarket boilerplate as the deletion of rights that the legal system otherwise confers, and as a matter for the rule of law rather than for consent only. Kim [47] treats the digital instances of the form — the terms accepted by clicking, browsing, or installing — and what assent means when the act of assent is a condition of access. Ben-Shahar and Schneider [48] address the remedy most often proposed, mandated disclosure, and find that it fails: the terms are not read, and requiring more of them is not read either. This literature takes the bilateral form as given; its questions are what may be done within the form: whether assent was real, which terms a court should refuse, what a drafter must disclose. Terms a machine can evaluate. Surden [49] separates the terms of a contract a machine can evaluate from those it cannot; work on smart legal contracts separates the operational parts of an agreement, which code executes, from the rest, which stays in prose [50]; and in security, Schneider [51] characterises the policies an execution monitor can enforce. Each divides a contract’s terms in two, by what a realisation can do with them. Section 8 divides clauses in three, and the extra line falls inside the realisation: between a clause no act of the contract can breach and a clause a party may breach while the contract records the breach against them. The second class is the one a two-way division has no room for, and it is the class the law needs: a remedy requires a provable breach and an identifiable obligor. The monitoring literature reaches the same boundary from the other side. There, compliance is computed by monitors that “receive inputs from trusted observers” [52], and where the timestamps cannot be trusted the response is to make the monitor robust rather than to remove it: compliance “is typically computed with respect to timed event traces with event timestamps assumed to be perfect”, and the remedy offered is a semantics for compliance when they are not [53]. A monitor is a participant that is not a party, and closure forbids one. Here the record is held by the parties themselves, and what 26

makes it evidence is Definition 31: it names the party answerable and it lies in someone else’s hands. Code as a regulator. Lessig [54] argued that architecture regulates conduct as law, markets and norms do, and that in the digital realm the architecture is code. A grassroots social contract is not code: the conditions of Section 7 concern who may take part in an act and whose will is required for it, rather than what the code makes a party do, and they are checked on the text rather than on the code. The digital social contract [5] takes the strongest version of the identification: the contract is a program, and a party can behave only according to it; the smart contract literature [55] pursues the same on a blockchain. Self-governance without an external authority. Ostrom [56] documented communities that devise, adopt and enforce their own rules over shared resources, without an owner and without a state administering them, and identified the conditions under which such arrangements endure. That a community constitutes itself is the same claim in the digital realm, and openness is its formal counterpart: any two people can come to record each other by acts of their own, so any person may start an instance and instances coexist. Commons scholarship concerns how a resource is governed in common, for physical resources [56] and for knowledge and networked production [57,58]; a grassroots social contract governs a relationship rather than a resource, and holds where nothing is held in common. The regulatory literature on platforms proceeds otherwise, by binding the operator: the General Data Protection Regulation [59] imposes duties on the party that processes personal data, and that route presupposes the party it regulates. Where a community’s platform is constituted from its members’ own devices [2,3,4], there is no operator to bind. Grassroots systems. The notion of a grassroots protocol is due to [2] and was recast in terms of interleaving and coalescence in [10], which also introduced volition-guarded transactions and volitionally grassroots protocols. Grassroots platforms have been specified for social networking [7,11] and for personal cryptocurrencies [9,28,12]. Three things are added here. Politeness is a condition on a protocol’s transactions, and Theorem 24 proves it sufficient for the protocol to be grassroots, so no proof about runs is needed. The second is the step before the specification: the legal text, and decidable conditions on it under which politeness is established from the acts rather than from the protocol. The third is what a realisation does with a clause of the contract, whether or not the contract provides an act for it, which depends on the same schemas. Neighbouring instruments. Four instruments stand near a grassroots social contract, and each differs in what it does rather than in how it is drafted. A licence states what one party may do with something another party is entitled to: the General Public License [60] presupposes the copyright it licenses, grants freedoms on conditions, and binds a taker because they would otherwise infringe. A grassroots social contract licenses nothing, and its obligations are owed by each party to every other and derive from no party’s prior entitlement, so a person who has never held any right that the others could infringe is bound exactly as the rest are. Bylaws bind the members of an association symmetrically and are adopted on joining, which makes them the closest neighbour, but they presuppose an association: an entity with legal personality, organs that act for it, and a membership register. A code of conduct states standards of behaviour, and its sanction is exclusion administered by whoever runs the forum, which is the party a grassroots social contract 27

does not have; terms of membership presuppose the same party, in its capacity as the one who admits. 10. Conclusion Proudhon’s conditions on a social contract, with two more, formalised as conditions on its acts, give it the property he envisioned for it: any two people may come into relation without anyone’s leave, two communities that adopted the contract independently can later become one, and every participant in an act is a party. A grassroots social contract is one meeting the conditions, and its realisation has all three. Such a contract has two artefacts, a legal text and a protocol realising it, and the grassroots literature has had only the second. This paper provides the passage between them. A clause of the text describes an act, and the acts become act schemas; the schemas compile into volition-guarded transactions over a local-states function in which a state records exactly the people its atoms name; and three conditions on the schemas make a contract syntactically grassroots, which is enough for the protocol realising it to be volitionally grassroots. The compilation and the conditions are algorithmic and the conditions are decidable, so a contract can be certified from its text, and the only step left to judgement is the first, rendering a text as schemas. The same schemas settle a second question. A contract binds its parties to clauses, some of which describe no act, and what its realisation does with a clause — leave it unbreachable, record its breach against the party in breach, or record the undertaking and who gave it — depends on the schemas too, and on one thing: whether the act that names the party answerable leaves the record in another party’s hands. Attestation and undertaking require exactly that of the schemas, and differ only in whether the breach is itself an act of the contract. Both contracts are certified from their schemas. Who holds a record of whom is a directed graph, and an instance is a connected component of the undirected graph of interactions. In the social graph the two coincide: befriending is the introductory act, and a friend edge can only have been laid by the two people it joins. A coin can be handed on and so can a signed item, so an edge may point at a person its source has never transacted with; an edge is laid either to a party to the act that lays it or to a person another party to that act records already, and that condition, read off the schemas, is enough for no edge ever to cross two instances. For coins it is conservation of money. The conditions also leave no participant that is not a party. Openness lets any person start an instance, and without permission. Closure leaves an instance requiring no registry that issues identifiers, no log that orders acts, and no authority that timestamps them, each of which would take part in an act without being a party to the contract. A community organised in this way requires no permission to form, no authority to operate, and no proprietor to govern it. Three further directions follow. The conditions are sufficient and not necessary, and a characterisation would say exactly which contracts are grassroots. Which further invariants of a contract can be read off its schemas, as conservation of money now is, is open. And the four things a schema carries are present, under other names, in the contract specification languages of Section 9; giving one of them a semantics in which each party holds its own state would let the conditions be checked on contracts already written in it.

28

References [1] [2]

[3]

[4] [5]

[6] [7] [8] [9] [10]

[11] [12] [13] [14]

[15]

[16] [17]

[18] [19] [20]

[21]

[22]

Proudhon PJ, Robinson JB. General idea of the revolution in the nineteenth century. Courier Corporation; 2004. Original work published 1851. Shapiro E. Grassroots Distributed Systems: Concept, Examples, Implementation and Applications (Brief Announcement). In: 37th International Symposium on Distributed Computing (DISC 2023). (Extended version: arXiv:2301.04391). Italy: LIPICS; 2023. p. 47:1, 47:7. Available from: https://arxiv.org/ abs/2301.04391. Shapiro E. A Grassroots Architecture to Supplant Global Digital Platforms by a Global Digital Democracy. arXiv:240413468, Proceedings of DAWO’24. 2024. Available from: https://arxiv.org/abs/ 2404.13468. Shapiro E. Characterising Global Platforms: Centralised, Decentralised, Federated, and Grassroots. arXiv preprint arXiv:251103286. 2025. Available from: https://arxiv.org/abs/2511.03286. Cardelli L, Orgad L, Shahaf G, Shapiro E, Talmon N. Digital social contracts: A foundation for an egalitarian and just digital society. In: CEUR Proceedings of the First International Forum on Digital and Democracy. vol. 2781. CEUR-WS; 2020. p. 51-60. Available from: https://ceur-ws.org/ Vol-2781/paper5.pdf. Shapiro E. Volition Elicitation: Operational Semantics for People and Their Machines; 2026. arXiv:2607.14138. Available from: https://arxiv.org/abs/2607.14138. Shapiro E. Grassroots Social Networking: Serverless, Permissionless Protocols for Twitter/LinkedIn/WhatsApp. In: OASIS ’23. Association for Computing Machinery; 2023. . Golike J, Shapiro E. Digital Speech Acts Retain Control of Copyright with People, Not Platforms. arXiv preprint arXiv:260619263. 2026. Available from: https://arxiv.org/abs/2606.19263. Shapiro E. Grassroots Currencies: A Foundation for a Grassroots Digital Economy. arXiv preprint arXiv:220205619. 2022. Available from: https://arxiv.org/abs/2202.05619. Lewis-Pye A, Shapiro E. Volition-Guarded Multiagent Atomic Transactions: Describing People and their Machines. arXiv preprint arXiv:260425596. 2026. Available from: https://arxiv.org/abs/ 2604.25596. Eitan O, Keidar I, Shapiro E. The Grassroots Social Graph: A Secure Operating System for Multiagent, Distributed, Peer-to-Peer, Smartphone-Based Platforms; 2026. In preparation. Shapiro E. Grassroots Bonds as a Foundation for Market Liquidity; 2026. arXiv:2603.13671. Available from: https://arxiv.org/abs/2603.13671. Shapiro E. Child-Safe Social Networking: From a Grassroots Social Contract to an App. In preparation. 2026. Sapkota R, Roumeliotis KI, Karkee M. Vibe Coding vs. Agentic Coding: Fundamentals and Practical Implications of Agentic AI; 2025. ArXiv:2505.19443. Available from: https://arxiv.org/abs/ 2505.19443. Fowler M. Understanding Spec-Driven-Development: Kiro, spec-kit, and Tessl. MartinFowlercom. 2025 October. Analyzes the shift toward using formal specifications and types as the primary interface for AI code generation. Available from: https://martinfowler.com/articles/exploring-gen-ai/ sdd-3-tools.html. GitHub. Spec Kit: Toolkit for Spec-Driven Development; 2025. Available at https://github.com/ github/spec-kit. GitHub repository. Sharifi S, Parvizimosaed A, Amyot D, Logrippo L, Mylopoulos J. Symboleo: Towards a Specification Language for Legal Contracts. In: IEEE 28th International Requirements Engineering Conference (RE). IEEE; 2020. p. 364-9. Parvizimosaed A, Sharifi S, Amyot D, Logrippo L, Roveri M, Rasti A, et al. Specification and Analysis of Legal Contracts with Symboleo. Software and Systems Modeling. 2022;21. Crafa S, Laneve C, Sartor G. Pacta sunt servanda: Legal Contracts in Stipula. Science of Computer Programming. 2022. ArXiv:2110.11069. Available from: https://arxiv.org/abs/2110.11069. Shapiro E. GLP: A Grassroots, Multiagent, Concurrent, Logic Programming Language for AI (full version). arXiv preprint arXiv:251015747, Summary in Proc of ICLP’26, EPTCS 450, pp 119–133. 2025. Available from: https://arxiv.org/abs/2510.15747. Shapiro E. Implementing Grassroots Logic Programs with Multiagent Transition Systems and AI (Full Version). arXiv:260206934 Summary to appear in Proc of LOPSTR+PPDP’26. 2026. Available from: https://arxiv.org/abs/2602.06934. Shapiro E. Types for Grassroots Logic Programs (Full version). arXiv preprint arXiv:260117957. 2026.

29

[23] [24] [25] [26] [27]

[28] [29] [30] [31] [32]

[33]

[34]

[35]

[36] [37]

[38] [39] [40] [41] [42]

[43] [44]

[45] [46]

Available from: https://arxiv.org/abs/2601.17957. Google. Dart Programming Language; 2024. https://dart.dev. Available from: https://dart. dev/. Fikes RE, Nilsson NJ. STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving. Artificial Intelligence. 1971;2:189-208. Montanari U, Rossi F. Contextual nets. Acta Informatica. 1995;32(6):545-96. Caldarelli G. Understanding the Blockchain Oracle Problem: A Call for Action. Information. 2020;11(11):509. Guerraoui R, Kuznetsov P, Monti M, Pavlovič M, Seredinschi DA. The consensus number of a cryptocurrency. In: Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing; 2019. p. 307-16. Lewis-Pye A, Naor O, Shapiro E. Grassroots Flash: A Payment System for Grassroots Cryptocurrencies. arXiv preprint arXiv:230913191. 2023. Available from: https://arxiv.org/abs/2309.13191. Keidar I, Lewis-Pye A, Shapiro E. Constitutional Consensus. arXiv preprint arXiv:250519216. 2025. Available from: https://arxiv.org/abs/2505.19216. Azzopardi S, Pace GJ, Schapachnik F, Schneider G. Contract automata. Artificial Intelligence and Law. 2016;24(3):203-43. Flood MD, Goodenough OR. Contract as automaton: representing a simple financial agreement in computational form. Artificial Intelligence and Law. 2022;30(3):391-416. Watt SJ, Goodenough O, Wong MW. Deontics and Time in Contracts: An Executable Semantics for the L4 DSL. In: Legal Knowledge and Information Systems: JURIX 2023. Frontiers in Artificial Intelligence and Applications. IOS Press; 2023. p. 119-24. Chircop S, Pace GJ, Schneider G. An Automata-Based Formalism for Normative Documents with RealTime. In: Legal Knowledge and Information Systems: JURIX 2022. vol. 362 of Frontiers in Artificial Intelligence and Applications. IOS Press; 2022. p. 158-63. Governatori G, Rotolo A. Modelling Contracts Using RuleML. In: Gordon TF, editor. Legal Knowledge and Information Systems: JURIX 2004. Frontiers in Artificial Intelligence and Applications. IOS Press; 2004. p. 141-50. Governatori G, Idelberger F, Milosevic Z, Riveret R, Sartor G, Xu X. On legal contracts, imperative and declarative smart contracts, and blockchain systems. Artificial Intelligence and Law. 2018;26(4):377409. Merigoux D, Chataing N, Protzenko J. Catala: A Programming Language for the Law. Proceedings of the ACM on Programming Languages. 2021;5(ICFP). Governatori G. Practical Normative Reasoning with Defeasible Deontic Logic. In: Reasoning Web. Learning, Uncertainty, Streaming, and Scalability. vol. 11078 of Lecture Notes in Computer Science. Springer; 2018. p. 1-25. Boella G, van der Torre L, Verhagen H. Introduction to Normative Multiagent Systems. Computational & Mathematical Organization Theory. 2006;12(2):71-9. Sartor G. Fundamental legal concepts: A formal and teleological characterisation. Artificial Intelligence and Law. 2006;14(1):101-42. Hage J. A model of juridical acts: part 1: the world of law. Artificial Intelligence and Law. 2011;19(1):23-48. Gelati J, Rotolo A, Sartor G, Governatori G. Normative autonomy and normative co-ordination: Declarative power, representation, and mandate. Artificial Intelligence and Law. 2004;12(1):53-81. Gelati J, Governatori G, Rotolo A, Sartor G. Declarative Power, Representation, and Mandate. A Formal Analysis. In: Bench-Capon T, Daskalopulu A, Winkels R, editors. Legal Knowledge and Information Systems: JURIX 2002. Frontiers in Artificial Intelligence and Applications. IOS Press; 2002. p. 41-52. Jones AJI, Sergot M. A Formal Characterisation of Institutionalised Power. Logic Journal of the IGPL. 1996;4(3):427-43. Grossi D, Meyer JJC, Dignum F. Modal Logic Investigations in the Semantics of Counts-as. In: Proceedings of the 10th International Conference on Artificial Intelligence and Law (ICAIL ’05). ACM; 2005. p. 1-9. Fornara N, Viganò F, Verdicchio M, Colombetti M. Artificial institutions: a model of institutional reality for open multiagent systems. Artificial Intelligence and Law. 2008;16(1):89-105. Radin MJ. Boilerplate: The Fine Print, Vanishing Rights, and the Rule of Law. Princeton, NJ: Princeton University Press; 2013.

30

[47] [48] [49] [50] [51] [52] [53]

[54] [55] [56] [57] [58] [59]

[60] [61] [62]

Kim NS. Wrap Contracts: Foundations and Ramifications. New York: Oxford University Press; 2013. Ben-Shahar O, Schneider CE. More Than You Wanted to Know: The Failure of Mandated Disclosure. Princeton, NJ: Princeton University Press; 2014. Surden H. Computable Contracts. UC Davis Law Review. 2012;46:629. Clack CD, Bakshi VA, Braine L. Smart Contract Templates: Foundations, Design Landscape and Research Directions; 2016. Available from: https://arxiv.org/abs/1608.00771. Schneider FB. Enforceable Security Policies. ACM Transactions on Information and System Security. 2000;3(1):30-50. Modgil S, Oren N, Faci N, Meneguzzi F, Miles S, Luck M. Monitoring compliance with E-contracts and norms. Artificial Intelligence and Law. 2015;23(2):161-96. Cambronero ME, Llana L, Pace GJ. Timed Contract Compliance Under Event Timing Uncertainty. In: Legal Knowledge and Information Systems: JURIX 2017. vol. 302 of Frontiers in Artificial Intelligence and Applications. IOS Press; 2017. p. 33-8. Lessig L. Code and Other Laws of Cyberspace. New York: Basic Books; 1999. De Filippi P, Wray C, Sileno G. Smart contracts. Internet Policy Review. 2021;10(2). Ostrom E. Governing the Commons: The Evolution of Institutions for Collective Action. Cambridge: Cambridge University Press; 1990. Hess C, Ostrom E, editors. Understanding Knowledge as a Commons: From Theory to Practice. Cambridge, MA: MIT Press; 2007. Benkler Y. The Wealth of Networks: How Social Production Transforms Markets and Freedom. New Haven, CT: Yale University Press; 2006. European Parliament and Council of the European Union. Regulation (EU) 2016/679 (General Data Protection Regulation); 2016. OJ L 119, 4.5.2016. Recital 26: anonymous information is information which does not relate to an identified or identifiable natural person; Art. 4(1) defines personal data. Free Software Foundation. GNU General Public License, Version 3; 2007. https://www.gnu.org/ licenses/gpl-3.0.html. Shapiro E. Multiagent Transition Systems: Protocol-Stack Mathematics for Distributed Computing. arXiv preprint arXiv:211213650. 2021. Available from: https://arxiv.org/abs/2112.13650. Shapiro E. Grassroots Platforms with Atomic Transactions: Social Graphs, Cryptocurrencies, and Democratic Federations. In: Proceedings of the 27th International Conference on Distributed Computing and Networking; 2026. p. 71-81. ArXiv preprint arXiv:2502.11299.

A. The Framework of Volition-Guarded Multiagent Atomic Transactions This appendix states formally what Section 4 recalls in brief, so that the statements and proofs of Section 6 can be read without recourse to another paper. Everything in it is from [10], and the proofs of its results are there and are not repeated. Earlier work introduced multiagent transition systems [61], grassroots protocols and platforms [2], and their definition via multiagent atomic transactions [62], which describe the behaviour of machines but not of the people operating them. A volition-guarded transaction is a machine transaction guarded by the volitions of some, all, or none of the people whose machines participate; a person’s volitional state is a set of equivalence classes of machine transactions they are willing their machine to take part in. The social graph illustrates the two extremes: befriending is guarded by both parties, while unfriending is guarded by either. A person may freely change their volitional state; an equivalence class is removed from every agent’s volitional state when a machine transaction in that class is taken, the will having been fulfilled. A.1. Agents, Machines and Volition-Guarded Transactions We assume a potentially infinite set of agents Π, an agent being a person operating a machine, but consider only finite subsets of it, so when referring to a particular set of agents P ⊂ Π we assume P to be nonempty and finite. We use ⊂ to denote the strict subset relation and ⊆ when equality is also possible, and use p ̸= q ∈ P as a shorthand 31

for p ∈ P ∧ q ∈ P ∧ p ̸= q. As standard, we use SP to denote the set of all total functions from P to S, and if c ∈ SP we use c p to denote the value of c at p ∈ P. Definition 35 (Machine State, Configuration, Transaction, Volition-Guarded Transaction [10]). Given an arbitrary set S of machine states, with a designated initial state s0 ∈ S, and agents Q ⊂ Π, a machine configuration over Q is a member of SQ , and a machine transaction over participants Q is a pair c → c′ ∈ (SQ )2 such that c ̸= c′ ; it is unary if |Q| = 1. Given such a machine transaction t, a volition-guarded multiagent atomic transaction over t—henceforth, volition-guarded transaction—is a pair (t, Q′ ) where Q′ ⊆ Q are its guards. Machine transactions are atomic and asynchronous [61]: they can be carried out by their participants at any time, regardless of the states of non-participants. Participants include both active agents, whose state changes, and stationary agents, whose state is a precondition but does not change. Volition-guarded transactions can be carried out only if their guards Q′ ⊆ Q are willing, and do not distinguish between agents that initiate a transaction and those willing to take part in it. When we say a transaction is guarded by {p, q}, both must be willing; when we say it is guarded by either p or q, we mean there are two volition-guarded transactions over the same machine transaction, (t, {p}) and (t, {q}), so that either person’s volition suffices. Distinct machine transactions can represent the same act in different configurations; a transaction equivalence relates them. Definition 36 (Transaction Equivalence [10]). Given a set of machine transactions R, a transaction equivalence is an equivalence relation ∼ on R such that t ∼ t ′ implies t and t ′ have the same participants, and R/∼ is countable. We write [t] for the equivalence class of t under ∼. All befriend transactions of p and q, differing only in the configurations in which they occur, form one equivalence class. A person wills a class, and taking one member of it fulfils that will. Definition 37 (Agent State and Configuration [10]). Given agents P, states S with initial state s0 , a set of machine transactions T each over its own participants Q ⊆ P and S, and equivalence ∼ on T , an agent state is a pair (V, m) ∈ A = (2T /∼ × S) where V is its volitional state and m ∈ S its machine state. The initial agent state is (0, / s0 ). An agent configuration c over P, S, T , and ∼ is a member c ∈ A P in which cvp ⊆ (T /∼) p for every p ∈ P, where (T /∼) p denotes the classes in T /∼ in which p is a participant; we write cvp for the volitional state and cmp for the machine state of agent p in c. Definition 38 (Volitional Transaction [10]). Given agents P, states S, machine transactions T over P and S, and equivalence ∼ on T : 1. A volition change of agent p ∈ P is a pair c → c′ of agent configurations over {p}, S, T , and ∼ such that cvp , c′vp ⊆ (T /∼) p and cvp ̸= c′vp , and cmp = c′mp . 2. A volitional machine transaction induced by a volition-guarded transaction (t, Q′ ), for some t = (d → d ′ ) ∈ T over Q ⊆ P with guards Q′ ⊆ Q, is a pair c → c′ where c ̸= c′ are agent configurations over P, S, T , and ∼ such that [t] ∈ cvq for every q ∈ Q′ ; cmp = d p and c′mp = d ′p for every p ∈ Q; cmp = c′mp for every p ∈ P \ Q; and c′vp = cvp \ {[t]} for every p ∈ P. 3. A volitional transaction is a volition change or a volitional machine transaction.

32

When a volitional machine transaction induced by (t, Q′ ) is taken, the class [t] is removed from every agent’s volitional state: the will is fulfilled by any equivalent transaction. A person may independently change their volitional state via volition changes, which may add or remove classes; beyond these, the framework removes a class from cvp only upon fulfilment. A.2. Transition Systems and the Induced Volitional System Definition 39 (Transition System, Computation, Run, Safe, Live, Correct [10]). A transition system is a tuple T S = (S, s0 , T, ∼), where: 1. S is an arbitrary non-empty set, referred to as the set of states. 2. Some s0 ∈ S is the designated initial state. 3. T ⊆ S2 is a set of correct transitions over S, where each transition t ∈ T is a pair (s, s′ ) of non-identical states s ̸= s′ ∈ S, also written as t = s → s′ . 4. ∼ is a partial equivalence relation on T : a symmetric and transitive relation on T , not necessarily reflexive. Its domain {t ∈ T : t ∼ t} is partitioned into countably many liveness classes T /∼; a transition outside the domain belongs to no class. A computation of T S is a nonempty, potentially infinite sequence of states r = s1 , s2 , · · · ; it is a run of T S if s1 = s0 . A prefix of a computation is a finite initial segment of it. A computation r = s1 , s2 , . . . is safe, also written r ⊆ T , if si → si+1 ∈ T for every two consecutive states. A class [t] ∈ T /∼ is enabled in a state s if s → s′ ∈ [t] for some s′ ∈ S. A run r is live if no class [t] ∈ T /∼ is enabled in every state of some suffix of r with no member of [t] occurring in the suffix. A run is correct if it is safe and live. A partial equivalence, rather than a total one, is used so that some transitions may carry no liveness requirement: only transitions in the domain of ∼ form classes and thereby incur a liveness obligation, while transitions outside the domain, belonging to no class, may occur in a correct run but are never required to. Lemma 40 (Extension [10]). Every finite safe run of a transition system is a prefix of a correct run of it. Definition 41 (Multiagent Transition System [10]). Given agents P ⊂ Π and an arbitrary set S of states with a designated initial state s0 ∈ S, a multiagent transition system over P and S is a transition system T S = (C, c0 , T, ∼) with configurations C := SP , initial configuration c0 := {s0 }P , transitions T ⊆ C2 a set of transactions over P and S, and ∼ a partial equivalence on T . Rather than specifying a multiagent transition system over a set of agents P directly, it is specified via machine transactions. A machine transaction over Q ⊆ P defines a set of multiagent transitions over P in which all members of P \ Q are stationary. Definition 42 (Transaction Closure [10]). Let P ⊂ Π, S a set of machine states, and C := SP . For any transition or transaction t = c → c′ , we write tq := cq → c′q and say p is stationary in t if c p = c′p . For a machine transaction t = (c → c′ ) over S with participants Q, the P-closure of t, t↑P, is the set of transitions over P and S defined by: ( {t ′ ∈ C2 : ∀q ∈ Q.(tq = tq′ ) ∧ ∀p ∈ P \ Q.(p is stationary in t ′ )} if Q ⊆ P t↑P := 0/ otherwise If R is a set of machine transactions, each t ∈ R over some Q and S, then the P-closure S of R, R↑P, is the set of transitions over P and S defined by R↑P := t∈R t↑P. Given a 33

relation ∼ on R, its P-closure ∼↑P is the relation on R↑P with tˆ (∼↑P) tˆ′ iff tˆ ∈ t↑P and tˆ′ ∈ t ′ ↑P for some t ∼ t ′ . A transition over P is unary if it lies in the P-closure of a unary transaction. If distinct transactions in R have disjoint P-closures, as when every participant of every transaction in R changes state, then each transition in R↑P has a unique inducing transaction, ∼↑P relates two transitions exactly when their inducing transactions are ∼related, and ∼↑P is a partial equivalence whenever ∼ is. Definition 43 (Volitional Multiagent Transition System [10]). Given agents P ⊂ Π, machine states S with initial state s0 , a set R of volition-guarded transactions such that every (t, Q′ ) ∈ R has the participants of t contained in P and distinct underlying machine transactions have disjoint P-closures, and an equivalence ∼ on the set TR := {t : (t, Q′ ) ∈ R for some Q′ } of underlying machine transactions, the volitional multiagent transition system induced by (S, R, ∼) over P is the multiagent transition system (A P , c0 , TV , ∼V ) where: 1. A := 2TR /∼ × S is the agent state space; 2. c0 ∈ A P is the initial agent configuration, with c0 vp = 0/ and c0 mp = s0 for every p ∈ P; 3. TV consists of all transitions e → e′ ∈ (A P )2 of one of two forms: (i) a volition change of some p ∈ P—evp , e′vp ⊆ (TR /∼) p and evp ̸= e′vp , emp = e′mp , and er = e′r for every r ∈ P \ {p}; or (ii) a volitional machine transaction induced by some volition-guarded transaction (t, Q′ ) ∈ R per Definition 38(2); 4. ∼V is the restriction of ∼↑P (Definition 42) to the volitional machine transactions, relating two of them whenever their inducing machine transactions are ∼equivalent, and leaves every volition-change transition outside its domain, so volition changes belong to no class and carry no liveness obligation. Definition 44 (Enabled [10]). Given a set of volition-guarded transactions, each (t, Q′ ) with t = d → d ′ a machine transaction over some Q ⊆ P and S with guards Q′ ⊆ Q, and an equivalence ∼ on machine transactions: the volition-guarded transaction (t, Q′ ) is machine-enabled in agent configuration c over P if cmp = d p for every p ∈ Q, and enabled if in addition [t] ∈ cvq for every q ∈ Q′ . An equivalence class [t] is enabled in c if some volition-guarded transaction (t ′ , Q′ ) with t ′ ∈ [t] is enabled in c. A volition-guarded transaction with an empty guard requires no volitions and is enabled whenever its machine precondition is met. A class of volitional machine transactions is enabled at a configuration in the sense of Definition 39 exactly when some volition-guarded transaction inducing it is enabled in the above sense, and this determines which runs are live and correct. Volition changes belong to no class and so impose no liveness obligation; personal choices remain free. A.3. Protocols, Grassroots Protocols and Coalescence A protocol is a family of multiagent transition systems, one for each set of agents P ⊂ Π, which share an underlying set of local machine states S with a designated initial state s0 . A local-states function maps every set of agents P ⊂ Π to a set of local machine states S(P) ⊂ S that includes s0 and satisfies P ⊂ P′ ⊂ Π =⇒ S(P) ⊂ S(P′ ). Definition 45 (Protocol [10]). A protocol F over a local-states function S is a family of multiagent transition systems that has exactly one transition system F (P) = 34

(C(P), c0 (P), T (P), ∼ (P)) for every P ⊂ Π, with agent states A (P), configurations C(P) := A (P)P , initial configuration c0 (P) ∈ C(P), and partial equivalence ∼ (P) on T (P) determined by the protocol, such that P ⊆ P′ ⊂ Π implies A (P) ⊆ A (P′ ) and c0 (P) p = c0 (P′ ) p for every p ∈ P. In a grassroots protocol two disjoint groups of agents can each operate independently — their interleaved correct runs are correct runs of the combined system — yet the combined system offers behaviours that neither group could produce on its own. Definition 46 (Interleaving [10]). Let P, P′ ⊂ Π be disjoint nonempty sets of agents, r = c0 , c1 , . . . a run of F (P), and r′ = d0 , d1 , . . . a run of F (P′ ). An interleaving of r and r′ is a sequence e0 , e1 , . . . of configurations in C(P ∪ P′ ) for which there exist nondecreasing sequences of indices (ik )k≥0 and ( jk )k≥0 with i0 = j0 = 0 such that for every k ≥ 0: 1. (ek ) p = (cik ) p for every p ∈ P, 2. (ek )q = (d jk )q for every q ∈ P′ , 3. if ek+1 exists, then exactly one of: (i) ik+1 = ik + 1 and jk+1 = jk , a P-step, or (ii) ik+1 = ik and jk+1 = jk + 1, a P′ -step. Moreover, if r is finite of length n then ik = n for some k, and if r is infinite then for every m ≥ 0 there is a k with ik = m; likewise for r′ and ( jk ). An interleaving is well defined: by Definition 45, A (P) ⊆ A (P ∪ P′ ) and A (P′ ) ⊆ A (P ∪ P′ ), so each ek , with p-components in A (P) and q-components in A (P′ ), is a configuration in C(P ∪ P′ ). Also e0 = c0 (P ∪ P′ ), by the agreement of initial configurations across F (P), F (P′ ) and F (P ∪ P′ ). Interaction, interactive run and first interaction are Definition 11 of Section 4. Definition 47 (Oblivious, Interactive, Grassroots [10]). A protocol F is: 1. oblivious if for every disjoint nonempty P, P′ ⊂ Π, every interleaving of a correct run of F (P) and a correct run of F (P′ ) is a correct run of F (P ∪ P′ ). 2. interactive if for every Q ⊂ Π and disjoint nonempty P, P′ ⊆ Q, every prefix of a correct run of F (Q) containing no interaction between P and P′ is a prefix of a correct run of F (Q) that contains one. 3. grassroots if it is oblivious and interactive. Being oblivious means two disjoint groups coexist without interference. Being interactive means two groups that have not yet interacted can still do so, and the condition is required at every such point and not at the initial configuration only, so a protocol whose groups can reach a state from which they can never couple is not interactive. The interaction graph, instances and coalescence are Definition 12 of Section 4. Proposition 48 (Coalescence [10]). Let F be a grassroots protocol, Q ⊂ Π, and P, P′ ⊆ Q disjoint instances in a prefix r of a correct run of F (Q). Then r is a prefix of a correct run of F (Q) in which P and P′ coalesce. A.4. Volitional Transactions-Based Protocols A volitional transactions-based protocol assigns to each set of agents the volitional multiagent transition system induced by its volition-guarded transactions. Definition 49 (Transactions Over a Local-States Function [10]). Let S be a local-states function. A set of transactions R is over S if every transaction t ∈ R is a multiagent 35

transition over Q and S(P′ ) for some Q ⊆ P′ ⊂ Π. Given such a set R and P ⊂ Π, R(P) := {t ∈ R : t is over Q and S(P′ ), Q ⊆ P′ ⊆ P}. Definition 50 (Volitional Transactions-Based Protocol [10]). Let S be a local-states function and R a set of volition-guarded transactions over S with equivalence ∼. The protocol F over R, S, and ∼ assigns to each set of agents P ⊂ Π the volitional multiagent transition system F (P) induced by (S(P), R(P), ∼) over P (Definition 43). In particular, C(P) = A (P)P with agent state space A (P) := 2TR(P) /∼ × S(P), monotone in P as Definition 45 requires, and c0 (P) has p-component (0, / s0 ) for every p ∈ P. Throughout, ∼ is an equivalence on TR , the machine transactions underlying the whole set R; for T ′ ⊆ TR we write T ′ /∼ for the set of ∼-classes with a representative in T ′ , and [t] for the class of t in TR /∼. Hence P ⊆ P′ implies TR(P) /∼ ⊆ TR(P′ ) /∼. The three results below are used in the proofs of Section 6. The first is the invariant that in a group’s own system an agent wills only transactions internal to the group, so the guard of a transaction that reaches another group cannot will it while the group runs alone. Lemma 51 (Volitional Containment [10]). Let F be a volitional transactions-based protocol over a set of volition-guarded transactions R with equivalence ∼. For every P ⊂ Π, every configuration c of F (P), and every p ∈ P: cvp ⊆ TR(P) / ∼, where TR(P) := {t : (t, Q′ ) ∈ R(P) for some Q′ }. Lemma 52 (Interleaving Safety [10]). Let F be a volitional transactions-based protocol and P, P′ ⊂ Π disjoint and nonempty. Every finite prefix of an interleaving of a correct run of F (P) and a correct run of F (P′ ) is a finite safe run of F (P ∪ P′ ). Proposition 53 ([10]). A volitional transactions-based protocol is oblivious provided that for every disjoint nonempty P, P′ ⊂ Π, no equivalence class whose transactions have participants spanning both P and P′ is ever enabled in any interleaving of correct runs of F (P) and F (P′ ). In a run of F (P ∪ P′ ) a member may will a transaction reaching the other group, which a group’s own run forbids; the volitional notion constrains the resulting coupling. Definition 54 (Volitionally Grassroots [10]). A volitional transactions-based protocol F is volitionally grassroots if it is grassroots and, for every disjoint nonempty P, P′ ⊂ Π and every safe run of F (P ∪ P′ ) interactive between P and P′ , the first interaction of P and P′ is induced by a volition-guarded transaction (t, Q′ ) with Q′ ∩ P ̸= 0/ and Q′ ∩ P′ ̸= 0. /

36