Theorem 6 (Axiomatizability Theorem for Tspec). Any model of Tspec is isomorphic to a structure of Mspec.

Proof. Let M be a model of T*spec*. We will show that M satisfies the conditions of the structures in M*spec* from Definition 3.

Since M satisfies axioms (2.6) and (2.7), we know that we can determine the vertex set EO = event occurrenceM for the graphs G1, G2 and G3.

Since M satisfies all axioms, from Proposition 1 we know that earlier thanM is a strict partial order, so it can be represented by an acyclic transitive graph G1 as from the condition (1) of Definition 3.

Since M satisfies axioms (2.12) and (2.13), we can represent the not later thanM
relation by a transitive graph G2 as from the condition (2) of Definition 3.

- To show that the condition (2)(a) is satisfied, we must show that G3 = G2 − G1 ⊆
IC(G1). Suppose for a contradiction that there is an edge (u,v) that appears on both G3 and IC(G1). Since G3 = G2 − G1, we know that (u,v) 6∈ E1, so (v,u) ∈
E1. This would mean that earlier thanM (v,u) and not later thanM (u,v). But this contradicts with Proposition 3.

- To show that the condition (2)(b) is satisfied, we assume for a contradiction that we have at least one of the following two triangles:

![0_image_0.png](0_image_0.png)

where the solid edges are edges of G1 and the dashed edges are edges of G3.

The left triangle implies that earlier thanM (u,v) and not later thanM (v,w) but not later thanM (u,w). This contradicts with axiom (2.14). Similarly the case of the right triangle also leads to a contradiction.

Since M satisfies axioms (2.9) and (2.10), we can represent nonsimultaneousM by a graph G4 as from the condition (3) of Definition 3. Let G5 = G4 −C(G1), it remains to show that G5 ⊆ IC(G2). Suppose for a contradiction that an edge (u,v) and (v,u) is shared by both the graph G5 and C(G2). Without loss of generality, we can assume that (u,v) ∈ G2. Thus, not later thanM (u,v) and nonsimultaneousM (u,v). But by axiom (2.11), we have that earlier thanM (u,v). This contradicts with our assumption that
(u,v) ∈ G5 = G4 −C(G1). ⊓⊔

## 3.3 Observations

We first introduce a more combinatorial representation of stratified orders.

Definition 4. *Given a set X, we call the pair* (P,◭) a ranking structure *of X if P is a* partitioning of the set X and ◭ is a total ordering on the set P. 

18