Questions about occupies-spatial-region

[michaelrabenberg]

I ran this scenario (alongside BFO-2020) through the reasoner that Werner and I use (natural-language summary below):

t([0,occupies-spatial-region,material-entity-1,region-1,time-1]).

t([0,instance-of,material-entity-1,material-entity,time-1]).

(cl:comment "at time-1 there's a part of region-1 that isn't occupied by any part of material-entity-1 [zzzf-1]"
      (exists (x)
            (and  (continuant-part-of x region-1 time-1)
                  (not  (exists (y)
                              (and  (continuant-part-of y material-entity-1 time-1)
                                    (occupies-spatial-region y x time-1)))))))

(cl:comment "at time-1 there's a part of material-entity-1 doesn't occupy any part of region-1 [zzzg-1]"
      (exists (x)
            (and  (continuant-part-of x material-entity-1 time-1)
                  (not  (exists (y)
                              (and  (continuant-part-of y region-1 time-1)
                                    (occupies-spatial-region x y time-1)))))))

That is, at time-1 all of the following are the case: (a) material-entity-1 is a material entity that occupies-spatial-region (OSR's) region-1, (b) region-1 has a part that isn't OSR'ed by any part of material-entity-1, and (c) material-entity-1 has a part that OSR's no part of region-1. This scenario yielded no contradiction on our end.

One question and two conditional requests:

Q. Do you think this scenario should yield a contradiction? I was surprised not to get one. If I occupy a spatial region, r, at t, how could I have a part that occupies no part of r at t, and how could there be a part of r that is occupied by no part of me at t?

CR1. If there's someone who answers "No" to Q, I'd be grateful if some such person could say why.

CR2. If there's someone who answers "Yes" to Q and knows (unlike me) how to use prover-9 or vampire or some such, I'd be grateful if some such person would run the scenario through some such prover to see if this might just be something our reasoner missed.

[alanruttenberg]

I'm wondering whether the issue is that some ?me-part can be part of material-entity-1 for the whole of time-1, but not occupy the same spatial region. I.e. the parts can move around.

In that case the part might not occupy a single spatial region for the whole of time-1, but there ought to be be a partition of time-1 such that within each element of the partition ?me-part occupies some part of spatial-region-1.

Quantifying over partitions won't work I think, but it could be weakened to asserting that there's always some ?tp part of time-1 where ?me-part occupies some part of region-1.

[alanruttenberg]

Or that if ?me-part occupies-spatial-region ?region-part at any ?tp that's part of time-1, ?region-part is a part of region-1

[alanruttenberg]

Or maybe force time-1 to be a temporal instant, so there's no time for the part to move around.

[alanruttenberg]

I just proved

(forall (tp sr me)
    (implies (and (temporal-part-of tp time-1)
                  (occupies-spatial-region me sr tp)
                  (continuant-part-of me material-entity-1 tp))
        (continuant-part-of sr region-1 tp)))

Surprisingly prover9 proved this in 40 seconds but vampire and z3 timed out after 3 minutes. Proof support was bre-1, bzp-1, kbr-1, mcd-1, mqp-1, cez-1, mlb-1, lzw-1, grv-1, mud-1, qaf-1 along with your two facts.

(occupies-spatial-region material-entity-1 region-1 time-1)
(instance-of material-entity-1 material-entity time-1)

Verified the proof with vampire by proving using the proof support, though z3 timed out trying.

Goes to show that it's definitely worth using all the provers. Prover9 is usually the weakest but won this time. z3 couldn't even prove it given the answer.

[alanruttenberg]

I'm not able to prove (yet?) that

(forall (tp sr me)
  (implies (and (temporal-part-of tp time-1)
                (occupies-spatial-region me sr tp)
                (instance-of me material-entity tp)
                (continuant-part-of sr region-1 tp))
      (continuant-part-of me material-entity-1 tp)))

Which I think gets to @michaelrabenberg 's zzzf-1

[alanruttenberg]

[Edit: suggested model here is wrong. See https://github.com/BFO-ontology/BFO-2020/issues/82#issuecomment-1983833119 for another attempt]

@michaelrabenberg is unhappy that

at time-1 there's a part of region-1 that isn't occupied by any part of material-entity-1

Try this out:

I claim this will be true in most cases because as we have things now almost if not all parts are explicitly asserted and so the parts of the spatial region wouldn't necessarily line up with the the parts of the material entity.

For this to be true we'd have to have an axiom to the effect that at all times if a material-entity occupies a spatial region, then for every part of the spatial region there's a part of the material entity that occupies it. But we don't. I have generally shied away from axioms like this that "generate" parts for fear that it will lead to infinite models, which I can't easily prove consistent. Maybe this one wouldn't - we'd have to check.

In the absence of that...

Suppose that the spatial region is a sphere with parts the left hemisphere and the right hemisphere, and suppose the material entity is a sphere of the same size occupying the spatial region but with parts the north hemisphere and south hemisphere.

In that case no part of the material entity occupies the right hemisphere of the spatial region.

--

If we did add the axiom we might be tempted to add one on the occurrent side too. That is, for every process occupying a spatiotemporal region, there exists a part of the process that occupies each part of that spatiotemporal region.

--

Does this make sense?

[wceusters]

I don't understand your sphere example. Of course there is a part of the sphere that occupies the right hemisphere of the spatial region, but it is not the north or south hemisphere of the material entity. When the material-entity-sphere is rotating in the sr it occupies, then at all times the occupation holds, there is some part of the ME that occupies a part of the SR and there is no part of the SR that is not occupied by a part of the ME. I assumed that grv-1 takes care of the 'completeness' of the occupation of a spatial region at a time, thus that when the relation holds, there is no part of the occupied sr that is not occupied by a part of the occupier. But when the tr is not a time-instant, it does of course not have to be the very same part of the occupier that at all parts of tr occupies the very same part of the sr. If it is not that, what is the point of grv-1 then? Or is the axiom not doing what the comment says?

[alanruttenberg]

@wceusters my model was written too hastily and I made a mistake. Consider instead that the material sphere has no asserted parts but the spatial region has the left and right hemisphere as parts. Then the same argument holds, I think.

grv-1 says that every part of the occupier occupies some part of the spatial region. It doesn't say every part of the region is occupied by part of the occupier.

If you don't like the idea of a macroscopic atom, think of some truly indivisible atomic particle. These occupy extended regions. Those regions can be divided, even though the particle can't, again yielding regions that are not occupied by part of the particle, since there are no parts of the particle.

[wceusters]

@alanruttenberg so in your view, it is not the case that every material entity has fiat object parts? Even for an atom, I could still by fiat declare it to have a top half and bottom half, like with your sphere example, even if it would be totally impossible to change these fiat object parts into objects by splitting the atom. The question is of course whether BFO should be silent about it or not, and it seems it is silent about it currently.

[alanruttenberg]

I thought that question might come up :-)

The answer is that I don't know. I think that it's plausible that there are mereological atoms and BFO certainly doesn't rule them out. There's also the issue that a fiat thing requires an act of fiat to establish it and so we probably can't count on that happening in all cases.

I think we agree that there's at least a question about what the ontology should commit to. In the case in question we could certainly experiment with having an axiom that says that for every spatial region there's a (possibly fiat) part of the occupier that occupies it.

Aside from the ontological question, the concern is mostly about the tractability of managing the consistency model and reasoning once we're starting to multiply parts. Is that the only place where we'll have to assert parts? If there are more than one case then do they add or multiply? If they multiply do we land up going exponential?

I already worry whether histories, given the way we've defined them, should have something in that direction. If we say the history includes all the things happening in the spatiotemporal region a history occupies, then it would seem we need to cut all processes at that spatiotemporal boundary in order to sum them. A process in which a neutrino in part passes through my body would need to have a an actual part which is the neutrino only passing through my body.

Whether we need to do that in order to do the kind of reasoning we currently expect to do is another story. I didn't think, at least in the first pass, that that was something essential, so I didn't go there. But depending on the problem it might be desirable.

To connect this with other choices, there was the choice of using a finite model theory of time, which excludes an axiom that says that between any two instants there's another. What that bought us was the ability to have relatively easy consistency proof. What that costs us is that we have to think a little harder when querying and quantifying over time.

[michaelrabenberg]

I regret that some other more pressing duties kept me from responding to any of this for so long. Thank you very much, Alan, for all of this, which has been very clarifying!

A couple of things for now:

I'm wondering whether the issue is that some ?me-part can be part of material-entity-1 for the whole of time-1, but not occupy the same spatial region. I.e. the parts can move around.

I see. What this requires is that material-entity-1 can fail to move around in time-1 even though it has parts that do move around in time-1. When I try to imagine an example like that, I end up thinking of things like the following: a perfectly solid sphere (S+) has a spherical proper part (s) in its interior that rotates during time-1 while the rest of S+ "stands still" in region-1. Then it's at least arguable that s, or at least some continuant part of s, doesn't occupy any spatial region at time-1 but S+ does occupy region-1 at time-1, and so it'd presumably be inappropriate for BFO to rule out such a possibility. (Less outré examples won't cut it, I don't think. I don't think I occupy any spatial region at any time, t, such that one of my blood cells moves around over the course of t.)

