'continuant part of' Elucidation in BFO 2 OWL Model Is Circular

[Anthony Petosa]

From the BFO 2 OWL model:

"b continuant part of c =Def b and c are continuants & there is some time t such that b and c exist at t & b continuant part of c at t"

This appears to be an oversight. Here is how this relation is elucidated in the BFO 2 reference document dated Jun 15th, 2015, Rev. date Sep 09th, 2020:

"b continuant part of c at t means: b and c are continuants & b is a part of c at t"

[petosa...@gmail.com]

b continuant part of c =Def b and c are continuants & there is some time t such that b and c exist at t & b continuant part of c at t”

 

Kindly explain what “b continuant part of c” on the right-hand side means.

 

From: bfo-d...@googlegroups.com <bfo-d...@googlegroups.com> On Behalf Of Werner Ceusters
Sent: Thursday, July 17, 2025 5:25 PM
To: BFO Discuss <bfo-d...@googlegroups.com>
Subject: [bfo-discuss] Re: 'continuant part of' Elucidation in BFO 2 OWL Model Is Circular

 

Werner Ceusters

5:23 PM (now) 

to BFO Discuss

It is not circular. The left hand side continuant part of has 2 arguments, and the right hand one has 3 arguments, hence different signature, different relation

--
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/f2ae26aa-d2e4-4c33-baca-6159d47a3b37n%40googlegroups.com.

[Anthony Petosa]

By the way, I am not sure what happened to my original post, which is now deleted. I claimed the 'continuant part of' relation's definition, as written in the BFO 2 OWL model, is circular. I concluded this based on the following:

