part of occurrent
BFO2 Reference: occurrent
occurrentPartOf
o-part-of
(forall (x y t) (if (and (occurrentPartOf x y t) (not (= x y))) (exists (z) (and (occurrentPartOf z y t) (not (exists (w) (and (occurrentPartOf w x t) (occurrentPartOf w z t)))))))) // axiom label in BFO2 CLIF: [124-001]
(forall (x y t) (if (and (occurrentPartOf x y t) (occurrentPartOf y x t)) (= x y))) // axiom label in BFO2 CLIF: [123-001]
BFO 2 Reference: a (continuant or occurrent) part of itself. We appreciate that this is counterintuitive for some users, since it implies for example that President Obama is a part of himself. However it brings benefits in simplifying the logical formalism, and it captures an important feature of identity, namely that it is the limit case of mereological inclusion.
The process of a footballer’s heart beating once is an occurrent part but not a temporal_part of a game of football.
[copied from inverse property 'has occurrent part'] b has_occurrent_part c = Def. c occurrent_part_of b. (axiom label in BFO2 Reference: [007-001])
(forall (x) (if (Occurrent x) (occurrentPartOf x x))) // axiom label in BFO2 CLIF: [113-002]
(forall (x y z) (if (and (occurrentPartOf x y) (occurrentPartOf y z)) (occurrentPartOf x z))) // axiom label in BFO2 CLIF: [112-001]
(forall (x y t) (if (exists (v) (and (occurrentPartOf v x t) (occurrentPartOf v y t))) (exists (z) (forall (u w) (iff (iff (occurrentPartOf w u t) (and (occurrentPartOf w x t) (occurrentPartOf w y t))) (= z u)))))) // axiom label in BFO2 CLIF: [125-001]
Mary’s 5th birthday occurrent_part_of Mary’s life
b occurrent_part_of c =Def. b is a part of c & b and c are occurrents. (axiom label in BFO2 Reference: [003-002])
occurrent_part_of is antisymmetric. (axiom label in BFO2 Reference: [123-001])
occurrent_part_of is reflexive (every occurrent entity is an occurrent_part_of itself). (axiom label in BFO2 Reference: [113-002])
occurrent_part_of is transitive. (axiom label in BFO2 Reference: [112-001])
occurrent_part_of satisfies unique product. (axiom label in BFO2 Reference: [125-001])
occurrent_part_of satisfies weak supplementation. (axiom label in BFO2 Reference: [124-001])
the first set of the tennis match occurrent_part_of the tennis match.
occurrent