On the computational realization of formal ontologies: Formalizing an ontology of instantiation in spacetime using Isabelle/HOL as a case study

In the ontology presented by Bittner (2018) what is physically possible according to the constraints imposed by classical mechanics is encoded in set-theoretic structures that give rise to KS -structures of the form (1) KS ( m , L ) = df ⟨ D ST , D E , K , V , ⊔ _ , ⊓ ‾ , TS , InstST , AtE ⟩ . The parameters m and L respectively specify the number of atomic particles and the Lagrangian field that constrains the physically possible changes a world with m atomic particles can undergo. Both parameters are determined empirically (Appendix C).

The sets D ST and D E of KS ( m , L ) are respectively the domains of regions of spacetime (sub-manifolds of the spacetime manifold) that can possibly exist and the domain of entities that can possibly exist. K is a modal frame structure on the set of physical possibilities. V is the interpretation function. The sets ⊔ _ , ⊓ ‾ , TS , InstST , AtE of KS ( m , L ) serve as the interpretations of the axiomatic primitives of the formal theory in the context of the physical possibilities in K . In the remainder of this subsection the focus is on K , D ST and D E . The interpretation function V is discussed when the syntax and the semantics of the formal language are introduced in Section 2.3. The sets ⊔ _ , ⊓ ‾ , TS , InstST and AtE are introduced as the computational representation of the formal ontology is developed.

Regions of spacetime and physical possibilities. The members of D ST are the regions of spacetime (sub-manifolds of the spacetime manifold in the sense of A.1). In particular D ST includes spacetime itself – a manifold of topology ST = ( ℜ × M ) , i.e., ST ∈ D ST . D ST also includes the set the members of Γ – the set of geometrically possible worldlines. Those are curves through spacetime along which processes that involve systems that are constituted of up to m particles and a Lagrangian field L can possibly evolve according to the laws of classical mechanics. (See also A.2, B.1.)

Σ is a set of T -slicings σ of spacetime. A T -slicing of spacetime is a smooth mapping σ : ℜ × T → ( ℜ × M ) such that for every instant t ∈ ℜ of time, σ t maps the points of an abstract n-dimensional Euclidean space, T , to the points of an n-dimensional slice σ t ( T ) ⊆ ST of the n + 1 -dimensional spacetime manifold ST (see also B.1). For all slicings σ ∈ Σ , the set of all time slices σ t ( T ) is a subset of D ST . Spatial regions are members of D ST that emerge from the intersection of worldlines and time slices. That is, if γ ∈ Γ and γ ∩ σ t ( T ) ≠ ∅ then γ ∩ σ t ( T ) ∈ D ST . A subset of the geometrically possible worldlines in Γ is physically possible, i.e., Γ L ⊆ Γ . That is, Γ L is a set of physically possible worldlines along which worlds/systems with m particles can evolve according to the Lagrangian L . (See C.)

The product Γ L × Σ is the set of all physical possibilities. In conjunction with two accessibility relations R Γ and R Σ the set of physical possibilities forms a frame structure K = ( Γ L × Σ ) . The accessibility relations R Γ and R Σ of the resulting frame structure are axiomatized as: (2) R Γ ⊆ { ⟨ ⟨ γ 1 , σ ⟩ , ⟨ γ 2 , σ ⟩ ⟩ ∣ ⟨ γ 1 , σ ⟩ , ⟨ γ 2 , σ ⟩ ∈ K } and R Γ is reflexive, symmetric, and transitive; R Σ ⊆ { ⟨ ⟨ γ , σ 1 ⟩ , ⟨ γ , σ 2 ⟩ ⟩ ∣ ⟨ γ , σ 1 ⟩ , ⟨ γ , σ 2 ⟩ ∈ K } and R Σ is reflexive, symmetric, and transitive. That is, both, ( Γ L , R Γ ) and ( Σ , R Σ ) are structures with an equivalence relation. In addition the two accessibility relations are compositionally related as indicated in (Fig. 1 (right)). For a justification of those choices see the original presentation of Bittner (2018).

OPEN IN VIEWER

Fig. 1.

T -slicings σ ′ and σ of a spacetime with worldlines γ 1 − γ 4 (left); two accessibility relations in distinct frames and two accessibility relations in a two dimensional product frame (right) (adapted from the work of Gabbay (2003, p. 125)).

The domain of entities. On the enforced interpretation D E is the domain of possible entities (particulars and universals) in a world with m atoms. While the number and kinds of atomic particles that exist are fixed, whether and which complex continuants are formed by the given atomic entities is a contingent matter. Whatever complex entities can exist, however, must obey the laws of mereology in a way that is consistent with the mereology of the underlying spacetime. The domain D E of possible entities and the domain D ST of regions of spacetime are linked via the relation of instantiation InstST ⊆ D E × D E × D ST × K . More details will be discussed as the computational representation of the formal ontology is developed.

For illustrative purposes and to check the consistency of the formal theory it will be useful to use a simple and finite set-theoretic model to illustrate some important aspects of the class of KS -structures. Due to its simplistic nature this model falls short of capturing many of the topological, geometric and differential structures that govern the underlying physics. More sophisticated models could be built by implementing Def. 1 of appendix B.1 and basing it on manifold theory and the theory of differential forms (Arfken et al., 2005). An important advantage of using a tool with the expressive power of Isabelle/HOL is that, at least in principle, it is possible to formalize models of this kind.

OPEN IN VIEWER

Fig. 2.

A simple toy model of spacetime in conjunction with examples for physically possible worldlines and timeslices. Color coding: (b) σ 0 0 ( T ) is blue, σ 1 0 ( T ) is magenta and σ 2 0 ( T ) is red; (c) σ 0 1 ( T ) is blue, σ 1 1 ( T ) is magenta, σ 2 1 ( T ) is red, σ 2 1 ( T ) is black; worldlines in (d) and/or (e) γ 0 is blue, γ 1 is brown, γ 2 is green, γ 4 is orange, γ 5 is purple, γ 6 is red, γ 7 is black.

The toy model has a two-dimensional ‘spacetime’. This spacetime is discrete and has six distinct spatio-temporal locations as indicated in Fig. 2(a), i.e., ST = { c 00 , c 10 , c 01 , c 11 , c 02 , c 12 } as indicated by the labeling in the figure. In this spacetime the domain of spacetime regions is the set of non-empty subsets of ST , i.e., D ST = { r ⊆ ST ∣ r ≠ ∅ } . As discussed above (Fig. 1), slicings of spacetime are mappings σ i from an abstract timeslice T of dimension n − 1 into an n dimensional spacetime ST . In this toy model the abstract time slice is T = ( { x 0 , x 1 } , g ) . The geometry g of T is mostly ignored here. In the model there are two slicings of spacetime Σ = { σ 0 , σ 1 } . The slicing σ 0 is σ 0 0 ( x i ) = c i 0 , σ 1 0 ( x i ) = c i 1 ,  σ 2 0 ( x i ) = c i 2 for i ∈ { 0 , 1 } (Fig. 2(b)) and the slicing σ 1 is σ 0 1 ( x i ) = c 10 , σ 1 1 ( x 0 ) = c 00 , σ 1 1 ( x 1 ) = c 11 , σ 2 1 ( x 0 ) = c 01 , σ 2 1 ( x 1 ) = c 12 , σ 3 1 ( x i ) = c 02 for i ∈ { 0 , 1 } (Fig. 2(c)). (Clearly, unlike σ 0 , σ 1 is not an isomorphism that preserves the geometry g. This is an artifact of the finite nature of ST in this model.)

The worldlines that are kinematically possible with respect to the slicing σ 0 are visualized in Fig. 2(d). The worldlines that are kinematically possible with respect to the slicings σ 0 and σ 1 are visualized in Fig. 2(e) and listed in Eq. (3). There are fewer worldlines in Fig. 2(e) because a worldline cannot have more than one ‘point’ of intersection with a time slice. This is because instantaneous changes are physically impossible.

