Proof. It suffices to build a model M that satisfies all of these axioms. Let E, EO and O be three *pairwise disjoint* sets, where

$$E=\{e_{i}:1\leq i\leq7\}$$ $$E O=\{o_{i}:1\leq i\leq7\}$$
O = {oba,obd}
We define the universe of M to be the set Udf= E ∪ EO ∪ O. We then give the following interpretations 1. eventM = E
2. event occurrenceM = EO
3. observationM = O
4. occurrenceM = {(ei,oi) : 1 ≤ i ≤ 7}
5. earlier thanM is exactly the graph G1 from Example 1 6. not later thanM is exactly the graph G2 from Example 1 7. nonsimultaneousM is exactly the graph G3 from Example 1 8. observed beforeM = {(o1,o2,oba) : o1 ✁a o2**} ∪ {**(o1,o2,obd) : o1 ✁d o2}, where
✁a and ✁d are relations from Example 3.

9. observed simultM = {(o1,o2,oba) : o1 ⌢a o2**} ∪ {**(o1,o2,obd) : o1 ⌢d o2}, where
⌢a is the following relation

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

and ⌢d is the following relation

o6 2o7

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

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

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

It is easy to check that axioms (2.1) to (2.5) are satisfied by this interpretation. We also see from Example 1 how the interpretation of earlier than, not later than and nonsimultaneous given by G1, G2 and G3 respectively satisfies that axioms from (2.6)
to (2.14). It is also clear from Example 2 and Example 3 that our interpretation satisfies axioms from (2.15) to (2.24). ⊓⊔

## 3 Models Of The Theory Tgso

By Theorem 2, we already know that Tgso is consistent, and hence the class of all models satisfying Tgso is nonempty. In this section, we will attempt to classify all the possible models of our theory Tgso. For convenience, we let T*univ* denote the theory consisting of axioms from (2.1) to (2.5), and we let T*spec* denote the specification-level theory consisting of axioms from (2.6) to (2.14).

14