BFO-2020
BFO-2020 copied to clipboard
BFO-ontology
Material entities (and sites) occupy 3D spatial regions (right?)
BFO literature seems consistently to say:
(A) Every material entity occupies a 3D spatial region. (B) Every site occupies a 3D spatial region.
But there appears to be no axiom(s) to the effect that (A) is true.
There is an axiom, [uqb-1], saying that every site that occupies a spatial region occupies a 3D one, but there appears to be no axiom(s) to the effect that every site occupies a spatial region, so the axioms don't seem to yield (B).
Perhaps these axioms could be added (I haven't formalized them):
(i) If a occupies spatial region b then if a is an instance of material entity then b is an instance of three dimensional spatial region (ii) If a is an instance of material entity, then a occupies a spatial region. (iii) If a is an instance of site, then a occupies a spatial region.
(i) is the analogue of [uqb-1] for material entities.
Another way to go would be to dispense with [uqb-1] and just include two axioms that more directly say that (A) and (B) are true.
For (ii) and (iii) there's already an axiom [mma-1] but it had a bug. It should be
(forall (c t)
(if
(and (instance-of c independent-continuant t)
(not (instance-of c spatial-region t)))
(forall (t2)
(exists (s)
(if (temporal-part-of t2 t) (occupies-spatial-region c s t2))))))
The mistake was that in the original in place of (forall(t2) (exists (s)... it had (:exists (s t2) ...
I will fix that, in which case (ii) and (iii) are theorems.
Hmm. I can't find [mma-1] in any of the clif files on the GitHub (and I hadn't seen it before). Is it in one of them?
Sorry, my bad. the old version of mma-1 is a theorem so wasn't included in the CLIF. Can't prove the new version, so I will change status of that to axiom and it will show up in an upcoming release.
Got it. Also just noticed that there needs to be a “and t2 is a temporal instant at t2” clause added to the final antecedent of the updated mma-1; as stated it implies that something that changes size over the course of some temporal interval occupies some spatial region at that interval.
How's that? The antecedent says it occupies a spatial region at t. If it occupies that region then it occupies the same region for any part of t. The quantification of t ranges over all temporal-regions.
Suppose some balloon, B, increases in size over some temporal interval, int. B is an ic at int and B is not a spatial region at int. Furthermore, int is a temporal part of int. So, the axiom as stated implies that there’s a spatial region B occupies at int. But B occupies different spatial regions at different parts of int, so that’s not true.
If however the axiom were weakened so that it implies only that at every temporal part of int that is a temporal instant B occupies some spatial region, then there’d be no issue.
How's that? The antecedent says it occupies a spatial region at t. If it occupies that region then it occupies the same region for any part of t. The quantification of t ranges over all temporal-regions.
I don't see that antecedent. Are you talking about the same axiom?
Ok, I see the problem. Weakening to temporal instant isn't right because we don't have dense time. Now I think that the original version was right after all.
Also a problem in with the proposals for (ii) and (iii) Id be curious how you would temporalize.
(ii) If a is an instance of material entity, then a occupies a spatial region.
is not temporalized. Once temporalized my claim is it has the same problem it is of the same form as the original mma-1.
The part of t formulation works because although not dense, there are no gaps in time. See https://github.com/BFO-ontology/BFO-2020/issues/69#issuecomment-1682739502
TODO:(temporalize ii) and (iii). Show they theorems. I will try but it would be a good exercise for you to work it out.
Werner: > I don't see that antecedent. Are you talking about the same axiom?
I can't remember what I was talking about either at the moment.
With the reversion of mma-1 to its original the below are both provable. Interestingly this is the first time I had to include a theorem for the reasoners to terminate. It was mma-1 which I double-checked is a theorem.
(ii)
(forall (t m)
(if
(instance-of m material-entity t)
(exists (s t2)
(and (temporal-part-of t2 t)
(occupies-spatial-region m s t2)))))
(iii)
(forall (t m)
(if (instance-of m site t)
(exists (s t2)
(and (temporal-part-of t2 t)
(occupies-spatial-region m s t2)))))
I am not sure what you mean with 'dense time', But it seems right that that at a temporal instant 'nothing' happens, so an inflating balloon isn't inflating at a time instant. The 'exists (s)' would be right because at any distinct time-instant of the interval, the balloon would occupy a distinct s. At all times that a material entity exists, it occupies some spatial region, but when the entity grows or shrinks, it is of course not the same spatial region. Since there are no 'size changing processes' in BFO, there is no axiom that states that if we have a material entity 'me' for which holds '(and (occupies-spatial-region me s t)(instance-of t temporal-interval))'. An ontology that would include such processes, must ensure that a corresponding axiom is available, i.e. that 'me' then does not participate in such process.
Dense time means that between every two instants there is another instant. (recurse) Did you read https://github.com/BFO-ontology/BFO-2020/issues/69#issuecomment-1682739502? If not please do.
(forall (t m) (if (instance-of m site t) (exists (s t2) (and (temporal-part-of t2 t) (occupies-spatial-region m s t2)))))
This works, because you did not universally quantify t2. My comment to add that t2 must be temporal instant was under the universal quantification of t2. You don't need it with existential one.
I did read *69 comment, but it doesn't use the term 'dense time'. Furthermore, I don't see what the impact would be on my suggestion. If it is stated that something is the case at a ti, then that statement doesn't state anything about neighboring ti's, does it?
The axiom I had was correct and is a theorem and the theory works in the sense that (ii) and (iii) are provable. The axiom we're discussing (https://github.com/BFO-ontology/BFO-2020/issues/74#issuecomment-1853337908) was a change that wasn't necessary, the result of me being confused.
This is a solved problem, and as such I'm going to pass on thinking about the instant formulation. Maybe it works, maybe it doesn't. If it works we're still behind as it would amount to having to add a new axiom, where the old theory already works.
The axiom I had was correct and is a theorem and the theory works in the sense that (ii) and (iii) are provable. The axiom we're discussing (#74 (comment)) was a change that wasn't necessary, the result of me being confused.
This is a solved problem, and as such I'm going to pass on thinking about the instant formulation. Maybe it works, maybe it doesn't. If it works we're still behind as it would amount to having to add a new axiom, where the old theory already works.
I'll take your word for it that the original [mma-1] is a theorem. There does remain the matter of claim (i), though, which I take it still does have to be added. It could be formulated in a manner exactly analogous to [uqb-1], just for material-entity instead of site.
Yes, (i) still needs to be addressed an it will be.
You can use [mcd-1], [cez-1], [bao-1], and [uas-1] to prove [mma-1]. I include it here for reference. So you ought to be able to take this and prove it yourself. Not a great idea to take my word for it if there's an alternative. I can send the prover9 output if that would be helpful.
(:forall (?c ?t)
(:implies (:and (instance-of ?c independent-continuant ?t)
(:not (instance-of ?c spatial-region ?t)))
(:exists (?s ?t2)
(:and (temporal-part-of ?t2 ?t)
(occupies-spatial-region ?c ?s ?t2)))))
Yes, (i) still needs to be addressed an it will be.
You can use [mcd-1], [cez-1], [bao-1], and [uas-1] to prove [mma-1]. I include it here for reference. So you ought to be able to take this and prove it yourself. Not a great idea to take my word for it if there's an alternative. I can send the prover9 output if that would be helpful.
(:forall (?c ?t) (:implies (:and (instance-of ?c independent-continuant ?t) (:not (instance-of ?c spatial-region ?t))) (:exists (?s ?t2) (:and (temporal-part-of ?t2 ?t) (occupies-spatial-region ?c ?s ?t2)))))
Please do.