Heterogeneous trust in reliable broadcast via modal logic and history structures

Anoma Research Topics |TECHNICAL REPORT Heterogeneous trust in reliable broadcast via modal logic and history structures Murdoch J. Gabbay Heliax and Isaac Sheff Heliax aHeliax AG *E-Mail: [email protected],[email protected] Abstract We propose a novel modal logic and semantics for specifying and proving properties of distributed full-information-transfer protocols (protocols that broadcast state to all participants in a distributed system). We use this to design and prove correctness of novel generalisations of Bracha’s ‘reliable broadcast’ algorithm to a heterogeneous trust setting (where distinct participants may have distinct trust assumptions); these proofs have been mechanically formalised and checked. Keywords: Heterogeneous distributed systems ; Distributed Broadcast ; Bracha Broadcast ; Modal Logic ; Kripke semantics ; History Structures Contents 1 Introduction 3 1.1 The problem ........................... 3 1.2 A nontrivial test bench: Bracha Broadcast ........... 6 1.3 Why broadcast? Why a new logic? Why heterogeneity? .... 7 1.4 Map of the paper ........................ 10 List of Figures 11 2 History structures and their logic 11 2.1 A brief discussion using programming terminology ...... 11 2.2 Prehistories ........................... 12 2.2.1 Finite subsets and maybe-sets ............. 12 2.2.2 Definition of prehistories ................ 13 2.3 History structures ........................ 14 2.3.1 Definition ........................ 14 2.3.2 Discussion and examples ................ 16 2.3.3 Element-transitivity .................. 18 2.3.4 Discussion of nothing: † ................ 19 2.3.5 Further discussion of nothing ............. 21 DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |1–107 3 Logic over history structures 24 3.1 Syntax .............................. 24 3.2 Examples predicates, and their intended meanings ....... 25 3.3 Models ............................. 27 3.3.1 Semifilters ....................... 27 3.3.2 Definition of models .................. 28 3.3.3 Discussion of models .................. 29 3.4 The Kripke semantics associated to a model, and validity . . . 30 3.4.1 Kripke (relational) semantics .............. 31 3.4.2 Sequentiality ...................... 33 3.4.3 Validity ......................... 33 3.5 Active and inactive participants ................. 36 3.6 Extending syntax with syntactic sugar ............. 37 4 The modalities 46 4.1 Quorum intersection properties ................. 46 4.2 Modal properties ........................ 47 5 Sequentiality and liveness 49 5.1 Properties of sequentiality ................... 49 5.2 A logical theory of liveness ................... 52 5.2.1 (Axiomatic) theories .................. 52 5.2.2 Definition of ThyLive .................. 54 5.2.3 More on the Knowledge axioms ............ 55 5.2.4 More on (LiveAlways) ................. 57 6 Theory ThyHBB1 58 6.1 Definition of the theory ..................... 58 6.2 Further discussion of some ThyHBB1 axioms ......... 63 6.3 Agreement ............................ 65 6.4 Liveness 2 ............................ 66 6.5 Liveness 1 ............................ 68 6.6 Further discussion ........................ 70 7 Theory ThyHBB2 71 7.1 Definition of the theory ..................... 71 7.2 Proofs of Agreement, Liveness 1, and Liveness 2 ....... 72 7.3 Discussion ............................ 74 8 Theory ThyHBB3 76 8.1 : the correlation relation .................... 77 8.2 Definition of the theory ..................... 78 8.3 Agreement ............................ 79 DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |2 8.4 Liveness 2 ............................ 80 8.5 Liveness 1 ............................ 82 8.6 Discussion ............................ 83 9 Conclusions 85 9.1 Looking back on the results ................... 85 9.2 Why heterogeneous protocols? ................. 87 9.2.1 It’s about the ecosystem ................ 87 9.2.2 Why this has not been done before ........... 89 9.2.3 Embracing heterogeneity ................ 89 9.3 Related work .......................... 90 9.3.1 Heterogeneous Paxos (2021) .............. 90 9.3.2 XRP Ledger and Stellar (2014/15) ........... 90 9.3.3 Epistemic logics .................... 91 9.3.4 The ATL logic family .................. 93 9.3.5 Event structures ..................... 93 9.3.6 Trace Diagrams ..................... 94 9.3.7 Temporal Logic ..................... 95 9.3.8 Cross-domain state updates ............... 95 9.3.9 Interoperability of state for blockchain ......... 95 9.4 Future work ........................... 96 References 98 A Reducing to the homogeneous case 102 A.1 Homogeneous ThyHBB1 and ThyHBB2 (Figures 7 and 9) . . 103 A.2 Homogeneous ThyHBB3 (Figure 11) ..............104 1. Introduction 1.1. The problem This is a paper about modal logic applied to heterogeneous distributed protocols, so we will start by sketching what modal logic,distributed protocol, and heterogeneous mean, and why they matter. Amodal logic is a logic where the validity of its predicates may reference some notion of place or time. Instead of a judgement ⊨𝜙 meaning ‘ 𝜙 is valid’, we have a judgement of the form 𝑤⊨𝜙 meaning ‘ 𝜙 is valid in some modal context 𝑤’ [BdRV01].1 1 If the reader is familiar with typing contexts and wonders how these differ from modal contexts, these are indeed both contexts, and an argument (out of scope for this paper) can be made that there is some technical overlap. But we hope the following intuitive rule might help: if your 𝑤 helps you to type 𝑥 , 𝑦 , and 𝑧 then it is probably a typing context; if your 𝑤 tells you who you are, where you are, and/or what time it is, then this is probably a modal context. Readers who remain confused might pause reading to DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |3 Classic motivations for modalities include sentences like ‘it is raining’ (whose validity depends on where and when we are), or ‘I see rain’ (whose validity may additionally depend on who is making the claim), or ‘tomorrow, it will rain’, or ‘eventually, it will rain’ (which quantifies over future times), or ‘it rains everywhere sometime’ (which is ambiguous in English but can be disambiguated using the precision of ordering modal operators), and so on.2 In this paper, our modalities will refer to notions of place, time, and to quorums of participants (we explain quorums in a moment). Adistributed protocol, or synonymously a distributed algorithm, is a protocol/algorithm that runs over many participants [ CGR11 ]. What makes the theory of distributed protocols different from that of parallel or concurrent ones is that in distributed protocols, some proportion of the participants may be faulty, by which we mean that they need not follow the protocol and may display arbitrary, possibly deliberately hostile, behaviour (a term byzantine is also well-established in the literature [ LSP82 ]; we may use this synonymously with ‘faulty’).3 Distributed protocols gained their modern relevance when computers became networked in the 1980s (this is when Ethernet was invented). A machine on a network cannot necessarily vouch for the correctness of other machines on that network; the best it can do is proceed on a failure assumption that not too many of them are faulty (for some appropriate notion of ‘too many’) — and hope that this assumption is accurate. The subsequent developments of peer-to-peer protocols and blockchains — and other systems such that being distributed is part of the essential character of what that system is meant to accomplish — have made distributed systems an integral part of how modern computing works. Applied and theoretical research activity in distributed algorithms has grown accordingly. The usual solution to the possibility of faulty participants, in general, is to treat a step in the protocol as completed only when some quorum of participants have attested to it. If we assume that quorums are large relative to the set of faulty participants then every quorum will contain a non-faulty (correct) participant 4 — so that with this assumption, if we know that a quorum of participants agree on some output, then we can rely on the output being the result of a correct run of the protocol by some correct participant. It is simplistic but reasonably look in the mirror, step outside, and go for a half-hour walk. 2 How? ♢ time □place (it rains) means ‘there is a time when it rains at all places’ and □place ♢ time (it rains) means ‘at all places there exists a time where it rains’. Traditionally, the box symbol carries some meaning of all/everywhere/always and the diamond symbol carries some meaning of exists/somewhere/sometime. Thank you for asking. 3 There are many subtly different notions of faulty/byzantine behaviour. This is material for an interesting discussion which is out-of-scope here, aside from emphasising that for us, by definition, ‘faulty’ will mean ‘might deviate arbitrarily from the protocol’. 4 We have to make a trust assumption here; e.g. “up to a third of participants may be faulty, but no more”. If our trust assumptions are inaccurate, then behaviour can no longer be guaranteed. Such is life. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |4 accurate to say that the typical distributed algorithm has the form ‘wait until we hear a quorum of participants return suitable messages, then proceed to our next relevant step on the assumption that at least one of them was an outcome of a correct run of the protocol thus far’. A protocol is heterogeneous when different participants, or perhaps even the same participant at different times, might differ on what sets they recognise as quorums. In other words: in a heterogeneous protocol, the notion of ‘trust’ (as expressed by what quorums participants assume may be trustworthy) may vary with time and/or participant. It is now time for some definitions: Definition 1.1.1.Assume P some set of participants in a distributed algorithm. Aquorum system O ⊆ powerset(P) is some set of sets of participants in a distributed algorithm. We call each 𝑂∈ O aquorum. We may also call O a trust assumption, a semifilter, or a learner. Definition 1.1.2.Aheterogeneous distributed algorithm is such that several trust assumptions are present, and which is used may potentially vary by time and participant. In other words, we have not one quorum system O, but some nonempty set of them: O={O1, . . . , O𝑛} ⊆ powerset(powerset(P)).5 Remark 1.1.3.Heterogeneity is a natural phenomenon which arises along axes of both space and time: 1. Multiple distributed systems — possibly with overlapping participants, but each with their own community identity — may seek to interact. There is not one national voting system; there are several. There is not one bank; there are many. There is not one blockchain; there are more than one. There is not one local council or residents’ committee or family; there are multitudes. All these systems may be more or less successful within themselves, but for practical outcomes it matters just as much how smoothly they can interact, across their different trust assumptions. 2. A single participant may revise its quorum system over time. Real-life examples of this include a change of citizenship, political leanings, or indeed our natural changes in our groups of friends with time. Whom we are friends with or trust when we are children may differ from whom we are friends with or trust when we are adolescents or adults. It is a truism that the world is distributed, but more than that, the world is heterogeneously distributed. As mathematicians, we should build maths to model this, so we can describe ... 5 In a real-world system, all these sets are finite, but unless stated otherwise, our discussion will not depend on this. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |5 Remark 1.1.4 (This paper in a nutshell). 1. We develop a logic enriched with modalities for talking about participants (places), times, participants’ knowlege at each particular place and time, and rich modal properties having to do with heterogeneous quorums and quorum intersections. 2. We apply our logic to invent and prove correctness properties of heterogeneous generalisations of Bracha’s reliable broadcast algorithm (see next Subsection): ThyHBB1 , ThyHBB2 , and ThyHBB3 , each of which is interesting in its own right. 3. The definitions and proofs in this paper have been formalised in the Lean 4 theorem prover, complete with clear instructions for use and with clear and precise linkages between the results in this paper and their formalised Lean code. The interested reader can download the files [ Har25 ] and run the verification locally. Remark 1.1.5.We have already stated that a heterogeneous distributed system is just one where multiple notions of quorum are in use. Even at this early stage, and even before we have set up the mathematics, it is useful to unpack some implications of this. Consider that Ethereum (a homogeneous system) bridged with Bitcoin (another homogeneous system) is heterogeneous (because Ethereum and Bitcoin have distinct quorums); and XRP Ledger (a heterogeneous system) bridged with Ethereum is also heterogeneous. These observations reflect that homogeneity is not a naturally compositional property, whereas heterogeneity is naturally compositional: a combination of two homogeneous systems is (most likely) heterogeneous, and if we combine a heterogeneous system with any other system, we get another heterogeneous system. Thus, going from homogeneity to heterogeneity is easy; remaining homogeneous (as a system scales up and interacts with other systems) is hard; reversing heterogeneity once established is very hard, and may be impossible. So to the reader who may be inclined to think of being heterogeneous as somehow an edge case, we would say: no. Homogeneity is the edge case. Heterogeneity is the natural state of affairs. This is how the world is. A state where everyone agrees on trust assumptions is an important special case, but it is not always a natural state of affairs, and even if we attain such agreement momentarily, the inherent noncompositonality of this agreement means that it may be difficult or impossible to maintain. 1.2. A nontrivial test bench: Bracha Broadcast A seminal distributed algorithm is Bracha Broadcast (BB), introduced in a paper by Bracha [ Bra87 ] (Bracha called it reliable broadcast there). In the homogeneous case as considered by Bracha — so there is one, globally agreed, DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |6 quorum system — this solves the problem of how a proposer can broadcast a value across the network, such that correct participants agree on the value proposed. BB has three correctness properties, which we sketch as follows (these are not mathematical statements, yet): • Liveness 1 If there is a quorum of correct participants (meaning: all participants in the quorum are live and correctly follow the protocol) 6 and precisely one value 𝑣 is proposed, then that correct quorum eventually concludes 𝑣. • Liveness 2 If there is a quorum of correct participants and one participant in that quorum concludes 𝑣 , then all participants in that quorum eventually conclude 𝑣. • Soundness / Agreement If two correct participants conclude 𝑣 and 𝑣′ respectively, then 𝑣=𝑣′. Note above that we write ‘there is a quorum’, without specifying who decides what a quorum is. This is because it is assumed that everyone agrees on this; Bracha’s trust assumptions where what we here call homogeneous. It turns out that many heterogeneous generalisations of Bracha’s reliable broadcast exist, and we will introduce three of them, which between them triangulate in a rich design space. We will state precise analogues of the liveness 1, liveness 2, and soundness properties later (see Figures 8,10, and 12); the above is just to give the reader a flavour. 1.3. Why broadcast? Why a new logic? Why heterogeneity? Other distributed problems exist, including for example Consensus. Why focus on Broadcast in this paper Broadcast is arguably a canonical simplest nontrivial distributed algorithm, and research shows how Consensus can be built on top of it [ Bra87 , Section 4, “The Consensus Protocol”].7 6 The pedantic reader (including the first author, when he was first introduced to these concepts) might now ask: but what do ‘live’ and ‘correctly follow the protocol’ mean precisely? Intuitively these concepts are clear enough for this introductory exposition, but what do they actually mean? Such a reader is in luck, because logic excels at giving precise mathematical form(s) to compelling but informal concepts. See Subsection 5.2. 7 For the interested reader, section 3 of [ CGR11 ] contains an exhaustive survey of broadcast algorithms, all making different safety assumptions and delivering different correctness guarantees. In particular crusader agreement [ Dol82 ] stands out as arguably simpler than Bracha Broadcast, and it has a termination property which our algorithms will not have — but only because it makes a strong assumption which we do not wish to make, of assuming a globally synchronous network (messages arrive reliably and on time). Arguably, a globally synchronous network makes less sense in a heterogeneous setting, because this is a global trust assumption on the network, and we do not want a crash in one trust system to prevent progress of another. So perhaps we should say that Bracha Broadcast is a simplest nontrivial useful distributed algorithm that makes sense (to us) in a heterogeneous setting. See Footnote 8. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |7 Thus, Heterogeneous Bracha Broadcast (HBB) is a kind of universal building block, a useful test subject, and a convenient place to start. It is simple enough to be accessible, and expressive enough to be useful.8 Furthermore, it turns out that Bracha’s reliable broadcast algorithm is a useful and fruitful object of study because it admits multiple, and multiple interesting, generalisations to the heterogeneous case. Other logics exist for specifying distributed algorithms. Why design a new one Our logic will let us specify and reason about distributed algorithms declaratively: in our analysis an algorithm is an axiomatic theory, and a run of the algorithm is a model of that theory. We mean by declarative that we elide details of control flow and evaluation order — where we deem these inessential, which is surprisingly often — so we can focus on the essence of what the protocol is. This method, which follows a thread of previous research [ GZ25 ], yields simplifications that are analogous to what we see moving from programming in a low-level imperative language to a higher-level functional or logic programming language: more compact assertions, less control flow, less worrying about evaluation order, and more (and more clear) high-level specification of what the program does. So one answer to the question above is: because it works well. But there are also two things going on in the logic we use in this paper, which are specific to this paper in particular. 1. Its logical modalities are tailored to talk about heterogeneous quorums and quorum intersections; see the three modalities ↓ , | → , and ♢ in Figure 3and their semantics. This yields a compact but expressive logic with which we will be able to concisely and precisely express complex reasoning on our three algorithms. This is so effective that once we have things set up, our correctness proofs can just proceed by symbolic manipulation (so-called ‘symbol 8Bracha’s reliable broadcast may be simple (at least in the tautological sense that it is simpler than more complex protocols) but this belies its considerable expressive power. It suffices to update state in several types of distributed systems, including cryptocurrencies (although many of them unnecessarily use Consensus, which is stronger) [GKM+19]. Broadcast has consensus number 1, meaning it can be used to update a distributed register despite byzantine failures, with the caveat that an entry may get stuck (never update again) if two simultaneous updates are proposed [ Her91 ]. For a cryptocurrency account, this should only happen if owner of that entry (i.e. the account holder) misbehaves. This might freeze that owner’s account, but it would not affect the rest of the system. Sui generalises this to a notion of owned objects, which can update much more quickly and easily (using broadcast) than the rest of Sui’s state (which uses consensus). If an object’s owner misbehaves then that object can become stuck (to the presumed detriment of the object’s misbehaving owner), but other objects, and the rest of Sui’s state, are unaffected and do not become stuck [BCD+24]. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |8 pushing’). The proof of Proposition 6.4.5 is a case in point. The notation might take a bit of getting used to, but the proof is succinct and precise — and the other proofs are basically just minor variations of it. This is a feature, because it is good when correctness proof are short, routine, and predictable. 2. Second, and furthermore, we use a novel epsilon-inductive notion of time 9 which we call History Structures. In a history structure, the time of an event is equal to the set of events that have happened before that event. We mean this literally. Time is not a number or a vector of numbers (cf. Lamport clocks [ Lam78 ] or vector clocks [ SM94 , RS96 ]). 10 For us, time is literally a set of past events, which themselves are indexed by times that are sets of past events, and so on. The slogan is that time is equal precisely to that which has happened before. It turns out that this interacts elegantly and naturally with our logical methodology and axiomatisation, as we shall see. Why heterogeneous distributed algorithms matter Heterogeneity reflects the following question: how, and in what mathematical circumstances, can distinct communities collaborate, even if they have distinct trust assumptions? Heterogeneity can provide diversity and resilience, in that different communities can make different choices and yet still interact, and the overall system can continue operating (in a suitable sense) even when some communities may fail. In order for heterogeneous trust systems to compete on the basis of userfacing experience and simplicity with ones featuring a single homogeneous trust assumption, the system overall must be able to automate the accounting of managing multiple trust systems, such that two users with trust preferences compatible in the actual course of history can interact as if they were using a homogeneous system. In the ideal case, the system would be as easy to use as a centralised one that relies on a single trusted party who behaved as expected — even thought it actually is composed of multiple communities with multiple trust assumptions, all stitched together in some mathematical way. So the challenge is how, and in what circumstances, we might reduce the differential user-facing complexity cost of a heterogeneous trust system to nearly zero. 9 ‘Epsilon-inductive’ is fancy set-theorist jargon for saying that something is built from sets, or sets of sets, or sets of sets of sets, and so on. See Definition 2.2.4, which is visibly epsilon-inductive because it builds a prehistory as a set of things that themselves contain prehistories. 10 Vector clocks seem to have been independently invented by several people during the 1980s. The surveys [ SM94 , RS96 ] includes historical comments in footnote 3 on page 6, and on page 4, respectively. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |9 Definition 2.3.5 (History structures).Define History(P,Event) the set of history structures History(P,Event) ⊆ PreHistory(P,Event) to be the set of hereditarily transitive elements in PreHistory(P,Event) , by which we mean that this is the greatest set of prehistories such that 𝐻∈History(P,Event)implies 𝐻transitive∧∀𝐻′≺−𝐻.(𝐻′∈History(P,Event)). Notation 2.3.6.Recall from Definition 2.2.6(3) that we call a prehistory a time. Henceforth, all times will be hereditarily transitive unless stated otherwise — i.e. all times are histories (Definition 2.3.5). Indeed, henceforth if the reader sees the symbol 𝐻 then they can assume it is a history (not just a prehistory), unless stated otherwise. This should always be clear from context. Remark 2.3.7.The following observation might help the reader to parse the meaning of (pre)history structures from Definitions 2.2.4 and 2.3.5. In an event-tuple 𝑝, 𝑥, 𝐻, the 𝐻is three things simultaneously: •a full epsilon-structure of events preceding the event-tuple, •now (i.e. the moment in time when the event ‘occurs’), and • (for histories, by transitivity) a full record of what 𝑝 knows at the time this event-tuple occurs. These are all equated in the strong sense that they are literally equal. We can sum this up as follows: 𝐻=the past (= a set of event-tuples) =now =what we know. This ‘epistemic’ approach to time is novel, to the best of our knowledge. 16 Existing approaches treat time as an exogenous concept, i.e. there is a clock and it tells us what time it is, typically as a (possibly structured) timestamp [ Lam78 , SM94 , RS96 ] (a number or a vector of numbers). Obviously, if time is a timestamp then we can talk about what has happened before that timestamp, or what an agent knows at that timestamp. For our purposes this level of indirection is not needed. There are no timestamps. Time is simply that which has happened before. 2.3.2. Discussion and examples Example 2.3.8 (Illustrating history structures).A history structure can be represented as a directed acyclic graph, or as a derivation tree. Of the two we 16 Epistemic: relating to knowledge. We discuss the relation of our logic to purpose-built epistemic logics, i.e. ones with modalities for reasoning directly about knowledge, in Subsection 9.3. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |16 (1) 𝑝⊢print(hello) 𝑝⊢print(world) 𝑝⊢exit() (2) 𝑝⊢print(hello)𝑝⊢print(world) 𝑝⊢exit() (1) (𝑝, print(hello),∅), (𝑝, print(world),{(𝑝, print(hello),∅)}), (𝑝, exit(),{(𝑝, print(hello),∅), (𝑝, print(world),{(𝑝, print(hello),∅)})})  (2) (𝑝, print(hello),∅),(𝑝, print(world),∅), (𝑝, exit(),{(𝑝, print(world),∅),(𝑝, print(hello),∅)}) Figure 1. Illustrating (pre)history structures (Examples 2.2.5 and 2.3.8) will favour a derivation tree style, just because there are particularly convenient LaTeX packages for typesetting these. Figure 1presents two history structures. Above are derivation-tree style presentations, and below are corresponding history structure written out in full. We assume events print and exit and just one participant 𝑝 . The two examples represent two sequencings of events print(hello),print(world), and exit(). In the first history: •𝑝sends hello to stout (standard output) at time 𝐻0=∅, •𝑝sends world to stout at time 𝐻1={(𝑝, print(hello), 𝐻0)}, and then •𝑝stops at time 𝐻2={(𝑝, print(world),∅),(𝑝, print(hello),∅)}. In the second history, •𝑝sends hello to stout at time 𝐻0=∅, •𝑝sends world to stout at the same time 𝐻0=∅, and then •𝑝stops at time 𝐻1={(𝑝, print(world), 𝐻0),(𝑝, print(hello), 𝐻0)}. Obviously the derivation-tree presentation is more readable, but the sets definition is definitive and is what we use to do the mathematics. Example 2.3.9.Here is a simple example of a prehistory 𝑃 that is not a history structure: 𝑃={ (𝑝, † ,{(𝑝, † ,∅)}) }. 𝑃 is not a history because it is not transitive: (𝑝, † ,{(𝑝, † ,∅)}) ∈ 𝑃 yet {(𝑝, † ,∅)} ⊈𝑃. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |17 Example 2.3.10.Example 2.3.8 only involved one participant. What if we have more? We demonstrate this with a simple message-passing example. Assume two participants 𝑝 and 𝑞 , and two actions propose and accept which we will treat as 0 -ary. Here are two example history structures in which 𝑝 takes action propose() and then 𝑞takes action accept(). We indicate participants with 𝑝⊢ and 𝑞⊢: 𝑝⊢propose() 𝑞⊢accept() 𝑝⊢propose(), 𝑞 ⊢accept() The difference is that in the left-hand history, 𝑞 knows that 𝑝 has proposed before it accepts; whereas in the right-hand history it does not. Here are the corresponding history structures in full: In the left-hand history: •𝑝proposes at time 𝐻0=∅. •𝑞accepts at time 𝐻1={(𝑝, propose(), 𝐻0)}. •The full history structure is H={(𝑞, accept(), 𝐻1), 𝐻1}. In the right-hand history: •𝑝proposes at time 𝐻0=∅. •𝑞accepts at the same time 𝐻0. •The full history structure is H={(𝑞, accept(), 𝐻0),(𝑝, propose(), 𝐻0)}. Finally, we illustrate a simple history where 𝑝 proposes and then 𝑞 learns that 𝑝has proposed: 𝑝⊢propose() 𝑞⊢ † Here is the corresponding history structure written in full: (𝑝, propose(),∅),(𝑞, † ,{(𝑝, propose(),∅)}) History structures are rich and complex, but structurally the examples above represent everything that can happen. The complexity just follows from scaling up. 2.3.3. Element-transitivity We mention that an alternative notion of transitivity on prehistories to that in Definition 2.3.2 is possible, but it will be too weak for our needs here: Definition 2.3.11.Call 𝐻∈PreHistory(P,Event) element-transitive when for every 𝐻′, 𝐻′′ ∈History(P,Event), 𝐻′′ ≺− 𝐻′∧𝐻′≺− 𝐻implies 𝐻′′ ≺− 𝐻. Lemma 2.3.12.Suppose 𝐻∈PreHistory(P,Event). Then: DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |18 1. If 𝐻 is transitive (Definition 2.3.2) then it is element-transitive (Definition 2.3.11). 2. The reverse implication need not hold: it is possible for 𝐻 to be elementtransitive but not transitive. 3. Every 𝐻∈History(P,Event)is element-transitive. Proof. We consider each part in turn: 1. Suppose 𝐻′′ ≺−𝐻′≺−𝐻 . Then 𝐻′⊆𝐻 by Definition 2.3.2 (transitivity of 𝐻 ). The reader can check from Definition 2.3.1(1) that 𝐻′′ ≺− 𝐻′⊆𝐻 implies 𝐻′′ ≺− 𝐻 , so we are done. 2. It suffices to provide a counterexample. Take P={𝑝, 𝑞} (so there are two participants) and Event =∅(so the only maybe-event is † ): 𝐻1={(𝑝, † ,∅)} 𝐻2={(𝑝, † , 𝐻1),(𝑞, † ,∅)} Here is an illustration in derivation tree style: 𝑝⊢ † 𝑝⊢ † 𝑞⊢ † Then 𝐻2is trivially element-transitive and 𝐻1≺− 𝐻2, yet 𝐻1⊈𝐻2. 3. By construction in Definition 2.3.5, 𝐻∈History(P,Event) is transitive. We use part 1of this result. □ 2.3.4. Discussion of nothing: † The end of time, and initial and final event-tuples. Discussing nothing requires us to build a little bit of machinery:17 Definition 2.3.13.Fix H∈History(P,Event). Then: 1. We may call H the end of time in H , because every 𝐻≺− H precedes it (Definition 2.2.6(4)) by transitivity (Definition 2.3.2). 2. Call an event-tuple (𝑝, 𝑥, 𝐻) ∈ H initial/ 𝒑 -initial when 𝐻 in H is ≺− -least / ≺−-least among tuples starting with 𝑝. 3. Call an event-tuple (𝑝, 𝑥, 𝐻) ∈ H final/ 𝒑 -final when 𝐻 in H is ≺− -final / ≺− -final among tuples starting with 𝑝. Remark 2.3.14.Initial and final event-tuples need not exist (the empty history H=∅ has neither), and if they exist they need not be unique (the right-hand history in Example 2.3.10 has two of each). Note that if (𝑝, 𝐸, 𝐻) ∈ H then 𝐻=H is impossible, so the end of time cannot be the time of an event-tuple in H , and in particular H is never the time of a final event-tuple. 17 We are mathematicians, so we appreciate that careers — good ones — have been made from studying nothing. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |19 The problem: final event-tuples. Why do we use Event † to build (pre)history structures in Definitions 2.2.4 and 2.3.5, instead of just Event ? This is motivated by the design of the Knowledge axiom-schemes (Knowledge ♢ ↓↓↓↓↓↓↓ ↓ ↓) and (Knowledge□ ↓↓↓↓↓↓↓ ↓ ↓)in the theory of liveness ThyLive in Figure 6. We will discuss these axioms in detail in Subsection 5.2. What matters here is that they express that live participants communicate information to one another; if some information 𝜙 becomes known to some live participant 𝑝 , then eventually every other live participant will know that someone (namely: 𝑝 ) knew 𝜙. The technical difficulty is that a history structure H is a finite set of eventtuples, so there is such a thing as a final event-tuple. As per Definition 2.3.13(3), this is a triple (𝑝, 𝐸, 𝐻) ∈ Hsuch that 𝐻is ≺−-maximal in H. If our notion of history is only mapped out in terms of event-tuples — i.e. if H consists only of triples (𝑝, 𝐸, 𝐻) where 𝐸∈Event — then this final event cannot be communicated, because another participant learning of this event would have to itself be an event, which would come later than the final event, contradicting finality of the final event. † : the solution. Broadly speaking we have the following options: 1. We can accept this infinite regression and make history structures infinite: I did 𝐸 ; you learned that I did 𝐸 ; I learned that you learned that I did 𝐸 , ... We have nothing against infinities but here this feels like a hack, because it does not correspond to how we think of distributed algorithms actually behaving. 2. We can tweak the meaning of our temporal modalities, or perhaps tweak ThyLive. 3. We can introduce † and maybe-events Event † as defined above. This is what we do. Thus we permit a triple (𝑝, † , 𝐻) in a participant’s history. This † -event-tuple does not record an event — in the technical sense that the event-tuple has † in its second entry, which is not in the set of events Event — but it does represent an 𝐻-update to the view that 𝑝has of history. We can think of this as corresponding roughly to 𝑝 receiving a message, e.g. as per a Lamport diagram [Lam78, Figure 1].18 Now suppose (𝑝, 𝐸, 𝐻) is a final event in H . If we have † , then the model can continue to evolve such that this event becomes known to another participant 𝑞 , 18 Though Lamport considers receiving a message to be an event, and we do not. Just under Figure 1, Lamport writes “We assume that sending or receiving a message is an event in a process”. Indeed, traditionally in distributed systems receiving a message is considered an event. We classify things a little differently to avoid infinite regression and to permit finite nonempty history structures and the existence of final events. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |20 by adding a tuple (𝑞, † ,{{(𝑝, 𝐸, 𝐻), 𝐻}}) . This is not technically an event. It is amaybe-event, which reflects 𝑞becoming aware of (𝑝, 𝐸, 𝐻). 2.3.5. Further discussion of nothing Remark 2.3.15 ( † viewed as a receive action).We can think of † as a generalisation of the notion of a ‘receive’ action, as follows: Let us view 𝐸∈Event as a broadcast event, so that (𝑝, 𝐸, 𝐻) means ‘ 𝑝 broadcasts 𝐸 at time 𝐻 ’. Then we can view † as a receive action, where (𝑝′, † , 𝐻 ∪ {(𝑝, 𝐸, 𝐻)}) is the time when information arrives at 𝑝′ that (𝑝, 𝐸, 𝐻) happened. Note that, following this analogy, not every ‘receive’ action needs to be via † . For instance, we can have (𝑝, 𝐸, 𝐻) ∈ H and also (𝑝′, 𝐸′, 𝐻 ∪ {(𝑝, 𝐸, 𝐻)}) ∈ H . By our analogy, this corresponds to 𝑝 broadcasting 𝐸 and then 𝑝′ broadcasting 𝐸′at the same time as it receives the broadcast from 𝑝.19 Nevertheless, we still need † in order to account for a final broadcast event, so that participants can learn of this event and update their local history without themselves broadcasting another event. Note that this Remark is just an analogy: history structures, events, and † are their own thing. Remark 2.3.16 ( † viewed as an 𝜖 transition).In the theories of automata there is a notion of automaton making a silent or internal transition. Traditionally these are called 𝜖 -transitions [ HMU07 , Subsection 2.5, “Finite Automata With Epsilon-Transitions”]. The traditional reading of this is an internal state change that does not involve interaction with the environment. A difficulty with interpreting † as a receive action, as we do in Remark 2.3.15, is that there is no restriction on an event-tuple (𝑝, † , 𝐻) that 𝐻 should contain information that is somewhere in the rest of some larger history for 𝑝 to ‘receive’. 𝐻could be arbitrary. In this sense, it also makes sense to think of † simply as an internal transition of 𝑝, more akin to the automata-theoretic 𝜖action. Yet † is not just a silent internal action without interaction with the environment, because 𝐻 could also contain information that is in the rest of some larger history, e.g. when we interpret it as a receive action. So we repeat the final line of Remark 2.3.16: history structures, events, and † are their own thing. Remark 2.3.17 ( † viewed as an attestation).Perhaps a better way to think of † is as marking a pure attestation: when (𝑝, † , 𝐻) ∈ H this means that 𝑝 attests to knowing of time 𝐻and the information encoded therein. 19 Think of this in the style of Mealy machines, in which every step has to receive a message, update state, and send a message. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |21 Of course (𝑝, 𝐸, 𝐻) ∈ H also means that 𝑝 attests to knowing of 𝐻 , but that happens in the sense that an event 𝐸 occurs at 𝑝 at time 𝐻 . In contrast, (𝑝, † , 𝐻) is a pure attestation; 𝑝 might have received the information that the time 𝐻 exists from the environment, or 𝑝 might have computed the time 𝐻 internally. In this sense, † generalises both receive and 𝜖 : it represents the act of attesting to some internal state change of knowledge, and in our model, knowledge and time are the same thing. Remark 2.3.18.It is perfectly feasible to have (𝑝, 𝐸, 𝐻) ∈ Hand also (𝑝, † , 𝐻 ∪ {(𝑝, 𝐸, 𝐻)}) ∈ H. For instance, this is a valid history structure:20 H={(𝑝, 𝐸, ∅),(𝑝, † ,{(𝑝, 𝐸, ∅)})}. In derivation tree style (and bearing in mind that there is only one participant) we can illustrate it as follows: 𝐸 † We could even replace 𝐸with † above, to obtain this: † † With respect to the encoding of natural numbers in Remark 2.3.19 below, this is the natural encoding of the number 2. It is surprisingly interesting to look at a history structure with no events. Thus, the only maybe-event possible is † itself: Remark 2.3.19.Consider history structures with no events and only one participant, so that Event =∅and Event † ={ † }and P={𝑝}. Then the definitions simplify up to isomorphism as follows: •PreHistory is a least fixedpoint under the rule 𝐻⊆fin PreHistory 𝐻∈PreHistory •History is the set of hereditarily transitive prehistories. 20It is a sequential one, in the sense of Definition 3.4.9(2). DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |22 This simplifies to: ∅∈History 𝐻∈History =⇒𝐻∪ {(𝑝, † , 𝐻)} ∈ History. The reader might recognise this as essentially identical to the construction of finite von Neumann ordinals: 0=∅𝑛+1=𝑛∪ {𝑛}. This is the standard von Neumann construction of the natural numbers in set theory, which has the nice property that a number 𝑛 is represented as the set of representations of numbers less than 𝑛[Dev93, Figure 7.2]. We can take this coincidence seriously and view history structures as a generalisation of the finite von Neumann ordinals, extending them with concurrency (given by letting P contain multiple participants) and with events (given by letting Event be nonempty). Thus we can view histories as concurrent numbers, where the mapping (𝑝, 𝑥, 𝐻) ↦−→ (𝑝, † , 𝐻 ∪ {(𝑝, 𝑥, 𝐻)}) corresponds to the mapping 𝑛↦→ {𝑛} used above to define 𝑛+1 . In this sense, we can loosely identify † with the successor operation. Conversely, von Neumann ordinals are obtained from History structures as the special case where there is just one participant, and only the one maybeevent † .21 Remark 2.3.20 (Taking stock).We have set up the following mathematical machinery so far: • History structures give us a notion of events happening in time and at places, where (𝑝, 𝐸, 𝐻) ∈ His interpreted as ‘event 𝐸happens at place 𝑝at time 𝐻’. • Semifilters give us the notion of quorum which is fundamental to many distributed algorithms, including broadcast algorithms of the type we will study here. Mathematically, this is all the machinery we need. In Section 3we will combine history structures with semifilters to define the syntax and semantics of a logic for reasoning about heterogeneous broadcast algorithms. 21 It might be interesting to take this seriously and replay the evolution of set-theoretic semantics for numbers. We list some questions in increasing order of speculativeness: What are the arithmetic properties of ‘concurrent naturals’? What are the arithmetic and topological properties of the spaces of ‘concurrent rationals’ and ‘concurrent reals’? What might ‘concurrent surreal numbers’ mean? And even: is the natural notion of ‘concurrent sets’ substantively different from its encoding in normal set theory as per the definition of prehistories above? Such ideas are out of scope for this paper, but they might be a starting point for nice research programme in mathematical foundations. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |23 𝑡::=(𝑎∈VSym)|(𝑣∈Value) 𝜙::=⊥ | 𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝜙|𝑡======= = =𝑡|∀∀∀∀∀∀∀ ∀ ∀𝑎.𝜙 |E(𝑡, . . . , 𝑡) | P(𝑡, . . . , 𝑡) | ↓𝜙| | → 𝜙| ♢ 𝑡1...𝑡𝑛𝜙|seq Above: E∈ESym and P∈PSym; and 𝑛≥0is any nonnegative integer. Figure 2. Syntax of predicates (Definition 3.1.3) 3. Logic over history structures 3.1. Syntax Definition 3.1.1. 1. A signature Σis a tuple Σ=(VSym,ESym,PSym,Value) of disjoint sets of variable symbols,event symbols,predicate symbols, and values. We assume that VSym is countably infinite and that Value is nonempty (so there are many variable symbols and at least one value). For reasons discussed in Remark 3.3.8, we may write Value synonymously as Learner . These are different concepts but we use a single set to represent both.22 2. We define sets of events and atomic predicates over Σby: Event(Σ)={E(𝑣1, . . . , 𝑣𝑛) | E∈ESym, 𝑣1, . . . , 𝑣𝑛∈Value} AtmPred(Σ)={P(𝑣1, . . . , 𝑣𝑛) | P∈PSym, 𝑣1, . . . , 𝑣𝑛∈Value} Notation 3.1.2.We do not impose an arity or sort system on our syntax, so if P∈PSym then P() , P(𝑣) , and P(𝑣1, 𝑣2) , are all valid syntax, and similarly for E∈ESym. In practice we will use each event and predicate symbol with a consistent arity (= number of arguments). In the 0 -ary case we may elide the empty brackets, writing P() just as P . For instance, we do this with live in our theory of liveness in Figure 6. Definition 3.1.3.Suppose Σis a signature. 1. We define the syntax of terms 𝑡 and predicates 𝜙 over Σ by the grammar in Figure 2. 2. By convention the modal operators ↓𝜙 , | → 𝜙 , and ♢ 𝑡1...𝑡𝑛𝜙 bind less tightly than ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒, so that for example ↓𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝜓brackets as (↓𝜙)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝜓. Also by convention the quantifier ∀∀∀∀∀∀∀ ∀ ∀𝑎.𝜙 binds as far to the right as possible, so that for example ∀∀∀∀∀∀∀ ∀ ∀𝑎.↓𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝜓 brackets as ∀∀∀∀∀∀∀ ∀ ∀𝑎.((↓𝜙)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝜓) . That said, we may 22 It is standard to use a single set to represent multiple domains. Set theory takes this to its extreme, where sets represent everything (e.g. ∅ can represent both the empty set and the number zero), and in computing, it is fundamental that all data can be serialised to binary bitstrings. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |24 use whitespace rather than brackets for clarity, so that for example ∀∀∀∀∀∀∀ ∀ ∀𝑎.𝜙 ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝜓 brackets as (∀∀∀∀∀∀∀ ∀ ∀𝑎.𝜙)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝜓 . Meaning will always be clear, and where there is any danger of confusion we may insert brackets, even if this is not required according to our conventions. 3. Aclosed predicate is one with no free variable symbols. It can still mention values; so if 𝑎∈VSym and 𝑣∈Value then 𝑎======= = =𝑣 is not closed, and ∃∃∃∃∃∃∃ ∃ ∃𝑎.𝑎======= = =𝑣 is closed. Remark 3.1.4.We read the predicates in Figure 2as follows: •⊥⊥⊥⊥⊥⊥⊥ ⊥ ⊥is false,⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒is implies, and ∀∀∀∀∀∀∀ ∀ ∀is for all, as usual. •𝑡======= = =𝑡′is equality; the equality holds when 𝑡and 𝑡′denote equal values. •E(𝑡1, . . . , 𝑡𝑛)is an event and P(𝑡1, . . . , 𝑡𝑛)is an atomic predicate. Both events and atomic predicates are predicates in our logical syntax (but an event is not an atomic predicate, nor vice-versa). This is intuitively justified because E(𝑡1, . . . , 𝑡𝑛)-the-predicate will assert that E(𝑡1, . . . , 𝑡𝑛)happens.23 Events and atomic predicates are syntactically similar, but they have different meanings in the denotation. Events are handled by a history structure, whereas predicates are handled by an interpretation. See the rules for interpreting 𝑤⊨𝐸 and 𝑤⊨𝑃in Figure 3. • We read ↓ as at the time of some event up to now or just in the past (where ‘the past’ may include now); and •We read | → 𝜙as 𝜙at the end of time. • We read ♢ 𝑙1...𝑙𝑛𝜙 as someone in every 𝒍1. . . 𝒍𝒏 -quorum intersection has 𝝓 or 𝒍1. . . 𝒍𝒏-quorum intersections admit 𝝓(cf. Remark 3.6.3(7)); and •seq as sequential (we define and study what this means in Definition 3.4.9 and Subsection 5.1). . The above are intuitions; they will be made formal in the denotation in Figure 3. 3.2. Examples predicates, and their intended meanings In Figure 3we will build a notion (in fact, three notions) of logical validity; and in Figures 4and 5we will extend our syntax with useful macros (syntactic sugar). However, even before we do that, we can use the syntax from Figure 2show how some properties of interest to distributed systems can be expressed. We assume an event echo ∈ESym and an atomic predicate symbol live ∈PSym: 23 This is just as in natural language. The English predicate ‘The cat sits on the mat’ asserts that the cat sits on the mat. That is, the sentence ‘The cat sits on the mat’ is true when the cat does sit on the mat, i.e. when the event “the cat sits on the mat” is actually happening, and it is false when the cat does not sit on the mat, i.e. what that event is not happening. Thus observe in English that the predicate ‘The cat sits on the mat’ and the event “the cat sits on the mat” are written identically (here we use single quote marks around the predicate and double quote marks around the (linguistic representation of) the event). DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |25 4. Define an in-place accessibility relation ≪− such that for (𝑝, 𝑥, 𝐻),(𝑝′, 𝑥′, 𝐻′) ∈ World(M), (𝑝′, 𝑥′, 𝐻′) ≪−(𝑝, 𝑥, 𝐻)when (𝑝′, 𝑥′, 𝐻′) ∈ 𝐻∧𝑝′=𝑝. Equivalently using Definition 2.2.6(1), 𝑤′≪−𝑤when 𝑤′∈time(𝑤) ∧ place(𝑤′)=place(𝑤). Lemma 3.4.3.Suppose Mis a model and 𝑤′,𝑤 ∈World(M). Then 𝑤′≪𝑤implies time(𝑤′) ≺− time(𝑤) ∧ time(𝑤′)⊊time(𝑤). Proof. Suppose 𝑤′≪𝑤 . By Definition 3.4.2(3) 𝑤′∈time(𝑤) . By assumption time(𝑤) ≺− H or time(𝑤)=H ; in either case, time(𝑤) is a history structure. By Definition 2.3.1(1) (since 𝑤′∈time(𝑤) ) time(𝑤′) ≺− time(𝑤) , and by Definition 2.3.2 and Remark 2.3.3 time(𝑤′)⊊time(𝑤).□ Lemma 3.4.4 is a correctness check that we can set Time(M)={𝐻|𝐻⪯ −H} in Definition 3.4.2(1), rather than {𝐻|𝐻⪯ −∗H} , where ⪯ −∗ denotes the transitive closure of ⪯ −: Lemma 3.4.4.Suppose Mis a model and 𝑤,𝑤′∈World(M). Then 𝑤′≪𝑤implies time(𝑤′) ≺− H. Proof. By Definition 3.4.2(2) time(𝑤) ⪯ −H , which means that time(𝑤) ≺− H or time(𝑤)=H. • If time(𝑤)=H then by Lemma 3.4.3 (since 𝑤′≪𝑤 ) time(𝑤′) ≺− H as required. • If time(𝑤) ≺− H then by Lemma 3.4.3 we have time(𝑤′) ≺− time(𝑤) ≺− H and by Lemma 2.3.12(1) (element-transitivity of history structures) time(𝑤′) ≺−H . □ Proposition 3.4.5 (Transitivity and irreflexivity of accessibility).Suppose M= (P,H, 𝜚, 𝜍) is a model. Then the accessibility relation ≪ from Definition 3.4.2(3) is transitive and irreflexive. That is: ∀𝑤,𝑤′,𝑤′′ ∈World(M). 𝑤′′ ≪𝑤′=⇒𝑤′≪𝑤=⇒𝑤′′ ≪𝑤 and ∀𝑤∈World(M).¬(𝑤≪𝑤). Proof. Suppose 𝑤′′ ≪𝑤′ and 𝑤′≪𝑤 . By Definition 3.4.2(3) 𝑤′′ ∈time(𝑤′) and by Lemma 3.4.3 time(𝑤′)⊊time(𝑤) , so 𝑤′′ ∈time(𝑤) . By Definition 3.4.2(3) again 𝑤′′ ≪𝑤as required. Irreflexivity is a simple corollary of Lemma 3.4.3, since time(𝑤)⊊time(𝑤) is impossible. □ DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |32 3.4.2. Sequentiality Remark 3.4.6.We need the notion of sequentiality for Figure 3, to interpret the proposition seq . Intuitively, 𝑝 is sequential in 𝐻 when 𝑝 performs its actions in sequence, according to 𝐻 . Sequentiality will be important to our later mathematics because, for our needs, sequential participants will be the ‘good’ ones. In Remark 5.1.6 we will note a more abstract but more permissive orderability condition that would also suffice for our needs. A technical definition will help us define sequentiality in Definition 3.4.9: Definition 3.4.7.Suppose 𝑝∈Pand 𝐻∈Time(M). Define 𝐻@𝑝the history 𝑯at 𝒑or set of event-tuples at 𝒑by 𝐻@𝑝={𝑤∈𝐻|place(𝑤)=𝑝}. Remark 3.4.8.Note that: 1. 𝐻@𝑝 is a prehistory but it need not be a history, because it might not be transitive (Definition 2.3.2) (this will not be a problem; we will only ever use it as a set). 2. Recalling from Definition 3.4.2(3) that 𝑤′≪𝑤when 𝑤′∈time(𝑤), a nice characterisation of 𝑤′≪−𝑤from Definition 3.4.2(4) is 𝑤′≪−𝑤if and only if 𝑤′∈time(𝑤)@place(𝑤). Definition 3.4.9 (Sequentiality).Suppose 𝑝∈Pand 𝐻∈Time(M). 1. Call 𝑝sequential at 𝐻when ∀𝑤,𝑤′∈𝐻@𝑝.(𝑤≪𝑤′∨𝑤′≪𝑤∨𝑤=𝑤′). In words: 𝑝is sequential in 𝐻when event-tuples at 𝑝occur in sequence in 𝐻. 2. Call 𝐻sequential when ∀𝑤,𝑤′∈𝐻.(𝑤≪𝑤′∨𝑤′≪𝑤∨𝑤=𝑤′) In words: 𝐻is sequential when event-tuples in 𝐻occur in sequence. 3.4.3. Validity Definition 3.4.10 (Validity).Suppose M is a model and 𝑤∈World(M) and 𝜙 is a closed predicate. Then we define three validity judgements as follows: 1. Define possible world validity 𝑤⊨𝜙inductively by the rules in Figure 3. Write 𝑤=(𝑝, 𝑥, 𝐻) . In the judgement “ 𝑝, 𝑥, 𝐻 ⊨𝜙 ”, we may follow Definition 2.2.6(2) and call 𝑝 the place, 𝑥 the (maybe-)event, and 𝐻 the time of the judgement. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |33 false 𝑤⊨⊥⊥⊥⊥⊥⊥⊥ ⊥ ⊥ ⇐⇒ ⊥ implies 𝑤⊨𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝜙′⇐⇒ (𝑤⊨𝜙=⇒𝑤⊨𝜙′) equality 𝑤⊨𝑣======= = =𝑣⇐⇒ ⊤ inequality 𝑤⊨𝑣======= = =𝑣′⇐⇒ ⊥ (𝑣′not equal to 𝑣) forall 𝑤⊨∀∀∀∀∀∀∀ ∀ ∀𝑎.𝜙 ⇐⇒ ∀𝑣∈Value.(𝑤⊨𝜙[𝑎:=𝑣]) event 𝑝, 𝑥, 𝐻 ⊨𝐸⇐⇒ (𝑥=𝐸∧ (𝑝, 𝐸, 𝐻) ∈ H) atomic predicate 𝑝, 𝑥, 𝐻 ⊨𝑃⇐⇒ 𝑃∈𝜚(𝑝, 𝐻) in the past 𝑤⊨↓𝜙⇐⇒ ∃𝑤′≪−𝑤. (𝑤′⊨𝜙) end of time 𝑝, 𝑥, 𝐻 ⊨ | → 𝜙⇐⇒ 𝑝, † ,H⊨𝜙 admission 𝑝, 𝑥, 𝐻 ⊨ ♢ 𝑙1...𝑙𝑛𝜙⇐⇒ ∀(𝑂1, . . . ,𝑂𝑛) ∈ 𝜍(𝑙1) × · · · × 𝜍(𝑙𝑛). ∃𝑝′∈𝑂1∩ · · · ∩ 𝑂𝑛.(𝑝′, † , 𝐻 ⊨𝜙) sequentiality 𝑝, 𝑥, 𝐻 ⊨seq ⇐⇒ 𝑝sequential at 𝐻 validity (end-of-time) ⊨𝜙⇐⇒ ∀𝑝∈P.(𝑝, † ,H⊨𝜙) validity (all-world) □ W⊨𝜙⇐⇒ ∀𝑤∈World(M).(𝑤⊨𝜙) Above: • We assume a fixed signature Σ=(VSym,ESym,PSym,Value) (Definition 3.1.1) and model M=(P,H, 𝜚, 𝜍) (Definition 3.3.3) for that signature. •𝑤∈World(M)is a world (Definition 3.4.2(2)). •𝑝∈P is a participant, and 𝐸 is an event in the sense of Definition 3.1.1(2), i.e. 𝐸=E(𝑣1, . . . , 𝑣𝑛)for some 𝑣1, . . . , 𝑣𝑛∈Value (and for some 𝑛). •𝑤′≪−𝑤 is from Definition 3.4.2(4) and means 𝑤′∈time(𝑤)∧place(𝑤′)= place(𝑤). •𝑝 being sequential at 𝐻 is from Definition 3.4.9 (see also Lemma 5.1.2). • The italic text in the leftmost column (‘false’, ‘implies’, etc) is just a reminder of how to read the connective. It has no formal meaning; it is just a useful hint. The terminology ‘admission’ for ♢ is put in context in Remark 3.6.3. • In the first line, ⊥⊥⊥⊥⊥⊥⊥ ⊥ ⊥ on the left represents the formal symbol from our predicate syntax in Figure 2(object-level), and ⊥ on the right represents logical false (meta-level). In the next line, ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ is an object-level symbol and =⇒ is meta-level implication. Similarly for ======= = = and = , for ∀∀∀∀∀∀∀ ∀ ∀ and ∀ , and so on. Figure 3. Validity (Definition 3.4.10) DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |34 2. Define omniscient or end-of-time validity by ⊨𝜙 when 𝑝, † ,H⊨𝜙 for every 𝑝∈P. 3. Define all-world validity by □ W⊨𝜙when 𝑤⊨𝜙for every 𝑤∈World(M). Where we write just ‘validity’, it will always be clear which kind of validity we refer to. When we write 𝑤⊨𝜙 , ⊨𝜙 , or □ W⊨𝜙 , it will always be clear (or unimportant) with respect to which model we intend this. Remark 3.4.11 (Validity and time).The treatments of validity and time in the judgement 𝑤⊨𝜙 from Definition 3.4.10 and Figure 3are subtle. We make some observations: 1. Possible world validity 𝑤⊨𝜙 is a standard-looking modal validity judgement that 𝜙is valid (or is not valid) at the possible world 𝑤∈World(M). However, Figure 3defines two more validity judgements: end-of-time validity ⊨ 𝜙 and all-world validity □ W⊨𝜙 . We discuss and contrast these in Subsection 5.2. Briefly: we use □ W⊨𝜙 to impose axioms on a model, and ⊨𝜙 to assert correctness properties that look retrospectively back on the model as viewed from the end of time. 2. In 𝑤⊨𝜙, note that: •𝑤 has the form (𝑝, 𝑥, 𝐻) for any 𝑝∈P and 𝑥∈Event † and 𝐻∈H∨𝐻= H. • We do not make the stricter requirement that 𝑤∈H . That is, 𝑤 does not have to be an event-tuple that actually occurs in H : this could be because 𝐻=H , or because 𝑥 is a maybe-event such that (𝑝, 𝑥, 𝐻)∉H (even though perhaps (𝑝, 𝑥′, 𝐻) ∈ Hfor some other choice of 𝑥′∈Event † ).27 This is deliberate: the | → modality takes us to the end of time, where by definition no events occur, so for the validity judgement ⊨𝜙 (meaning 𝑝, † ,H⊨𝜙 for every 𝑝 ) to make sense, we need to consider possible worlds other than just those in H. Similarly when we interpret 𝑤⊨ ♢ 𝑙1...𝑙𝑛𝜙 we consider (𝑝′, † ,time(𝑤)) , a possible world for which there is no guarantee that (𝑝′, † ,time(𝑤)) ∈ H. This is why we define World(M)=P×Event † ×Time(M) in Definition 3.4.2(2). This is inherent and a feature of our design. Conversely, defining World(M) to be just equal to Hwould be too weakly-structured for what Figure 3requires. 27 This comes from the fact that we define World(M)=P×Event † ×Time(M)in Definition 3.4.2(2). Design alternative: We could refine Definition 3.4.2(2) such that World(M)=H∪ {(𝑝, † , 𝐻) | 𝐻⪯ −H} , where ⪯ − is the notion of non-strict element of from Definition 2.3.1(2). It turns out (this is not obvious) that with this definition our results would work just as well. The key observation is that if we start from 𝑤 in the refined set then every operation on possible worlds in Figure 3keeps us within it. For computational purposes (e.g. model-checking) the refined set may be helpful, because it is smaller; but for our purposes Definition 3.4.2(2) suffices, and it is conceptually simple, so we use that. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |35 3. Continuing the previous point and contrasting with it — the in the past modality ↓ looks specifically for a possible world in H . We unpack the clause for 𝑤⊨↓𝜙 in Figure 3: 𝑤⊨↓𝜙⇐⇒ ∃𝑤′≪−𝑤. (𝑤′⊨𝜙)Figure 3 ⇐⇒ ∃𝑤′≪𝑤. (place(𝑤′)=place(𝑤) ∧ 𝑤′⊨𝜙)Def. 3.4.2(4) ⇐⇒ ∃𝑤′∈time(𝑤).(place(𝑤′)=place(𝑤) ∧ 𝑤′⊨𝜙)Def. 3.4.2(3) It follows from the above and from Lemma 3.4.3 that time(𝑤′) ∈ H. Note also that the interpretation of 𝑤⊨𝐸 (for 𝐸 an event) also appeals to whether a possible world is in H. So two notions of possible world coexist in Figure 3, in a kind of creative tension: • There are 𝑤∈World(M) , which we call possible worlds in Definition 3.4.2(2). •There are 𝑤∈H, which we call event-tuples in Definition 2.2.6(1). We require the former to interpret □ W⊨𝜙 and | → and ♢ in Figure 3, and we require the latter to interpret ↓and 𝐸. 3.5. Active and inactive participants It will be helpful later if we make a short technical detour and introduce the notion of (in)active participants: Definition 3.5.1 ((In)active participants).Call 𝑝 active in H when H@𝑝≠∅ . Unpacking Definition 3.4.7 this means that there exists some 𝑤∈H with place(𝑤)=𝑝 . If 𝑝 is not active (so H contains no event-tuple starting with 𝑝 ) then call it inactive in H. Usually H will be fixed or understood, so we will just call 𝑝 (in)active, without mentioning H explicitly. Intuitively, a participant is active when it is the location of at least one event. Remark 3.5.2.The empty model from Example 3.3.5 is characterised precisely by being such that all of its participants are inactive. The minimal model from Example 3.3.6 is simplest such that all of its participants are active. Lemma 3.5.3.Suppose M is a model with history structure H and suppose 𝑝∈P. Then the following are equivalent: 1. 𝑝, † ,H⊨↓⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤. 2. 𝑝is active (there is an event-tuple in Hstarting with 𝑝; Definition 3.5.1). As a corollary, ⊨↓⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤if and only if all participants are active. Proof. We just unpack the definitions in Figure 3.□ DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |36 Sugar for basic propositions & predicates ¬¬¬¬¬¬¬ ¬ ¬𝜙=(𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒⊥⊥⊥⊥⊥⊥⊥ ⊥ ⊥) ⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤=¬¬¬¬¬¬¬ ¬ ¬⊥⊥⊥⊥⊥⊥⊥ ⊥ ⊥ 𝜙∨∨∨∨∨∨∨ ∨ ∨𝜙′=((¬¬¬¬¬¬¬ ¬ ¬𝜙)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝜙′)𝜙∧∧∧∧∧∧∧ ∧ ∧𝜙′=¬¬¬¬¬¬¬ ¬ ¬((¬¬¬¬¬¬¬ ¬ ¬𝜙) ∨∨∨∨∨∨∨ ∨ ∨ (¬¬¬¬¬¬¬ ¬ ¬𝜙′)) 𝜙⇔⇔⇔⇔⇔⇔⇔ ⇔ ⇔𝜙′=(𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝜙′) ∧∧∧∧∧∧∧ ∧ ∧ (𝜙′⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝜙) ∃∃∃∃∃∃∃ ∃ ∃𝑎.𝜙 =¬¬¬¬¬¬¬ ¬ ¬∀∀∀∀∀∀∀ ∀ ∀𝑎.¬¬¬¬¬¬¬ ¬ ¬𝜙 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01𝑎.𝜙 =∀∀∀∀∀∀∀ ∀ ∀𝑎,𝑏.𝜙 ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝜙[𝑎:=𝑏]⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝑎======= = =𝑏∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑎.𝜙 =(∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01𝑎.𝜙) ∧∧∧∧∧∧∧ ∧ ∧∃∃∃∃∃∃∃ ∃ ∃𝑎.𝜙 Sugar for time ⇓𝜙=¬¬¬¬¬¬¬ ¬ ¬↓¬¬¬¬¬¬¬ ¬ ¬𝜙 ↕𝜙= | → ↓𝜙⇕𝜙=¬¬¬¬¬¬¬ ¬ ¬↕¬¬¬¬¬¬¬ ¬ ¬𝜙= | → ⇓𝜙 Sugar for the modality ♢ ↓↓↓↓↓↓↓ ↓ ↓ □𝑙1...𝑙𝑛𝜙=¬¬¬¬¬¬¬ ¬ ¬ ♢ 𝑙1...𝑙𝑛¬¬¬¬¬¬¬ ¬ ¬𝜙 □ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙=□𝑙1...𝑙𝑛↓𝜙 ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙= ♢ 𝑙1...𝑙𝑛↓𝜙 □ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓𝑙1...𝑙𝑛𝜙=□ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛⇓𝜙 ♢ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓𝑙1...𝑙𝑛𝜙= ♢ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓𝑙1...𝑙𝑛⇓𝜙 □𝜙=□∅𝜙 ♢ 𝜙= ♢ ∅𝜙 Above, 𝜙[𝑎:=𝑏]denotes the usual capture-avoiding substitution of 𝑏for 𝑎. Figure 4. Extended (sugared) syntax (Definition 3.6.1) 3.6. Extending syntax with syntactic sugar The core syntax from Figure 2is expressive, and it will be convenient to use sugar as follows: Definition 3.6.1 (Syntactic sugar).We define syntactic sugar as described in Figure 4, and we unpack the corresponding denotation in Figure 5. Remark 3.6.2 (de Morgan dualities).We recall some standard background on logic and negation.28 Logical connectives — quantifiers, modalities, and propositional connectives — tend to come in pairs, which are dual to one another by negation in a standard way. Standard dualities include: 1. forall/exist duality ∀∀∀∀∀∀∀ ∀ ∀𝑎.𝜙 =¬¬¬¬¬¬¬ ¬ ¬∃∃∃∃∃∃∃ ∃ ∃𝑎.¬¬¬¬¬¬¬ ¬ ¬𝜙and ∃∃∃∃∃∃∃ ∃ ∃𝑎.𝜙 =¬¬¬¬¬¬¬ ¬ ¬∀∀∀∀∀∀∀ ∀ ∀𝑎.¬¬¬¬¬¬¬ ¬ ¬𝜙. 2. and/or duality 𝜙∧∧∧∧∧∧∧ ∧ ∧𝜓=¬¬¬¬¬¬¬ ¬ ¬(¬¬¬¬¬¬¬ ¬ ¬𝜙∨∨∨∨∨∨∨ ∨ ∨ ¬¬¬¬¬¬¬ ¬ ¬𝜓)and 𝜙∨∨∨∨∨∨∨ ∨ ∨𝜓=¬¬¬¬¬¬¬ ¬ ¬(¬¬¬¬¬¬¬ ¬ ¬𝜙∧∧∧∧∧∧∧ ∧ ∧ ¬¬¬¬¬¬¬ ¬ ¬𝜓). 3. every/some duality In modal logic, we have □𝜙=¬¬¬¬¬¬¬ ¬ ¬ ♢ ¬¬¬¬¬¬¬ ¬ ¬𝜙 and ♢ 𝜙=¬¬¬¬¬¬¬ ¬ ¬□¬¬¬¬¬¬¬ ¬ ¬𝜙 . All definitions will be written out in full, but the reader should just note that usually these connectives come in pairs and we will structure our definitions accordingly. 28 The reader who is already familiar with de Morgan dualities should please be patient: de Morgan duality is surprising and not necessarily intuitive to the uninitiated reader. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |37 𝑤⊨⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤ ⇐⇒ ⊤ 𝑤⊨¬¬¬¬¬¬¬ ¬ ¬𝜙⇐⇒ 𝑤⊭𝜙 𝑤⊨𝜙∨∨∨∨∨∨∨ ∨ ∨𝜙′⇐⇒ (𝑤⊨𝜙)∨(𝑤⊨𝜙′) 𝑤⊨𝜙∧∧∧∧∧∧∧ ∧ ∧𝜙′⇐⇒ (𝑤⊨𝜙)∧(𝑤⊨𝜙′) 𝑤⊨𝜙⇔⇔⇔⇔⇔⇔⇔ ⇔ ⇔𝜙′⇐⇒ ((𝑤⊨𝜙) ⇐⇒ (𝑤⊨𝜙′)) 𝑤⊨∃∃∃∃∃∃∃ ∃ ∃𝑎.𝜙 ⇐⇒ ∃𝑣∈Value.(𝑤⊨𝜙[𝑎:=𝑣]) 𝑤⊨∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01𝑎.𝜙 and 𝑤⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑎.𝜙 are as expected 𝑤⊨⇓𝜙⇐⇒ ∀𝑤′≪−𝑤. (𝑤′⊨𝜙) 𝑤⊨↕𝜙⇐⇒ ∃𝑤′∈H@place(𝑤).(𝑤′⊨𝜙) 𝑤⊨⇕𝜙⇐⇒ ∀𝑤′∈H@place(𝑤).(𝑤′⊨𝜙) 𝑤⊨□𝑙1...𝑙𝑛𝜙⇐⇒ ∃(𝑂1, . . . ,𝑂𝑛) ∈ 𝜍(𝑙1) × · · · × 𝜍(𝑙𝑛). ∀𝑝′∈𝑂1∩ · · · ∩ 𝑂𝑛.(𝑝′, † ,time(𝑤)⊨𝜙) (𝑤⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙) ⇐⇒ ∀(𝑂1, . . . ,𝑂𝑛) ∈ 𝜍(𝑙1) × · · · × 𝜍(𝑙𝑛). ∃𝑤′≪𝑤. (𝑝′, 𝐻′⊨𝜙) 𝑤⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙⇐⇒ ∃(𝑂1, . . . ,𝑂𝑛) ∈ 𝜍(𝑙1) × · · · × 𝜍(𝑙𝑛). ∀𝑝′∈𝑂1∩ · · · ∩ 𝑂𝑛.∃𝑤′≪𝑤. (place(𝑤′)=𝑝′∧𝑤′⊨𝜙) 𝑤⊨ ♢ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓𝑙1...𝑙𝑛𝜙⇐⇒ ∀(𝑂1, . . . ,𝑂𝑛) ∈ 𝜍(𝑙1) × · · · × 𝜍(𝑙𝑛). ∃𝑝′∈𝑂1∩ · · · ∩ 𝑂𝑛.∀𝑤′≪𝑤. (place(𝑤′)=𝑝′=⇒𝑤′⊨𝜙) 𝑤⊨□ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓𝑙1...𝑙𝑛𝜙⇐⇒ ∃(𝑂1, . . . ,𝑂𝑛) ∈ 𝜍(𝑙1) × · · · × 𝜍(𝑙𝑛). ∀𝑝′∈𝑂1∩ · · · ∩ 𝑂𝑛.∀𝑤′≪𝑤. (place(𝑤′)=𝑝′=⇒𝑤′⊨𝜙) 𝑝, 𝑥, 𝐻 ⊨ ♢ 𝜙⇐⇒ ∃𝑝′∈P.𝑝′, † , 𝐻 ⊨𝜙 𝑝, 𝑥, 𝐻 ⊨□𝜙⇐⇒ ∀𝑝′∈P.𝑝′, 𝑥, 𝐻 ⊨𝜙 Above, 𝑤′≪𝑤is from Definition 3.4.2(3) and means 𝑤′∈time(𝑤). Note that Figure 4defines syntactic sugar — like ⇓𝜙=¬¬¬¬¬¬¬ ¬ ¬↓¬¬¬¬¬¬¬ ¬ ¬𝜙 — and this Figure unpacks the denotation of that sugar as per Figure 3. It is not the case that there are (for example) two ⇓ symbols — indeed, formally there is no symbol ⇓ at all, since it is a macro for ¬¬¬¬¬¬¬ ¬ ¬↓¬¬¬¬¬¬¬ ¬ ¬. Figure 5. Denotation of sugar from Figure 4(Definition 3.6.1) DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |38 Remark 3.6.3.We briefly discuss the sugar in Figure 4, with more details to follow in the Remarks and Lemmas that follow: 1. ¬¬¬¬¬¬¬ ¬ ¬,∧∧∧∧∧∧∧ ∧ ∧, and ∨∨∨∨∨∨∨ ∨ ∨are defined from ⊥⊥⊥⊥⊥⊥⊥ ⊥ ⊥and ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒using standard encodings. 2. ∃∃∃∃∃∃∃ ∃ ∃𝑎.𝜙 =¬¬¬¬¬¬¬ ¬ ¬∀∀∀∀∀∀∀ ∀ ∀𝑎.¬¬¬¬¬¬¬ ¬ ¬𝜙 is also standard: it is the usual de Morgan dual definition of ∃∃∃∃∃∃∃ ∃ ∃ in terms of ∀. 3. ⇓ is the de Morgan dual to ↓ . ↓𝜙 means that 𝜙 holds at the time of some present or past event at the current place, so its de Morgan dual ⇓𝜙 means that 𝜙 holds at the time of every present or past event at the current place. 4. ↕𝜙 and ⇕𝜙 are temporal modal operators (see Subsection 1.3 of [ GHR94 ] for an old but very approachable survey of the genre): •↕𝜙 — read sometime 𝜙 — means that 𝜙 holds at the time of some maybeevent at the current place. •⇕𝜙 — read everytime 𝜙 — means that 𝜙 holds at the time of every maybe-event at the current place. These are de Morgan duals: ↕𝜙 is equivalent to ¬¬¬¬¬¬¬ ¬ ¬⇕¬¬¬¬¬¬¬ ¬ ¬𝜙 and ⇕𝜙 is equivalent to ¬¬¬¬¬¬¬ ¬ ¬↕¬¬¬¬¬¬¬ ¬ ¬𝜙. 5. □𝑙1...𝑙𝑛𝜙=¬¬¬¬¬¬¬ ¬ ¬ ♢ 𝑙1...𝑙𝑛¬¬¬¬¬¬¬ ¬ ¬𝜙 . This defines □𝑙1...𝑙𝑛𝜙 as the de Morgan dual to ♢ 𝑙1...𝑙𝑛𝜙 . 6. The ∅in ♢ 𝜙= ♢ ∅𝜙and □𝜙=□∅𝜙denotes the empty list (of learners). 7. Eight modalities are definable and will be of interest. We list them: (a) ♢ 𝑙1...𝑙𝑛𝜙 means ‘ 𝜙 holds somewhere in every 𝑙1. . .𝑙𝑛 -quorum intersection’. We may read this as all 𝑙1. . .𝑙𝑛-quorum intersections admit 𝝓. (b) □𝑙1...𝑙𝑛𝜙 means ‘ 𝜙 holds everywhere in some 𝑙1. . .𝑙𝑛 -quorum intersection’. We may read this as some 𝑙1. . .𝑙𝑛-quorum intersection agrees on 𝝓. (c) ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙 means ‘ 𝜙 held in the past somewhere in every quorum intersection’. We may read this as all 𝑙1. . .𝑙𝑛-quorum intersections admit past 𝝓. (d) □ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙 means ‘ 𝜙 held in the past everywhere in some quorum intersection’. We may read this as some 𝑙1. . .𝑙𝑛-quorum intersection agrees on past 𝝓. (e) ♢ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓𝑙1...𝑙𝑛𝜙 means ‘ 𝜙 held up to (not including) now somewhere in every quorum intersection’. We may read this as all 𝑙1. . .𝑙𝑛 -quorum intersections admit 𝝓 up to (but not necessarily including) now. (f) □ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓𝑙1...𝑙𝑛𝜙 means ‘ 𝜙 held up to (not including) now everywhere in some quorum intersection’. We may read this as DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |39 some 𝑙1. . .𝑙𝑛 -quorum intersection agrees on 𝝓 up to (but not necessarily including) now. (g) We may read ♢ 𝜙 as 𝜙 holds somewhere (now), and □𝜙 as 𝜙 holds everywhere (now). We will justify the terminology above, with the results that follow below. In our usage, ‘admit’ is the de Morgan dual to ‘agree’, because ♢ is the de Morgan dual to □. That is: we admit 𝜙if we do not agree on not-𝜙. We check correctness of some parts of Figure 5: Lemma 3.6.4.Suppose M is a model and 𝑤∈World(M) . Then as per Figure 5: 1. The following are equivalent: •𝑤⊨↕𝜙 •∃𝑤′∈H.(place(𝑤′)=place(𝑤) ∧ 𝑤′⊨𝜙) •∃𝑤′∈H@place(𝑤). 𝑤′⊨𝜙. 2. The following are equivalent: •𝑤⊨⇕𝜙 •∀𝑤′∈H.(place(𝑤′)=place(𝑤)=⇒𝑤′⊨𝜙) •∀𝑤′∈H@place(𝑤). 𝑤′⊨𝜙. 3. The following are equivalent: •𝑤⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙 •∀(𝑂1, . . . ,𝑂𝑛) ∈ 𝜍(𝑙1) × · · · × 𝜍(𝑙𝑛).∃𝑤′≪𝑤.(place(𝑤′) ∈ 𝑂1∩ · · · ∩ 𝑂𝑛∧𝑤′⊨𝜙) Proof. Part 2follows from part 1by de Morgan duality, so we focus on part 1. We reason as follows, where we take 𝑤=(𝑝, 𝑥, 𝐻): 𝑤⊨↕𝜙⇐⇒ 𝑤⊨ | → ↓𝜙Figure 4 ⇐⇒ 𝑝, † ,H⊨↓𝜙Figure 3 ⇐⇒ ∃𝑤′≪−(𝑝, † ,H). 𝑤′⊨𝜙Figure 3 ⇐⇒ ∃𝐻′, 𝑥′.(𝑝, 𝑥′, 𝐻′) ∈ H∧𝑝, 𝑥′, 𝐻′⊨𝜙Definition 3.4.2(4) The equivalences then follow from the definitions ( H@place(𝑤) is from Definition 3.4.7). DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |40 For part 3we unpack ♢ ↓↓↓↓↓↓↓ ↓ ↓as ♢ and ↓and use Figure 3as follows: 𝑝, 𝑥, 𝐻 ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙 ⇐⇒ 𝑝, 𝑥, 𝐻 ⊨ ♢ 𝑙1...𝑙𝑛↓𝜙Figure 4 ⇐⇒ ∀(𝑂1, . . . ,𝑂𝑛) ∈ 𝜍(𝑙1) × · · · × 𝜍(𝑙𝑛). ∃𝑝′∈𝑂1∩ · · · ∩ 𝑂𝑛. 𝑝′, † , 𝐻 ⊨↓𝜙Figure 3 ⇐⇒ ∀(𝑂1, . . . ,𝑂𝑛) ∈ 𝜍(𝑙1) × · · · × 𝜍(𝑙𝑛). ∃𝑝′∈𝑂1∩ · · · ∩ 𝑂𝑛.∃𝑤′≪𝑤. (place(𝑤′)=𝑝′∧𝑤′⊨𝜙)Figure 3 ⇐⇒ ∀(𝑂1, . . . ,𝑂𝑛) ∈ 𝜍(𝑙1) × · · · × 𝜍(𝑙𝑛).∃𝑤′≪𝑤. (place(𝑤′) ∈ 𝑂1∩ · · · ∩ 𝑂𝑛∧𝑤′⊨𝜙)Fact □ Remark 3.6.5.We unpack some common special cases of Figures 4and 5: 1. 𝑝, 𝑥, 𝐻 ⊨□𝑙𝜙means that there exists an 𝑙-quorum 𝑂such that 𝑝′, † , 𝐻 ⊨𝜙for every 𝑝′∈𝑂. In words we say: an 𝒍-quorum agrees that 𝝓. 2. 𝑝, 𝑥, 𝐻 ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙 means that there exists an 𝑙 -quorum 𝑂 such that for every 𝑝′∈𝑂 , some (𝑝′, 𝑥′, 𝐻′) ∈ 𝐻exists such that 𝑝′, 𝑥′, 𝐻′⊨𝜙. Equivalently, 𝑤⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙 when there exists an 𝑙 -quorum 𝑂∈𝜍(𝑙) of participants such that for every 𝑝′∈𝑂 there exists 𝑤′≪𝑤 (Definition 3.4.7) such that place(𝑤′′)=𝑝′and 𝑤′′ ⊨𝜙. Equivalently again, 29 𝑤⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙 when there exists an 𝑙 -quorum 𝑂∈𝜍(𝑙) of participants such that for every 𝑝′∈𝑂 there exists 𝑤′∈𝐻@𝑝′ such that 𝑤′′ ⊨𝜙 . In words we say: an 𝒍-quorum agrees that 𝝓in the past. 3. 𝑝, 𝑥, 𝐻 ⊨□ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓𝑙𝜙 means that there exists an 𝑙 -quorum 𝑂 such that for every 𝑤′∈𝐻 , we have 𝑤′⊨𝜙. 4. We leave it to the reader to unpack □𝑙1...𝑙𝑛𝜙,□ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙, and □ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓𝑙1...𝑙𝑛𝜙. We may read □ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙as a(n 𝒍1. . . 𝒍𝒏-)quorum intersection agrees that 𝝓. 5. Matters simplify further when 𝐻=H: Thus: •⊨ ♢ 𝑙𝑙′𝜙 and 𝑝, † ,H⊨ ♢ 𝑙𝑙′𝜙 mean that for every 𝑙 -quorum and 𝑙′ -quorum, there exists a 𝑝′in their intersection such that 𝑝′, † ,H⊨𝜙. •⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝑙′𝜙 and 𝑝, † ,H⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝑙′𝜙 mean that for every 𝑙 -quorum and 𝑙′ - quorum, there exists a 𝑝′ in their intersection and some 𝑤′∈H such that place(𝑤′)=𝑝′and 𝑤′⊨𝜙. •We leave it to the reader to unpack □𝑙𝑙′𝜙,□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝑙′𝜙, ♢ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓𝑙𝑙′𝜙, and □ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓𝑙𝑙′𝜙. Remark 3.6.6.We unpack the modalities ♢ , □ , ♢ ↓↓↓↓↓↓↓ ↓ ↓ , ♢ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓ , □ ↓↓↓↓↓↓↓ ↓ ↓ , and ♢ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓ . We consider each modality in turn. 29 Is unpacking this three times overdone? Not really. We will use □ ↓↓↓↓↓↓↓ ↓ ↓𝑙 a lot, so it might help some readers to explicitly unpack a range of possible contexts. If these three formulations and their equivalence are already obvious to the reader, then so much the better. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |41 1. By Remark 3.6.5(2) 𝑤⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙 when there exists 𝑂∈𝜍(𝑙) such that for every 𝑝′∈𝑂 there exists 𝑤′≪𝑤 such that place(𝑤′)=𝑝′ and 𝑤⊨𝜙 . Now 𝑂⊆P is assumed nonempty by Definition 3.3.2(3), so by assumption there exists some 𝑝′∈𝑂 and 𝑤′≪𝑤 such that place(𝑤′)=𝑝′ and 𝑤′⊨𝜙 . Thus there exists 𝑤′≪𝑤such that 𝑤′⊨𝜙, and by Remark 3.6.6(3)𝑤⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝜙. 2. ⊨□𝑙𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ 𝜙 follows by similar arguments to part 1, or directly from part 1 taking 𝜙= | → 𝜙′. ⊨□𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ 𝜙 also follows by similar arguments to part 1, using the fact in Definition 3.3.3 that we assumed P≠∅. 3. The intersection 𝑂1∩ · · · ∩ 𝑂𝑛might be empty. 4. 𝑝 need not be in every quorum intersection (indeed, as just observed, the intersection might be empty). □ Lemma 4.2.2.Suppose 𝑤∈World(M)and 𝜙is a closed predicate. Then 𝑤⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝜙. This corresponds to the traditional (4) axiom from modal logic, which is usually written dually as “ □𝐴=⇒□□𝐴 ” and is one of the signature axioms of the modal logic S4 . In the standard Kripke semantics for (standard) modal logic, it corresponds to the accessibility relation being transitive. Proof. We reason using equation (1) in Remark 3.6.6 and Proposition 3.4.5 (transitivity of the accessibility relation), as follows: 𝑤⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝜙⇐⇒ ∃𝑤′′ ≪−𝑤′≪−𝑤. 𝑤′′ ⊨𝜙Equation (1) =⇒ ∃𝑤′′ ≪−𝑤. 𝑤′′ ⊨𝜙Proposition 3.4.5 ⇐⇒ 𝑤⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝜙Equation (1)□ Lemma 4.2.3.Suppose 𝑤∈World(𝑚𝑜𝑑𝑒𝑙) and 𝑙∈Learner and 𝜙 is a closed predicate. Then: 1. 𝑤⊨↓□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙. 2. 𝑤⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙. This axiom seems analogous to the traditional (B) axiom, usually written dually as “ ♢ 𝐴=⇒□ ♢ 𝐴 ” (‘B’ stands for the logician Brouwer), and is the signature axiom of the modal logic B . In the standard Kripke semantics for (standard) modal logic, it corresponds to the accessibility relation being symmetric. 3. The reverse implications need not hold. Proof. We consider each part in turn: DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |48 1. By Figure 3, if 𝑤⊨↓□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙 then there exists 𝑤′≪−𝑤 (Definition 3.4.2(4)) such that 𝑤′⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙 . By Remark 3.6.5(2) there exists an 𝑙 -quorum 𝑂∈𝜍(𝑙) of participants such that for every 𝑝′∈𝑂 there exists 𝑤′≪𝑤 such that place(𝑤′)=𝑝′ and 𝑤′⊨𝜙. By Proposition 3.4.5 (transitivity of the accessibility relation; since 𝑤′≪𝑤 ) also 𝑤′′ ≪𝑤and by Remark 3.6.5(2) again, 𝑤⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙as required. 2. The argument for part 2is almost identical. 3. It suffices to provide a counterexample. Consider Event ={𝐸1, 𝐸2, 𝐹 } (three distinct events) and P={𝑝} (just one participant) and one learner 𝑙 with one quorum equal to P. Define 𝐻1={(𝑝, 𝐸1,∅)} 𝐻2={(𝑝, 𝐸2,∅)} 𝐻3={(𝑝, 𝐹, 𝐻1)} ∪ 𝐻1𝐻4={(𝑝, 𝐹, 𝐻2)} ∪ 𝐻2 H=𝐻3∪𝐻4 We illustrate Hin derivation tree style: 𝑝⊢𝐸1 𝑝⊢𝐹 𝑝⊢𝐸2 𝑝⊢𝐹 end of time Then the reader can check that 𝑝, † ,H⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝐹 but 𝑝, † ,H⊨¬¬¬¬¬¬¬ ¬ ¬↓□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝐹 and 𝑝, † ,H⊨ ¬¬¬¬¬¬¬ ¬ ¬ ♢ ↓↓↓↓↓↓↓ ↓ ↓□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝐹.36 □ 5. Sequentiality and liveness 5.1. Properties of sequentiality As per Definition 3.4.9, 𝑝 is sequential at 𝐻 when event-tuples in 𝐻 starting with 𝑝 are linearly ordered. Our logic in Figures 2and 3internalises sequentiality via a predicate seq. In this Subsection, we study sequentiality in more detail. Example 5.1.1.We start with an example to illustrate how sequentiality can be quite subtle. Consider 𝐻={(𝑝, 𝐸, ∅),(𝑝, † ,{(𝑝, 𝐸, ∅)})} and H=𝐻∪ {(𝑝, 𝐸′,∅)}. In derivation tree style we illustrate Has 𝑝⊢𝐸 𝑝⊢ † 𝑝⊢𝐸′ Note that 𝑝, † , 𝐻 ⊨seq (this is trivially so, because there is only one event in the past of 𝐻) but 𝑝, † ,H⊭seq. 36This kind of behaviour is what our theory of liveness from Figure 6is designed to exclude. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |49 With the machinery we have built so far, we can give an attractive characterisation of the clause for 𝑤⊨seq in Figure 3: Lemma 5.1.2.Suppose M is a model and 𝑤∈World(M) . Then the following are equivalent: 1. 𝑤⊨seq. 2. {𝑤′∈World(M) | 𝑤′≪−𝑤}is linearly ordered by ≪. Proof. By Figure 3 𝑤⊨seq holds when place(𝑤) is sequential in time(𝑤) . We check the equivalence by unpacking the definition of sequentiality (Definition 3.4.9(1)) and of the in-place accessibility relation (Definition 3.4.2(4)) and seeing that it is so. □ Lemma 5.1.3.Suppose Mis a model and 𝑤,𝑤′∈World(M). Then 𝑤′≪𝑤implies {𝑤′′ ∈World(M) | 𝑤′′≪−𝑤′}⊆{𝑤′′ ∈World(M) | 𝑤′′≪−𝑤}. Proof. By routine reasoning from the definition of ≪− (Definition 3.4.2(4)) and transitivity of ≪on history structures (Proposition 3.4.5). □ Proposition 5.1.4 (Sequentiality monotone).Suppose M is a model and 𝑤′,𝑤 ∈ World(M). Then: 1. If 𝑤′≪−𝑤then 𝑤⊨seq implies 𝑤′⊨seq. 2. 𝑤⊨seq ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒⇓seq. Proof. We consider each part in turn: 1. By Lemma 5.1.2 𝑤⊨seq when {𝑤′∈World(M) | 𝑤′≪−𝑤} is linearly ordered by ≪. We use Lemma 5.1.3. 2. By Figure 5 𝑤⊨⇓seq when ∀𝑤′≪−𝑤.𝑤′⊨seq , but this just re-states part 1of this result. □ Proposition 5.1.5 is fundamental to our treatment of sequentiality: Proposition 5.1.5.Suppose that: •Mis a model and 𝑤=(𝑝, 𝑥, 𝐻) ∈ World(M). •𝑙,𝑙′∈Learner. •𝜙and 𝜙′are closed predicates and 𝐸,𝐸′are distinct events (meaning 𝐸≠𝐸′). Then: 1. 𝑤⊨ ♢ 𝑙𝑙′seq ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′𝜙′implies 𝑤⊨seq ∧∧∧∧∧∧∧ ∧ ∧ ↓𝜙∧∧∧∧∧∧∧ ∧ ∧ ↓𝜙′. 2. 𝑤⊨seq ∧∧∧∧∧∧∧ ∧ ∧ ↓𝐸∧∧∧∧∧∧∧ ∧ ∧ ↓𝐸′implies 𝑤⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(𝐸∧∧∧∧∧∧∧ ∧ ∧ ↓𝐸′) ∨∨∨∨∨∨∨ ∨ ∨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(𝐸′∧∧∧∧∧∧∧ ∧ ∧ ↓𝐸). 3. 𝑤⊨ ♢ 𝑙𝑙′seq ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝐸∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′𝐸′implies 𝑤⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(𝐸∧∧∧∧∧∧∧ ∧ ∧ ↓𝐸′) ∨∨∨∨∨∨∨ ∨ ∨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(𝐸′∧∧∧∧∧∧∧ ∧ ∧ ↓𝐸). DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |50 Proof. We consider each part in turn. We may write 𝑤 as (𝑝, 𝑥, 𝐻) without comment: 1. Assume 𝑤⊨ ♢ 𝑙𝑙′seq ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′𝜙′. • Following the clause for ♢ in Figure 3, 𝑤⊨ ♢ 𝑙𝑙′seq means that any 𝑙 -quorum intersects any 𝑙′ -quorum at some 𝑝′∈P such that 𝑝, † , 𝐻 ⊨seq . • By Figure 4 □ ↓↓↓↓↓↓↓ ↓ ↓𝑙=□𝑙↓ , and it follows that 𝑤⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙 and 𝑤⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′𝜙′ mean that there exist an 𝑙 -quorum of participants 𝑝′ satisfying 𝑝′, † , 𝐻 ⊨↓𝜙 and an 𝑙′-quorum of participants 𝑝′satisfying 𝑝′, † , 𝐻 ⊨↓𝜙′. Therefore, there exists 𝑝′∈P such that 𝑝′, † , 𝐻 ⊨seq ∧∧∧∧∧∧∧ ∧ ∧ ↓𝜙∧∧∧∧∧∧∧ ∧ ∧ ↓𝜙′ , and so 𝑤⊨seq ∧∧∧∧∧∧∧ ∧ ∧ ↓𝜙∧∧∧∧∧∧∧ ∧ ∧ ↓𝜙′as required. 2. Suppose 𝑤⊨seq ∧∧∧∧∧∧∧ ∧ ∧ ↓𝐸∧∧∧∧∧∧∧ ∧ ∧ ↓𝐸′. Since 𝑤⊨seq , by Lemma 5.1.2 events in 𝐻@𝑝 are linearly ordered. We assumed that 𝐸≠𝐸′ , and so 𝐸 happens before 𝐸′ or vice versa. The result follows. 3. We combine parts 1and 2of this result. □ Remark 5.1.6 (Design alternative: Sequentiality vs. orderability).Sequentiality is a maximalist condition: intuitively, it is the strongest well-behavedness property we could require on a participant, short of allowing it to control other participants or to see the future. When we look at how our sequentiality property is actually used in the proofs, we see that its full power is not required. It would suffice to replace seq in Figure 3with the following weaker (and thus more general) orderability predicate ord: 𝑤⊨ord ⇐⇒ ∀𝐸≠𝐸′∈Event.𝑤 ⊨(↓𝐸∧∧∧∧∧∧∧ ∧ ∧↓𝐸′)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↓(𝐸∧∧∧∧∧∧∧ ∧ ∧↓𝐸′) ∨∨∨∨∨∨∨ ∨ ∨ ↓(𝐸′∧∧∧∧∧∧∧ ∧ ∧↓𝐸)(2) Morally this is just Proposition 5.1.4(2). We could even present orderability as an axiom-scheme ThyOrd with one axiom for each choice of distinct 𝐸 and 𝐸′ as follows: (Order) ord ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒(↓𝐸∧∧∧∧∧∧∧ ∧ ∧ ↓𝐸′)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↓(𝐸∧∧∧∧∧∧∧ ∧ ∧ ↓𝐸′) ∨∨∨∨∨∨∨ ∨ ∨ ↓(𝐸′∧∧∧∧∧∧∧ ∧ ∧ ↓𝐸) This expresses intuitively that events at 𝑝 are orderable in the sense that if 𝑝 has 𝐸and 𝐸′then it has 𝐸′followed by 𝐸, or 𝐸followed by 𝐸′. Orderability is weaker than sequentiality, because the above need not be the same instances of 𝐸 and 𝐸′ . We construct an example to illustrate this, in the derivation-tree style of Examples 2.3.8 and 2.3.10. Assume one participant 𝑝 DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |51 and an event echo. Consider the following history structure: 𝑝⊢echo(1) 𝑝⊢echo(0) 𝑝⊢echo(2) 𝑝⊢echo(0) 𝑝⊢echo(1) 𝑝⊢echo(3) 𝑝⊢echo(2),echo(3) This example history structure 𝑝 is orderable in the sense of equation 2, but it is not sequential in the sense of Definition 3.4.9. This is because sequentiality requires events to be linearly ordered, which clearly they are not in the example above; but nothing in the orderability clause insists that the 𝐸 and 𝐸′ mentioned to the left of the implication are the same instances as the 𝐸 and the 𝐸′ that occur in order to the right of the implication. In fact, an even simpler example is possible: H={(𝑝, † ,∅),(𝑝, echo(),∅)} or in tree form 𝑝⊢ † 𝑝⊢echo() 𝑝 is orderable in H , but not sequential. The reader might like to prove this (answer in footnote).37 Orderability is weaker than sequentiality, and weak assumptions are generally preferable if they lead to the same results. We could remove seq from Figures 2 and 3and instead use a predicate ord with a ‘theory of orderability’ ThyOrd — much as we will define a ‘theory of liveness’ ThyLive in Figure 6. This would be morally satisfying (a smaller core logic with more heavy lifting done by axioms is generally good practice) and more general. Nevertheless, for now we use sequentiality: it is easier to think about, has a clear visual interpretation, and it is pragmatically justified as corresponding to what we think of as a participant following a protocol step-by-step. 5.2. A logical theory of liveness 5.2.1. (Axiomatic) theories We have built a notion of model (Definition 3.3.3), and notions of logical validity over a model given by 𝑤⊨ , ⊨ , and □ W⊨ from Figure 3. We are nearly ready to put this together to develop an axiomatic theory of what it means to be live, which we will do in Definition 5.2.4 and Figure 6. First, we need to state what an axiomatic theory is, and what it means for such a theory to be valid in a model. Recall from from Figure 3, that •⊨𝜙means 𝑝, † ,H⊨𝜙for every 𝑝∈P, and 37 There is only one event to order, namely echo() . The other event-tuple in this example uses the maybeevent † . This is not an event! Thus, it is not in the domain of quantification for the 𝐸 and 𝐸′ in equation (2) . DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |52 •□ W⊨𝜙means 𝑤⊨𝜙for every 𝑤∈World(M). Our notion of validity of a theory in a model is based on □ W⊨𝜙, as follows: Definition 5.2.1.Suppose Σis a signature (Definition 3.1.1). 1. An axiom (over Σ) is a closed predicate 𝜙in the syntax of Figure 2. 2. Suppose M is a model for Σ (Definition 3.3.3) and suppose 𝜙 is an axiom (over Σ). Call 𝜙valid of Mwhen □ W⊨𝜙meaning ∀𝑤∈World(M). 𝑤 ⊨𝜙. (3) 3. A theory is a (possibly infinite) set of axioms.38 4. Suppose M is a model for Σ (Definition 3.3.3) and suppose Thy is a theory over Σ. We define □ W⊨Thy by □ W⊨Thy when ∀𝜙∈Thy.(□ W⊨𝜙). In words, a theory is valid when each of axioms is valid. In this case we may say that Msatisfies or is a model of Thy. Remark 5.2.2.Note that an axiom 𝜙 being valid in a model M is based □ W⊨𝜙 , as per equation 3in Definition 5.2.1 above. That is, on its validity the time and place of every possible world. Note that this definition is not based on ⊨𝜙 (validity at every possible world at the end of time, i.e. having the form (𝑝, † ,H)).39 In fact this is a matter of emphasis: we can derive the effect of ⊨𝜙 using the validity judgement □ W⊨ , just by writing □ W⊨ | → 𝜙 . And indeed we do just this, in the two Knowledge axioms in Figure 6. Remark 5.2.3 (Design choice).An interesting design tension exists between two notions of everywhere: •we have ‘at all events in history’, as in □ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓, and •we have ‘at all possible worlds’, as in □ W. We use both notions, implicitly or explicitly, in our proofs. There are deep reasons for this: it comes from the fact that our syntax in Figure 2contains events and predicates. Events and predicates coexist in our syntax and our axioms, by design. For example, axiom (Safe) in Figure 7 mentions both a predicate safe and an event propose. 38 Infinite theories naturally exist. For instance, if the set of events Event is infinite (we will not consider any examples where this happens) then we might want an axiom-scheme parametric over infinitely many events. Technically, ThyLive in Figure 6is infinite provided there is at least one event and one learner, because it contains the Knowledge axiom-schemes, which are parameterised over events and lists of learners. See the discussion in Remark 5.2.6(1). 39...It is also not based on ⊨ | → □ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓𝜙(validity at every possible world in H). DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |53 (LiveAlways) live ⇔⇔⇔⇔⇔⇔⇔ ⇔ ⇔ | → live (LiveSeq) live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒seq (Knowledge ♢ ↓↓↓↓↓↓↓ ↓ ↓) | → ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛(live ∧∧∧∧∧∧∧ ∧ ∧𝜙)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙 (Knowledge□ ↓↓↓↓↓↓↓ ↓ ↓) | → □ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛(live ∧∧∧∧∧∧∧ ∧ ∧𝜙)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕□ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙 Above: 𝜙 is a closed predicate and the | → modality takes us to the end of time in the model (which we typical write as H ). Modalities like | → , ♢ ↓↓↓↓↓↓↓ ↓ ↓ , and □ ↓↓↓↓↓↓↓ ↓ ↓ bind less lightly than ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ . live is a predicate symbol and we shorten live() to live , as per Notation 3.1.2. Figure 6. ThyLive: a theory of liveness (Definition 5.2.4) Events interact most naturally with □ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓ (because the history of a model is fundamentally a set of event-tuples); whereas predicates interact most naturally with □ W (because predicates are true or false at a possible world regardless of whether anything happens there). Our proofs will flow naturally, but under the surface there is this subtle design tension between predicates whose design shape suits □ W , and events whose design shape suits □ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓ . We accommodate this design tension as follows: • The predicate syntax in Figure 2includes event-based modalities like ↓ , ♢ ↓↓↓↓↓↓↓ ↓ ↓ , and □ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓. There is no □ Wmodality in the syntax. • Our notion of axiomatic validity in Definition 3.4.10 uses an ‘at all possibleworlds’ based modality □ W. This is a design choice: it seems to work well, but please just note that this was not a priori obvious, and other design choices might be possible and in other circumstances other choices might even be preferable. There is a design space here and we are free to use it as must convenient. 5.2.2. Definition of ThyLive Intuitively, we call a participant 𝑝live when: 1. 𝑝does not crash, and 2. 𝑝correctly follows the algorithm. Perhaps surprisingly, it is possible to render this intuition as an axiomatic theory ThyLive . Recall from Definition 5.2.1 that a theory is a set of closed predicates, which in this context we call axioms: Definition 5.2.4.Assume a signature with a predicate-symbol live . Let the theory of liveness ThyLive be as defined in Figure 6. Note in Figure 6that when we write 𝐸∈Event , we really do mean 𝐸∈Event and not 𝐸∈Event † . Our syntax from Figure 2does not admit † . Remark 5.2.5.We discuss the axioms of ThyLive in Figure 6: DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |54 •(LiveAlways): being live is a property of place, not of time. (LiveAlways) expresses that 𝑝 being live does not depend on the time 𝐻 . This makes sense, because liveness is a property of a participant, not of the time of any event. During a run of an algorithm we cannot predict whether 𝑝 will crash, because that would involve seeing the future. What ‘ 𝑝 remains live during the run of the algorithm’ refers to is a property of 𝑝 that only makes sense after the run of the algorithm is complete. Note a subtlety that there is another important component to being live, that a live participant should progress according to the protocol. However, what ‘progress according to the protocol’ means is protocol-dependent. This part of liveness can be and is expressed on per-protocol basis as so-called forward rules in Figures 7,9, and 11. •(LiveSeq): live participants are sequential. This is definitional. We define live to mean ‘does not crash and is sequential’. Being sequential, along with obeying the forward rules, captures the notion of ‘following the protocol’. •(Knowledge ♢ ↓↓↓↓↓↓↓ ↓ ↓)and (Knowledge□ ↓↓↓↓↓↓↓ ↓ ↓): live participants communicate events. The (Knowledge) axioms (actually axiom-schemes) reflects that if a live participant 𝑝 knows something, it will (eventually) communicate this information to all other live participants. So for example: if a quorum of live participants do some 𝐸 , then (eventually) every live participant will know that a quorum of live participants have done 𝐸 . The (Knowledge) axiom opens with | → because this property is only true at the end of time. There are no guarantees about how long communication takes. 5.2.3. More on the Knowledge axioms Remark 5.2.6 (Some general observations on the Knowledge axioms). 1. (Knowledge ♢ ↓↓↓↓↓↓↓ ↓ ↓) and (Knowledge□ ↓↓↓↓↓↓↓ ↓ ↓) are axiom-schemes: technically, there is one pair of knowledge axioms for each choice of event and list of learners. Axiom-schemes are a standard device in logic.40 2. The | → modality in (Knowledge ♢ ↓↓↓↓↓↓↓ ↓ ↓) and (Knowledge□ ↓↓↓↓↓↓↓ ↓ ↓) is required. For example, this axiom is subtly wrong: (Wrong) ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛(live ∧∧∧∧∧∧∧ ∧ ∧𝜙)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛𝜙. The reason is that, as discussed in Remark 5.2.2, axioms apply at events, but liveness is not about any single event, it is about events as viewed from the end of time. 40 In contrast, if an axiom mentions 𝑣 or 𝑙 — like the ones in Figure 7— then this does not necessarily mean that they are axiom-schemes. As per standard notation in logic, an axiom is considered to be universally quantified over any free variables. Our logic has quantification over values, so an axiom that mentions values just has invisible ∀∀∀∀∀∀∀ ∀ ∀ quantifiers quantifying those values at top level. We do not have an explicit quantification over events in the logic, so we use axiom-schemes. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |55 To see what is wrong with (Wrong) as an axiom, consider a model with a live 𝑝 that performs no action other than an initial event-tuple (𝑝, † ,∅) . Then at that initial event-tuple ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙1...𝑙𝑛(live ∧∧∧∧∧∧∧ ∧ ∧𝜙) is trivially false, so (Wrong) is trivially satisfied. This is not what we intend, but we only see this from the end of time. We will invoke the Knowledge axioms directly in what follows, but importantly, we also use them via Proposition 5.2.8 and in particular via the corollaries in Corollary 5.2.9. We need a technical observation for Proposition 5.2.8: Lemma 5.2.7.Suppose M is a model and 𝑤∈World(M) and 𝜙 is a closed predicate. Then 𝑤⊨↕ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝜙implies place(𝑤), † ,H⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝜙. In words: if at some time 𝑝 knows of a past 𝜙 , then at the end of time there is a past 𝜙. Proof. By routine calculations from Figure 5.□ Proposition 5.2.8.Suppose M is a model and □ W⊨ThyLive (Figure 6) and suppose 𝐸is an event. Then ⊨□𝑙live and ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧𝐸)implies ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝐸). In words: if there is an 𝑙 -quorum of live participants, and some live participant has an event 𝐸 , then eventually there is an 𝑙 -quorum of live participants who know that 𝐸occurred. Proof. Suppose ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧𝐸). In words: there is an event in Hat which a live participant has 𝐸. We assumed □ W⊨ThyLive so — taking the empty list of learners in the (Knowledge ♢ ↓↓↓↓↓↓↓ ↓ ↓)axiom-scheme — we have □ W⊨ | → ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧𝐸)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝐸. So consider some live 𝑝∈P . We have that 𝑝, † ,H⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧𝐸) implies 𝑝, † , 𝐻 ⊨live implies 𝑝, † , 𝐻 ⊨↕ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝐸 . It follows that 𝑝, † , 𝐻 ⊨↕ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝐸 and so by Lemma 5.2.7 𝑝, † ,H⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝐸 . Since we assume that an 𝑙 -quorum of live participants exists, we have ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝐸)as required. □ Corollary 5.2.9.Suppose M is a model and □ W⊨ThyLive (Figure 6) and suppose 𝐸∈Event. Then: 1. ⊨□𝑙live and ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝐸)implies ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝐸). 2. ⊨□𝑙live and ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧𝐸)implies ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝐸). DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |56 3. ⊨□𝑙live and ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′𝐸)implies ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′𝐸). Proof. Part 1is from Proposition 5.2.8 taking 𝜙= ♢ ↓↓↓↓↓↓↓ ↓ ↓𝐸 and using Lemma 4.2.2 ( ♢ ↓↓↓↓↓↓↓ ↓ ↓ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝐸implies ♢ ↓↓↓↓↓↓↓ ↓ ↓𝐸). Part 2is from Proposition 5.2.8 taking 𝜙=𝐸. Part 3is from Proposition 5.2.8 taking 𝜙=□ ↓↓↓↓↓↓↓ ↓ ↓𝐸 , and using Lemma 4.2.3(2) ( ♢ ↓↓↓↓↓↓↓ ↓ ↓□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝐸implies □ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝐸). □ 5.2.4. More on (LiveAlways) Lemma 5.2.10.Suppose M is a model and satisfies ThyLive from Figure 6. Suppose 𝑤,𝑤′∈H and place(𝑤)=place(𝑤′) , and suppose 𝑙∈Learner . Then: 1. 𝑤⊨live if and only if place(𝑤), † ,H⊨live. 2. 𝑤⊨live if and only if 𝑤′⊨live. 3. ⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒⇓live. Proof. Part 1just restates (LiveAlways) , unpacking the meaning of | → in Figure 3. 41 Part 2follows by two uses of part 1. Part 3follows by one use of part 1.□ Proposition 5.2.11 is conceptually simple, and it turns out to be a key property for our Liveness 2 results (Propositions 6.4.5,7.2.2, and 8.4.5): Proposition 5.2.11.Suppose M is a model and 𝑙1,𝑙2∈Learner and suppose 𝜙 is a closed predicate. Suppose further that ⊨ ♢ 𝑙1𝑙2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤and ⊨□𝑙2live. Then ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙1𝜙implies ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧𝜙). In words: if 𝑙1 and 𝑙2 have nonempty quorum intersections 42 and 𝑙2 has a quorum of live participants, then any 𝑙1 -quorum of 𝜙 contains at least one live participant. Proof. Suppose ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙1𝜙 . By Lemma 4.1.1(2) (since ⊨ ♢ 𝑙1𝑙2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤ ) every 𝑙1 -quorum intersects every 𝑙2 -quorum. Using Lemma 5.2.10(2) ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧𝜙) as required. □ Lemma 5.2.12 has in common with Lemma 4.2.2 that it expresses in our logic a(nother) version of the (4) axiom from the modal logic S4 . It is nice how the same basic axiomatic property arises in different ways, here for □ ↓↓↓↓↓↓↓ ↓ ↓𝑙+live: 41 It is important here that 𝑤∈H , instead of the more general condition that 𝑤∈World(H) . If we want to more general property we need to strengthen our notion of axiomatic validity to use □ W . See Remark 5.2.3. For our purposes, the Lemma as stated is enough. 42 This terminology is from Notation 4.1.2; it means that every intersection between an 𝑙1 -quorum and an 𝑙2-quorum, is nonempty. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |57 • then 𝑙 has sequential quorum intersections with all other learners, meaning by Notation 4.1.2 that for every 𝑙 -quorum 𝑂 and every learner 𝑙′ (including 𝑙 ) and every 𝑙′-quorum 𝑂′, there exists 𝑞∈𝑂∩𝑂′such that 𝑞, † , 𝐻 ⊨seq. The disjunct in (Safe) is there to give us the Liveness 1 property in Proposition 6.5.3, and specifically to give us Lemma 6.5.2: that if at most one value is proposed then every learner is safe. Note from Figure 7that being safe depends on quorum intersections being sequential. But the sequentiality condition is overspecified: sequentiality applies to all maybe-events, but in this protocol we only care about nonsequential echo events for distinct values. 49 If only one value is proposed then that is impossible. Remark 6.2.3.We study the fine structure of the (Echo!) axiom. This expresses that if a live participant knows of a propose(𝑣) then at some time that participant will perform echo(𝑣′) for some 𝑣′ (which need not be equal to 𝑣). We mention a few subtleties to how this is constructed: 1. In full, (Echo!) is as follows — we just write out the implicit universal quantification over the 𝑣: ∀∀∀∀∀∀∀ ∀ ∀𝑣.live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ∃∃∃∃∃∃∃ ∃ ∃𝑣′.↕echo(𝑣′). 2. Equivalent forms of (Echo!) exist, including: live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒(∃∃∃∃∃∃∃ ∃ ∃𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣))⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ∃∃∃∃∃∃∃ ∃ ∃𝑣′.↕echo(𝑣′) live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ∃∃∃∃∃∃∃ ∃ ∃𝑣′.↕echo(𝑣′) 3. This axiom is subtly wrong: live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ | → ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ∃∃∃∃∃∃∃ ∃ ∃𝑣′. | → ↓echo(𝑣′). We leave it to the reader to think why (sketch answer in footnote).50 4. This axiom is wrong: (live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕echo(𝑣′) This is wrong because by (EchoNE) a participant should echo at most one value. If a proposer proposes two values, each other participant is supposed supposed to pick one value and echo at most that value (and no other). 49 Likewise for ThyHBB2 . In ThyHBB3 we care about nonsequential echo and also nonsequential vote events. A rule of thumb is: nonsequentiality matters where it might break an axiom with a name of the form (EDup) for 𝐸∈Event. 50 | → ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣) means that some participant knows of a propose(𝑣) , but does not guarantee that it is a live participant. A corrected version is | → ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ∃∃∃∃∃∃∃ ∃ ∃𝑣′. | → ↓echo(𝑣′) , but this is over-long because it folds in some of the power that is already included in the Knowledge axioms. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |64 5. This axiom is correct and equivalent to what is written: (live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕∃∃∃∃∃∃∃ ∃ ∃𝑣′.echo(𝑣′). (We flip the existential quantifier ∃∃∃∃∃∃∃ ∃ ∃𝑣′ and the sometime modality ↕ .) While both forms are correct, as a matter of style and convenience here and elsewhere, we will follow a policy of putting quantifiers outside modalities where possible. This means that (working top-down through the predicate) we get to a proposition sooner rather than later. Remark 6.2.4 (A design alternative).We note in passing that (EchoNE) from Figure 7is not the only possible non-equivocation axiom. We could impose a stronger condition: (EchoNE’) echo(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓echo(𝑣′)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝑣======= = =𝑣′. All of our correctness properties would work just as well. We prefer (EchoNE) precisely because it is a weaker assumption; the weaker assumption means that our correctness results are stronger. Intuitively — this is not a mathematical statement — (EchoNE’) corresponds to an algorithm where we echo the first value we hear proposed, if we echo anything at all. 51 (EchoNE) corresponds to an algorithm where we echo at most one of the values that we hear proposed, but it need not necessarily be the first one that we hear about. 6.3. Agreement Proposition 6.3.1 (Soundness / Agreement).Suppose 𝑙1,𝑙2,𝑙′ 1,𝑙′ 2∈Learner and 𝑣1, 𝑣2∈Value and ⊨ ♢ 𝑙′ 1𝑙′ 2seq. Then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙1, 𝑣1)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 2,𝑙2, 𝑣2)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝑣1======= = =𝑣2. Proof. If 𝑣1=𝑣2 then there is nothing to prove, so it will be convenient (for the step marked (∗∗) below) to assume 𝑣1≠𝑣2 and derive a contradiction. We 51By axiom (Echo?), if we know of an echo(𝑣)then we also know of a propose(𝑣). DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |65 reason as follows: ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙1, 𝑣1) ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 2,𝑙2, 𝑣2) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 1vote(𝑙1, 𝑣1) ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2vote(𝑙2, 𝑣2)(Deliver?) =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙1, 𝑣1) ∧∧∧∧∧∧∧ ∧ ∧ ↓vote(𝑙2, 𝑣2)∨ ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙2, 𝑣2) ∧∧∧∧∧∧∧ ∧ ∧ ↓vote(𝑙1, 𝑣1) Prop 5.1.5(3), 𝑣1≠𝑣2, ⊨ ♢ 𝑙′ 1𝑙′ 2seq =⇒𝑤⊨vote(𝑙2, 𝑣2) ∧∧∧∧∧∧∧ ∧ ∧ ↓vote(𝑙1, 𝑣1)2nd disjunct(∗), some 𝑤∈Hby Remark 3.6.6(3) =⇒𝑤⊨safe(𝑙2) ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙2echo(𝑣2) ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙1echo(𝑣1)(Vote?),Lemma 4.2.3(1) =⇒𝑤⊨ ♢ 𝑙2𝑙1seq ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙2echo(𝑣2) ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙1echo(𝑣1)(Safe)(∗∗), 𝑣1≠𝑣2 =⇒𝑣1=𝑣2Prop 5.1.5(3), 𝑣1≠𝑣2,(EchoNE) =⇒ ⊥ 𝑣1≠𝑣2 We expand on two steps in the derivation above: (∗) Just above the step marked (∗) , we have a disjunct between ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙1, 𝑣1) ∧∧∧∧∧∧∧ ∧ ∧ ↓vote(𝑙2, 𝑣2) or ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙2, 𝑣2) ∧∧∧∧∧∧∧ ∧ ∧ ↓vote(𝑙1, 𝑣1) . The first possibility is precisely symmetric with the second, so we just consider the second disjunct. (∗∗) At the step marked (∗∗) we go from safe(𝑙2)to ♢ 𝑙2𝑙1seq. The behaviour of safe is determined by (Safe) in Figure 7. This characterises safe using two disjuncts ∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) or ∀∀∀∀∀∀∀ ∀ ∀𝑙′. ♢ 𝑙𝑙′seq . The former disjunct is not valid because we are at a world at which we know of (quorums of, and thus) of some past echo(𝑣2) and echo(𝑣1) , and using (Echo?) we know of some past propose(𝑣2) and propose(𝑣1) — and we assumed 𝑣1≠𝑣2 . Thus, the latter disjunct must be valid. We note 𝑣1≠𝑣2 using Proposition 5.1.5(3) above because the result requires distinct events. □ 6.4. Liveness 2 Lemma 6.4.1.Suppose 𝑤′≪−𝑤∈World(M). Then: 1. 𝑤⊨safe implies 𝑤′⊨safe. 2. 𝑤⊨safe ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒⇓safe. Proof. From the definition of safe in Figure 7, using Proposition 5.1.4 ( seq monotone). □ Lemma 6.4.2.Suppose 𝜙and 𝜓are closed predicates and 𝑙∈Learner. Then: 1. ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙and □ W⊨𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕𝜓implies ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜓. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |66 2. If □ W⊨ThyLive then ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧𝜙)and □ W⊨(live ∧∧∧∧∧∧∧ ∧ ∧𝜙)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕𝜓implies ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧𝜓). Proof. We consider each part in turn: 1. Suppose ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙 . By Remark 3.6.5(2) this means that there is an 𝑙 -quorum 𝑂 such that for each 𝑝∈𝑂 there exists 𝑤𝑝∈H@𝑝 such that 𝑤𝑝⊨𝜙 . By our assumptions 𝑤𝑝⊨𝜙⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕𝜓 for each 𝑝∈𝑂 , and so by Lemma 3.6.4(1) there exists some 𝑤′ 𝑝∈H@𝑝 such that 𝑤′ 𝑝⊨𝜓 . This is true of every 𝑝∈𝑂 , and ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜓follows. 2. First, note from Lemma 5.2.10(2) that □ W⊨(live ∧∧∧∧∧∧∧ ∧ ∧𝜙)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕𝜓implies □ W⊨(live ∧∧∧∧∧∧∧ ∧ ∧𝜙)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕(live ∧∧∧∧∧∧∧ ∧ ∧𝜓). We can now just use part 1of this result. □ Lemma 6.4.3.Suppose 𝜙 and 𝜓 are closed predicates and □ W⊨ThyLive . Then ⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕𝜙and □ W⊨(live ∧∧∧∧∧∧∧ ∧ ∧𝜙)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕𝜓implies ⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕𝜓. Proof. We unpack definitions using Figures 3(validity), 4(syntactic sugar) and 5(its denotation): • By Figure 3and Lemma 3.6.4(1), ⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕𝜙 means that for every live participant 52 𝑝∈P there exists some 𝑤𝑝∈H@𝑝 (Definition 3.4.7) such that 𝑤𝑝⊨𝜙. • By Figure 3, □ W⊨(live ∧∧∧∧∧∧∧ ∧ ∧𝜙)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕𝜓 means that for every 𝑤∈H , if place(𝑤) is live (by (LiveAlways) the time does not matter) then 𝑤⊨𝜙 implies that there exists some event-tuple 𝑤′∈Hsuch that place(𝑤)=place(𝑤′)and 𝑤′⊨𝜓. •⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕𝜓 holds when for every live participant 𝑝∈P there exists some 𝑤𝑝∈H@𝑝such that 𝑤𝑝⊨𝜓. Putting the first two assumptions together we obtain the required conclusion. □ Lemma 6.4.4.Suppose 𝜙is a closed predicate and 𝑙∈Learner. Then ⊨□𝑙↕𝜙if and only if ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙. Proof. By Figure 4, ↕ is sugar for | → ↓ . By Figure 3, ⊨□𝑙↕𝜙 means 𝑝, † ,H⊨ | → ↓𝜙 for every 𝑝∈𝑂 for 𝑂 some 𝑙 -quorum. But it is clear from Figure 3that 𝑝, † ,H⊨ | → ↓𝜙 if and only if 𝑝, † ,H⊨↓𝜙 . Thus we can simplify ⊨□𝑙↕𝜙 to ⊨□𝑙↓𝜙, and by Figure 4this is just ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝜙as required. □ 52 Recall from Lemma 5.2.10(2) that by (LiveAlways) in Figure 6, it does not matter when 𝑝 is live; 𝑝 is either live or not live, at all 𝑤∈H@𝑝. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |67 Proposition 6.4.5 (Liveness 2).Suppose 𝑙′ 1,𝑙, 𝑙′ 2∈Learner and 𝑣∈Value . Suppose further that ⊨ ♢ 𝑙′ 1𝑙′ 2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤and ⊨safe(𝑙)and ⊨□𝑙′ 2live. In words: 𝑙′ 1 and 𝑙′ 2 have nonempty quorum intersections (Notation 4.1.2) and 𝑙′ 2has a live quorum. Then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙′ 2,𝑙, 𝑣). As corollaries, ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2deliver(𝑙′ 2,𝑙, 𝑣)and ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 2,𝑙, 𝑣). Proof. We reason as follows: ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙, 𝑣) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 1vote(𝑙, 𝑣)(Deliver?) =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧vote(𝑙, 𝑣1)) Prop 5.2.11,⊨ ♢ 𝑙′ 1𝑙′ 2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤ ∧∧∧∧∧∧∧ ∧ ∧□𝑙′ 2live =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑣)) (Vote?) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2(live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑣)) Corollary 5.2.9(3),⊨□𝑙′ 2live =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2(live ∧∧∧∧∧∧∧ ∧ ∧safe(𝑙) ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑣)) Lemma 6.4.1,⊨safe(𝑙) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2(live ∧∧∧∧∧∧∧ ∧ ∧vote(𝑙, 𝑣)) Lemma 6.4.2(2),(Vote!) =⇒⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2vote(𝑙, 𝑣)(Knowledge□ ↓↓↓↓↓↓↓ ↓ ↓) =⇒⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙′ 2,𝑙, 𝑣)Lemma 6.4.3,(Deliver!) =⇒⊨□𝑙′ 2↕deliver(𝑙′ 2,𝑙, 𝑣)⊨□𝑙′ 2live =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2deliver(𝑙′ 2,𝑙, 𝑣)Lemma 6.4.4 =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 2,𝑙, 𝑣)Lemma 4.2.1(1)□ 6.5. Liveness 1 Lemmas 6.5.1 and 6.5.2 will help us prove Proposition 6.5.3. Lemma 6.5.1. ⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣) implies □ W⊨(live∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣))⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕echo(𝑣) . Proof. Suppose ⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣) (i.e. precisely one value is proposed). To prove □ W⊨(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕echo(𝑣) it suffices by Figure 3to show for every 𝑤∈Hthat 𝑤⊨live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)implies 𝑤⊨↕echo(𝑣). So suppose 𝑤⊨live ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣). Using (Echo!) 𝑤⊨↕echo(𝑣′)for some 𝑣′∈Value. It follows using (Echo?) that ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣′) . However, we also assumed that ⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣), so 𝑣=𝑣′and we are done. □ DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |68 Lemma 6.5.2.Suppose 𝑙∈Learner. Then ⊨∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01 ∃01𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒⇕safe(𝑙). In words: if there exists at most one proposed value, then every learner is safe. ( ⇕ is from Figures 4and 5and we check its denotation in Lemma 3.6.4(2).) Proof. By the construction of safe in Figure 7.□ Proposition 6.5.3 (Liveness 1).Suppose 𝑙∈Learner and ⊨□𝑙live and ⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣). Then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙, 𝑙, 𝑣). As corollaries, ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙deliver(𝑙,𝑙, 𝑣)and ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙,𝑙, 𝑣). Proof. We reason as follows: ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) Corollary 5.2.9(1),⊨□𝑙live =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧echo(𝑣)) Lemma 6.4.2(2) & Lemma 6.5.1,⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑙, 𝑣)) Lemma 5.2.12 =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑣)) ∧∧∧∧∧∧∧ ∧ ∧ ⇕safe(𝑙)Lemma 6.5.2,⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧vote(𝑙, 𝑣)) Lemma 6.4.2(2),(Vote!) =⇒⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕□ ↓↓↓↓↓↓↓ ↓ ↓𝑙vote(𝑙, 𝑣)(Knowledge□ ↓↓↓↓↓↓↓ ↓ ↓) =⇒⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙, 𝑙, 𝑣)Lemma 6.4.3,(Deliver!) =⇒⊨□𝑙↕deliver(𝑙, 𝑙, 𝑣)⊨□𝑙live =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙deliver(𝑙,𝑙, 𝑣)Lemma 6.4.4 =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙,𝑙, 𝑣)Lemma 4.2.1(1)□ Remark 6.5.4.The statement of Proposition 6.5.3 contains a nested pair of knowledge modalities ♢ ↓↓↓↓↓↓↓ ↓ ↓ : ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) . The outermost one is omniscient and the inner one is relative to a place and a (non-end-of-time) time. It might be helpful to unpack this. The outer ♢ ↓↓↓↓↓↓↓ ↓ ↓ is omniscient, in the sense that it is evaluated at the end of time, so it has the value of there exists some 𝑤∈Hat some live participant 𝑝, and .. . DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |69 Note the use of ‘there exists’ above. The inner ♢ ↓↓↓↓↓↓↓ ↓ ↓ takes the local view and has the value of at 𝑤,𝑝knows of a propose(𝑣)event. Note the use of ‘at 𝑤 , 𝑝 knows’ above. This is non-omniscient because we evaluate at 𝑤∈H . Putting this together, we arrive at the full meaning of ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)): There exists some event by a live participant such that at the time of that event the live participant knows of a past propose(𝑣)message. That is a bit of a mouthful, and we can shorten it (with some mild loss of precision) to: Some live participant learns of a propose(𝑣). 6.6. Further discussion Remark 6.6.1.Recall from Notation 6.1.3 and Remark 6.1.4 that we read 𝑝, 𝑥, 𝐻 ⊨deliver(𝑙′,𝑙, 𝑣) as ‘ 𝑝 delivers 𝑣 for (𝑙′,𝑙) ’, and this implies that the delivering participant 𝑝 has observed an 𝑙′ -quorum of participants who observed an 𝑙-quorum of participants who observed propose(𝑣). Let us reflect on the correctness properties from Figure 8: • The Agreement property (Proposition 6.3.1) is strong: provided 𝑙′ 1 and 𝑙′ 2 have sequential quorum intersections (Notation 4.1.2), we have a guarantee that any 𝑝 and 𝑝′ that deliver values for (𝑙′ 1,𝑙1) and (𝑙′ 2,𝑙2) respectively, will agree on the value that they deliver. •The Liveness 2 guarantee (Proposition 6.4.5) is weak in the following sense: An adversary could wait for some 𝑝 to deliver 𝑣 for (𝑙′ 1,𝑙) , for some 𝑙 . Then the adversary creates an nonsequential quorum intersection for that 𝑙 , and advertise it to all other participants. This would prevent Proposition 6.4.5 from making any useful predictions about deliveries for (𝑙′ 2,𝑙) for any 𝑙′ 2 , because the condition ⊨safe(𝑙)would no longer hold. • The Liveness 1 guarantee (Proposition 6.5.3) is as one would expect; no weaker or stronger than what makes sense. Protocols ThyHBB2 and ThyHBB3 will go some way to correcting the weak Liveness 2 guarantee of ThyHBB1 , or rather, they will make different trade-offs. See a comparative discussion of ThyHBB1 and ThyHBB2 in Remark 7.3.1. Remark 6.6.2.A few words on how the predicate symbols live and safe are used in ThyHBB1. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |70 1. Both live() (we drop the empty brackets and write this just as ‘ live ’) and safe(𝑙) are atomic predicates (Definition 3.1.1(2)). We have not imposed an arity system on our syntax, but we use live as a 0 -ary proposition which is true at a live participant. The property of being live is a property of a place/participant, but not a time, in a sense made formal by axiom (LiveAlways). In contrast, the property of a learner 𝑙 being safe is a property both of a place and a time, as per axiom (Safe) . A learner 𝑙 is only safe at a participant 𝑝 and at a time 𝐻 and it might become not-safe at 𝑝 at a later 𝐻′ — unless 𝐻=H in which case the system is omniscient and 𝑙 is indeed safe until the end of time because, well, we are at the end of time and 𝑙is safe. Regardless, the content of the assertion safe(𝑙) is that 𝑙 is safe here and until now, i.e. it is a local assertion, whereas the content of the assertion live is that here is live, forever, i.e. it is an omniscient assertion about behaviour now and into the future. 2. Note that propose , echo , vote , and deliver are event-symbols, not predicate symbols. Events are very similar to atomic predicates but they are handled differently in the denotation; see the discussion in Remark 3.1.4. Remark 6.6.3 (What really matters (for correctness)).The central characteristic of an honest participant is being sequential. The central characteristic of a dishonest (= hostile, byzantine) participant is not being sequential. Because we assume that all messages are cryptographically signed, so forging messages is impossible, (non)sequentiality is the only (mis)behaviour that really counts, so that just two things really matter for determining our correctness properties: intersection properties of quorums, and sequentiality properties of participants within those quorums. Ultimately, everything will boil down to conditions of these two forms. 7. Theory ThyHBB2 ThyHBB1 is not the only way to generalise Bracha’s reliable broadcast. Here we present ThyHBB2 , a slightly simpler theory that makes different trade-offs between liveness and agreement. 7.1. Definition of the theory Definition 7.1.1 (Theory ThyHBB2). 1. Assume a signature with event-symbols propose , echo , vote , and deliver , and with a predicate-symbol live. 2. Define ThyHBB2 to be the theory with axioms as per Figure 9. 3. For the rest of this Section, we fix a model M of ThyHBB2 , meaning that □ W⊨ThyHBB2 as per Definition 5.2.1. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |71 Remark 7.1.2.We we did in Remark 6.1.7 for ThyHBB1 , we can extract an abstract protocol from the axioms as follows, where we interpret atomic predicates as messages: 1. A proposer broadcasts propose(𝑣)for some value 𝑣. 2. 𝑝 broadcasts echo(𝑣) for precisely one proposed value, provided it observes any proposals at all. 3. If 𝑝receives an 𝑙-quorum of echo(𝑣)messages, it broadcasts vote(𝑙, 𝑣). 4. If 𝑝receives an 𝑙′-quorum of vote(𝑙, 𝑣)messages, it broadcasts deliver(𝑙′,𝑙, 𝑣). We spell out the intuitive logical content of each broadcast: •propose(𝑣)means I propose 𝑣. •echo(𝑣)means I saw propose 𝑣. •vote(𝑙, 𝑣) means I saw an 𝑙 -quorum of participants who each saw someone propose 𝑣. •deliver(𝑙′,𝑙, 𝑣) means I saw an 𝑙′ -quorum of participants who each saw an 𝑙-quorum of participants who each saw someone propose 𝑣. Theorem 7.1.3.We collect the correctness properties for ThyHBB2 in Figure 10, for ease of reference. Proof. The relevant results are Propositions 7.2.3,7.2.2, and 7.2.1 respectively. □ 7.2. Proofs of Agreement, Liveness 1, and Liveness 2 Proposition 7.2.1 (Agreement).Suppose 𝑙1,𝑙2,𝑙′ 1,𝑙′ 2∈Learner and ⊨ ♢ 𝑙1𝑙2seq. Then for every 𝑣1, 𝑣2∈Value, ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙1, 𝑣1) ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 2,𝑙2, 𝑣2)implies 𝑣1=𝑣2. Proof. If 𝑣1=𝑣2then we are done, so suppose 𝑣1≠𝑣2. We reason as follows: ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙1, 𝑣1) ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 2,𝑙2, 𝑣2) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 1vote(𝑙1, 𝑣1) ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2vote(𝑙2, 𝑣2)(Deliver?) =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙1, 𝑣1) ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙2, 𝑣2)Lemma 4.2.1(1) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙1echo(𝑣1) ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙2echo(𝑣2)(Vote?) =⇒𝑣1=𝑣2Prop 5.1.5(3), 𝑣1≠𝑣2, ⊨ ♢ 𝑙1𝑙2seq,(EchoNE) We note 𝑣1≠𝑣2 using Proposition 5.1.5(3) above because the result requires distinct events. □ DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |72 Proposition 7.2.2 (Liveness 2).Suppose 𝑙′ 1,𝑙′ 2,𝑙 ∈Learner and ⊨ ♢ 𝑙′ 1𝑙′ 2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤and ⊨□𝑙′ 2live. Then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙′ 2,𝑙, 𝑣). As corollaries, ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2deliver(𝑙′ 2,𝑙, 𝑣)and ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 2,𝑙, 𝑣). Proof. We reason as follows: ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙′′ 1, 𝑣1) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 1vote(𝑙′′ 1, 𝑣1)(Deliver?) =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧vote(𝑙′′ 1, 𝑣1)) Prop 5.2.11,⊨ ♢ 𝑙′ 1𝑙′ 2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤ ∧∧∧∧∧∧∧ ∧ ∧□𝑙′ 2live =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′′ 1echo(𝑣1)) (Vote?) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2(live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′′ 1echo(𝑣1)) Corollary 5.2.9(3),⊨□𝑙′ 2live =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2(live ∧∧∧∧∧∧∧ ∧ ∧vote(𝑙, 𝑣)) Lemma 6.4.2(2),(Vote!) =⇒⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2vote(𝑙, 𝑣)(Knowledge□ ↓↓↓↓↓↓↓ ↓ ↓) =⇒⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙′ 2,𝑙, 𝑣)Lemma 6.4.3,(Deliver!) =⇒⊨□𝑙′ 2↕deliver(𝑙′ 2,𝑙, 𝑣)⊨□𝑙′ 2live =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′ 2deliver(𝑙′ 2,𝑙, 𝑣)Lemma 6.4.4 =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 2,𝑙, 𝑣)Lemma 4.2.1(1)□ Proposition 7.2.3 (Liveness 1).Suppose 𝑙∈Learner and ⊨□𝑙live and ⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣). Then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙, 𝑙, 𝑣). As corollaries, ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙deliver(𝑙,𝑙, 𝑣)and ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙,𝑙, 𝑣). DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |73 If 𝑣1=𝑣2then we are done, so suppose 𝑣1≠𝑣2. We reason as follows: ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙1, 𝑣1) ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙2, 𝑣2) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙1vote(𝑙1, 𝑣1) ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙2vote(𝑙2, 𝑣2)(Deliver?) =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙′ 1, 𝑣1) ∧∧∧∧∧∧∧ ∧ ∧ ↓vote(𝑙′ 2, 𝑣2)∨ ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙′ 2, 𝑣2) ∧∧∧∧∧∧∧ ∧ ∧ ↓vote(𝑙′ 1, 𝑣1) Prop 5.1.5(3), 𝑣1≠𝑣2,⊨ ♢ 𝑙1𝑙2seq =⇒𝑣1=𝑣2(VoteNE),⊨□ ⇓⇓⇓⇓⇓⇓⇓ ⇓ ⇓(𝑙1𝑙2) We note 𝑣1≠𝑣2 using Proposition 5.1.5(3) above because the result requires distinct events. □ Remark 8.3.2 (Design alternative).There is a wrinkle in axiom (⇓) in Figure 11, that the modality ⇓ only quantifies over worlds 𝑤∈H , not over all possible worlds 𝑤∈World(H) . An alternative axiom | → (𝑙1𝑙2)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝑙1𝑙2 eliminates that possibility. This is weaker in the sense that the left-hand side of the implication goes to the end of time (the left-hand side of the implication in (⇓) as written does not do that), but it is stronger in the sense that the right-hand side works at all possible worlds. Perhaps surprisingly, either axiom will work in our proofs.56 8.4. Liveness 2 Lemma 8.4.1 will help us prove Lemma 8.4.3(1): Lemma 8.4.1.Suppose 𝑙1,𝑙2,𝑙3∈Learner and suppose 𝜙1 , 𝜙2 , and 𝜙3 are three closed predicates. Then ⊨ ♢ 𝑙1𝑙2𝑙3⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒(□𝑙1𝜙1∧∧∧∧∧∧∧ ∧ ∧□𝑙2𝜙2∧∧∧∧∧∧∧ ∧ ∧□𝑙3𝜙3)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ (𝜙1∧∧∧∧∧∧∧ ∧ ∧𝜙2∧∧∧∧∧∧∧ ∧ ∧𝜙3). Proof. Suppose ⊨ ♢ 𝑙1𝑙2𝑙3⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤. By Lemma 4.1.1(2), 1. an 𝑙1-quorum of 𝑝∈Pthat satisfies 𝑝, † ,H⊨𝜙1, and 2. an 𝑙2-quorum of 𝑝∈Pthat satisfies 𝑝, † ,H⊨𝜙2, and 3. an 𝑙3-quorum of 𝑝∈Pthat satisfies 𝑝, † ,H⊨𝜙3, must intersect at some 𝑝 , which will satisfy 𝑝, † ,H⊨𝜙1∧∧∧∧∧∧∧ ∧ ∧𝜙2∧∧∧∧∧∧∧ ∧ ∧𝜙3 . The result follows. □ Lemma 8.4.2 will help us prove Lemma 8.4.3(2): Lemma 8.4.2.Suppose 𝑙∈Learner and 𝑣∈Value and 𝑤∈H. Then: 56 The dedicated reader might look all this design space and conclude that ↓ and ⇓ should just quantify over possible preceding possible worlds, rather than just preceding worlds that are event-tuples in H . Unfortunately, that does not work! We need ↓ as written in order to express the Knowledge axioms in Figure 6. The design tension here is real. We could have two ‘in-the-past’ modalities (one for event-tuples in history and one for all possible worlds), or we can do as we have done and live with the wrinkle in (⇓). Since this wrinkle is harmless in our current proofs, this seems a valid tradeoff. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |80 1. 𝑤⊨vote(𝑙, 𝑣)implies ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′echo(𝑣)for some 𝑙′∈Learner. 2. ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙, 𝑣)implies ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′echo(𝑣)for some 𝑙′∈Learner. Proof. Part 1is by a simple inductive argument on time(𝑤) , using (Vote?) from Figure 11. Part 2follows since by Remark 3.6.6(3) ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙, 𝑣) just means 𝑤⊨vote(𝑙, 𝑣)for some 𝑤∈H.□ Lemma 8.4.3.Suppose 𝑙,𝑙1,𝑙2∈Learner — we do not assume 𝑙𝑙1 or 𝑙1𝑙2 ; these are just any three learners — and ⊨□𝑙seq. Then for any 𝑣, 𝑣1, 𝑣2∈Value: 1. ⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙1echo(𝑣1) ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙2echo(𝑣2)implies 𝑣1=𝑣2. 2. ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙1, 𝑣1) ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙2, 𝑣2)implies 𝑣1=𝑣2.57 3. □ W⊨(live ∧∧∧∧∧∧∧ ∧ ∧ ⇕𝑙1𝑙2∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙1, 𝑣)) =⇒ ↕vote(𝑙2, 𝑣). 4. □ W⊨(live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕vote(𝑙, 𝑣). Proof. We consider each part in turn: 1. Using Lemma 8.4.1 (since we assume (3twined) in Figure 11) we have ⊨ ♢ (seq ∧∧∧∧∧∧∧ ∧ ∧ ↓echo(𝑣1) ∧∧∧∧∧∧∧ ∧ ∧ ↓echo(𝑣2)). The result now follows using Proposition 5.1.5(2) and (EchoNE). 2. From part 1of this result, using Lemma 8.4.2. 3. From (Vote’!), noting that by part 2of this result, only 𝑣can ever be voted for. 4. From (Vote!) , noting that by part 2of this result, only 𝑣 can ever be voted for. □ Lemma 8.4.4.Suppose 𝑙1,𝑙2∈Learner. Then: 1. ⊨ ♢ (𝑙1𝑙2)implies ⊨ ♢ 𝑙1𝑙2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤. 2. ⊨□(𝑙1𝑙2)implies ⊨ ♢ 𝑙1𝑙2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤. Proof. Part 2follows from part 1using Lemma 4.2.1(2) (that □implies ♢ ). For part 1, suppose ⊨ ♢ (𝑙1𝑙2) . Unpacking what this means using Remark 3.6.6(1), there exists 𝑝∈P such 𝑝, † ,H⊨𝑙1𝑙2 . Using (seq)𝑝, † ,H⊨ ♢ 𝑙1𝑙2seq and (since seq ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤) also 𝑝, † ,H⊨ ♢ 𝑙1𝑙2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤.□ 57 This result might seem to imply (VoteNE) , because if vote(𝑙, 𝑣) and ↓vote(𝑙′, 𝑣′) then certainly ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙, 𝑣) and ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙′, 𝑣′) , and then by this result 𝑣1=𝑣2 . However, this result assumes the existence of a quorum of sequential participants, whereas (VoteNE) does not. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |81 Proposition 8.4.5 (Liveness 2).Suppose 𝑙1,𝑙2∈Learner, and ⊨□(𝑙1𝑙2)and ⊨□𝑙2live. Then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙1, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙2, 𝑣). As corollaries, ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙1, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙2deliver(𝑙2, 𝑣)and ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙1, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙2, 𝑣). Proof. Note that: •⊨ ♢ 𝑙1𝑙2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤by Lemma 8.4.4 (since ⊨□(𝑙1𝑙2)).58 •□ W⊨⇕(𝑙1𝑙2)because we assume ⊨□(𝑙1𝑙2)and (⇓). We reason as follows: ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙1, 𝑣1) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙1vote(𝑙1, 𝑣1)(Deliver?) =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧vote(𝑙1, 𝑣1)) Prop 5.2.11 ⊨ ♢ 𝑙1𝑙2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤ ∧∧∧∧∧∧∧ ∧ ∧□𝑙2live =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙2(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑙1, 𝑣1)) Corollary 5.2.9(2),⊨□𝑙2live =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙2(live ∧∧∧∧∧∧∧ ∧ ∧vote(𝑙2, 𝑣)) Lemma 8.4.3(3),□ W⊨⇕(𝑙1𝑙2) =⇒⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕□ ↓↓↓↓↓↓↓ ↓ ↓𝑙2vote(𝑙2, 𝑣)(Knowledge□ ↓↓↓↓↓↓↓ ↓ ↓) =⇒⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙2, 𝑣)Lemma 6.4.3,(Deliver!) =⇒⊨□𝑙2↕deliver(𝑙2, 𝑣)⊨□𝑙2live =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙2deliver(𝑙2, 𝑣)Lemma 6.4.4 =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙2, 𝑣)Lemma 4.2.1(1)□ 8.5. Liveness 1 Proposition 8.5.1 (Liveness 1).Suppose 𝑙∈Learner and ⊨□𝑙live and ⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣). Then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙, 𝑣). As corollaries, ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙deliver(𝑙, 𝑣)and ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙, 𝑣). 58 We can also get this property as a special case of (3twined) , but that is an axiomatic constraint on the entire model whereas ⊨□(𝑙1𝑙2) is a specific assumption in this particular result. It is better to use the assumption and to avoid invoking the axiomatic constraint, where we can — it means that later on its easier to see where the axioms are really needed, and so how we might tweak them; see Remark 8.6.2. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |82 Proof. Note that because ⊨□𝑙live , by (LiveSeq) from Figure 6also ⊨□𝑙seq . We reason as follows: ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) Corollary 5.2.9(1),⊨□𝑙live =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧echo(𝑣)) Lemma 6.4.2(2) & Lemma 6.5.1,⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣) =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑣)) Lemma 5.2.12 =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙(live ∧∧∧∧∧∧∧ ∧ ∧vote(𝑙, 𝑣)) Lemmas 6.4.2(2)&8.4.3(4),⊨□𝑙seq =⇒⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕□ ↓↓↓↓↓↓↓ ↓ ↓𝑙vote(𝑙, 𝑣)(Knowledge□ ↓↓↓↓↓↓↓ ↓ ↓) =⇒⊨live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙, 𝑣)Lemma 6.4.3,(Deliver!) =⇒⊨□𝑙↕deliver(𝑙, 𝑣)⊨□𝑙live =⇒⊨□ ↓↓↓↓↓↓↓ ↓ ↓𝑙deliver(𝑙, 𝑣)Lemma 6.4.4 =⇒⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙, 𝑣)Lemma 4.2.1(1)□ Remark 8.5.2.We abuse Lemma 6.5.1 in the proof of Proposition 8.5.1 above, because it concerns echo in ThyHBB1 , and here we are working with echo in ThyHBB3 . However, the (Echo?) and (EchoNE) rules of ThyHBB1 are identical to the (Echo?) and (EchoNE) rules of ThyHBB3 , and it is clear that the result transfers. 8.6. Discussion Remark 8.6.1. ThyHBB3 assumes a correlation relation  . We make minimal assumptions on such that our proofs work. These are: • Symmetry (symm) and transitivity (tran) ; at every 𝑤∈World(M) , the relation {(𝑙,𝑙′) | 𝑤⊨𝑙𝑙′}is a partial equivalence relation. • Monotonicity (⇓) ; if 𝑙 and 𝑙′ stop correlating then they cannot (re)correlate later. • Sequentiality (seq) : correlated learners must have sequential quorum intersections (and conversely, if they do not, they they do not correlate). Other properties for  are possible. We do not need any to prove our correctness properties, but it is interesting to mention a few here: 1. ∀∀∀∀∀∀∀ ∀ ∀𝑙,𝑙′.↓(𝑙𝑙′)All learners correlate at first. The intuition is that learners with no behaviour should correlate, and only when they start to display behaviour might we decide that these behaviours do not correlate. 2. □(𝑙𝑙′)⇔⇔⇔⇔⇔⇔⇔ ⇔ ⇔ ♢ (𝑙𝑙′)Correlation is a property of time, but not of place. The intuition is that, given the same information, participants should globally agree on what the correlation relation should be. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |83 3. ∀∀∀∀∀∀∀ ∀ ∀𝑙,𝑙′. ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙𝑙′All learners correlate somewhere, sometime. This is perhaps the most interesting property. Algorithmically, this reflects an intuition (which we do not prove here) that if 𝑙 never correlates with 𝑙′ anywhere, at any time, then their  -equivalence partitions are in some sense running two concurrent algorithms. Even if they use the same messages, these two partitions cannot block one another so they can be thought of logically as two distinct runs of the algorithm, which happen to be run on the same network, but which are logically distinct nonetheless. Remark 8.6.2 (Discussion of (3twined) ).The proof of Proposition 8.4.5 uses (3twined) once, and this is the only place that our correctness properties for ThyHBB3 use that axiom.59 Specifically, we use (3twined) in Proposition 8.4.5 via the use of Lemma 8.4.3(1), whose proof requires a nonempty intersection between an 𝑙 -quorum of sequential participants, and 𝑙1and 𝑙2-quorums of echo messages. This is the only place in which we use (3twined) , so we should examine the proof to see precisely how this property is used — and whether something weaker might suffice. The actual property we require is this: ∀∀∀∀∀∀∀ ∀ ∀𝑙1, 𝑙2,𝑙3.□ ↓↓↓↓↓↓↓ ↓ ↓𝑙2seq =⇒𝑙1𝑙2⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↓(𝑙2𝑙3)=⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙1𝑙3seq. ( (3twined) in Figure 11 also quantifies over its learners, but as standard in writing axioms, we elide top-level universal quantifiers.) If we follow Remark 8.6.1(1) and assume that all learners correlate at first, then this simplifies to: ∀∀∀∀∀∀∀ ∀ ∀𝑙1, 𝑙2,𝑙3.𝑙1𝑙2⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙2seq ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓𝑙1𝑙3seq.(4) This looks a bit like a cross between (3twined) and the notion of a ‘safe’ learner from ThyHBB1. We could assume property (4) in ThyHBB3 instead of (3twined) and the proofs would work just as well. We prefer (3twined) because: • It is a purely structural restriction on quorums whose validity does not depend on behaviour during a run of the protocol. •It is very simple. • It corresponds nicely to the standard ‘ 2𝑓+1 ’-style assumption on quorum sizes that appears frequently in the literature (e.g. [ HM00 , page 4, 𝑄(3) property] or [ACTZ24, Definition 2]). Nevertheless, we note that a design space exists here, which could be explored in future work. 59We could also use (3twined) to deduce ♢ 𝑙1𝑙2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤, but we have that from 𝑙1𝑙2. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |84 Remark 8.6.3 (Alternative vote axioms).Arguably the following backward and forward rules for vote are more elegant than what is in Figure 11 (the other rules, including (VoteNE), are unchanged): (AltVote?) vote(𝑙, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ∃∃∃∃∃∃∃ ∃ ∃𝑙′𝑙.□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′echo(𝑣) (AltVote!) (live ∧∧∧∧∧∧∧ ∧ ∧ ⇕(𝑙′𝑙) ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′echo(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ∃∃∃∃∃∃∃ ∃ ∃𝑣′.↕vote(𝑙, 𝑣′) This gives vote(𝑙, 𝑣) and intuition of I saw an 𝑙′ -quorum of participants who saw someone propose 𝑣 for an 𝑙′ that correlates with 𝑙 — note that it may be that 𝑙′=𝑙. This treatment of vote is simpler and cleaner than the one in Figure 11, but it is also weaker. We see this clearly when we contrast the alternate forward rule (AltVote!) , which only guarantees progress for 𝑙 that correlate with themselves, with (Vote!) in Figure 11, which has no such restriction. In practice we are most interested in learners that do indeed correlate with themselves, so this restriction is not critical. Nevertheless, we prefer to state the stronger (more live) theory. Remark 8.6.4 (Wrong treatement of seq ).In view of Proposition 5.1.4 ( seq monotone) it might be tempting to unify axioms (seq) and (⇓) in Figure 11 into a single axiom as follows: (wrong) 𝑙𝑙′⇔⇔⇔⇔⇔⇔⇔ ⇔ ⇔ ♢ 𝑙𝑙′seq. But this would be wrong. As outlined in Remark 8.1.1(2), a participant might need to pick a side in some dispute between two other learners, and as a result decide to break 𝑙𝑙′— even though ♢ 𝑙𝑙′seq still holds. Remark 8.6.5 (Concluding remarks on ThyHBB3 ). ThyHBB3 succeeds on its own terms: it describes a short and simple protocol that naturally generalises homogeneous Bracha Broadcast, with correctness properties that resemble those for Bracha Broadcast. If there is a defect it is that the 3-twined quorum intersection property that any three quorums intersect (needed for the Liveness 2 property; see Remark 8.6.2) might be too strong an assumption for some use-cases. That said, and to be fair, assuming nonempty triple quorum intersections (e.g. as in “assume 3𝑓+1 participants of which at most 𝑓 are faulty”) is a standard assumption in the literature, including for broadcast and consensus protocols. 9. Conclusions 9.1. Looking back on the results Let us summarise our ideas at a high level: DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |85 1. Prehistories equate time with an epsilon-structure of past events: a point in time is a set of place-event-time tuples, the time of each is itself a set of tuples, and so on. History structures are just hereditarily transitive prehistories. Intuitively, transitivity means that knowledge of time is transitive: if we know of an event from a participant that knew of some other event, then we know of that other event. This corresponds to modelling full information protocols. 2. We use (pre)histories to design a modal logic, tailored to specifying and reasoning distributed protocols. We include built-in modalities for specifying things like occurrence of events in the past, quorums of present and past events, quorum intersections, and sequentiality / non-equivocation. Using this, we can write clean and compact formal axiomatisations of relevant properties (see next point). 3. We use our modal logic to specify distributed protocols symbolically as axiomatic theories. A model of the axioms corresponds to a concrete run of the protocol; the class of all models corresponds to the set of all possible runs of the protocol. Essentially, phrasing things in this way turns distributed protocol design and verification into axiomatic logic and model theory. Verification of a correctness property 𝜙 is just a proof that 𝜙 is valid in every model of the axioms: if a structure validates the axioms, then it satisfies 𝜙. 4. We use this machinery to design three protocols for Heterogeneous Bracha Broadcast (HBB) — ThyHBB1 , ThyHBB2 , and ThyHBB3 — each of which is a generalisation of broadcast to the case with multiple learners, and the three of which taken together give an idea of the design space involved. We formally state and prove their correctness properties.60 We can shorten this to three slogans and a claim: 1. Slogan 1: Times are sets. 2. Slogan 2: Protocols are theories. 3. Slogan 3: Protocol verification is proof and model-checking. 4. Claim: Heterogeneous broadcast can be studied as the above. We do not mean these slogans reductively, rather: set theory, modal logic, and model-theory are well-developed fields and we can usefully import their ideas to represent and prove things about distributed protocols. The development in this paper has been formalised in Lean 4. The relevant files are easily available [ Har25 ], along with (clear and straightforward) usage 60 Other protocols are possible, but HBB is an excellent start: a simple but nontrivial and useful protocol which occupies a (for us) helpful spot in the design space. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |86 instructions.61 The logic-and-models approach offers precision: English is good for exposition and for giving context, but logic has a way of distilling complex ideas into short predicates with precise meanings. Informal arguments reduce to precise and concise formal reasoning. In the ideal case, verification of correctness properties reduces to symbol-pushing. Furthermore, we would argue that the understanding of the protocol is deeper for a logic formalisation, for the same reason that logic helps deepen understanding in other fields: this encourages (and forces) us to state assumptions, to identify key lemmas, and to phrase assumptions in abstract yet precise form. The reader can find this exhibited in, for example, the specification of ThyHBB3 in Figure 11, its correctness properties in Figure 12, and in their proofs. Remark 9.1.1.Our modal logic is specific, in the sense that the maths is shaped by and optimised for the requirements of specific algorithms. Conversely, our three algorithms only exist because we designed them using this logic. We might not have found them otherwise. The logic and its semantics, and the protocols, came into existence by a constructive symbiosis. There is a real and useful sense in which the logic, semantics, and protocols have constrained, motivated, guided, and validated the design of the other. 9.2. Why heterogeneous protocols? 9.2.1. It’s about the ecosystem Why should we consider heterogeneous distributed protocols? The short answer is: because they are ubiquitous. The longer answer is as follows: Any distributed protocol must include some form of trust model. In this paper, we represent the trust model as a semiframe (a.k.a. a quorum system) as per Definition 3.3.2. But let us step back from the mathematics and its definitions and note that: •if you use Ethereum, you trust Ethereum (to some extent); •if you use a bank, you trust that bank (to some extent); • if you live in a country, you trust that country’s society and governance (to some extent); • if you eat a pre-made sandwich, you trust the industrial complex that manufactured it to (probably) not give you food poisoning; •if you go to a nightclub, you to trust the staff to keep you safe; and so on. So the world is naturally an ecosystem of distributed systems, each 61 We emphasise the ‘clear and straightforward’. Anybody who can get this far in the paper can certainly follow the formalised development. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |87 one based on and requiring some kind of trust assumption. That is: the world is distributed and heterogeneous. There is a tendency within a system to use that system, and to pretend that the rest of the world is somehow out-of-scope. Indeed, some trust models have been very successful: Ethereum, the US dollar, large sandwich brands. This may generate an illusion of homogeneity, but this is an illusion — and this illusion can become expensive, and even self-defeating. At best, a very popular, trusted system can lead to high prices as the system is oversubscribed. At worst, a homogeneous, dominant trust model can lead to monopolistic and rent-seeking behaviour [Doc25].62 There will always be a bottleneck. There will always be someone who wants a different service. There will always be someone who will not (or cannot, e.g. for regulatory reasons) submit to your trust model.63 As helpful as it is to optimise individual distributed systems to be faster and more reliable, this will just result in improved individual distributed systems, and to the extent that these might gain users, these improvements will only make more pressing the bottlenecking question of how to make multiple distributed systems interact well, as a healthy ecosystem. There can never be One Final Trusted Party. Therefore, and inevitably, we must ask ourselves: how can we approach heterogeneous distributed systems? How can distributed systems collaborate gracefully, reliably, and at low cost? What is the mathematics of an ecosystem with heterogeneous trust? History structures, our modal logic, and our three heterogeneous trust broadcast protocols are this paper’s preliminary, theoretical, provisional answer. 62 Enshittification or platform decay [ Doc25 ]: the tendency of a useful platform (‘trust model’, in our terms) to create value, succeed, dominate — then extract rent from each of the parties who trusted it until the original value proposition is completely undermined. Enshittification seems more accurate than ‘platform decay’, because ‘decay’ suggests a natural process that happens through neglect, whereas ‘enshittification’ more accurately suggests the outcome of active choices made by participants in an economic framework. A classic text 1960s text on business management [ Dru67 , page 14] comes at a related point, when it writes of a tendency of executives in an organisation to make poor decisions because they simply forget that the outside world exists: “The executive is within an organisation [but] there are no results within an organisation. All the results ...are produced by a customer who converts the ...efforts of the business into ...profits through his willingness to exchange his purchasing power for ...products and services”. The underlying common theme here is that it never just about the system, it’s always about how that system interacts with the rest of the world. Where we forget that, things go wrong. 63 It may help to put numbers to this. The market capitalisation of Ethereum at time of writing is (according to an internet search) roughly 0.5 trillion USD. This is a lot of money. However, it is less than the total assets of the House of Saud at 1.4 trillion USD, or of J.P. Morgan’s assets under management at 3.4 trillion USD. The numbers are subject to change but what will not change is that J.P. Morgan, House of Saud, and Ethereum will never merge. They will never fully trust each other. The real world is inherently heterogeneous. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |88 9.2.2. Why this has not been done before We see two reasons that protocols like ThyHBB1 , ThyHBB2 , and ThyHBB3 have not been studied before: 1. Distributed systems in the modern sense are relatively new. The founding papers are from the 1980s, but it has only been with the rise of the internet and then blockchains that distributed systems have assumed the modern reach and relevance that we now associate to them. In a nutshell, these issues have only become pressing in the last ten years or so. The mathematics is very much still catching up. 2. Distributed systems are hard, and heterogeneous distributed systems are even harder, because of how the trust model may vary by participant and by time. A goal of this paper is to establish heterogeneous distributed systems as a field of study and to show how they can be accurately and conveniently approached via modal logic over (pre)histories. These ideas are new — though we would argue that they are also necessary and inevitable. In short, as we see it, heterogeneous broadcast is at the cutting edge both of practical necessity and of what modern mathematics can deliver. This paper is intended to improve the state of the art in both dimensions: it makes new things possible, and it opens up new mathematical ways of making further progress. 64 So: if heterogeneity is unavoidable, then how do existing systems deal with it? With difficulty, and sometimes at considerable expense. Mostly, existing systems deal with heterogeneous trust work by reducing the system to its worst common denominator. Because this denominator may very low (i.e. participants do not trust one another) this often means in effect inventing more trusted parties, at great expense. To caricature the situation: if two parties that do not trust one another want to transact, it is necessary for them to find or create, and pay for, a third neutral trusted party to mediate between them. While possible, this is expensive and it does not scale — not least because it just pushes the problem down a level. What happens if the transaction above is successful and now a fourth party wants to interact? Should they invent a fifth neutral trusted party (more expense), or should they accept a single shared trusted arbiter of all truth (brings its own challenges)? Where does this end, if not in centralising all trust? 9.2.3. Embracing heterogeneity The mathematics in this paper — preliminary, theoretical, and provisional as it may be — is of a different colour, in that it embraces heterogeneity in existing 64 There is an irony to our solution, in that the techniques we import are from modal logic and model theory, which are old fields (older than distributed systems). But then again perhaps we should not be surprised: modal logic and model theory were designed to handle complexity, so perhaps (heterogeneous) distributed algorithms are just another thing they are good at. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |89 blockchain bridges take a similar approach, with different details when chains are not compatible with IBC. Such protocols are extremely useful, but they are fundamentally asynchronous point-to-point communication, so they do not and cannot carry the guarantees that broadcast can. In contrast, Heterogeneous Broadcast ensure that multiple chains receive the same message together, or not at all (specifically, this is Liveness 2). We can use this for cross-chain atomic transactions with Sui-style owned objects [ BCD+24 ], without requiring a multi-phase commit [ Her18 ] using cross-chain messaging protocols. Broadcast-based cross-chain transactions would be much faster than multi-phase commits. Another advantage of this approach is that in a multi-phase commit, each chain locks state until the other chains respond. If another (involved) chain never responds, everyone else’s state remains locked: liveness of all involved state is bounded by the least live chain, which is not ideal. Protocols that directly address heterogeneity would be immune or less susceptible to this issue. 9.4. Future work Several future directions are clear: 1. Model checking. A model-checker for our logic would be helpful. This would accelerate the development loop for candidate protocols, because we could write down axioms and some desired correctness properties and ask the machine to find a refuting counterexample if it can, i.e. a model that satisfies the axioms but does not satisfy the correctness properties. This would help with triage of protocols. We would still want formal proofs of correctness for the final, successful, axiomatisation. 2. Theorem-proving. An implementation of our logic in a theorem-prover would likewise be useful, for machine checking these formal proofs, once we have them. 3. 𝑛 -round HBB. We have given three HBB protocols in this paper, but the design space is large and we have by no means exhausted it. In particular, preliminary investigation suggests that an 𝑛 -round protocol (where 𝑛 is the number of learners) would provide stronger agreement guarantees. The intuition is that after 𝑛 rounds, any hostile behaviour that does exist will become known to all 𝑛 learners, thus in some sense reducing the 𝑛 -learner heterogeneous case to something closer to the simpler homogeneous case. The relevant protocols remain to be developed and checked. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |96 4. Heterogeneous Paxos. Continuing the previous point, broadcast is useful for many kinds of algorithms (e.g. payment algorithms, where all we want to do is reliably broadcast actions by individual participants), but consensus would be a step up in power. Consensus can be expressed using broadcast [ Bra87 , Section 4, “The Consensus Protocol”], but a Heterogeneous Paxos algorithm would be useful. As noted in Subsection 9.3.1 the logic of this paper was used to formalise and find a bug in the correctness proofs of the heterogeneous paxos algorithm from [ SWRM21 ]. Its replacement remains to be designed and checked, and if we do then we will use this logic to do so. 5. Implementation. It remains to implement a prototype system based on the heterogeneous protocols in this paper or evolved from these (e.g. see previous point). Subsections 9.3.8 (cross-domain state updates) and Subsection 9.3.9 (interoperability) outline some concrete use-cases (these examples are not exhaustive). 6. Other protocols. Protocol design is an active area of research. It remains to use the declarative methodology of this paper to study further protocols, and to design new ones. One particular interest is heterogeneous protocols, but the design space of distributed protocols, heterogeneous or not, is vast. We would put to the reader that each protocol family has its own distinct character, each of which may correspond to a distinct family of logics which remains to be discovered and studied. A lot of interesting theoretical work, with useful practical outcomes, may be possible here, giving declarative formalisations of distributed protocols. 7. Methodology. Having now analysed a number of protocols in declarative logical style, including Paxos [ GZ25 ] and both homogeneous and heterogeneous broadcast, the first author puts to the reader that we do not really understand a protocol until we have declaratively axiomatised it. We may think that we do, but the declarative axiomatic method is as much of a step up in clarity and precision applied to distributed protocols, as it was when Euclid invented and applied it to geometry [ Euc83 ]. The first author would argue that our understanding of every protocol could be deepened and enriched by a declarative axiomatisation in the general spirit of this paper, and that we should be applying the techniques in this paper and its companion papers (e.g. [ GZ25 ]) more widely to protocols both large and small. 8. Morphisms. An interesting question is what an appropriate notion of morphism of models would be (Definition 3.3.3). Since morphisms are DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |97 structure-preserving maps, to answer this question is to decide on the essential structure of a model. This is similar to the question we posed in Remark 3.6.9(2), as to what abstractly the structure of one of our Kripke models is. One likely answer, given that our modalities refer to quorums and quorums are semitopological (cf. Subsection 3.3.1 and footnote 26), is to decide that we have been studying semitopological Kripke structures (i.e. Kripke structures where possible worlds are enriched with notions of points and semitopological structure). This seems natural. A notion of ‘topological Kripke structure’ has been created [ Pym02 ], though we do not believe they would necessarily be closely related to what we do here. This is future research. 9. Time-heterogeneity; more heterogeneity. In Remark 1.1.3 we discussed how in the real world quorums (trust assumptions) vary both by space and by time. In this paper we use a notion of learner, each of which identifies a different set of trust assumptions, but this is not the only way to set things up. Notably, we could extend our framework and logic such that trust assumptions can evolve, e.g. they could evolve over time. In fact our protocol ThyHBB3 already includes some element of this, by using logic to express a correlation relation  between learners. Nevertheless, there is clear scope for more exploration of a design space where trust assumptions are allowed to vary even more. On a related note, this paper is about heterogeneous distributed systems, but (as noted in the previous paragraph) it is not the most heterogeneous situation imaginable. So we can ask: what is the most heterogeneous possible mathematically interesting notion of trust? Right now we are clearly nowhere near that limit. We see this because our definitions are full of mathematical structure: semifilters; modal logics; history structures. To be clear: this paper is designed to have structure in search of specific broadcast protocols, not remove it in search of generality for its own sake (though even if all we care about is generality for its own sake, studying specific protocols still informs the shape of the interesting design space). In future work we could go the other way and generalise, generalise, generalise, trying to distil most general possible accounts (there may be more than one) of what heterogeneous trust can mean. References ACTZ24. Orestis Alpos, Christian Cachin, Björn Tackmann, and Luca Zanolini. Asymmetric distributed trust. Distributed Computing, 37(3):247–277, 2024. URL: https: //doi.org/10.1007/s00446-024-00469-1, doi:10.1007/S00446-024-00469-1 . (cit. on pp. 46 and 84.) DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |98 Acz88. Peter Aczel. Non-wellfounded Set Theory. Number 14 in CSLI lecture notes. CSLI, 1988. (cit. on p. 15.) AHK97. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. In Proceedings 38th Annual Symposium on Foundations of Computer Science, pages 100–109, 1997. http://doi.org/10.1109/SFCS.1997.646098. (cit. on p. 93.) AW04. Hagit Attiya and Jennifer Welch. Fault-Tolerant Consensus, chapter 5, pages 91–124. John Wiley & Sons, Ltd, 2004. URL: https://onlinelibrary.wiley.com/doi/ abs/10.1002/0471478210.ch5, arXiv:https://onlinelibrary.wiley.com/doi/ pdf/10.1002/0471478210.ch5,doi:10.1002/0471478210.ch5. (cit. on p. 46.) BCD+24. Sam Blackshear, Andrey Chursin, George Danezis, Anastasios Kichidis, Lefteris Kokoris-Kogias, Xun Li, Mark Logan, Ashok Menon, Todd Nowacki, Alberto Sonnino, Brandon Williams, and Lu Zhang. Sui lutris: A blockchain combining broadcast and consensus, 2024. URL: https://arxiv.org/abs/2310.18042, arXiv: 2310.18042. (cit. on pp. 8,95, and 96.) BdRV01. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge University Press, 2001. (cit. on pp. 3and 30.) Bra84. Gabriel Bracha. An asynchronous [(n - 1)/3]-resilient consensus protocol. In Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing, PODC ’84, page 154–162, New York, NY, USA, 1984. Association for Computing Machinery. doi:10.1145/800222.806743 . (cit. on pp. 46 and 102.) Bra87. Gabriel Bracha. Asynchronous byzantine agreement protocols. Information and Computation, 75(2):130–143, 1987. URL: https://www.sciencedirect.com/ science/article/pii/089054018790054X, doi:10.1016/0890-5401(87)90054-X . (cit. on pp. 6,7,46,97, and 102.) BvdH14. Nick Bezhanishvili and Wiebe van der Hoek. Structures for epistemic logic. In Alexandru Baltag and Sonja Smets, editors, Johan van Benthem on Logic and Information Dynamics, pages 339–380. Springer International Publishing, Cham, 2014. Available online at https://doi.org/10.1007/978-3-319-06025-5_12. doi:10.1007/978-3-319-06025-5_12. (cit. on p. 91.) CDL+12. Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. Tla+ proofs. In Dimitra Giannakopoulou and Dominique Méry, editors, FM 2012: Formal Methods, pages 147–154, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Extended version: https: //proofs.tlapl.us/doc/web/content/Documentation/Publications/fm-long.pdf. doi: 10.1007/978-3-642-32759-9_14. (cit. on p. 95.) CGR11. Christian Cachin, Rachid Guerraoui, and Luís E. T. Rodrigues. Introduction to Reliable and Secure Distributed Programming (2nd edition). Springer, 2011. doi:10.1007/978-3-642-15260-3. (cit. on pp. 4and 7.) CJKR12. Allen Clement, Flavio Junqueira, Aniket Kate, and Rodrigo Rodrigues. On the (limited) power of non-equivocation. In Proceedings of the 2012 ACM Symposium on Principles of Distributed Computing, PODC ’12, page 301–308, New York, NY, USA, 2012. Association for Computing Machinery. doi:10.1145/2332432. 2332490. (cit. on p. 63.) CMSK07. Byung-Gon Chun, Petros Maniatis, Scott Shenker, and John Kubiatowicz. Attested append-only memory: making adversaries stick to their word. SIGOPS Operating Systems Review, 41(6):189–204, October 2007. doi:10.1145/1323293.1294280 . (cit. on p. 63.) Cos. Cosmos Developer Portal. IBC token transfer. https://tutorials.cosmos.network/ academy/3-ibc/7-token-transfer.html. Accessed: 2025-10-29. (cit. on p. 95.) DDFN07. Ivan Damgård, Yvo Desmedt, Matthias Fitzi, and Jesper Buus Nielsen. Secure protocols with asymmetric trust. In Kaoru Kurosawa, editor, Advances in Cryptology - ASIACRYPT 2007, 13th International Conference on the Theory and Application of Cryptology and Information Security, Kuching, Malaysia, December 2-6, 2007, Proceedings, volume 4833 of Lecture Notes in Computer Science, pages 357–375. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |99 Springer, 2007. doi:10.1007/978-3-540-76900-2\_22. (cit. on p. 46.) Dev93. Keith Devlin. The Joy of Sets: Fundamentals of Contemporary Set Theory. Undergraduate Texts in Mathematics. Springer New York, NY, 2 edition, August 1993. doi:10.1007/978-1-4612-0903-4. (cit. on p. 23.) Doc25. Corey Doctorow. Enshittification: Why Everything Suddenly Got Worse and What To Do About It. Verso Books, October 2025. (cit. on p. 88.) Dol82. Danny Dolev. The byzantine generals strike again. Journal of Algorithms, 3(1):14–30, 1982. URL: https://www.sciencedirect.com/science/article/pii/ 0196677482900049,doi:10.1016/0196-6774(82)90004-9. (cit. on p. 7.) Dru67. Peter F. Drucker. The effective executive. Harper & Row, 1st edition, 1967. (cit. on p. 88.) Euc83. Euclid. In I.L. Heiberg and H. Menge, editors, Euclidus Opera Ominia. 1883. Online at https://farside.ph.utexas.edu/books/Euclid/Euclid.html (permalink). (cit. on p. 97.) Gab24. Murdoch J. Gabbay. Semitopology: decentralised collaborative action via topology, algebra, and logic. College Publications, August 2024. ISBN: 9781848904651. (cit. on pp. 27,28,46, and 90.) Gab25a. Murdoch Gabbay. Semiframes: algebras of heterogeneous consensus, 2025. Journal paper to appear, available online at https://arxiv.org/abs/2310.00956. arXiv:2310.00956. (cit. on p. 28.) Gab25b. Murdoch J. Gabbay. Semitopology: a topological approach to decentralised collaborative action. The Journal of Logic and Computation, January 2025. https://doi.org/10.1093/logcom/exae050. doi:10.1093/logcom/exae050 . (cit. on pp. 27,46, and 90.) Gar24. James Garson. Modal Logic. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Spring 2024 edition, 2024. Available online at https://plato.stanford. edu/archives/spr2024/entries/logic-modal/. (cit. on pp. 30 and 47.) GHR94. Dov M Gabbay, Ian Hodkinson, and Mark Reynolds. Temporal Logic: Mathematical Foundations and Computational Aspects, volume 1. Oxford University Press, 07 1994. doi:10.1093/oso/9780198537694.001.0001. (cit. on p. 39.) GKL24. Éric Goubault, Roman Kniazev, and Jérémy Ledent. A Many-Sorted Epistemic Logic for Chromatic Hypergraphs. In Aniello Murano and Alexandra Silva, editors, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), volume 288 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30:1–30:18, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs. CSL.2024.30,doi:10.4230/LIPIcs.CSL.2024.30. (cit. on p. 91.) GKM+19. Rachid Guerraoui, Petr Kuznetsov, Matteo Monti, Matej Pavlovič, and DragosAdrian Seredinschi. The consensus number of a cryptocurrency. In Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC ’19, page 307–316, New York, NY, USA, 2019. Association for Computing Machinery. Extended version: https://arxiv.org/abs/1906.05574. doi:10.1145/3293611.3331589. (cit. on pp. 8and 95.) GKWZ03. Dov M. Gabbay, Agnes Kurucz, Frank Wolter, and Michael Zakharyaschev. Manydimensional modal logics: theory and applications, volume 148 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2003. (cit. on p. 47.) Goe20. Christopher Goes. The Interblockchain Communication Protocol: An Overview, May 2020. https://github.com/cosmos/ibc/blob/ 8d9d3b6fe7309b034df8457760b3bbd11d24b8e1/archive/papers/2020-05/ build/paper.pdf#L2. (cit. on p. 95.) GZ25. Murdoch J. Gabbay and Luca Zanolini. A declarative approach to specifying distributed algorithms using three-valued modal logic, 2025. Journal draft submitted for publication. Available at https://arxiv.org/abs/2502.00892. arXiv:2502.00892 . (cit. on pp. 8,46,61,78, and 97.) DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |100 Har25. Anthony Hart. Heterogeneous Broadcast in Lean 4, Nov 2025. https://doi.org/10. 5281/zenodo.17611734 Direct download link of zip archive: https://zenodo.org/ api/records/17611735/files-archive. doi:10.5281/zenodo.17611735 . (cit. on pp. 6and 86.) Her91. Maurice Herlihy. Wait-free synchronization. ACM Trans. Program. Lang. Syst., 13(1):124–149, January 1991. doi:10.1145/114005.102808 . (cit. on pp. 8and 95.) Her18. Maurice Herlihy. Atomic cross-chain swaps. In Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing, PODC ’18, page 245–254, New York, NY, USA, 2018. Association for Computing Machinery. doi:10.1145/ 3212734.3212736. (cit. on p. 96.) HM00. Martin Hirt and Ueli Maurer. Player simulation and general adversary structures in perfect multiparty computation. Journal of Cryptology, 13(1):31–60, January 2000. doi:10.1007/s001459910003. (cit. on pp. 46 and 84.) HMU07. John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Pearson/Addison Wesley, Boston, 3rd edition, 2007. Available online (permalink). (cit. on p. 21.) ics24. Draft Spec for Multi-Denom Packets ICS20 v2, March 2024. https://github.com/ cosmos/ibc/blob/main/spec/app/ics-020-fungible-token-transfer/README.md. (cit. on p. 95.) IT11. ITU-T. ITU-T Z.120 (02/2011): Message Sequence chart (MSC). Technical report, ITU-T Recommendations, 2011. https://handle.itu.int/11.1002/1000/11063 (persistent link to direct download: https://www.itu.int/rec/dologin_pub.asp?lang= e&id=T-REC-Z.120-201102-I!!PDF-E&type=items). (cit. on p. 94.) Jec06. Thomas Jech. Set theory. Springer, 2006. Third edition. (cit. on p. 14.) Joh87. Peter T. Johnstone. Notes on logic and set theory. Cambridge University Press, 1987. (cit. on p. 15.) Lam78. Leslie Lamport. Time, clocks and the ordering of events in a distributed system. Communications of the ACM 21, 7 (July 1978), 558-565. Reprinted in several collections, including Distributed Computing: Concepts and Implementations, McEntire et al., ed. IEEE Press, 1984., pages 558–565, July 1978. (cit. on pp. 9, 16,20, and 94.) Lam02. Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., USA, 2002. Available online at https://lamport.azurewebsites.net/tla/book.html. (cit. on p. 95.) LSP82. Leslie Lamport, Robert Shostak, and Marshall Pease. The byzantine generals problem. ACM Trans. Program. Lang. Syst., 4(3):382–401, July 1982. https: //doi.org/10.1145/357172.357176.doi:10.1145/357172.357176. (cit. on p. 4.) Mal99. Dahlia Malkhi. Quorum systems. In Encyclopedia of distributed computing. Kluwer, 1999. Tutorial chapter, available online at https://malkhi.com/files/ Quorums1999.pdf (permalink). (cit. on p. 27.) Maz15. David Mazières. The Stellar consensus protocol: a federated model for Internet-level consensus. Technical report, Stellar Development Foundation, 2015. https://www.stellar.org/papers/stellar-consensus-protocol.pdf (permalink: https://web.archive.org/web/20240629063518/https://stellar.org/ learn/stellar-consensus-protocol). (cit. on p. 90.) MR97. Dahlia Malkhi and Michael Reiter. Byzantine quorum systems. In Proceedings of the Twenty-Ninth Annual ACM Symposium on Theory of Computing, STOC ’97, page 569–578, New York, NY, USA, 1997. Association for Computing Machinery. doi:10.1145/258533.258650. (cit. on p. 27.) Pym02. David J. Pym. Topological Kripke Semantics, pages 67–87. Springer Netherlands, Dordrecht, 2002. doi:10.1007/978-94-017-0091-7_5. (cit. on p. 98.) RS96. Michel Raynal and Mukesh Singhal. Logical time: capturing causality in distributed systems. Computer, 29(2):49–56, 1996. Available online at https://decomposition.al/CSE232-2021-09/readings/extra/ DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |101 raynal-singhal-logical-time-survey.pdf (permalink). doi:10.1109/2.485846 . (cit. on pp. 9and 16.) SM94. Reinhard Schwarz and Friedemann Mattern. Detecting causal relationships in distributed computations: In search of the holy grail. Distributed Computing, 7:149–174, March 1994. Available online at https://vs.inf.ethz.ch/publ/papers/ holygrail.pdf (permalink). doi:10.1007/BF02277859. (cit. on pp. 9and 16.) SWRM21. Isaac Sheff, Xinwen Wang, Robbert van Renesse, and Andrew C. Myers. Heterogeneous Paxos. In Quentin Bramas, Rotem Oshman, and Paolo Romano, editors, 24th International Conference on Principles of Distributed Systems (OPODIS 2020), volume 184 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1–5:17, Dagstuhl, Germany, 2021. Schloss Dagstuhl–Leibniz-Zentrum für Informatik. ISSN: 1868-8969. URL: https://drops.dagstuhl.de/opus/volltexte/ 2021/13490,doi:10.4230/LIPIcs.OPODIS.2020.5. (cit. on pp. 90,95, and 97.) SYB14. David Schwartz, Noah Youngs, and Arthur Britto. The Ripple Protocol Consensus Algorithm. Ripple Labs Inc White Paper, 5(8):151, 2014. (cit. on p. 90.) TW92. Edwin F. Taylor and John Archibald Wheeler. Spacetime Physics, Second Edition. W. H. Freeman and Co., New York, USA, 1992. Available online at https://www. eftaylor.com/spacetimephysics/. (cit. on p. 94.) uml17. UML: Unified modeling language. Technical report, Object Management Group Standards Development Organization (OMG SDO), 2017. https://www.omg.org/ spec/UML/2.5.1/. (cit. on p. 94.) vdHW03. Wiebe van der Hoek and Michael Wooldridge. Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Studia Logica, 75(1):125–157, Oct 2003. doi:10.1023/A:1026185103185. (cit. on p. 93.) Wik25. Wikipedia. Kleene fixed-point theorem — Wikipedia, the free encyclopedia, 2025. https://en.wikipedia.org/w/index.php?title=Kleene_fixed-point_theorem& oldid=1289692885. (cit. on p. 14.) WN95. Glynn Winskel and Mogens Nielsen. Models for Concurrency. In Handbook of Logic in Computer Science, volume 4. Oxford University Press, 1995. (cit. on p. 93.) A. Reducing to the homogeneous case We consider what happens to our axiomatisations and correctness properties when we assume there is just one learner. We further assume that any three quorums intersect at a sequential participant (in our logic: ♢ 𝑙𝑙𝑙 seq ), as per the original algorithm by Bracha — see “In this section we show that the protocol in Fig. 1 achieves Asynchronous Byzantine agreement for 0≤𝑡<𝑛/3 ” [ Bra84 , Subsection 3.2] or “[we present] a randomized consensus protocol that tolerates up to 𝑡<𝑛/3 Byzantine processes” [Bra87, Page 133]. Given one learner and sequential triple quorum intersections, it is easy to check that: 1. ⊨ ♢ 𝑙𝑙 ⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤and ⊨ ♢ 𝑙𝑙𝑙 ⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤and ⊨ ♢ 𝑙𝑙 seq always. 2. In ThyHBB1, every participant is safe. 3. In ThyHBB3 , we have (3twined) and (seq) . We will also assume that every learner is correlated. Since there is only one learner, and all quorum intersections contain a sequential participant, this is reasonable. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |102 We obtain axiomatisations and correctness properties as below. We sum up the outcome: 1. ThyHBB1 and ThyHBB2 become textually identical to one another and to the idea of Bracha Broadcast. 2. ThyHBB3 is textually slightly different because of the disjunct in its (Vote?) rule and because of (Vote’!) , but a very small amount of proof shows that this is only apparent: the disjunct and (Vote’!) are logically redundant and can be removed. There is also the (VoteNE) rule, but with our assumptions this is also redundant because it can be derived from (EchoNE) and the other axioms. So ThyHBB3 simplifies to the same thing as ThyHBB1 and ThyHBB2. In conclusion: in the homogeneous case, our three protocols — boringly and reassuringly — reduce to the same core. A.1. Homogeneous ThyHBB1 and ThyHBB2 (Figures 7and 9) Backward rules (HBB) (Echo?) echo(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣) (Vote?) vote(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑣)) (Deliver?) deliver(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙vote(𝑣) Other rules Include axioms of ThyLive from Figure 6 (EchoNE) echo(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↓echo(𝑣′)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝑣======= = =𝑣′ Forward rules (Echo!) (live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ∃∃∃∃∃∃∃ ∃ ∃𝑣′.↕echo(𝑣′) (Vote!) (live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕vote(𝑣) (Deliver!) (live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙vote(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑣) 1. Liveness 1 If ⊨□𝑙live and ⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑣). 2. Liveness 2 If 𝑣∈Value and ⊨□𝑙live then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑣). 3. Soundness / Agreement If 𝑣1, 𝑣2∈Value then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑣1)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑣2)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝑣1======= = =𝑣2. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |103 A.2. Homogeneous ThyHBB3 (Figure 11) Backward rules (Echo?) echo(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣) (Vote?) vote(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒(□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑣) ∨∨∨∨∨∨∨ ∨ ∨ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑣)) (Deliver?) deliver(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙vote(𝑣) Other rules Include axioms of ThyLive from Figure 6 (EchoNE) echo(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↓echo(𝑣′)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝑣======= = =𝑣′ (VoteNE) vote(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↓vote(𝑣′)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝑣======= = =𝑣′ Forward rules (Echo!) (live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ∃∃∃∃∃∃∃ ∃ ∃𝑣′.↕echo(𝑣′) (Vote!) (live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ∃∃∃∃∃∃∃ ∃ ∃𝑣′.↕vote(𝑣′) (Vote’!) (live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓vote(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ∃∃∃∃∃∃∃ ∃ ∃𝑣′.↕vote(𝑣′) (Deliver!) (live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙vote(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑣) 1. Liveness 1 If ⊨□𝑙live and ⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒deliver(𝑣). 2. Liveness 2 If ⊨□𝑙live then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑣). 3. Soundness / Agreement If 𝑣1, 𝑣2∈Value then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑣1)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑣2)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝑣1======= = =𝑣2. DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |104 Backward rules (HBB) (Echo?) echo(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣) (Vote?) vote(𝑙, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑣) (Deliver?) deliver(𝑙′,𝑙, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′vote(𝑙, 𝑣) Other rules Include axioms of ThyLive from Figure 6 (EchoNE) echo(𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↓echo(𝑣′)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝑣======= = =𝑣′ Forward rules (Echo!) (live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ∃∃∃∃∃∃∃ ∃ ∃𝑣′.↕echo(𝑣′) (Vote!) (live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙echo(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕vote(𝑙, 𝑣) (Deliver!) (live ∧∧∧∧∧∧∧ ∧ ∧□ ↓↓↓↓↓↓↓ ↓ ↓𝑙′vote(𝑙, 𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙′,𝑙, 𝑣) Figure 9. Theory ThyHBB2 (Definition 7.1.1) 1. Liveness 1 If 𝑙∈Learner and ⊨□𝑙live and ⊨∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1 ∃1𝑣. ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓(live ∧∧∧∧∧∧∧ ∧ ∧ ♢ ↓↓↓↓↓↓↓ ↓ ↓propose(𝑣)) ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙, 𝑙, 𝑣). In words: suppose there is a live 𝑙 -quorum and suppose precisely one value is proposed. Then if some live participant finds out about that proposed value, then every live participant eventually delivers. 2. Liveness 2 If 𝑙′ 1,𝑙′ 2,𝑙 ∈Learner and 𝑣∈Value and ⊨ ♢ 𝑙′ 1𝑙′ 2⊤⊤⊤⊤⊤⊤⊤ ⊤ ⊤and ⊨□𝑙′ 2live then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙, 𝑣)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒live ⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒↕deliver(𝑙′ 2,𝑙, 𝑣). In words: suppose 𝑙′ 1 and 𝑙′ 2 have nonempty quorum intersections and there is a live 𝑙′ 2 -quorum. Then if some participant delivers 𝑣 for (𝑙′ 1,𝑙) then every live participant delivers 𝑣for (𝑙′ 2,𝑙). 3. Soundness / Agreement If 𝑙1,𝑙2,𝑙′ 1,𝑙′ 2∈Learner and 𝑣1, 𝑣2∈Value and ⊨ ♢ 𝑙1𝑙2seq then ⊨ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 1,𝑙1, 𝑣1)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒ ♢ ↓↓↓↓↓↓↓ ↓ ↓deliver(𝑙′ 2,𝑙2, 𝑣2)⇒⇒⇒⇒⇒⇒⇒ ⇒ ⇒𝑣1======= = =𝑣2. In words: suppose 𝑙1 and 𝑙2 have sequential quorum intersections. Then if some participant delivers 𝑣1 for (𝑙′ 1,𝑙1) and another delivers 𝑣2 for (𝑙′ 2,𝑙2) , then 𝑣1=𝑣2. Figure 10. Correctness properties for ThyHBB2 (Theorem 7.1.3) DOI: 10.5281/zenodo.17636313 Anoma Research Topics |Tuesday 25th November, 2025 |105