Mathematical Terms
- Theorem
- A statement that has been rigorously proven based on axioms, definitions, and previously established theorems. In Paxos, theorems establish the correctness properties of the protocol, like safety and liveness.
- Constraint
- A condition or requirement that must hold true within the system. For example, a quorum intersection is a constraint ensuring that chosen values cannot conflict.
- Lemma
- An intermediate result used to prove a larger theorem. Lemmas in Paxos typically reason about acceptor behavior, ballot ordering, or quorum intersection.
- Corollary
- A statement that follows directly from a theorem or lemma. In Paxos, a corollary might be that a specific value will eventually be learned by all learners once a quorum accepts it.
- Prime notation (x′, B′)
- For any variable, a prime (') indicates a related or subsequent instance, e.g., x' is a later value or copy of x, or B' is another ballot distinct from B.