proper occurrent part of is not declared transitive about bfo-2020 HOT 6 CLOSED

Reported by Stefan Schulz. It's declared transitive in the FOL, but in an oversight it wasn't on the list of transitive properties for which the OWL transitivity axiom was added.

Where is it in FOL, i.e. the ISO version? kad-1 declares it for occurrent-part-of with as consequence that if 'a pop b' and 'b pop c' only follows that 'a op c'.

from bfo-2020.

Sorry, my mistake - it's declared to be a theorem in the source from which the CL is generated, which is where I looked, and theorems are not included in the common logic. If follows from the definition of proper-occurrent-part-of, transitivity of occurrent-part-of and antisymmetry of occurrent-part-of: okr-1, kad-1, and xlu-1

It isn't in the OWL because all the OWL assertions are generated from specs and then verified provable, and the list for which there should be transitive assertions inadvertently omitted proper-occurrent-part-of. I've fixed the source but not regenerated the OWL yet.

If the forward relation is transitive, then that the inverse is transitive is also a theorem.

from bfo-2020.

I never trust myself to reason. Here's a transcript of what I did. First I ask to prove the transitivity. Then I ask for how it was proved, and it includes the antisymmetry. Then I try to prove it without transitivity. Then I ask for a model where the two axioms are true but the transitivity isn't.

>> (vampire-prove '((:kind :occurrent-mereology))
                 '(:forall (?x ?y ?z) (:implies (:and (proper-occurrent-part-of ?x ?y) (proper-occurrent-part-of ?y ?z))
                                          (proper-occurrent-part-of ?x ?z))))
:proved

>> (get-vampire-proof-support)

(:definition-of-proper-occurrent-part-of :occurrent-part-of-is-antisymmetric :occurrent-part-of-transitive)

>> (vampire-prove '(:definition-of-proper-occurrent-part-of :occurrent-part-of-transitive) 
                      '(:forall (?x ?y ?z) (:implies (:and (proper-occurrent-part-of ?x ?y) (proper-occurrent-part-of ?y ?z))
                                               (proper-occurrent-part-of ?x ?z))))

:failed

>> (z3-find-model '(:definition-of-proper-occurrent-part-of :occurrent-part-of-transitive 
                        (:not (:forall (?x ?y ?z) (:implies (:and (proper-occurrent-part-of ?x ?y) (proper-occurrent-part-of ?y ?z))
                                               (proper-occurrent-part-of ?x ?z))))))

#<z3-model domain size 3, 2 predicates, 15 tuples>

>> (pprint-model *)
(proper-occurrent-part-of c2 c3)
(proper-occurrent-part-of c2 c1)
(proper-occurrent-part-of c3 c2)
(proper-occurrent-part-of c3 c1)
(proper-occurrent-part-of c1 c2)
(proper-occurrent-part-of c1 c3)
(occurrent-part-of c2 c2)
(occurrent-part-of c2 c3)
(occurrent-part-of c2 c1)
(occurrent-part-of c3 c2)
(occurrent-part-of c3 c3)
(occurrent-part-of c3 c1)
(occurrent-part-of c1 c2)
(occurrent-part-of c1 c3)
(occurrent-part-of c1 c1)

from bfo-2020.

Here's a smaller model (courtesy of mace4)

(occurrent-part-of c1 c1)
(occurrent-part-of c1 c2)
(occurrent-part-of c2 c1)
(occurrent-part-of c2 c2)
(proper-occurrent-part-of c1 c2)
(proper-occurrent-part-of c2 c1)

from bfo-2020.

I realize that my earlier attempt to prove manually was wrong (printed here again since I accidently deleted the comment):
Proper-occurrent-part-of a b input (1)
Occurrent-part-of a b okr-1/(1) (2)
Not = a b okr-1/(1) (3)
Proper-occurrent-part-of b c input (4)
Occurrent-part-of b c okr-1/(4) (5)
Not = b c okr-1/(4) (6)
Occurrent-part-of a c kad-1/(2)/(5) (7)
Not = a c (3)/(6) (8)
Proper-occurrent-part-of a c okr-1/(8)/(7) !

(8) does not follow from (3) and (6) as under these, it would also be possible that a = c.

So assume a = c

assume = a c (8b)
proper-occurrent-part-of c b (1)/(8b) (9)
occurrent-part-of c b okr-1/(9) (10)
= c b xlu-1/(10)/(5) (11)
contradiction (11)/(6)

Thus assumption (8b) is wrong, hence not = a c where we are back above and thus proper-occurrent-part-of a c.

from bfo-2020.

fixed now

from bfo-2020.