What would be unacceptable would be for S+ to have a part that occupies a spatial region at time-1 but that doesn't occupy a part of region-1 at time-1. But the axiom you proved rules that out, if I'm following.

grv-1 says that every part of the occupier occupies some part of the spatial region. It doesn't say every part of the region is occupied by part of the occupier.

Here's the axiom you said you couldn't prove:

(forall (tp sr me) (implies (and (temporal-part-of tp time-1) (occupies-spatial-region me sr tp) (continuant-part-of me material-entity-1 tp)) (continuant-part-of sr region-1 tp)))

If this can't be proved, then (if I'm following) BFO even allows for occupied parts of the region that aren't occupied by (parts of) the occupier. I ran such a scenario and didn't get a contradiction (natural-language summary below):

t([0,occupies-spatial-region,material-entity-1,region-1,time-1]). t([0,instance-of,material-entity-1,material-entity,time-1]). t([0,continuant-part-of,mini-region-1,region-1,time-1]).

(cl:comment "at time-1 something occupies mini-region-1 [zzzh-1]" (exists (x) (occupies-spatial-region x mini-region-1 time-1)))

(cl:comment "at time-1 no part of material-entity-1 occupies mini-region-1 [zzzi-1]" (not (exists (x) (and (occupies-spatial-region x mini-region-1 time-1) (continuant-part-of x material-entity-1 time-1)))))

