Below is the fundamental axiom for Actor events (i.e. communications:
∀[S:ActorSystem, P predicateOn Event<S>] // For every ActorSystem S and every predicate P on events of S
(∀[x:Primordial<S>] P[Creation[x]] // If P holds for the creation event of every primordial of S
⋀ ∀[e:FromOutside<S>] P[e] // and P holds for every event from outside S
⋀ ∀[e:Event<S>, e1:ImmediatelyFollows<e>] // and for every event of S
P[e]⇒P[e1]) // if P holds for the event, then P holds for each immediately following event
⇒ ∀[e:Event<S>] P[e] // then P holds for every event of S