BFO Parthood Definitions

[Anthony Petosa]

The BFO 2020 model defines 'continuant part of at some time' as follows:

b continuant part of c at some time =Def for some time t (b exists at t and c exists at t and b continuant part of c at t & t is a temporal region & b and c are continuants)

The 'b continuant part of c at t' makes the definition nearly recursive. The phrase 'b continuant part of c at some t' would make it fully recursive. To rectify this, I recommend one of two solutions:

• Add a 'continuant part of' OWL Object Property as the super-property of the 'continuant part of at some time' property and transcribe its elucidation from the "Basic Formal Ontology 2.0 Specification and User's Guide" (Smith, Barry, June 26, 2015) documentation, which reads
  
  "b continuant part of c at t =Def. b is a part of c at t & t is a time & b and c are continuants.'
  
  From elsewhere in the documentation, we understand 'part of' aligns with a modified version of 'Minimal Extensional Mereology' axioms defined by Simons. Page 17 of the document expresses these as antisymmetry, transitivity, weak supplementation, and unique product, and it provides their axiomatic rules. Page 18 states
  
  "BFO 2.0 includes two relations of parthood, namely parthood as it obtains between continuants - called 'continuant part of' - parthood as it obtains between occurrents - called 'occurrent part of'...Note that Simons' axioms cited above are stated without reference to time, whereas some of the parthood relations BFO defines are temporally qualified. Therefore the relations and definitions described above are not relations in BFO, rather they serve as templates used to define BFO relations."
  
  
• Add either an rdfs:comment or a skos:scopeNote on the four 'continuant part of' relations in BFO to cite the BFO documentation.

Note, the recursive issue does not appear on the 'occurrent part of' elucidation.

'b occurrent part of c =Def c has occurrent part b'

The 'has occurrent part' elucidation reads

'b has occurrent part c means: c is a part of b & b and c are occurrents'

Unlike 'continuant part of some time,' 'has occurrent part' is elucidated in terms of the 'part of' Simons minimal extensional mereology axioms.

[Alan Ruttenberg]

continuant part at t is a distinct relation, a ternary relation. Continuant part of at some time is a binary relation defined as

    (forall (p q)
     (iff (continuant-part-of-at-some-time p q). <---- the new relation
      (exists (t)
       (and (exists-at p t) 

               (exists-at q t) 

               (continuant-part-of p q t))))) <--- the relation it is defined in terms of

The standard already has the definition of continuant part of (at t)

A.1.2.5 continuant part of
ELUCIDATION: b continuant part of c at t means: b and c are continuants & b is a part of c at
DOMAIN: continuant
RANGE: continuant

continuant part of (at t) can not be in the OWL version of the ontology, because OWL can only support binary relations.

--
You received this message because you are subscribed to the Google Groups "BFO Discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to bfo-discuss...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/bfo-discuss/6fc36de9-1229-4c8a-84bf-5993582797f4n%40googlegroups.com.