Theory guide

Run python -m muql check examples/semitopology.md. The nonempty opens are exactly {a} and {a,b,c}. The generator {a} and the whole point set are already closed under unions; {a,b} and {a,c} are not added. Every nonempty open contains a, so every finite collection of these opens has a nonempty intersection.

Here ◇ and □ range over points in the current quorum; ∃ꟴ and ∀ꟴ range over nonempty quorums. The combined symbols compose these operations: ∃ꟴ□(live) means some quorum is entirely live. See the notation guide for all four combinations and ASCII spellings.

The ASCII aliases somewhere and everywhere mean ◇ and □, respectively: they keep the current quorum. Use someQuorumSomePoint for ∃ꟴ◇ and everyQuorumEveryPoint for ∀ꟴ□ when the formula must also range over quorums.

Run python -m muql check examples/fixedpoints.md. The scope has three stages and one point. Stutter mode makes the final stage its own future successor. pulse is unconstrained, so recurrence identities are tested against every three-valued pulse sequence in this scope.

Use μ for a least fixed point and ν for a greatest fixed point; ASCII mu and nu work identically. Temporal operators keep their readable word names. See the notation guide for every spelling.

The first Simple theory in §6.1 of the Paxos paper (p.46) abstracts a protocol in which anyone may propose, everyone accepts a proposal, and a proposer decides when someone accepts. There is only one unnamed value, so all three predicates are nullary. These are the five exact axioms. The two properties below are small tutorial consequences, not named theorems from the paper.

Notation: ⇀ is strong implication (-\ in ASCII), → is weak (->), and ∃ꟴ◇ means “some quorum, some point”. All symbols have ASCII equivalents; either style is accepted.

This is the second Simple theory (§6.1, p.47). The backward implications remain strong; forward implications become weak so their conclusions may be b. Each predicate has a dense set of uncrashed participants. The paper's Uncrashed schema is written as three individually named axioms for easier experiments. The two properties are tutorial consequences.

Notation: ⇀ is strong implication (-\ in ASCII), → is weak (->), and ∃ꟴ◇ means “some quorum, some point”. All symbols have ASCII equivalents; either style is accepted.

This is the third Simple theory (§6.1, p.47). An initial period may lose messages; eventually the forward rules apply at every point in every quorum forever. The logical model has no explicit messages. ultimately expresses the network assumption.

The original theory is about infinite natural time. This literate input retains its temporal formulas in Unicode notation; finite checking must be interpreted according to the package's stated temporal support and boundaries. The added properties are tutorial consequences of the intended infinite theory.

Notation: ⇀ is strong implication (-\ in ASCII), → is weak (->), and ∃ꟴ◇ means “some quorum, some point”. All symbols have ASCII equivalents; either style is accepted.

The fourth Simple theory (§6.1, pp.47–48) combines eventual synchrony with a dense set of uncrashed participants for each predicate. Strong backward rules justify true events; weak forward rules permit crashed outcomes. All source axioms are retained. Properties are tutorial consequences, and infinite-time formulas retain the package's documented finite-checking limitations.

Notation: ⇀ is strong implication (-\ in ASCII), → is weak (->), and ∃ꟴ◇ means “some quorum, some point”. All symbols have ASCII equivalents; either style is accepted.

Four participants each cast one Boolean vote. A vote of b represents conflicting messages; an observation of b means that no result was observed. These are different interpretations of the same logical truth value.

This file transcribes Figure 3 and Proposition 2.5.7 of Gabbay, arXiv:2512.21137v3, with Unicode symbols for the connectives. Every axiom is checked at every participant. The quorum generators are the four three-person subsets; their unions are implicit.

The formulas use Unicode for readability. Every symbol also has an ASCII spelling, and the two styles can be mixed.

One sender broadcasts a payload. Participants may echo it, become ready, and deliver it. The four predicates record the declarative outcome, rather than a sequence of message arrivals.

The axioms below transcribe Figure 10 of Gabbay, arXiv:2512.21137v3. The properties are Figure 11. The three-way intersection assumption from Remark 4.2.1 is explicit. Backward rule names end in ?, forward rule names in !, and the ready relay is BrReady!!, following the paper's direction convention.

Read ∃ꟴ□ as “some quorum, every point”, ∃ꟴ◇ as “some quorum, some point”, and ∀ꟴ□ as “every quorum, every point”. The notation guide lists their ASCII spellings and explains the remaining symbols.

Section 4.3 of the companion paper, v3 claims that BrDeliver! can be weakened to existential delivery and recovered from the other axioms. For Figure 10 as printed, the claim fails.

This file contains the same Bracha axioms, except for that one proposed replacement. A one-participant, two-payload scope already suffices. The singleton quorum is three-way intersecting, so the failure is unrelated to quorum geometry.

The notation guide gives an ASCII equivalent for each Unicode symbol below. In particular, → is weak implication (->).

Participants start with either zero or one. An output of half records a failure to choose one binary value. The payload half is distinct from the logical truth value b.

These are the Figure 13 axioms and Figure 14 properties of Gabbay, arXiv:2512.21137v3. The ambient three-way intersection condition in Remark 5.3.1 is explicit. The domain must contain exactly the three listed payloads for this transcription.

Here ⇀ is strong implication (-\ in ASCII), while → is weak (->). The notation guide explains the quantifiers and quorum symbols; Unicode and ASCII can be mixed in any formula.

This is a direct transcription of TyPax, Definition 6.3.1 and Figure 11 (pp.49–50) of the attached paper, *A declarative approach to specifying Paxos using three-valued modal fixpoint logic*, by Murdoch J. Gabbay and Luca Zanolini. It includes all 20 named axioms, including the send step and the nonpositive μ expression for leader uniqueness.

A point is a participant. A stage is a ballot or logical round, not a message or machine instruction. b means a computation has crashed; both b and t count as valid. Consequently, P → Q permits a crashed conclusion, while P ⇀ Q requires a true conclusion whenever P is true.

The finite scope below chooses three participants, two ordinary values and the special value undef. The three pair quorums generate the usual majority semitopology. The checker reports results for its documented finite temporal semantics; these are not proofs of the paper's infinite-time theorems.

Notation: ⇀ is strong implication (-\ in ASCII), → is weak (->), and ∃ꟴ◇ means “some quorum, some point”. All symbols have ASCII equivalents; either style is accepted.

This is TySPax, Definition 8.2.1 and Figure 12 (pp.67–68) of the attached Paxos paper. All 12 axioms are present. This is the paper's own abstraction: send and undef disappear, leaders need not be unique, and all writes at a stage must agree globally. The forward write rule is also changed, so this theory is not obtained merely by deleting some TyPax axioms.

The scope is finite. The safety formulas include history from time zero, while infinite-time liveness remains subject to the checker limitations documented in the main README. A finite result does not establish Theorem 8.2.2 unboundedly.

Notation: ⇀ is strong implication (-\ in ASCII), → is weak (->), and ∃ꟴ◇ means “some quorum, some point”. All symbols have ASCII equivalents; either style is accepted.