An introduction to lockless algorithms

It's also important what rules *aren't* stated. There's no requirement e.g. that for any two events P and Q, you can always determine either that P happens before Q or that Q happens before P. It's perfectly acceptable for there to be no ordering between them (except where the axioms say there must be an ordering).

That's contrary to the everyday human concept of time, where you would say every event happens at a precise number of seconds past midnight and you can always work out which happened first. That concept is problematic to implement in computers, because it's simply impractical for physically separated processors to have perfectly synchronised nanosecond-precision clocks and to attach timestamps to every message they share. So we throw away that concept of time and time-lines and define a brand new concept (called "happens before", but could equally be called "op" or "→") from scratch.

The axioms are trying to define that new concept with the minimal set of requirements on where there must be a well-defined ordering between events, so it's just barely strong enough to achieve the goal (in this case to define some useful kind of synchronisation between concurrent threads). And in this particular case, transitivity is one property that is required else the mathematical proofs stop working, so it has to be stated explicitly in the definition.