Definitions of proper-continuant-part-of and proper-occurrent-part-of are not parallel

[michaelrabenberg]

Here's the definition of proper-continuant-part-of:

(cl:comment "x proper continuant part of y means x is a continuant part of y but y is not continuant part of x [sls-1]"
(forall (x y t)
(iff (proper-continuant-part-of x y t)
(and (continuant-part-of x y t) (not (continuant-part-of y x t))))))

Informally: A is a part of B but B is not a part of A. This is one way in which non-time-indexed proper parthood is often defined.

Here's the definition of proper-occurrent-part-of:

(cl:comment "A proper occurrent part of b means a is an occurrent part of b and a is not the same as b [okr-1]"
(forall (x y)
(iff (proper-occurrent-part-of x y)
(and (occurrent-part-of x y) (not (= x y))))))

Informally: A is a part of B and A ≠ B. This is another way in which non-time-indexed proper parthood is often defined.

These definitions aren't parallel to each other. In the absence of a compelling reason to the contrary, I think they should be made parallel to each other--either both should follow the first pattern or both should follow the second pattern.

I myself think the second pattern more directly captures the intuitive notion of proper parthood than does the first, so I'd recommend changing sls-1 to parallel okr-1.

[wceusters]

But that (not(= x y)) is the case for continuants too follows directly from [sls-1] itself in light of what '=' means in FOL. There is no other axiom needed. Similarly for [okr-1]. Both forms are truly equivalent under FOL semantics.
And remember, there is no non-time-indexed parthood for continuants in BFO2020.

[michaelrabenberg]

Not suggesting adding a new axiom; suggesting replacing one with the analogue of the other. In particular, I'd advocate having instead of the current continuant axiom the following sort of thing (haven't formalized correctly; hope the idea is clear though; added parentheses to clarify where the sides of the biconditional start and stop):

For all x y t, (x proper-continuant-part-of y at t) iff (x continuant-part-of-y at t & x=/=y).

It's mostly a design choice. Do you want the axiom to "directly" (so to speak) deliver non-identity from a proper-continuant-parthood input and the reasoner to infer after that that there isn't a continuant-parthood symmetry, or do you want the axiom to directly deliver that there isn't a parthood symmetry and the reasoner to infer after that that there's non-identity? Perhaps there'd be efficiency benefits to getting the non-identity conclusion as soon as possible. (I don't know.)

But it's not entirely a design choice. If the axiom is supposed to be a definition of proper continuant parthood, as the comment suggests (it contains the term "means"), then there are considerations that go beyond what you can infer from the axiom that bear on what you should include in it.

[alanruttenberg]

I believe the issue has to do with change extensionality of the mereology of object aggregates from being at a time, to over the lifetime. a) If the parts are the same at any time, then the things are the same vs b) If the parts are the same at all times, then the things are the same. (a) is supposed to be true for continuants other than object aggregates. My commit note suggests that the change of the proper parthood definition was related to that. You have to be careful because its a combination of axioms that implies extensionality.

The breakdown led to the possibility that for object aggregates a and b, both could be part of each other without being the same.

In that case, since a != b, and a part of b, we would conclude that a proper part of b, which is wrong for the above.

What motivated it in the first place was the position that organizations were object aggregates, and that you could have two organizations that had the same members for some period of time.

This is another unpretty part of BFO.

Over the years I think I've come to the conclusion that the view of organizations as object aggregates is too simple. It might be worth reconsidering the choice that was made.

(evaluate-formulas '((:kind :continuant-mereology) (:kind :proper))
                        '((instance-of a object-aggregate t)
                          (instance-of b object-aggregate t)
                          (:not (:equal a b))
                          (continuant-part-of a b)
                          (continuant-part-of b a)))
==> :satisfiying-model

(evaluate-formulas '((:kind :occurrent-mereology) (:kind :proper)) 
                        '((instance-of a occurrent t)
                          (instance-of b occurrent t)
                          (:not (:equal a b))
                          (occurrent-part-of a b)
                          (ocurrent-part-of b a)))
==>:failed
(definition-of-occurrent occurrent-part-of-is-reflexive-on-occurrent definition-of-proper-occurrent-part-of)

Unfortunately it seems I didn't fix extensionality for continuants other than object aggregates, so its also currently true that you can have objects a and b that are part of each other.
[typo "aren't" -> "are" fixed]