The parameter of the γ i is understood to correspond to the (coordinate) time (Def. 2 of B.1) according to the slicing σ 0 of ST , i.e., τ ∈ 0 … 2 . (The aim here is to approximate worldlines that are possible in a spacetime that is consistent with the Special Theory of Relativity – See also B.2.) (3) γ 0 ( τ ) = c 0 τ , γ 5 ( 0 ) = c 10 , γ 5 ( 1 ) = c 11 , γ 5 ( 2 ) = c 02 , γ 1 ( τ ) = c 1 τ , γ 7 ( 0 ) = c 10 , γ 7 ( 1 ) = c 01 , γ 7 ( 2 ) = c 02 . If one demands, in accordance with classical mechanics, that distinct particles cannot occupy the same location in spacetime then worldlines of distinct particles cannot intersect. In this example it is assumed that there exist two atomic particles that occupy locations along the kinematically possible worldlines in this spacetime. The worldlines γ 0 and γ 1 are the only kinematically possible particle worldlines that do not intersect. The only kinematically possible complex worldline in this example is γ 0 2 = ⋃ { γ 0 , γ 1 } . (The underlying physical environment that is encoded in the Lagrangian field L would be such that neither of the two atomic particles can change its spatial location.) On these assumptions, K = Γ L × Σ , the set of physical possibilities, is K = { γ 0 2 } × { σ 0 , σ 1 } .

In what follows the two atomic particles are called At 0 and At 1 . Respectively At 0 and At 1 evolve along the worldlines γ 0 and γ 1 . In addition it is assumed that there exists a complex object Compl 0 that is constituted by the atoms At 0 and At 1 . The worldline of Compl 0 is γ 0 2 . Within the realm of physical possibilities in K an ontology that commits to the existence of continuant particulars, occurrent particulars as well as to universals which are instantiated by such particular entities (e.g., BFO (Smith, 2016), DOLCE (Gangemi et al., 2003), etc.) then is committed to acknowledging the existence of at least the following entities: the continuants At 0 , At 1 , and Compl 0 ; the occurrents Occ 0 , Occ 1 , and Occ 2 (the respective lives of the above continuants); and at least two universals ( UC 0 and UO 0 ) which are respectively instantiated by the continuants and occurrents. On the given assumptions the set of physically possible entities is: D E = { At 0 , At 1 , Compl 0 , Occ 0 , Occ 1 , Occ 2 , UC 0 , UO 0 } .

This example is constructed to minimize the number of physical possibilities without being trivial. This simplicity of the example model greatly reduces the complexity of the (mostly brute force and case-based) proofs that establish that the axioms of the formal ontology are satisfied in this toy model. In general, within the framework of highly expressive languages, the more skilled the developer of the computational realization of an ontology, the more realistic and sophisticated the models that are realized can be. In the conclusions of this paper I will argue for the need of skilled proof engineers.

In this section the syntax and the semantics of the formal language that is used to express the ontology of Bittner (2018) is introduced. This language includes three disjoint sets of variable symbols: Var ST , VAR ST , and Var E . Var ST contains variables denoted by letters u, v, w, possibly with subscripts ( u 1 , v 2 , etc.). VAR ST contains variables denoted by capital letters A, B, etc. Var E contains variables x, y, z, possibly with subscripts. Var is the union Var ST ∪ VAR ST ∪ Var E . The sets D ST , P ( D ST ) and D E of Section 2.1 are respectively the domains for the variables in Var ST , VAR ST , and Var E .

Pred is a set of predicate symbols. If F is an n-ary predicate symbol in Pred and t 1 , … , t n are variables in Var then F t 1 … t n is a well-formed formula. Complex, non-modal formulas are formed inductively in the usual ways, i.e., if α and β are well-formed formulas, then so are ¬ α , α ∧ β , α ∨ β , α → β , ( x ) α , ( ∃ x ) α (Gabbay, 2003; Hughes and Cresswell, 2004). All quantification is restricted to a single sort of variables. If not marked explicitly, restrictions on quantification are understood by conventions on variable usage. Finally, the modalities □ Γ , □ Σ , ♢ Γ and ♢ Σ are included in the formal language, i.e., if α is a well-formed formula, then so are □ i α and ♢ i α with i ∈ { Γ , Σ } .

A model of such a multi-dimensional sorted modal language is a structure ⟨ D ST , D E , K , V ⟩ . D ST and D E are as described above and form the non-empty domains of quantification. K is a non-empty set of possible worlds, which, as discussed above, has the internal structure of a product of two sets Γ L and Σ. K gives rise to the product frame of the two-dimensional modal logic (Gabbay, 2003) presented here. V is the interpretation function: if F ∈ Pred is an n-ary predicate then V ( F ) is a set of n + 1 -tuples of the form ( d 1 , … , d n , κ ) with d 1 , … , d n ∈ D and κ ∈ K , where D = P ( D ST ) ∪ D ST ∪ D E . In all possible worlds κ ∈ K the variables respectively range over all the members of D ST , P ( D ST ) and D E . A variable assignment μ is a function such that (i) for every variable u ∈ Var ST , μ ( u ) ∈ D ST , (ii) for every variable x ∈ Var E , μ ( x ) ∈ D E , and (iii) for every variable A ∈ VAR ST , μ ( A ) ∈ P ( D ST ) .

Every well-formed formula has a truth value which is defined as follows:

A well-formed formula α is true in ⟨ D ST , D E , K , V ⟩ , i.e. V μ ( α ) = 1 , if and only if V μ ( α , κ ) = 1 for all κ ∈ K and all assignments μ. Formula α is valid if α is true in all models. To simplify the presentation, the explicit distinction between V and V μ will be omitted. Variables in the object language are written in italics and for corresponding domain members the Sans Serif font is used.

The formal theory includes the rules and axioms of a first order modal predicate logic with identity (Hughes and Cresswell, 2004) as well as the S5-axiom schemata K □ i , T □ i , and 5 □ i for i ∈ { Γ , Σ } . ♢ i is defined in the usual way as the dual of □ i for i ∈ { Γ , Σ } ( D ♢ i ). The Barcan formula and its converse are true in all models ( B C □ i ).

Both modal operators are independent and the order of their application is immaterial ( M S □ ). All axioms of the formal theory below are true in all possible worlds have an implicit leading □ operator. In addition, leading universal quantifiers are omitted. Axioms B C □ i and M S □ ensure that the order of leading universal quantifiers and leading □ operators is immaterial.

Consider Fig. 3. The depicted Isabelle/HOL/Isar code illustrates the declaration of the computational representation of a product frame K = ( Γ L × Σ ) of the form described in Fig. 1 (right) and Eq. (2). In lines 1–5 a record type (’a RS_frame) is declared which instances are ordered quadtuples of the form (r_carrier, aR, s_carrier, aS). In this declaration r_carrier stands for a variable of the type “set of sets with members of type (’a)”, declared by the expression r _ carrier : : (’a set) set . Respectively, aR stands for a variable of the type “function of type ( ( ’a set ) × ( ’a set ) → bool ) ” – the computational representation of a binary relation with arguments of type (’a set). The types of s_carrier and aS are declared in analogy to the types of r_carrier and aR. The expression (infixl “R ₁ ” 50) declares that the binary relation aR is abbreviated as R and the arguments are written in infix notation. The number 50 specifies the strength of the binding to minimize the number of parenthesises that are needed and thereby to facilitate readability. The subscript ₁ specifies that the relation R has an argument which is the record structure itself. This argument is written as a subscript can be omitted in many situations. (This is somewhat similar to the this or self pointers in languages such as C + + or Python.) Similarly to aR and R ₁ , aS has the infix notation S ₁ .