That is, at time-1, all of the following claims are true: (i) material-entity-1 is a material entity that OSR's region-1; (ii) mini-region-1 is a continuant part of region-1; (iii) something occupies mini-region-1; (iv) no continuant part of material-entity-1 occupies mini-region-1. I don't know what I think about this possibility.

[alanruttenberg]

I see. What this requires is that material-entity-1 can fail to move around in time-1 even though it has parts that do move around in time-1. When I try to imagine an example like that, I end up thinking of things like the following: a perfectly solid sphere (S+) has a spherical proper part (s) in its interior that rotates during time-1 while the rest of S+ "stands still" in region-1. Then it's at least arguable that s, or at least some continuant part of s, doesn't occupy any spatial region at time-1 but S+ does occupy region-1 at time-1, and so it'd presumably be inappropriate for BFO to rule out such a possibility. (Less outré examples won't cut it, I don't think. I don't think I occupy any spatial region at any time, t, such that one of my blood cells moves around over the course of t.)

The body example fails only because the body changes it's spatial region constantly - breathing, blood vessels expanding at each pump of the heart, etc. Maybe migration of cells in the bone marrow relative to the bone, if immobilized.

Other examples: the pistons in a running engine, assuming the engine is rigidly mounted, the particles decaying in radioactive material, titling back the passenger seat in a car at rest, tumblers moving as you unlock a lock, fan blades in a fan. Lots of non-outré examples,

I'll look into your new example when I'm back from travel tomorrow.

[michaelrabenberg]

Other examples: the pistons in a running engine, assuming the engine is rigidly mounted, the particles decaying in radioactive material, titling back the passenger seat in a car at rest, tumblers moving as you unlock a lock, fan blades in a fan. Lots of non-outré examples,

If I have an empty cubic box with 1-inch-thick walls, does it occupy a solid cubic spatial region (that includes where the empty interior is) or a spatial region shaped like its walls? If the former then of course your examples work, but I would have thought the latter so I assumed such examples didn't work. (This isn't terribly important though because all that matters to the present issue is whether some examples work.)

[alanruttenberg]

Material entities can have immaterial parts such as holes and cavities. Whether the space in question is part of the box or not would be a domain question. In the case of engines and pistons I'd say the spaces are parts because, at least, they need to be designed to accommodate the piston movement.

On March 13, 2024 2:29:00 PM EDT, Michael Rabenberg @.***> wrote:

Other examples: the pistons in a running engine, assuming the engine is rigidly mounted, the particles decaying in radioactive material, titling back the passenger seat in a car at rest, tumblers moving as you unlock a lock, fan blades in a fan. Lots of non-outré examples,

If I have an empty cubic box with 1-inch-thick walls, does it occupy a solid cubic spatial region (that includes where the empty interior is) or a spatial region shaped like its walls? If the former then of course your examples work, but I would have thought the latter so I assumed such examples didn't work. (This isn't terribly important though because all that matters to the present issue is whether some examples work.)

-- Reply to this email directly or view it on GitHub: https://github.com/BFO-ontology/BFO-2020/issues/82#issuecomment-1995296184 You are receiving this because you were mentioned.

