search

BFO-ontology / BFO-2020

A repository for BFO 2020 artifacts specified in ISO 21838-2:2020
78 stars 28 forks source link

Domain and range of member part of at all/some time/s aren't specific enough #8

Open alanruttenberg opened 3 years ago

alanruttenberg commented 3 years ago

They are currently both material entity. It should be that member part of should have domain object and range object aggregate.

Thanks to tschneider@engineeringsemantics.com for the questions that surfaced this.

alanruttenberg commented 3 years ago

I tracked this down, and it turns out it was an explicit choice I made. The (flawed) rationale was that since object aggregate, fiat object part, and object are not disjoint and not rigid, for practical purposes any material entity could be the domain and range.
This is fixed in the next release

alanruttenberg commented 3 years ago

OK, so not so flawed. Here's definition for member-part-of-at-some-time:

(forall (p q)
  (if (has-member-part-at-some-time p q)
   (rdf-type object-aggregate p)))

What's rdf-type? We have to have an interpretation of rdf:type, since the way we prove the OWL axioms is by translating them to FOL and then using a FOL prover. The only interpretation of rdf:type works is an at-all-times definition. We can't (currently) have time-dependent instantiation in OWL. [If someone has an idea, please do say].

Here's the definition of rdf:type.

(forall (c i)
 (iff (rdf-type c i)
  (and (forall (t) (if (exists-at i t) (instance-of i c t)))
   (exists (t) (exists-at i t)))))

Object aggregate, object, and fiat object part are not rigid. So something could be an object and then an object aggregate. [It may be that that's the wrong way to look at it, but let's assume it for the moment]

If those classes aren't rigid then we can have a model in which something is an object for a while, then object aggregate for a while, during which it has a member.

The putative axiom says that if something has a member-part-at-some-time then it's always (rdf-type) an object aggregate. But the example above is a counterexample.

So the formula isn't provable since it isn't true, under the assumptions above. Therefore, I pushed the domain/range up to the nearest rigid superclass, which is material entity. It's not as specific, but at least it is true.

The weakest part of the above is the assertion that the subclasses of material entity aren't rigid. If they were, then this problem wouldn't arise. Can somebody make an argument for that?

alanruttenberg commented 3 years ago

One thought is to define subclasses of material entity which are rigid and use those in the OWL. e.g.

rigid object =def a material entity that is an object any any time that it exists rigid object aggregate =def a material entity that is an object aggregate at any time it exists

We can label these object and object aggregate in the OWL file, add the rigid label as an alternative time, and document this fact in the scope note.

We'll need to make sure that the OWL->FOL translation gets the right classes

There's a reasonable argument to make that whether we formalize this or not this is what the OWL version must mean, because the temporal interpretation rdf:type is all-times. I need to understand why, despite this, we have the issue. Maybe this is something that I missed that should to be factored into the definitions of the all and some times property definitions.