OBOFoundry/COB

not sure how a plan can be sibling of both disposition and role

Opened this issue · 6 comments

If COB is going to be consistent with BFO (perhaps this isn't a requirement?), it not clear to me how plan can be a sibling of both role and disposition.

Role and disposition bifurcate the logical space of what counts as a realizable entity:

  • Disposition: the bearer is necessarily (must) be changed if the disposition ceases to exist
  • Role: the bearer is not necessarily changed

As far as I can tell, this doesn't leave room for a third type of realizable unless disposition and role are defined differently.

Yes. I am aware that role and disposition are not declared as being disjoint in the OWL. Based on the BFO lexical definitions, they should be disjoint.
In my discussions with Barry, he considered plan to be a type of disposition. However, he may have changed his mind, but I can follow up with him.

Sorry, I am hung up on it. But, I don't think COB (or really any formal ontology) should not include logically contradictory entities (even if the contradiction is not represented in the OWL). Perhaps you consider this contradiction a feature, but I consider it a bug.

A better approach (I think) would be to define (in RO) relations such as agent executes and executes during (as suggested in #217), and stay away from defining ontologically contentious/suspicious entities.

From Bjoern:
Barry said to place 'plan' under 'realizable entity' as that is clearly
what it is and how it is linked to planned process. Barry (and everyone
else) also agreed that we should not 'talk too much' about plan - i.e. not
subclass it, or worry too much about how it defines, but rather subclass
and define in detail the 'plan specification'

Barry's response:
We should place 'plan' under disposition. It is the disposition created in the one who is following the plan when, often using a plan specification, the decision to follow the plan is made.

I want to clear up a fundamental point of logic here.

It may seem counter-intuitive, but this is perfectly logically coherent:

P DisjointUnion C1, C2.   ## C1 and C2 bifurcate the space of P
C3 sub P

There are two coherent possibilities:

  • C3 is uncommitted as to whether it subclasses C1 or C2
  • there are satisfiable class expressions C3 and C1 and C3 and C2

For example:

Disease DisjointUnion MendelianDisease, NonMendelianDisease. ## space is trivially bifurfacted
Hemachromatosis Sub Disease

this is entirely logically coherent. Whether you would want to model something this way is another matter, but my comment is scoped to logical coherency.

To go back to the original comment:

Role and disposition bifurcate the logical space of what counts as a realizable entity:

Disposition: the bearer is necessarily (must) be changed if the disposition ceases to exist
Role: the bearer is not necessarily changed

Sure, let's take these as axioms

As far as I can tell, this doesn't leave room for a third type of realizable unless disposition and role are defined differently.

This doesn't follow, unless you are using "type" in some BFO sense that is stricter than "subClassOf" in OWL. Neither disjointness axioms nor stricter DisjointUnion axioms (I assume you mean this when you say "bifurcate the logical space") are sufficient to prevent satisfiable alternate subclasses of the parent. You need some kind of metaclass-level reasoning outside OWL to do this.

Yes. I am aware that role and disposition are not declared as being disjoint in the OWL. Based on the BFO lexical definitions, they should be disjoint.

I always recommend making a separate PR for things like this, rather than bundling things up in already confusing issues where we talk at cross purposes.

Here, I went ahead and made one:

note this goes even further than making them disjoint, it makes the subtypes exhaustive

Sorry, I am hung up on it. But, I don't think COB (or really any formal ontology) should not include logically contradictory entities (even if the contradiction is not represented in the OWL). Perhaps you consider this contradiction a feature, but I consider it a bug.

Of course all COB developers agree there should be no logical contradictions. But the onus is on you here to show a contradiction using reasoning rather than claiming it in ambiguous natural language.

You can see there are neither contradictions nor unsatisfiable classes with HermiT:

image

@cmungall Thanks for the logic lesson :)
I did not make a PR b/c I think @phismith comment needs to be addressed first.

But the onus is on you here to show a contradiction using reasoning rather than claiming it in ambiguous natural language.

I think your statement is bit strong here. Sure ... my reasoning could have been stated more clearly (see my assumption below). However, there are plenty of issue threads in which we argue our points in natural language. We tend to only delve into the nitty gritty of reasoners/formal logic when necessary.

This doesn't follow, unless you are using "type" in some BFO sense that is stricter than "subClassOf" in OWL.

No. I wasn't using 'type' in stricter sense. Rather, I was interpreting plan as being an entity that was neither a role or a disposition. In the PR, if you make plan, role, and disposition disjoint, then the ontology will become incoherent. Yes, you can fault me for this, but I think the judgment should not be too harsh. Plan has neither a definition nor any annotations providing giving guidance on how to interpret its relation to role or disposition.

So, under the current axiomatization in the PR, an instance of a plan must be either a disposition or a role. (If you assert that a plan is neither a disposition or role, the ontology becomes incoherent.) This raises the question (in my mind) of what is an example of an instance of plan that is an instance of role? Does the "uncommitted" stance on what a plan is make things clearer or muddy the waters?