Message ID: @.***> -- Sent from my Android device with K-9 Mail. Please excuse my brevity.

[alanruttenberg]

@michaelrabenberg the example in https://github.com/BFO-ontology/BFO-2020/issues/82#issuecomment-1994494307 would be ok if the occupier of mini region was site, since the region occupied by a site can overlap the region occupied by a material entity (or another site, for that matter).

That said, it should be ruled out in the case that the mini-occupier isn't a proper part of the first occupant and both are material entities. I tried a couple of ways to fix this, one modifying grv-1 and one adding another axiom, but I can't get a reasoner to show an inconsistency, which either means it's too hard to prove or I'm missing something.

Here's the grv-1 attempt

(forall (c r t)
 (if
  (and (instance-of c independent-continuant t)
   (not (instance-of c spatial-region t))
   (instance-of r spatial-region t))
  (exists (t2)
   (and (temporal-part-of t2 t)
    (iff (occupies-spatial-region c r t2)
     (and
      (forall (cp)
       (if (continuant-part-of cp c t2)
        (forall (rp)
         (if (occupies-spatial-region cp rp t2)
          (continuant-part-of rp r t2)))))
|      (if (instance-of c material-entity t2)
|       (forall (c2 r2)
|        (if
|         (and (instance-of c2 material-entity t2)
|              (proper-continuant-part-of r2 r t2)
|              (occupies-spatial-region c2 r2 t2))
|         (proper-continuant-part-of c2 c t2))))
      (not
       (exists (rprime)
        (and (not (= rprime r)) (continuant-part-of rprime r t2)
         (occupies-spatial-region c rprime t2))))))))))

New axiom attempt:

(forall (t m s)
 (if
  (and (occupies-spatial-region m s t)
   (instance-of m material-entity t))
  (forall (tp m2 sp)
   (if
    (and (temporal-part-of tp t)
        (proper-continuant-part-of sp s tp)
        (instance-of m2 material-entity tp)
        (occupies-spatial-region m2 sp tp))
    (proper-continuant-part-of m2 m tp)))))

I've stared at these for too long. Maybe you can see a problem.

[alanruttenberg]

I didn't stare at my version of the setup enough - there was a typo. The additional axiom rather than the grv-1 modification yielded the inconsistency, with support sls-1, lzw-1, njq-1 and the new axiom.

Here's the setup

(and (occupies-spatial-region m1 s1 t1)
 (instance-of m1 material-entity t1)
 (proper-continuant-part-of s1-mini s1 t1)
 (exists (x)
  (and (occupies-spatial-region x s1-mini t1)
       (instance-of x material-entity t1)
       (not (continuant-part-of x m1 t1)))))

It's late and the proof support seems a little thin so I'm a little worried I've still got something wrong. So, please verify.

[michaelrabenberg]

It seems like it should work to me. The new axiom entails this:

(1) (if (and (occupies-spatial-region m1 s1 t1) (instance-of m1 material-entity t1)) (forall (tp m2 sp) (if (and (temporal-part-of tp t1) (proper-continuant-part-of sp s1 tp) (instance-of m2 material-entity tp) (occupies-spatial-region m2 sp tp)) (proper-continuant-part-of m2 m1 tp)))))

Given your setup, the antecedent of (1) is satisfied. So, we get this:

(2) (forall (tp m2 sp) (if (and (temporal-part-of tp t1) (proper-continuant-part-of sp s1 tp) (instance-of m2 material-entity tp) (occupies-spatial-region m2 sp tp)) (proper-continuant-part-of m2 m1 tp))))

Now suppose, by your setup:

(3) (exists (x) (and (occupies-spatial-region x s1-mini t1) (instance-of x material-entity t1) (not (continuant-part-of x m1 t1))))

Let 'a' refer to such a thing (innocently, given the proof to follow). So:

(5) (occupies-spatial-region a s1-mini t1) (6) (instance-of a material-entity t1) (7) (not (continuant-part-of a m1 t1)))

From (2), we get this:

(8) (if (and (8a) (temporal-part-of t1 t1) (8b) (proper-continuant-part-of s1-mini s1 t1) (8c) (instance-of a material-entity t1) (8d) (occupies-spatial-region a s1-mini t1)) (8e) (proper-continuant-part-of a m1 t1))))

(8b) is in your setup. (8c) = (6). (8d) = (5). (8a) is, I very confidently assume, entailed by BFO, but I can't see how it's entitled by the proof support you said you got so I guess that part of the matter is a bit mysterious to me. But at any rate those four jointly yield (8e), which contradicts (7). And 'a' was chosen arbitrarily so there's no issue with that. Does that seem right?