Locales in Isabelle/HOL/Isar provide an infrastructure that supports the assignment of sets of axioms to types of structures. (This is similar to axiomatic type classes in HASKELL (Jones, 1993; Wenzel, 2005).) Consider the lines 6–19 of Fig. 3. Line 6 starts the declaration of the locale S5_RS_frame. In line 7 the name L is assigned to an arbitrary but fixed quadtuple of type (’a RS_frame). As part of the record and locale declaration the Isabelle/HOL/Isar system defines a number of functions. For example, the system introduces declarations which ensure that the expression (r_carrier L) is interpreted as a function call which returns the content of the first slot of the quadtuple L – a set of type (’a set) set. Similarly, the expression R L is a function call that returns the content of the second slot of L – a binary relation on a set of type (’a set) set. Finally, (s_carrier L) and S L respectively provide access to the third and fourth slot of L.

The record structure L is a computational representation of a KS -structure with a product frame K = ( Γ L × Σ ) . The set (r_carrier L) represents the set Γ L and R L represents the accessibility relation R Γ on Γ L ; similarly, the set (s_carrier L) represents the set Σ and S L represents the accessibility relation R Σ on Σ. As discussed in Section 2.1 the product frames K are S5 frames. That is, Γ L and Σ – represented respectively by (r_carrier L) and (s_carrier L) – are required to be non-empty and the accessibility relations R Γ and R Σ  – represented respectively by R L and S L  – are subject to the constraints of reflexivity, symmetry, and transitivity. These constraints are expressed as axioms of the locale S5_RS_frame in lines 9–19.

While in the somewhat declarative style of the semi-formal presentation worlds/possibilities are presented as sets of tuples of the form Γ L × Σ , in the more operational computational representation record types are used to store tuples of sets of the form ( Γ L , Σ ) . The set theoretic product is generated from ( Γ L , Σ ) when formulas are evaluated in specific wolds ( γ , σ ) ∈ Γ L × Σ . In line 20 of Fig. 3 the datatype (’a RS) is declared to hold ordered pairs of the form ( γ , σ ) ∈ Γ L × Σ . The functions r_RS and s_RS of lines 21 and 22 provide access respectively to the first and second components of ordered pairs of type (’a RS).

3.2. The propositional segment of the modal language

Figure 4 displays parts of the formal declaration of the propositional section of the modal language of Section 2.3 and Eq. (4). The code is adopted with modifications from Benzmüller (2015) and Benzmüller and Woltzenlogel Paleo (2015). Unlike Benzmüller et al. who use type declarations for worlds and domains of quantification here record structures and locales are used. This choice allows for more flexibility in the specification of the semantics of the formal language and the models of the axiomatic theory.

OPEN IN VIEWER

Fig. 4.

The interpretation of modal propositional formulas in ’a RS_frame product frames. (Adopted from the work by Benzmüller (2015) and Benzmüller and Woltzenlogel Paleo (2015)) (see S5_2D_base.thy).

