Revision to definition of bfo:occurs-in

[michaelrabenberg]

I propose a revision to the textual definition of bfo:occurs-in. It is shorter and more readable than the current version, and I think it captures the intended semantics of the current version no worse than the current version does.

Here is the current version, with some clause-numbers added:

b occurs in c =Def. (1) b is a process or a process boundary and (2) c is a material entity or immaterial entity & (3) there exists a spatiotemporal region r and b occupies spatiotemporal region r & (4) for all t, if b exists at t then c exists at t & there exist spatial regions s and s' where b spatially projects onto s at t & c occupies spatial region s' at t & s is a continuant part of s' at t

I think clause (3) is superfluous and should be deleted. The 'r' variable doesn't reappear later in the definition, so (3) merely serves to restrict things that occur in things to things that (inter alia) occupy spatiotemporal regions. But this restriction is implied by clause (1), given [qyy-1], which says that every process or process boundary occupies a spatiotemporal region.

[Paragraph deleted here; changed my mind about it.]

Thus I propose the following revised definition:

b occurs in c =Def. b is a process or a process boundary and c is a material entity or immaterial entity & for all t, if b exists at t then c exists at t & there exist spatial regions s and s' where b spatially projects onto s at t & c occupies spatial region s' at t & s is a continuant part of s' at t

Smaller point: Clause (2) is “c is a material entity or immaterial entity”; it is not the extensionally equivalent but more compact “c is an independent continuant.” Perhaps that revision would be an improvement too.

[wceusters]

Re point 1): I tend to agree with the only caveat that as with 'history', the definition is created to put limitations that are not expressed in the axioms, though as you point out, it seems unlikely wrt the spatiotemporal region bit. There is no axiom in which 'occurs-in' is used and that also uses 'spatiotemporal-region'.

Re point2): axiom [tfw-1] is more restrictive than the definition

''' (cl:comment "occurs-in has domain process or process-boundary and range material-entity or site [tfw-1]"
(forall (a b)
(if (occurs-in a b)
(and
(exists (t)
(or (instance-of a process t)
(instance-of a process-boundary t)))
(exists (t)
(or (instance-of b material-entity t) (instance-of b site t)))))))
'''

In general, and in addition to your comment, 'occurs-in' is one of these relations for which both axioms, comments and definitions/elucidations can be improved

a) [jil-1]'s comment reads funny as it seems to imply that the first argument doesn't need to be an occurrent, but that is excluded by the previous axiom

''' (cl:comment "occurs-in is dissective on first argumentwhen it is an occurrent [jil-1]"
(forall (p q r)
(if (and (occurs-in p q) (occurrent-part-of r p)) (occurs-in r q))))
'''

b) There are two axioms that when converted to clausal form generate clauses with tautologies. That is not a sign that the axiom is wrong, but rather that it can be simplified.:

The first one is [czc-1]: it leads to 6 clauses, 3 of which are tautological
''' (cl:comment "occurs-in is lower bound location [czc-1]"
(forall (p c1 c2)
(if
(and (occurs-in p c1)
(forall (t)
(iff (exists-at p t)
(and (exists-at c2 t) (continuant-part-of c1 c2 t)))))
(occurs-in p c2))))
'''
The other one is [yex-1] which generates 2 tautological clauses out of 4
''' (cl:comment "occurs-in is a lower bound on second argument [yex-1]"
(forall (p c1 c2)
(if
(and (occurs-in p c1)
(forall (t) (iff (exists-at p t) (located-in c1 c2 t))))
(occurs-in p c2))))
'''

[michaelrabenberg]

Re point 1): I tend to agree with the only caveat that as with 'history', the definition is created to put limitations that are not expressed in the axioms, though as you point out, it seems unlikely wrt the spatiotemporal region bit. There is no axiom in which 'occurs-in' is used and that also uses 'spatiotemporal-region'.

But there is an axiom in which 'process or process boundary' and 'occupies spatiotemporal region' are both used, and in particular in which it's asserted that any instance of process or process boundary bears occupies-spatiotemporal-region to something, namely [qyy-1]; and I'm confident BFO will never get revised to allow for things that aren't processes or process boundaries to occur-in things. Indeed clause (1) of the definition of occurs-in rules out such a thing.

Re point2): axiom [tfw-1] is more restrictive than the definition

''' (cl:comment "occurs-in has domain process or process-boundary and range material-entity or site [tfw-1]" (forall (a b) (if (occurs-in a b) (and (exists (t) (or (instance-of a process t) (instance-of a process-boundary t))) (exists (t) (or (instance-of b material-entity t) (instance-of b site t))))))) '''

Interesting.

a) [jil-1]'s comment reads funny as it seems to imply that the first argument doesn't need to be an occurrent, but that is excluded by the previous axiom

''' (cl:comment "occurs-in is dissective on first argumentwhen it is an occurrent [jil-1]" (forall (p q r) (if (and (occurs-in p q) (occurrent-part-of r p)) (occurs-in r q)))) '''

I too think the "when it is an occurrent" could be deleted.

b) There are two axioms that when converted to clausal form generate clauses with tautologies. That is not a sign that the axiom is wrong, but rather that it can be simplified.:

The first one is [czc-1]: it leads to 6 clauses, 3 of which are tautological ''' (cl:comment "occurs-in is lower bound location [czc-1]" (forall (p c1 c2) (if (and (occurs-in p c1) (forall (t) (iff (exists-at p t) (and (exists-at c2 t) (continuant-part-of c1 c2 t))))) (occurs-in p c2)))) ''' The other one is [yex-1] which generates 2 tautological clauses out of 4 ''' (cl:comment "occurs-in is a lower bound on second argument [yex-1]" (forall (p c1 c2) (if (and (occurs-in p c1) (forall (t) (iff (exists-at p t) (located-in c1 c2 t)))) (occurs-in p c2)))) '''

Do you have simplified suggestions?

[wceusters]

It is not difficult, but time-consuming to propose simplifications. One way is to rewrite the disjunctions generated by the axiom that did not lead to a tautology back to separate axioms. For [yex-1], for example, the two non-tautological clauses rewritten as separate axioms are:

[yex-1-a]
'''
(forall (p c1 c2)
(if (and (occurs-in p c1)
(exists (t)
(and (exists-at p t)
(located-in c1 c2 t))))
(occurs-in p c2)
)
)
'''

and [yex-1-b]

'''
(forall (p c1 c2)
(if (occurs-in p c1)
(exists (t)
(or (exists-at p t)
(located-in c1 c2 t)
(occurs-in p c2))
)
)
)
'''
It seems to me that [yex-1-a] is the core of what is intended.
[yex-1-b] does not add anything since it is always true because of the first disjunction which by itself follows from [tfw-1] and [lqn-1].

Therefore, I think that [yex-1] may be replaced by the much simpler [yex-1-a].

I leave [czc-1] as an exercise for you. :-)

[wceusters]

By the way, the trick with the three quotes that Alan suggested to keep the indentations in the axioms doesn't seem to work, or what did I do wrong?

[alanruttenberg]

needs to be backquotes ``` vs '''
e.g.

(forall (p c1 c2)
    (if (occurs-in p c1)
        (exists (t)
           (or (exists-at p t)
               (located-in c1 c2 t)
               (occurs-in p c2)))))