• "a definition in which the definiendum (the expression being defined) or a variant of it appears in the definiens (the expression that defines it)" [source: https://www.dictionary.com/browse/circular%20definition]

As an aside, ISO 11179-4 describes "avoid circular reasoning":

• "Two definitions shall not be defined in terms of each other. A definition should not use another concept's definition as its definition. This results in a situation where a concept is defined with the aid of another concept that is, in turn, defined with the aid of the given concept."

The bottom line is that whether we call this a circular definition, a recursive definition - whatever: I don't care - I simply pointed out that the BFO 2 OWL model's 'continuant part of' definition has not been updated to match the correct 'continuant part of' definition in the BFO 2 reference document dated Jun 15th, 2015, Rev. date Sep 09th, 2020:

"b continuant part of c at t means: b and c are continuants & b is a part of c at t"

The 'part of' wording in the correct definition is explained by Section 3.1 ("Relations of parthood") in the BFO 2 Rev. 2020-09-09 reference guide.

Excerpted from https://github.com/BFO-ontology/BFO-2020/blob/master/src/owl/bfo-core.ttl and emphasized in bold:

###  http://purl.obolibrary.org/obo/BFO_0000176
<http://purl.obolibrary.org/obo/BFO_0000176> rdf:type owl:ObjectProperty ;
                                             owl:inverseOf <http://purl.obolibrary.org/obo/BFO_0000178> ;
                                             rdfs:domain <http://purl.obolibrary.org/obo/BFO_0000002> ;
                                             rdfs:range <http://purl.obolibrary.org/obo/BFO_0000002> ;
                                             dc11:identifier "221-BFO" ;
                                             rdfs:label "continuant part of"@en ;
                                             skos:definition "b continuant part of c =Def b and c are continuants & there is some time t such that b and c exist at t & b continuant part of c at t"@en ;
                                             skos:example "Milk teeth continuant part of human; surgically removed tumour continuant part of organism"@en ;
                                             skos:scopeNote "Users that require more sophisticated representations of time are encouraged to import a temporal extension of BFO-Core provided by the BFO development team. See documentation for guidance: <https://github.com/BFO-ontology/BFO-2020/tree/master/src/owl/profiles/temporal%20extensions>"@en .

This should be corrected.

[seanno...@gmail.com]

It seems that Google groups are not supported anymore and behave erratically. See: https://groups.google.com/g/imsai8080esp/c/rsj5yLHaSOc

 

I tried to answer yesterday but mails get deleted as well.

 

I am not going to waste time on this and perhaps the group should move to github.

 

W

[Woland's Cat]

Not GitHub. Discourse is far better for this kind of community - in fact it would only need one discourse instance for the entire OBO community.

We use both in openEHR (here's the Discourse site) but serious discussions are all on Discourse.

--
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/1BEEA3C468CF44F9AA1EA524B38D551B%40Vaio2025.

--
Thomas Beale
Health IT blog | Culture blog | The Objective Stance | ORC-ID

[petosa...@gmail.com]

If Discourse is better for this purpose than GitHub, then I’ll add my thumbs up vote.

To view this discussion visit https://groups.google.com/d/msgid/bfo-discuss/8de6dbca-6273-4a29-9ef7-8a9877101638%40gmail.com.

[seanno...@gmail.com]

That doesn't mean anything because the definition is not : "b continuant part of c =Def b and c are continuants & there is some time t such that b and c exist at t & b continuant part of c at t”, but " b continuant part of c =Def b and c are continuants & there is some time t such that b and c exist at t & b continuant part of c at t”. Just like "eto" in "Petosa" doesn't mean anything.

To view this discussion visit https://groups.google.com/d/msgid/bfo-discuss/105b01dbf763%244166a2f0%24c433e8d0%24%40gmail.com.

[seanno...@gmail.com]

[Alan Ruttenberg]

Please don't suggest Discourse for BFO issues. The github issue list is the forum of record for BFO-2020. Conversations are archived there. Let's not fragment things further.

To view this discussion visit https://groups.google.com/d/msgid/bfo-discuss/8de6dbca-6273-4a29-9ef7-8a9877101638%40gmail.com.

[Anthony Petosa]

From  the BFO 2 reference document (Jun 15th, 2015, Rev. date Sep 09th, 2020), p.6:

"Relation of parthood disambiguated

Hitherto BFO has distinguished parthood between continuants and occurrents by means of the at t suffix used for the former; henceforth we will use the explicit distinction between continuant_part_of and occurrent_part_of (still using the at t suffix for the former)."

Yes, I am keenly aware of the temporal component for BFO Continuants, but this still does not answer my question.

Example:

:werner_ceusters_left_arm continuant part of :werner_ceusters = :werner_ceusters_left_arm and :werner_ceusters are continuants & there is some t such that :werner_ceusters_left_arm and :werner_ceusters exist at t & :werner_ceusters_left_arm continuant part of  :werner_ceusters at t

So, Werner, your left arm is a 'continuant part of' you because your left arm & you are continuants, they exist at the same time reference and your left arm is a continuant part of you at this time reference.

How does this get us any closer to understanding the 'continuant part of' relation? I will ask again, what does the 'continuant part of' phrase mean in 'continuant part of at t'?

Let us return to the 'continuant part of' elucidation that is captured in the BFO 2 reference document (Jun 15th, 2015, Rev. date Sep 09th, 2020), which is the very latest version to the best of my knowledge. Ironically, it is not available here, https://github.com/BFO-ontology/BFO-2020/tree/master/documentation/user%20guides.

b continuant part of c at t means: b and c are continuants & b is a part of c at t & [002-BFO]

I refer to Section 3.1 ("Relations of parthood"). In case you did not read it, I added its content below.

==========================================================================================

3.1 Relations of parthood

As our starting point in understanding the parthood relation, we take the axioms of Minimal Extensional Mereology as defined by Simons [46, pp. 26-31], assuming, with Simons, the axioms of first order predicate calculus. The axioms (reformulations of SA1-3 and SA6 in Simons’ numbering) are:

Antisymmetry: If x part of y, then if y part of x, then x = y.

Transitivity: If x part of y, and y part_of z, then x part_of z.

Weak Supplementation: If x part_of y & not x = y, then there is some z such that (z part_of y and z has no part in common with x).

Unique Product: If x and y have a part in common, then there is some unique z such that for all w (w is part of z if and only if (w is part of x and w is part of y)).

Where Simons takes as primitive the relation of proper parthood, we use here and in the remainder of this document parthood relations that include not only proper parthood but also identity as a special case. The corresponding proper_part_of relations are then defined in the obvious way as follows:

            x proper_part_of y =Def. x part_of y & not x ­= y.

BFO 2.0 includes two relations of parthood, namely parthood as it obtains between continuants – called continuant_part_of – and parthood as it obtains between occurrents – called occurrent_part_of, as follows. 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 a templates used to define BFO’s relations.

==========================================================================================

The 'part of' relation is fundamental. I imagine at best one can elucidate its meaning but not formally define it, and when offering an elucidation, I do not see how one would avoid expressing its meaning in terms of itself. This self-reference occurs with 'continuant part of' in the BFO 2020 OWL model but not in the BFO 2 reference document. The reason I believe the reference document's elucidation of continuant_part_of is better than that in the BFO 2020 OWL model is that it expresses continuant_part_of in terms of part_of. The reference document neither defines nor elucidates the 'part of' relation but instead refers to Simons' Minimal Extensional Mereology axioms, which the reference document claims they "serve as a templates (sic) used to define BFO's relations."

Therefore, while the BFO 2 reference document continuant_part_of elucidation includes a relation (i.e., 'part of') that is neither defined nor elucidated by BFO, at least we understand the 'part of' properties, and this gives us enough information to better understand both the 'part of' relation and its BFO derivative.

[seanno...@gmail.com]

Anthony,

 

you continue to use the binary form of ‘continuant-part-of’ - which is in the context of the BFO a poor-man’s version for people interested in OWL-vocabularies - of the ternary form as axiomatized in BFO2020-FOL.I said I am not interested in OWL nor in the problems caused by the restrictions of OWL so don’t ask me (I refer to your “So, Werner, ...”). The only reason why I reacted on your first mail, is that you were wrong in claiming the definition of ‘b continuant-part-of c” is circular. It isn’t because relations with different signatures are not identical despite the same name being used.

However, if your question is deeper in the sense of what criteria should be applied to be allowed to state that ‘a continuant-part-of b at t’, then that is NOT defined in BFO and left open to intuition on the basis of examples, thereby assuming that when domain-ontology developers use this relation for subtypes of continuant, they establish these criteria for these subtypes. What BFO2020-FOL does tell you is that IF you use the relation, the axioms in the file ‘continuant-mereology.cl’ (and depending one elsewhere stated) should not be violated.

 

W

 

From: Anthony Petosa

Sent: Monday, July 21, 2025 11:32 AM

To: BFO Discuss

To view this discussion visit https://groups.google.com/d/msgid/bfo-discuss/41309ed6-ea4f-4246-82dc-3e730e41057fn%40googlegroups.com.

[Anthony Petosa]

> I said I am not interested in OWL nor in the problems caused by the restrictions of OWL

> so don’t ask me (I refer to your “So, Werner, ...”).

You are not obligated to answer. I responded to your response; it's called a dialog.

> The only reason why I reacted on your first mail, is that you were wrong in claiming the definition

> of ‘b continuant-part-of c” is circular. It isn’t because relations with different signatures are not identical

> despite the same name being used.

Fine, but let's not get hung up on 'circular.' I think everyone reading this post understands my point. If not, please chime in. Just because the 'continuant part of at t' portion of the elucidation includes a temporal component, which can be expressed by an FOL ternary relation, does not mean that it gets to the root of my question. 

This question goes out to the entire membership of this list. Werner, feel free to respond, or not.

What does 'continuant part of' mean? Do not explain its axiomatization. Tell me in English what it means without using the phrase 'continuant part of' in your explanation. For anyone interested in responding, imagine your target audience has absolutely no background in BFO and Mereology. The challenge is to explain something complex as simplistically as possible.

I look forward to your feedback. Thank you.

[Pierre Grenon]

> Fine, but let's not get hung up on 'circular.' I think everyone reading this post understands my point. 

Not really.

The thread has a fairly clear title, it is about the alleged circularity of a formal definition and it's been answered. So that's that.

Perhaps others follow, for myself, I lost track of what the problem is at this point as the question now seems to be:

what is the (non-axiomatic) meaning of the English phrase "continuant part"?

BFO is formalised in an axiomatic manner. In such contexts, some terms are defined from others. In such contexts, there are always undefined ('primitive') terms.

It's not straightforward to give a simple explanation of a technical, defined term in such contexts. The fact that some terms are exhibited under the guise of a natural language phrase has to be seen charitably as an intuitive help to the human reader but not as carrying any semantic force.

BFO enforces axiomatically certain strong conditions on parthood. As a result, continuant parthood is simply parthood between continuants. It takes formalisation and axioms to demonstrate or just illustrate this and it has nothing to do with the intuitive understanding of English phrases that are contingently used as names or symbols.

In the cases discussed in this thread, modulo whether a context is involved in addressing temporal qualification or not, which makes things slightly wonky when trying to articulate, it really is a rather straightforward matter of syntactic sugar and as you pointed out, it all tracks down to parthood.

BFO does not explain parthood (or "part"), it is a primitive. For technical primitive terms, for which there is only appeal to intuition (or tradition), if one really insists on some explanation and there is use of a natural language name when glossing over these terms, the normal recourse is to look into a dictionary. 

So, the non-axiomatic meaning of "continuant part" is, when applied to continuants:

"some but not all of some thing"

https://www.oxfordlearnersdictionaries.com/definition/english/part_1

Kind regards,

Pierre

To view this discussion visit https://groups.google.com/d/msgid/bfo-discuss/7b2a36fc-3b2a-4e96-bda4-d862cc488277n%40googlegroups.com.

[Anthony Petosa]

> BFO is formalised in an axiomatic manner. In such contexts, some terms are defined from others. In such contexts, there are always undefined ('primitive') terms.

True. Are you claiming that since 'part of' is neither defined nor elucidated but instead only cited in the BFO 2 reference document (i.e., the section on Simons' minimal Extensional Mereology), that it is not considered a BFO primitive? If so, then:

• Why is the BFO reference document's 'continuant part of' elucidation expressed in terms of 'part of at t' while the BFO 2020 OWL model elucidates it in terms of 'continuant part of at c'? Is this a typo or deliberate? Which version is correct?
• The BFO reference document not only includes 'part of at c' in its elucidation, but it goes through the trouble of applying Simons' axioms to the 'continuant part of' relation. The document also derives a theorem from these axioms that 'continuant part of' is reflexive.

Clearly, the document's author(s) placed some weight on this. So, to understand 'continuant part of,' at least in the way BFO describes it, requires that one adheres to a temporalized version of Simons' axioms, which the BFO 2 reference document clearly conveys. The 'part of' relation is primitive; granted. This is why the axioms are helpful; they describe its properties, even if 'part of' itself can neither be defined nor elucidated. At least we know what distinctly characterizes it.

Frankly, providing two different elucidations on 'continuant part of' is sloppy and confusing. Why make it more difficult for BFO adoption? This makes no sense.

The Common Logic representation for the 'continuant part of' elucidation:

(cl:comment 'label:continuant-part-of-domain-range')

(cl:comment 'continuant-part-of is time indexed and has domain: continuant and range: continuant')

(forall (a b t)

   (if (continuant-part-of a b t)

      (and (instance-of a continuant t) (instance-of b continuant t) (instance-of t temporal-region t))

  )

)

This is a more precise explanation of 'continuant part of' than are both the BFO 2 reference document and the BFO 2020 OWL model elucidations. I know the point has been made that one should rely on the formal representations and not on definitions or elucidations. If we look at this this way, then whether the elucidation claims 'continuant part of at t' or 'part of at t' is irrelevant. However, in terms of broad adoption, why is there not a greater effort to grab the attention of a wider audience by explaining BFO in simpler terms?

When I advocate BFO, all I get is a shoulder shrug. A great majority consider it an 'ivory tower' model, and this perception is enforced by the lack practical documentation. Sure, we need the BFO 2 reference document & we need the formal axiomatizations, but we also need an interpretation that is useful to business consumers. Otherwise, as I have experienced so many times, they will simply ignore it. So, unless the goal is to set down a nice shiny object in a place of honor on some high shelf and admire it from a distance, can we spend less time polishing and more time explaining?

How's that for veering off topic?...smile...

[Bill Hogan]

In case it's helpful:

Let F'' (f double prime) stand for b continuant part of c

Let F''' (f triple prime) stand for b continuant part of c at t

Then F''(x, y) means x continuant part of y

And F'''(x, y, z) means x continuant part of y at z

F'' and F''' are different relations because they have different arity, despite using the same symbol F (or the label 'continuant part of'). In much of FOL symbolization and syntax, the primes are left off for better readability and the two predicates / relations are defined this way:

Fxy

Fxyz

And the number of variable letters after the predicate letter indicates arity. But by the semantics of FOL, Fxy and Fxyz are by definition different predicates/relations.

So we could then write:

Fbc iff b & c are continuants and there is some time t such that b and c exist at t and Fbct 

So Fbc is not defined in terms of itself, it's defined in terms of Fbct, a different relation/predicate.

To view this discussion visit https://groups.google.com/d/msgid/bfo-discuss/3385D1B8023249A5911A34937F9223E6%40Vaio2025.

[Anthony Petosa]

Hi, Bill and thank you for the reply.

Okay; got it. Given the arity difference these are two different predicates. So, 'b continuant-part-of c' simply claims a relation between 'b and 'c' but does not specify when this relation occurs, whereas 'b continuant-part-of c at t' offers that temporal specificity. Also, the existential quantification based on time claims there is at least one 't' during which this b->c continuant-part-of relation exists, but this does not guarantee the b->c  continuant-part-of relation holds for every time value, t. The statement would need to be expressed in terms of universal quantification for that to hold. The BFO 2020 OWL model represents these two relations as 'continuant part of at some time' and 'continuant part of at all times,' respectively.

Next, I would like to discuss how Common Logic & FOL ternary relations are reified into binary relations so they can be represented in the OWL grammar.

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 Common Logic 'continuant-part-of is time indexed and has domain: continuant and range: continuant" statement with ternary predicates

(forall (b c t)

  (if

     (continuant-part-of b c t)

        (and

           (instance-of b continuant t)

           (instance-of b continuant t)

           (instance-of t temporal-region t)

        )

     )

  )

)

The Common Logic 'continuant-part-of is time indexed and has domain: continuant and range: continuant" statement reified for binary predicates (i.e., arity <= 2)

(forall (b c t)
  (iff
    (continuant-part-of-at b c t)
    (and
      (instance-of b continuant)
      (instance-of c continuant)

      (forall (t)

        (if

          (and

          (exists-at b t)

          (exists-at c t)

          )

          (exists (p)

            (and
              (instance p continuant-part-relation)
              (has-part-subject p b)
              (has-part-whole p c)
              (has-time p t)

            )

          )

        )

      )

    )

  )

)

Rewritten in FOL syntax...

∀b ∀c ∀t

[

   continuant-part-of-at(b, c, t) ↔

   (

      instance-of(b, continuant) ∧

      instance-of(c, continuant) ∧

      ∃p

      (

         instance(p, continuant-part-relation) ∧

         has-part-subject(p, b) ∧

         has-part-whole(p, c) ∧

         has-time(p, t)

      )

   )

]

If the preceding Common Logic & FOL statements are correct, then how do we align this with the BFO 2020 OWL model representation of 'b continuant part of c at t'? The 'continuant part of at some time' OWL Object Property simply claims its Continuant domain & range values and that it is the inverse property of the 'has continuant part at some time' OWL Object Property. The BFO 2020 OWL model states the 'Continuant' OWL Class is an rdfs:subClassOf this OWL Property Restriction (in Manchester Notation): 'continuant part of at some time only continuant.'

Where and how do the earlier reified statements fit in, or should one manage this differently in BFO 2020? For example, instead of using the reification in the form it is defined, should we model enough RDF triples at the instance level to ensure we capture what is required for 'continuant part of at some time' relation? For example,

• Instantiate 'b' & 'c' as Continuant and 't' as Temporal-Region
• Assert a 'continuant part of at t' object property assertion where 'b' is asserted to be a 'continuant part of some time' 'c'
• Assert 'b' & 'c' 'exists at' 't'

The only part that concerns me is what is to prevent someone from modeling two different 't' instances and having 'b' & 'c' each relate to one or the other, but not to both, on the 'b' & 'c' 'exists at' relations? The Allen Calculus (a.k.a., 'Allen's Interval Algebra') identifies thirteen ways in which two time intervals are related. The one that is appropriate here is 'equals,' where the subject & object of this relation start & end at the same time. I am not sure how we would apply this to temporal instances, which is what I would want if I instantiate t as a BFO Temporal Instant.

The same concerns apply for the 'continuant part of at all times' relation.

b continuant part of c at all times =Def for all times t, (b exists at t, implies b continuant part of c at t & t is a temporal region & b and c are continuants)

Common Logic syntax with binary predicate reification

(forall (b c t)
  (iff
    (continuant-part-of-at b c t)
    (and
      (instance-of b continuant)
      (instance-of c continuant)
      (exists (p)
        (and
          (instance p continuant-part-relation)
          (has-part-subject p b)
          (has-part-whole p c)
          (has-time p t)

        )

      )

    )

  )

)

FOL syntax with binary predicate reification

∀b ∀c

[

   continuant-part-of-at(b, c, t) ↔

   (

      instance-of(b, continuant) ∧

      instance-of(c, continuant) ∧

      ∀t

      [

        (exists-at(b, t) ∧ (exists-at(c, t)) →

        ∃p

        (

           instance(p, continuant-part-relation) ∧

           has-part-subject(p, b) ∧

           has-part-whole(p, c) ∧

           has-time(p, t)

        )

      ]

   )

]

Lastly, going full circle, I understand (I think) what the formal logic says and that 'b continuant part of c' & 'b continuant part of c at t' are independent predicates, but this still does not answer my question concerning the meaning of 'continuant part,' independent of its Predicate Logic formulation.

I can understand it better when following the BFO 2 reference documentation, which clearly aligns this relation with Simons' Minimal Extensional Mereology axioms. At least these provide the characteristics of the 'part of' and, by derivation, the 'continuant part of' relations. Again they neither define nor elucidate the meaning of 'b continuant part of c at t.' However, mathematically at least, it hints at what to expect in terms of class membership. I know, this does not equate with Mereology. If you have a better recommendation on defining this relation in a manner that passes the Mereology smell test, I would love to hear it.

I concede that the term 'circular' in my post's title is wrong, but I hope you follow what I mean by my trying to understand the 'continuant part of' relation intuitively without having to rely on a formal logic. Again, improving BFO's understandability likely will improve its adoption for practical use in the business world.

[Woland's Cat]

This is the root of the problem (if there is one). The definition looks
circular to those used to (some forms of) mathematical logic, because
the 'function' names are not differentiated. They should arguably be
something like continuant-part-of and continuant-part-of-at-time.
Different traditions of logic have different syntactic forms of course,
but personally, I also find it an annoyance that I mentally have to keep
translating an F into F'' and F''' or similar.

What is going on here is similar to 'method overloading' in mainstream
languages like Java. There are many who like it, and there are those who
think it hides semantics and creates errors (I am in the latter camp).
In languages that support curried functions, name overloading is just a
headache.

The real problem is that one always has the nagging feeling that there
might have been a mistake. We are not used to seeing mistakes in the
axiomatisation of BFO (or anything much in BFO-land), but it would be
better to always know the design intention.

[Michael DeBellis]

I've been following this discussion with great interest, but have only been lurking because I don't feel qualified to take a position... until now. 

What is going on here is similar to 'method overloading' in mainstream languages like Java. There are many who like it, and there are those who think it hides semantics and creates errors (I am in the latter camp).

In mainstream software development, method overloading in object-oriented languages like Java and C# is not just accepted but widely regarded as a best practice for improving code clarity, reuse, and maintainability. While it can be misused (as can any language feature), it's seen as a net positive by all practitioners I work with or know. The idea that it “hides semantics” isn't a common concern among experienced developers.

In languages that support curried functions, name overloading is just a headache.

  Curried functions are powerful and elegant in certain paradigms, especially in purely functional languages like Haskell. But pure functional programming is very rare in the real world. Some functional concepts — such as treating functions as first-class values and avoiding side effects have found real-world success, especially in frameworks like MapReduce used for processing petabytes of data in data stores like Hadoop. But currying itself remains a niche concept in day-to-day industry development. Most large-scale systems today are written in object-oriented or hybrid languages, where overloading is a standard and effective practice.  

Michael

https://www.michaeldebellis.com/blog

--
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/eca169f5-a17f-4195-a315-f3dd106935f6%40gmail.com.

[David Poole]

Your logic specification is wrong (and has many weird logical consequences)

(forall (b c t)
  (iff
    (continuant-part-of-at b c t)

     **condition**)

Should be

(forall (b c)

  (iff
    (continuant-part-of-at b c t)

       (Exists t
           **condition**)

(It might be easiest to think of it in terms of Clark’s completion of a logic program).

David

On Jul 22, 2025, at 11:16 AM, Anthony Petosa <petosa...@gmail.com> wrote:

[CAUTION: Non-UBC Email]

To view this discussion visit https://groups.google.com/d/msgid/bfo-discuss/337f7d73-b071-4d6e-b183-66460a27e9c0n%40googlegroups.com.

[David Poole]

Sorry iI meant

>> (forall (b c)
>> (iff
>> (continuant-part-of-at b c)
> (Exists t
> **condition involving t))

[Anthony Petosa]

David, thank you for the correction; combination of typos and errors. How's this rewrite? If it still is not accurate, then feel free to rewrite it as you see fit.

I am especially interested in the reification, where for all 't' and when both 'b' & 'c' exist, there is a 'p' relation linking it to 'b' as part, 'c' as whole and 't' as time. If this is formulated properly, then I am interested in seeing how the existing BFO 2020 OWL model aligns to the reified version of the "continuant-part-of is time indexed and has domain: continuant and range: continuant" statement that is part of the BFO 2020 documentation on GitHub.

(forall (b c)

  (iff
    (continuant-part-of b c)

    (and
      (instance-of b continuant)
      (instance-of c continuant)
      (forall (t)
        (if
          (and
            (exists-at b t)
            (exists-at c t)
          )
          (exists (p)
            (and
              (instance p continuant-part-relation)
              (has-part-subject p b)
              (has-part-whole p c)
              (has-time p t)
            )
          )
        )
      )
    )
  )
)

∀b ∀c

[
  continuant-part-of(b, c) ↔
  (

    instance-of(b, continuant) ∧
    instance-of(c, continuant) ∧
    ∀t

    [
      (exists-at(b, t) ∧ exists-at(c, t)) →
      ∃p

      (
        instance(p, continuant-part-relation) ∧
        has-part-subject(p, b) ∧
        has-part-whole(p, c) ∧
        has-time(p, t)
      )
    ]

  )
]

[Alan Ruttenberg]

Can you give me the identifier for the axiom? I'm assuming you mean some axiom in the BFO-2020 axiomatization. 

Also, it helps if you say why you think it's wrong.

Thanks,

Alan

To view this discussion visit https://groups.google.com/d/msgid/bfo-discuss/76B56088-B4C1-42D1-B0B5-359B456E792E%40cs.ubc.ca.