In the first line of this code fragment propositional formulas are declared as functions of type (’a, ’b) RS_predicate. Functions of this type are mappings that take a product frame (represented by a variable of type (’a RS_frame) and a particular world (represented by a variable of type (’a RS)) to a boolean truth value.1

Modal operators are declared for both components of the product frames K of the KS -structure represented by the record structure L. The modal operators □ R and ◇ R are evaluated in the standard ways with respect to the worlds in (r_carrier L) and the associated accessibility relation R _L . Similarly, the modal operators □ S and ◇ S are evaluated in the standard ways with respect to the worlds in (s_carrier L) and the accessibility relation S _L (lines 8–15 of Fig. 4). Consider lines 8 and 9. It may be good practice to not only to rely on the type checking in the call of the modal operator, but to explicitly constrain the worlds in the call of the modal operator to the members of the respective carrier sets as indicated in the lines 8 ′ and 9 ′ below:

Similarly for the other modal operators of lines 8–15 of Fig. 4.

As pointed out in Section 2.1, there are two domains of interpretations in KS -structures: D ST the domain of regions of spacetime and D E the domain of physically possible entities. In the context of KS -structures the domain of regions is special in the sense that the worldlines and the slicings of spacetime that constitute the carrier sets of the frame structures are regions of spacetime, i.e., members of D ST . This is encoded in the computational representation as depicted in Fig. 5.

The record type ’a RS_frame for KS -structures is extended by two additional slots: one slot for the set carrier of type (’a set) and a second slot for the set e_carrier of type (’b set) (lines 2–3 of Fig. 5). The type variable ’a of the ’a RS_frame structures of Fig. 3 is a place holder for the sort of regions while the type variable ’b is a place holder for the sort of entities. The resulting record type is denoted (’a, ’b) two_sort_RS_frame.

The locale two_sort_S5_RS_frame is declared to inherit all axioms of the locale S5_RS_frame. In addition four axioms are included. Two axioms ensure that both (carrier L) and (e_carrier L) are non-empty. Two additional axioms require that the sets (r_carrier L) and (s_carrier L) are both subsets of (carrier L). The axioms labeled respectively: carrier, carrierE, Rcarrier1 and Scarrier1 (lines 5–10 of Fig. 5). Axioms Rcarrier1 and Scarrier1 illustrate the simplicity of postulating constraints among subsets of a given type. This is an important advantage of using locales and records over the built-in infrastructure for type declarations in Isabelle/HOL as it is used by Benzmüller et al.

OPEN IN VIEWER

Fig. 5.

Domains of quantification. (See S5_2D_base.thy).

Consider Fig. 6 which displays the declarations of the quantifiers of the modal language of Eq. (4). Again, the code is adopted with modifications from the work by Benzmüller (2015) and Benzmüller and Woltzenlogel Paleo (2015). In the figure the declaration of quantifiers that range over members and subsets of the set carrier are listed explicitly. The declaration of quantifiers that range over members and subsets of the set e_carrier are similar and are omitted here except for the declarations in lines 29–31.

In the first line of the code fragment open formulas in which free variables can range over the types ’a, ’a set, ’b, and ’b set are declared as functions of type (’a, ’b, ’c) two_sort_RS_predicate. Functions of this type implement mappings that take a product frame with two domains of quantification (represented by a variable of type (’a, ’b) two_sort_RS_frame and a particular world (represented by a variable of type (’a RS)) to a boolean truth value. The type system of Isabelle/HOL is able to infer that record variables of type (’a, ’b) RS_predicate can be obtained from record variables of type (’a, ’b, ’c) two_sort_RS_predicate by disregarding the two slots that are added in the declaration of (’a, ’b, ’c) two_sort_RS_predicate. The type system thereby ensures that the declarations of negation, conjunction, disjunction, implication and logical equivalence of Fig. 4 extend to formulas of type (’a, ’b, ’c) two_sort_RS_predicate.

Universal and existential quantifiers for variables of type ’a and ’b are declared as depicted in lines 3–14 of Fig. 6. The declaration of every quantifier has two components. One component is semantic and the other is syntactic in nature. The syntactic component of the declaration of a quantifier provides means for Isabelle/HOL to express the binding of a variable within the scope of a quantifier as a typing problem using λ-expressions (e.g., lines 6–8). (For details see the work by Wenzel (2017).) At the semantic level (universal) quantification is restricted not only to variables of a given type but to the members of sets that are part of the structures that provide the domain of interpretation. This allows for a natural correspondence between the semi-formal definition of the semantics in Eq. (4) and the formal treatment in the computational representation. For example in line 5 the universal quantifier ( ∀ a ) is restricted not only to variables of type ’a but to the members of the set (carrier L) (of type ’a set). The variable L is a place holder for a structure of type (’a, ’b) two_sort_RS_frame. When instantiated as intended, the set (carrier L) will have regions of spacetime as members. Similarly for the quantifiers ∃ a , ∀ b , ∃ b (lines 9–14), ∀ A , etc. in S5_2D_base.thy.

OPEN IN VIEWER

Fig. 6.

The interpretation of formulas of modal predicate logic in (’a RS_frame) product frames with type-restricted quantification (adopted from the work by Benzmüller (2015) and Benzmüller and Woltzenlogel Paleo (2015)). (See S5_2D_base.thy).

In Isabelle/HOL one can then define the notion of validity. A formula P of type (’a, ’b) two_sort_RS_predicate is valid in a structure L of type (’a, ’b) two_sort_RS_frame, signified as ⌊ P ⌋ L , if and only if P is true for all members of (r_carrier L and all members of (s_carrier L) (lines 1–3 of Fig. 7). On the enforced interpretation in KS -structures the members of (r_carrier L) represent dynamically possible worldlines in Γ L and the members of (s_carrier L) represent kinematically possible slicings Σ of spacetime. A common textbook notation that is equivalent to ⌊ P ⌋ L is ( ⊧ L P). Since L is arbitrary but fixed one also writes ( ⌊ P ⌋ and ⊧ P).

Within this framework Isabelle/HOL is able to prove the usual theorems about the logical interrelations between □ and ◇ (e.g., line 4 of Fig. 7), the validity of the S5 axioms (e.g., T in lines 6), as well as the Barcan formula (line 7). In addition one can prove that the order of the quantifiers □ R and □ S is immaterial (line 5). In contrast to the semi-formal presentation of the theory, in the computational representation all of these properties have to be proved for all types of variables and the associated typed quantifiers ∀ a , ∀ b , ∀ A , ∃ a , … as well as for all types of modal operators including □ R , □ S , □ , ◇ R , …  . For example, line 4 displays a lemma for ∀ a and □ R , while line 5 displays a lemma for ∀ b , □ R and □ S . All the properties of modal formulas with unary predicates immediately generalize to formulas with n-ary predicates as shown for the Barcan formula in line 7. The term (P x) in line 6 is of type (’a, ’b) two_sort_RS_predicate and so is the term (P x y) in line 7. Of course, the term P in line 6 is of type ’a => (’a, ’b) two_sort_RS_predicate while the term P in line 7 is of type ’a => ’a => (’a, ’b) two_sort_RS_predicate.

OPEN IN VIEWER

Fig. 7.

Validity of formulas of type (’a, ’b) two_sort_RS_predicate in structures of type (’a, ’b) two_sort_RS_frame. (Adopted from the work by Benzmüller (Benzmüller, 2015; Benzmüller and Woltzenlogel Paleo, 2015)) (see S5_2D_base.thy).

Theorems and lemmata in Isabelle/HOL/Isar are to be read as follows: the keywords lemma/theorem are synonymous; the statement enclosed by the quotation marks is the actual statement that is proved; in parenthesis in front of the statement is the locale in the context of which (type declarations, definitions, and axioms associated with the locale) the statement was proved; following the statement enclosed by the keywords using and by are names of axioms and theorems that are used in the proof; and finally following the keyword by the (built in) proof method (auto, fast, etc.) that was used in the proof is listed. If no axioms and definitions are listed in the using section of a lemma/theorem then the proof was found using axioms and theorems in Isabelle/HOL, simplification rules of the lambda calculus, and by expanding definitonal expressions labeled as abbreviations.

This concludes the setup of the formal language for the axiomatic theory. The computational realization is the formalized theory in S5_2D_base.thy. In what follows the ontology will be developed hierarchically. At each level of the theory hierarchy three formal components are introduced in a way that mirrors the methodology in this section: (1) at every level new axiomatic primitives are introduced by extending the record structures that represent the KS -structures; (2) axioms characterizing the new primitive are collected in corresponding locales; (3) at the level of the modal language of the formal ontology every formula is typed. The type of a formula is determined by the class of structures in which it is interpreted and correspondingly, the set of axioms that are associated with these structures. The hierarchical development of the ontology and the correspondence of the three components of the theory at every level are summarized in Table 2 on page 285.

The automatically generated presentation of the fully formalized and computationally verified formal ontology can be found at: http://www.buffalo.edu/ bittner3/Theories/OntologyCM/.

4.1. Mereology in a lattice-theoretic framework

On the algebraic view of mereology is natural to reuse the fully formalized computational realization of lattice theory in HOL/Algebra/Lattice.thy (Ballarin, 2017). In the highly expressive framework of HOL it is also natural to declare lattice structures in a way that mirrors the ways in which lattices are introduced in mathematics. Unlike lattices in HOL/Algebra/Lattice.thy, however, mereological structures lack a minimal element. For this reason a modified version of HOL/Algebra/Lattice.thy is used here.

4.1.1. The semi-formal presentation of mereology

To capture the mereological structure of spacetime regions in the semi-formal presentation of Bittner (2018) the primitive binary operation ⊔ : D ST × D ST → D ST is introduced in the (first-order) object language of the formal theory. On the intended interpretation in KS -structures ⊔ is the mereological union of regions u 1 and u 2 . More precisely, ⊔ is interpreted as an operation that yields the least upper bound ⨆ : P ( D ST ) → D ST of the set { u 1 , u 2 } with respect to the ordering imposed on D ST by ⊑ (Champollion and Krifka, 2015). The second primitive of the semi-formal presentation of the formal theory of Bittner (2018) is the ternary functional relation ⊓. On the intended interpretation in KS -structures ⊓ is the mereological intersection that holds between regions u 1 , u 2 and u 3 if and only if the greatest lower bound ⊓ : P ( D ST ) → ( D ST ∪ ∅ ) of the set { u 1 , u 2 } exists and u 3 = ⊓ { u 1 , u 2 } (Eq. (6)) (Champollion and Krifka, 2015).2

²

This presentation traces over the difficulties that arise in the context of a mereology of regions which are represented by manifolds rather than by topologically regular sets. See also A.1 and (Butterfield, 2007; Arnold, 1997).

(6) V ( ⊔ ) = ⊔ _ = df { ⟨ u 1 , u 2 , u 3 , κ ⟩ ∈ D ST × D ST × D ST × K ∣ u 3 = ⨆ { u 1 , u 2 } } V ( ⊓ ) = ⊓ ‾ = df { ⟨ u 1 , u 2 , u 3 , κ ⟩ ∈ D ST × D ST × D ST × K ∣ u 3 = ⊓ { u 1 , u 2 } } The binary predicate of parthood, P u v , is defined to hold if and only if the union of u and v is identical to v ( D P ). The predicate ST holds of a region which has all regions as parts ( D ST ). Proper parthood ( PP ), overlap (O), and summation are defined in the standard ways in D O and D Sum (Simons, 1987).

On the enforced interpretation in KS -structures (Eq. (1)) the parthood predicate P holds of the relation ⊑ on D ST ; the predicate ST holds of the maximal element ST of D ST ; the overlap predicate is true if two regions share a member of D ST ; and the Sum predicate holds of least upper bounds of some non-empty subsets of D ST as indicated in Eq. (7). (7) V ( P ) = { ⟨ u 1 , u 2 , κ ⟩ ∈ D ST × D ST × K ∣ u 1 ⊑ u 2 } V ( ST ) = { ⟨ ST , κ ⟩ ∈ D ST × K ∣ ST = ⨆ D ST } V ( O ) = { ⟨ u , v , κ ⟩ ∈ D ST × D ST × K ∣ ∃ w ∈ D ST : w ⊑ u ∧ w ⊑ v } V ( Sum ) ⊆ { ⟨ u , A , κ ⟩ ∈ D ST × P ( D ST ) × K ∣ A ≠ ∅ ∧ u = ⨆ A } Axioms are introduced requiring that ⊔ is idempotent, associative, commutative (A1–A3) and that there exists a spacetime region which has all regions as parts (A4). Furthermore an axiom of separation (Champollion and Krifka, 2015) is required to hold (A5). Introducing ⊓ as a relational primitive implicitly acknowledges that mereological intersections do not always exist. An axiom is introduced requiring that an intersection of two overlapping regions always exists (A6).

As specified in Eq. (6) the mereological unions and intersections are the same at all possible worlds. This explicates at the level of the interpretation of the formal theory that the mereological structure of spacetime is absolute in the sense that it is the same on all physical possibilities and slicings. In the object language this is mirrored in axioms A7 and A8.

4.1.2. Computational realization in Isabelle/HOL/Isar

The computational realization of the mereology of the previous section in Isabelle/HOL/Isar can be found in the file Plattice.thy (which is adopted from HOL/Algebra/Lattice.thy). Axiomatic primitives of the computational realization are introduced in two steps: (i) by extending record structures of type (’a, ’b) two_sort_RS_frame and (ii) by extending the locale two_sort_S5_RS_frame of Fig. 5. A record type R 2 is an extension of record type R 1 if R 2 includes all the ‘slots’ of R 1 and R 2 has at least one ‘slot’ that is not included in R 1 . Similarly, a locale L 2 extends the locale L 1 if L 2 includes all the axioms of L 1 and adds further axioms. This is summarized for all the primitives and axioms of the formalized ontology in Table 2 on page 285.

Following the standard lattice theory in HOL/Lattice.thy there is a single primitive predicate for partial orderings. The declarations that introduce this primitive in the computational realization are depicted in Fig. 8. First the record type (’a, ’b) porder_two_sort_RS_frame is declared that includes a slot for the function le :: “’a => ’a => bool” as depicted in line 2 of the figure. To emphasize that le is the computational representation of parthood relation in KS -structures the symbol ⊑ is used to refer to le in the declarations that follow. The locale S5_RS_2S_partial_order states the axioms of reflexivity, antisymmetry, and transitivity for ⊑ and mirrors the declarations of HOL/Algebra/Lattice.thy.

In contrast to the semi-formal presentation of the theory in Section 4.1.1, in the higher-order language of the computational representation the predicate ⊔ is defined rather than introduced as a primitive. The definition of ⊔ in line 7 of Fig. 9 expresses the usual lattice theoretic understanding of this operation in terms of least upper bounds. The necessary declarations are displayed in lines 1–6. These definitions explicitly formalize what is expressed semi-formally in the specification of the intended interpretation V ( ⊔ ) in Eq. (6). In writing the axioms A1–A3 for ⊔ as equations one implicitly assumes that binary mereological unions always exist. In the computational representation it is explicitly postulated that least upper bounds of arbitrary non-empty subsets (of (carrier L), i.e., D ST ) always exist (lines 9–10 of Fig. 9). In the mereological context this amounts to postulating the existence of mereological unions for arbitrary non-empty subsets of D ST .

OPEN IN VIEWER

Fig. 8.

Partial orderings. Adopted from the work by Ballarin (2017). (See Plattice.thy).

OPEN IN VIEWER

Fig. 9.

Formalized axioms for complete upper semi-lattices. Adopted from the work by Ballarin (2017) (see Plattice.thy).

While in the semi-formal presentation in Section 4.1.1 the predicate ⊓ is a primitive, the corresponding predicate is_meet of the HOL-based computational representation is introduced by definition. The definition of is_meet in lines 3 and 4 of Fig. 10 mirrors the usual lattice-theoretic definitions in terms of greatest lower bounds (see definition of greatest and Lower in Plattice.thy). As in the case of the operation ⊔ above these declarations explicitly formalize what is expressed semi-formally in the specification of the intended interpretation V ( ⊓ ) in Eq. (6). The absence of a minimal element in mereology means that not every set of domain members has a greatest lower bound. To single out pairs of domain members that (when jointly considered as a set of cardinality two) do have a greatest lower bound the relation of overlap is used in the usual ways as specified in the declaration of the locale partial_lower_semilattice in lines 7–8 of Fig. 10. This corresponds to A6 in the semi-formal presentation.

OPEN IN VIEWER

Fig. 10.

Formalized axioms for partial lower semi-lattice. Adopted from the work by Ballarin (2017). (See Plattice.thy).

The axioms that form a general extensional mereology (Simons, 1987) are collected in the locale S5_RS_2S_GEM (Fig. 11) which inherits all the axioms and definitions of the locales complete_upper_ semilattice and partial_lower_semilattice via the locale partial_lattice and adds two further axioms. The axiom noBot ensures that the set carrier L (i.e., D ST ) does not have a minimal element. This requirement is implicit in the semi-formal presentation. Corresponding to axiom A5 the remainder principle RP is included.

OPEN IN VIEWER

Fig. 11.

Formalized axioms for the mereology of spacetime. (See Plattice.thy).

Isabelle/HOL provides computational tools for generating models for sets of formulas (e.g., nitpick (Blanchette, 2017)). For the development of an axiomatic theory this is helpful to avoid inconsistent sets of axioms, i.e., sets of axioms that do not have models at all. From the point of formal ontology development this is not sufficient. The whole point of developing a formal ontology is it to create axiomatic systems that constrain sets of models to a subset of intended models. Unfortunately, this is rather difficult and without formal languages with significant expressive power often impossible.

However, there is a ‘space’ of intermediate possibilities between the two extrema merely of demonstrating the consistency of an axiomatic theory on one hand and demonstrating that the theory exactly constrains a certain class of models on the other hand. This intermediate ‘space’ is of interest from the perspective of developing formal ontologies. Often, when developing a formal ontology one has a set of prototypical examples in mind that guide the development of the formal theory. For example, in the specification document of Basic Formal Ontology (Smith, 2016) the authors provide prototypical examples as parts of the Elucidations that complement the semi-formal definitions and axioms. When considered as formal models these examples must satisfy all the axioms of the corresponding formal ontology. In the context of the formal ontology considered in this paper the example of Section 2.2 plays this role.

In the remainder of this subsection first the formal specification of the example of Section 2.2 will be illustrated and then the proof that demonstrates that this model satisfies the mereological axioms is discussed.

4.2.1. The computational realization of the example model (mereology)

There is a difficulty when specifying a formal model for verifying the consistency of a set of axioms: the model itself cannot be specified means of axioms. This is because the axioms specifying the model may be inconsistent or they may fail to sufficiently specify that model and thus fail to serve the purpose of verifying the original set of axioms. As a solution to this problem Isabelle/HOL offers a definitional approach to the specification of formal models (Nipkow et al., 2002). Within this definitional approach one assumes that the axiomatization of HOL in Isabelle/HOL is consistent and can be extended by means of a restricted class of definitions and declarations in ways that cannot lead to inconsistencies. In the formal specification of the example model of Section 2.2 only the kinds of definitions and declarations are used that fall within the definitional approach.

OPEN IN VIEWER

Fig. 12.

Space and regions of spacetime, timeslices, and dynamically possible worldlines of the example model. (ST_model_base.thy).

Consider Fig. 12. Lines 1–10 depict the declarations that constitute the computational representation of the mereology associated with the spacetime consisting of six atomic regions as depicted in the left of Fig. 2. Lines 10–20 depict the declarations that represent the slicings of spacetime in the middle of Fig. 2. The accessibility relation among slicings of spacetime is declared in lines 21–22. Declarations of the dynamically possible worldlines in conjunction with the declaration of the associated accessibility relation are depicted in lines 23–28. In lines 29–32 a record structure ST_frame of type “(Reg, Reg) porder_two_sort_RS_frame” is declared which slots are ‘filled’ with the respective sets and relations of the example model as declared in the figure.

In addition one can verify intuitions about the enforced model by proving simple lemmata. Many examples can be found in the file ST_model_base.thy. Of course many of those lemmata are trivial in the context of the simple example model but they illustrate how easy it is to prove properties of the set-theoretic structures that serve as models of the axiomatic theory.

4.2.2. Using records and locales for linking axioms and models

The structure ST_frame is an enforced model of the computational realization of the spacetime mereology which axioms are collected in the locales S5_RS_2S_GEM, partial_lattice, complete_upper_ semi-lattice, partial_lower_semilattice, S5_RS_2S_partial_order, two_sort_S5_RS_frame, and S5_RS_frame. The top level of the formalized proof that shows that ST_frame (abbreviated in the proof as ?L) indeed has all the required properties is displayed in Fig. 13. When processing the declaration of the locale S5_RS_2S_GEM the underlying proof assistant generates a number of proof obligations in form of the rule S5_RS_2S_GEM.intro that, when fulfilled for a given structure (ST_frame in this case) constitute a proof that the structure at hand satisfies all the axioms that are associated with the respective locale (Lines 5–15 of Fig. 13). The layout of the proof in addition illustrates that the proof assistant also ensures that all the axioms of the parent locales are satisfied: line 3 shows that all the axioms associated with the locale partial_lattice are satisfied as a consequence of the theorem m_set_is_partial_lattice_M and the rules of inference that are available to theorem prover auto. The complete proof can be found in the file ST_model_proof_MereologyOnly.thy.

OPEN IN VIEWER

Fig. 13.

The record structure ST_frame satisfies the axioms of the locale S5_RS_2S_GEM. ∧ is an alternative way of expressing universal quantification. (See ST_model_proof_MereologyOnly.thy).

In order to present the formalized theory in the more concise and conceptually clearer form that is employed in the semi-formal presentation of Section 4.1.1, the rather complex and hard to read axioms, definitions, and theorems from the level of axiomatization are lifted to the modal language of Section 3. In the modal language all explicit references to semantic features such as the record structures that provide the enforced interpretation are hidden. This information, although transparent to the user, remains available to the system (and can be used in the proofs). Explicit typing of formulas (discussed below) in conjunction with formal features such as currying and the rules of α-, β-, and γ- reduction of the underlying lambda calculus (part of the rules of inference in HOL) allow the system to route implicit arguments through the proofs in a way that is transparent to the user (for details see the work by Benzmüller (2015) and Benzmüller and Woltzenlogel Paleo (2015)). An illustration of how the modal formula “ ⌊ □ ( ∀ a x . P _ M x x ) ⌋ stated in the context of the locale S5_RS_2S_GEM is ‘understood’ by the system, is displayed in Fig. 14.

OPEN IN VIEWER

Fig. 14.

Lines 2–6 illustrate how Isabelle/HOL expands the theorem stated in line 1.

As an illustration of the typing of formulas consider lines 1 and 2 of Fig. 15. Every atomic formula in the lifted mereology is a function of type (’a, ’b, ’c) M_porder_predicate which has two arguments: (1) a record structure of type (’a, ’b, ’c) porder_two_sort_RS_frame which holds the domain of interpretation including the domains of the variables, the interpretation of the axiomatic primitives, possible worlds, was well as accessibility relations; and (2) the current world of type (’a RS). Like every closed atomic formula in a two-valued logic expressions of type (’a, ’b, ’c) M_porder_predicate are functions that evaluate to the boolean values of true or false.

OPEN IN VIEWER

Fig. 15.

The excerpts from the lifted mereology of PLattice_lifted_theory.thy.

For example, the predicate P_M is a function of type ’a => ’a => (’a, ’b, ’c) M_porder_ predicate (line 3 of Fig. 15). Therefore, the expression (P_M x y) is a function that, when presented with an argument of type (’a, ’b, ’c) porder_two_sort_RS_frame and an argument of type (’a RS) yields a boolean truth value, the computation of which is specified in line 4–5. The body of the definition of every predicate links this predicate to its enforced interpretation. In line 4 the predicate P_M is linked to the predicate ⊑ L . While the typing system ensures that all arguments are of the correct type, every definition ensures that every argument is a member of the correct carrier set: in lines 4–5 it is verified that x,y ∈ carrier L. Complex expressions such as ∀ a x. P_M x x, □ ( ∀ a x . P _ M x x ) are functions of type (’a, ’b, ’c) M_porder_predicate => (’a, ’b, ’c) M_porder_predicate and are evaluated as specified in the computational realization of the formal language in Section 3. Similarly for the predicate J_M (lines 6–8 of Fig. 15) and all the other predicates in the semi-formal presentation of the theory.

Using the definitions of the predicates of the modal language one can prove: (i) all the axioms stated in the semi-formal presentation are theorems in the formalized modal presentation. Those theorems state that the respective formulas are valid the class of underlying structures in the sense defined in lines 1–3 of Fig. 7. For example, the lemmata in lines 11 and 12 of Fig. 15 are formalized versions of axioms A1 and A7 of Section 4.1.1. (ii) One can prove formalized versions of the theorems listed in the semi-formal development of the formal theory. For example, the lemmata inlines 15 and 16 of the figure are formalized versions of theorems T1 and T3 of Bittner (2018). (iii) Finally, one has to prove that all the definitions in the semi-formal presentation are provable as logical equivalences in the formalized theory. Lines 13 and 14 of Fig. 15 prove definition D P as a logical equivalence.

As specified in the definition of J_M, mereological unions are the same at all possible worlds. This is reflected by the theorem in line 12 of Fig. 15. Similar patterns hold for all purely mereological predicates in PLattice_lifted_theory.thy.

5.1. Semi-formal presentation

In the semi-formal presentation of the theory by Bittner (2018) a third primitive is added to the axiomatic theory: the unary predicate TS . On the enforced interpretation in KS -structures (Eq. (1)), TS holds of time slices σ t ( T ) induced by the T -slicing σ: (8) V ( T S ) = TS = df { ⟨ u , ⟨ γ , σ ⟩ ⟩ ∈ D ST × K ∣ ∃ t ∈ ℜ : u = σ t ( T ) } In terms of the primitive time slice predicate spatial and soatio-temporal regions are defined: Spatial regions are regions that are parts of some time slice ( D SR ). Spatio-temporal regions are regions that overlap two distinct time slices ( D STR ). Two regions are simultaneous if and only if they are parts of the same time-slice ( D SIMU ). D SR SR u ≡ ( ∃ t ) ( TS t ∧ P u t ) D STR STR u ≡ ( ∃ t 1 ) ( ∃ t 2 ) ( TS t 1 ∧ TS t 2 ∧ O u t 1 ∧ O u t 2 ∧ ¬ O t 1 t 2 ) D SIMU SIMU u v ≡ ( ∃ w ) ( TS w ∧ P u w ∧ P v w ) On the intended interpretation SR u means: Spatial regions u are parts of spacetime which, on a given T -slicing σ are sub-regions of some time slice induced by σ. On the slicing σ the region u is not extended at all in time. By contrast, on a given slicing, spatio-temporal regions extend across time slices. This interpretation reflects at the level of the formal models that which regions of ST count as spatial regions depends on the underlying slicing σ. (9) V ( SR ) = { ⟨ u , ⟨ γ , σ ⟩ ⟩ ∈ D ST × K ∣ ∃ i ∈ ℜ : u ⊑ σ i ( T ) } V ( STR ) = { ⟨ u , ⟨ γ , σ ⟩ ⟩ ∈ D ST × K ∣ u ⊑ γ ∧ ∃ i , j ∈ ℜ : V ( STR ) = i ≠ j ∧ u ∩ σ i ( T ) ≠ ∅ ∧ u ∩ σ j ( T ) ≠ ∅ } V ( SIMU ) = { ⟨ u , v , ⟨ γ , σ ⟩ ⟩ ∈ D ST × D ST × K ∣ ∃ t ∈ ℜ : u ⊑ σ t ( T ) ∧ v ⊑ σ t ( T ) } The following mereological axioms for TS are added: distinct time slices do not overlap (A9); there are at least two non-overlapping time slices (A10); every region overlaps some time-slice (A11). If ST has the global or local structure of a Minkowski spacetime then there are many slicings, i.e., # Σ > 1 . In such spacetimes the axiom A M holds requiring that simultaneity is not absolute.

In Minkowski spacetimes some regions of spacetime are spatial regions on some slicings but not on others. Similarly for some spatio-temporal regions.

5.2. Computational realization

In analogy to the introduction of the primitive partial ordering predicate ⊑ in the lattice theoretic formalization of mereology in Section 4, the primitive timeslice predicate of the timeslice mereology is introduced in the computational realization (i) by introducing record structures of type (’a, ’b) TS_porder_two_sort_RS_frame as extensions of records of type (’a, ’b) porder_two_sort_RS_frame and (ii) by introducing the locale TS_mereology as an extension of the locale S5_RS_2S_GEM (see TS_mereology.thy).

OPEN IN VIEWER

Fig. 16.

Locale for time slice mereology (TS_mereology.thy).

The first axiom of the locale TS_mereology (lines 5–6 of Fig. 16) mirrors the constrains of the enforced interpretation of the predicate TS in Eq. (8). The representation of timeslices in the computational realization (lines 5–6 of Fig. 16 and elsewhere) is somewhat simplified compared to the semi-formal presentation. In the latter slicings of spacetime are mappings of the form σ : ℜ × T → ℜ × M (Fig. 1, Def. 1 of B.1). By contrast, in the computational representation slicings of spacetime are included explicitly as sets of the form (s_carrier L). In the semi-formal presentation the set (s_carrier L) could be written as { { u ∈ M ∣ ∃ t ∈ ℜ : ( t , u ) = σ t ( T ) } ∣ σ ∈ Σ } . Representing slicings as mappings is important when certain structure-preserving aspects of the mappings are used to distinguish different kinds of spacetime geometries (Section B.1, Section B.2) and the work by Bittner (2018). The focus in this paper is only on a single spacetime geometry (a simplified version of Minkowski spacetime). For this reason the mapping structure can be neglected.

The remaining axioms of the locale are respectively semantic expressions of axioms A9–A11 of the semi-formal theory. As an example of the computational representation of the axioms in TS_mereology.thy the computational representation of axiom A9 is depicted in lines 8–9 of Fig. 16. The definitions of the predicates for spatial and spatio-temporal regions as well as the predicate of simultaneity mirror the respective specifications of the intended interpretation in the semi-formal presentation of the theory. In particular, lines 10–12 correspond to the first definition in Eq. (9). The original definitions of SR , STR , and SIMU in the object language of the semi-formal presentation will be recovered as theorems in the version of the formalized theory that is lifted to the modal level of theory presentation (Section 5.4).

In the context of the locale TS_mereology one can prove that on every slicing of spacetime the least upper bound of the set of all timeslices on that slicing is identical to spacetime itself (lines 13–15 of Fig. 16. Lines 13–14 contain the statement of the theorem and line 15 states that in the proof the (previously proved) lemmata Set_of_TS_imp_ST and ST_impl_Set_of_TS as well as the built-in proof method blast are used.

The locale TS_mereology is extended in TS_mereology.thy by the locale M_TS_mereology. The latter extends the former by adding an axiom that stipulates that simultaneity is relative (lines 16–20 of Fig. 16). In the context of the locale M_TS_mereology the axiom A M of the semi-formal presentation will become provable at the modal level of the computational realization (Section 5.4).

The verification of the consistency of the axioms collected in the locales TS_mereology and M_TS_mereology and the verification their satisfaction in the example model is achieved in two steps: (1) extend the computational realization of the example model to include a structure that can serve as the interpretation for the primitive timeslice predicate; (2) verify that this model satisfies the axioms collected in the locales TS_mereology and M_TS_mereology.

Firstly, the computational realization of the example of Section 2.2 is extended by declaring a unary predicate isTS_M that holds of the time slices of a given slicing of spacetime (lines 1–2 of Fig. 17). To link the model to the axioms that are collected in the relevant locales a record with the name ST_frame_M is declared (lines 3–5).

The proof in which it is demonstrated that the structure ST_frame_M satisfies all the axioms collected in the locales TS_mereology and M_TS_mereology is realized by an exhaustive analysis of all possible cases. The resulting proof is rather lengthy and tedious and its computational realization is the theorem m_set_is_Inst_TS_mereology in ST_model_proof.thy. It is important to acknowledge at this point that despite the tedious nature of the proof it would be rather difficult to execute a proof of this form without the computer keeping track of all the cases that must be verified.

OPEN IN VIEWER

Fig. 17.

Time slices and spatial regions (ST_model_base.thy).

Creating a modal presentation of the non-modal timeslice mereology included in the locale M_TS_Mereology and the associated record structures of type (’a, ’b) TS_porder_two_sort_RS_ frame is similar to creating a modal presentation of the mereology in Section 4.3.

Every closed modal formula in the lifted timeslice mereology is of type (’a, ’b, ’c) TS_ mereology_predicate which has two implicit arguments: (1) a record structure of type (’a, ’b, ’c) TS_porder_ two_sort_RS_frame which, as above, holds the domains of the variables, the interpretation of the axiomatic primitives, etc. and (2) the current world of type (’a RS) (lines 1–2 of Fig. 18). The timeslice predicate TS_M of the modal language then is defined in terms of the timeslice primitive TS _L as depicted in lines 3–5 of the figure. Modal versions of predicates holding of spatial regions, spatio-temporal regions, and pairs of simultaneous regions are defined analogously in terms of their non-modal counterparts (see S5_2D_lifted_theory.thy).

In the context of the locale TS_mereology one can then formally prove the all the definitions, axioms, and theorems that are stated in the semi-formal presentation of Section 5.1 as theorems (lines 6–11 of Fig. 18 and S5_2D_lifted_theory.thy). In the context of the locale M_TS_mereology axiom A M is provable (lines 12–13 where Id_a_M is a modal wrapper of the identity relation).

OPEN IN VIEWER

Fig. 18.

Excerpts from the lifted timeslice mereology (from S5_2D_lifted_theory.thy).

6.1. Semi-formal presentation

A primitive ternary relation Inst between two entities and a region is introduced in the object language of the formal theory. Inst x y u is interpreted as y is instantiated by x at region u (or, equivalently, x instantiates y at region u or x is an instance of y at region u). On the intended interpretation: V ( Inst ) = df InstST ⊆ D E × D E × D ST × K where the set InstST is part of the underlying KS structure (Eq. (1)). The following axioms (some are adopted from the work by Bittner and Donnelly (2006)) are included in the formal theory to constrain InstST : if x instantiates y at u then it is not physically possible that some z is an instance of x at some region v (A12); every entity instantiates or is instantiated on some physical possibility (A13); every entity is instantiated or instantiates at spatial regions or at spatio-temporal regions (A14); if x instantiates at a spatial region then on all slicings: x instantiates at spatial regions (A15); if x is instantiated at a spatio-temporal region then on all slicings: x is instantiated at spatio-temporal regions (A16); if x instantiates y at a spatio-temporal region u then x is uniquely located (A17); if x instantiates at two simultaneous spatial regions u and v then u and v are identical (A18). A 12 Inst x y u → ¬ ♢ ( ∃ z ) ( ∃ v ) ( Inst z x v ) A 13 ♢ ( ∃ y ) ( ∃ u ) ( Inst x y u ∨ Inst y x u ) A 14 Inst x y u → ( SR u ∨ STR u ) A 15 Inst x y u ∧ SR u → □ Σ ( z ) ( v ) ( Inst x z v → SR v ) A 16 Inst y x u ∧ STR u → □ Σ ( z ) ( v ) ( Inst z x v → STR v ) A 17 Inst x y u ∧ Inst x z v ∧ STR u ∧ STR v → u = v A 18 Inst x y u ∧ Inst x z v ∧ SR u ∧ SR v ∧ SIMU u v → u = v

In terms of the instantiation primitive one can define: Entity x is located at region u if and only if there exists an entity y such that x instantiates y at u or x is instantiated by y at u ( D L ); Entity x exists at timeslice t iff there is a region at which x is located and that overlaps t ( D E ). An entity is persistent iff it is not confined to a single time-slice ( D Pe ). Entity x is a particular if and only if x is a persistent entity that instantiates at some region ( D Part ). Entity x is a universal if and only if x is a persistent entity that is instantiated at some region ( D Uni ). Persistent entities are distinguished into continuants and occurrents. Entity x is a continuant iff x is persistent and x is located at some spatial region ( D Cont ). By contrast, x is a occurrent iff x is located at some spatio-temporal region ( D Occ ). D L L x u ≡ ( ∃ y ) ( Inst x y u ∨ Inst y x u ) D E E x t ≡ TS t ∧ ( ∃ u ) ( L x u ∧ O u t ) D Pe Pe x ≡ ( ∃ u ) ( ∃ v ) ( L x u ∧ L x v ∧ ¬ SIMU u v ) D Part Part x ≡ Pe x ∧ ( ∃ y ) ( ∃ u ) ( Inst x y u ) D Uni Uni x ≡ Pe x ∧ ( ∃ y ) ( ∃ u ) ( Inst y x u ) D Cont Cont x ≡ Pe x ∧ ( ∃ u ) ( L x u ∧ SR u ) D Occ Occ x ≡ ( ∃ u ) ( L x u ∧ STR u ) Intuitively, L x u means: spatio-temporal entity x is exactly located at region u. I.e., x takes up the whole region u but does not extend beyond u. On the intended interpretation: V ( L ) = { ⟨ x , u , κ ⟩ ∈ D E × D ST × K ∣ ∃ y ∈ D E : ⟨ x , y , u , κ ⟩ ∈ InstST ∨ ⟨ y , x , u , κ ⟩ ∈ InstST } V ( E ) = { ⟨ x , t , ⟨ γ , σ ⟩ ⟩ ∈ D E × D ST × K ∣ ∃ τ ∈ ℜ : t = σ τ ( T ) ∧ ∃ u ∈ D ST : ⟨ x , u , ⟨ γ , σ ⟩ ⟩ ∈ V ( L ) ∧ u ∩ t ≠ ∅ } V ( Pe ) = { ⟨ x , ⟨ γ , σ ⟩ ⟩ ∈ D E × K ∣ ∃ : u , v ∈ D ST : (10) ⟨ x , u , κ ⟩ ∈ V ( L ) ∧ ⟨ x , v , κ ⟩ ∈ V ( L ) ∧ ⟨ x , u , v , κ ⟩ ∉ V ( SIMU ) } V ( Part ) = { ⟨ x , κ ⟩ ∈ V ( Pe ) ∣ ∃ y ∈ D E : ∃ u ∈ D ST : ⟨ x , y , u , κ ⟩ ∈ InstST } V ( Uni ) = { ⟨ x , κ ⟩ ∈ V ( Pe ) ∣ ∃ y ∈ D E : ∃ u ∈ D ST : ⟨ y , x , u , κ ⟩ ∈ InstST } V ( Cont ) = { ⟨ x , κ ⟩ ∈ V ( Pe ) ∣ ∃ u ∈ D ST : ⟨ x , u , κ ⟩ ∈ V ( L ) ∧ ⟨ u , κ ⟩ ∈ V ( SR ) } V ( Occ ) = { ⟨ x , κ ⟩ ∈ V ( Pe ) ∣ ∃ u ∈ D ST : ⟨ x , u , κ ⟩ ∈ V ( L ) ∧ ⟨ u , κ ⟩ ∈ V ( STR ) }

Finally, an axiom is included that ensures that every persistent entity has a worldline (A19). Region u is the worldline of entity x if and only if u a spatio-temporal region that is the mereological sum of all locations at which x is located ( D WLOf ); D WLOf WLOf x u ≡ STR u ∧ u Sum { v ∣ L x v } A 19 Pe x → ( ∃ u ) ( WLOf x u ) On the intended interpretation WLOf is: V ( WLOf ) = { ⟨ x , u , ⟨ γ , σ ⟩ ⟩ ∈ D E × D ST × K ∣ ⟨ u , ⟨ γ , σ ⟩ ⟩ ∈ V ( STR ) ∧ (11) u = ⨆ { v ∈ D ST ∣ ⟨ x , v , ⟨ γ , σ ⟩ ⟩ ∈ V ( L ) } ∧ u ⊑ γ } On this interpretation all entities instantiate at or along the physically possible worldlines.

The mereological structure of the subdomain of continuants is characterized by the ternary parthood relation P c which, holds between a time slice t and two continuant particulars x and y that are instantiated respectively at regions u 1 and u 2 such that u 1 is a part of u 2 and u 2 is part of the time slice t ( D P c ). By contrast, the mereological structure of the subdomain of occurrents is characterized by the binary parthood relation P o defined as: x is part of y if and only if the location of x is part of the location of y and the location of x is a spatio-temporal region ( D P o ). D P c P c x y t ≡ Cont x ∧ Cont y ∧ TS t ∧ D P c P c x y t ≡ ( ∃ u 1 ) ( ∃ u 2 ) ( ∃ z 1 ) ( ∃ z 2 ) ( Inst x z 1 u 1 ∧ Inst y z 2 u 2 ∧ P u 1 u 2 ∧ P u 2 t ) D P o P o x y ≡ ( ∃ u 1 ) ( ∃ u 2 ) ( ∃ z 1 ) ( ∃ z 2 ) ( Inst x z 1 u 1 ∧ Inst y z 2 u 2 ∧ P u 1 u 2 ∧ STR u 1 ) On the intended interpretation P c and P o mean: (12) V ( P c ) = { ⟨ x 1 , x 2 , t , κ ⟩ ∈ D E × D E × D ST × K ∣ ⟨ t , κ ⟩ ∈ V ( TS ) ∧ ∃ y 1 , y 2 ∈ D E : ∃ u 1 , u 2 ∈ D ST : u 1 ⊑ u 2 ⊑ t ∧ ⟨ x 1 , y 1 , u 1 , κ ⟩ ∈ InstST ∧ ⟨ x 2 , y 2 , u 2 , κ ⟩ ∈ InstST } V ( P o ) = { ⟨ x 1 , x 2 , κ ⟩ ∈ D E × D E × K ∣ ∃ y 1 , y 2 ∈ D E : ∃ u 1 , u 2 ∈ D ST : ⟨ x 1 , y 1 , u 1 , κ ⟩ ∈ InstST ∧ ⟨ x 2 , y 2 , u 2 , κ ⟩ ∈ InstST ∧ u 1 ⊑ u 2 , ⟨ u 1 , κ ⟩ ∈ V ( STR ) ∧ ⟨ u 2 , κ ⟩ ∈ V ( STR ) } In Minkowski spacetime the parthood relation among continuants ( P c ) is logically linked to the underlying slicing of spacetime. This is an immediate consequence of axiom ( A M ). Only continuants that exist simultaneously at a time can be parts at that time.