Problem (?) with axiom "regions-precede-if-they-meet" [suk-1]

[kataph]

The axiom "regions-precede-if-they-meet", [suk-1], says, in prover9 syntax:

all i1 all i2 all l1 all f2 ((((-(bfoiof(i1,tinstbcat,i1))) & (-(bfoiof(i2,tinstbcat,i2))) & (lastInstantOf(l1,i1)) & (firstInstantOf(f2,i2)) & ((l1) = (f2)))) -> (precedes(i1,i2)))

But all other axioms about the preceding relation seems to entail that a time region precedes another only if they are disjoint. For example, this axiom:

% if one occurrent precedes another then they do not overlap temporally all p all q ((((precedes(p,q)) | (precedes(q,p)))) -> (-(exists overlap (((bfotpart(overlap,p)) & (bfotpart(overlap,q))))))) # label("precedes-doesnt-overlap")

makes so that the axiom suk-1 can never hold true (unless the antecedent of the axiom is void).

Therefore, is the axiom suk-1 actually an intended part of the BFO axiomatisation?

[wceusters]

But is it not so that the first or last instant of a temporal region can either be part of the temporal region or precede/just follow it? See [acg-1] and [qga-1]. Note: I work with the CL-version, not the Prover9, but I would be surprised if they say different things.

[kataph]

Thank you for your answer.

I see what you are saying. You are right, but I don't think it prevents the following "problem": BFO cannot "talk" about adjacent closed temporal itervals (if it is a problem at all, but it is at least weird from my point of view).

To see this lets take an example. Suppose that we want to talk about two topologically closed time intervals, say t12 and t23. As per BFO axioms, they both need to have first and last instants. Call the first/last instant of t12 as t1/t2, and the first/last instant of t23 as t2/t3. We assume that the first instant of t23 is equal to the last instant of t12 since we are talking about adjacent intervals. Now, t1 and t2 are temporal part of t12, and t2 and t3 are temporal part t23, since we are talking about topologically closed intervals. The axioms that you mentioned do hold, we just need to mention that t1(t2) does not precede t12(t23) and that t2(t3) is not preceded by t12(t23). Graphically we have

|-------------------|-----------------|                 t1,t2 tpart t12    t2,t3 tpart t23     t1(t2) firstInstOf t12(t23)  t2(t3) lastInstOf t12(t23)
t1                  t2               t3                t1(t2) NOT precedes t12(t23)       t2(t3) NOT is preceded by t12(t23)

This arrangement, if t12 does not precede t23, should satisfy all axioms of BFO about temporal regions (including acg-1 and qga-1), with the single exception of suk-1.

In order to be able to approximate the previous arrangement as a model of BFO (a full model of BFO would require other entities, but you see what I mean) we should talk about open intervals instead:

| (---------------) | (--------------) |  t1,t2 NOT tpart t12    t2,t3 NOT tpart t23   t1(t2) firstInstOf t12(t23)   t2(t3) lastInstOf t12(t23)
t1        t12       t2        t23      t3            t1(t2)  precedes t12(t23)       t2(t3)  is preceded by t12(t23)

Then, if t12 precedes t23, suk-1 is true, as well as all the other axioms about temporal regions, including acg-1 and qga-1.

If this is correct (please, correct me if it is not), it is quite weird because in BFO I could talk of non-adjacent closed intervals:

|---------------|     |-----------------|        t1,t2 tpart t12     t2',t3 tpart t23      t1(t2') firstInstOf t12(t23)     t2(t3) lastInstOf t12(t23)
t1              t2    t2'                 t3                t1(t2') NOT precedes t12(t23)       t2(t3) NOT is preceded by t12(t23)    t2 != t2'
                                                                          t12 precedes t23

and it should be possible to extend this arrangement to a model of BFO

[wceusters]

I think I am not seeing something you intend. You say "This arrangement, if t12 does not precede t23, should satisfy all axioms of BFO about temporal regions (including acg-1 and qga-1), with the single exception of suk-1." This sentence is just below a configuration which for BFO is clearly such that t12 DOES precede t23: it follows from suk-1: If you transform suk-1 to CNF, you get (in Kowalski form): if [s(=),C,D], AND [s(has-first-instant),B,D], AND [s(has-last-instant),A,C] then [s(instance-of),A,s(temporal-instant),A], OR [s(instance-of),B,s(temporal-instant),B], OR [s(precedes),A,B]. So the IF-sentences here are the configuration you picked. Clearly, the first OR-sentences in the conclusion are false, but the third one is true: A precedes B, so the axiom returns true. Is it that you want it to be false? The point, I believe, is that BFO is neutral to existence of open/closed intervals. You can certainly introduce other axioms for the sort of open/closed intervals you have in mind. That would not violate any BFO axiom as far as I am aware of. BFO is not exhaustive in its universals.

[alanruttenberg]

Thanks Werner. I'll have a look too this weekend. I agree it is a little quirky. Note, however, that I have defined the Allen relations against BFO and verified that all the Allen relation axioms hold, given those definitions. The Allen relations only relate intervals. Werner has it right that we haven't committed to the open vs closed interval distinction. Personally, I don't have a lot of love for sets of measure 0. They are perhaps ontologically necessary, but they aren't physical, at least by any theory I known. A similar choice is to not have a density axiom. To me that feels like too strong a commitment given what we know, and don't know, about physics. It's a bonus that it lets BFO have finite models which makes it much easier to prove consistency.

[kataph]

@wceusters

I think I am not seeing something you intend. You say [...] A precedes B, so the axiom returns true. Is it that you want it to be false?

Indeed, it must be false, or we get a contradiction: as per your reasoning, we get that t12 precedes t23. But, this is impossible, since t12 and t23 have t2 as common point, and, therefore, t12 does NOT precede t23, as per axiom [aou-1], which I quoted above, that says that things that overlap have no precedence relation between them. Therefore, the first arrangement I wrote cannot be modeled in BFO, unless you remove some axioms from BFO theory, for example [suk-1]

[kataph]

@alanruttenberg Thankyou for your most kind attention

I have defined the Allen relations against BFO and verified that all the Allen relation axioms hold, given those definitions. The Allen relations only relate intervals.

Undoubtedly you are correct: if you, say, define the meet relation by stating that the last instant of the first interval is the first instant of the second interval, and so on, then I have no doubt that all desired axioms hold. But BFO is quite stronger then that, so it could be that some models of Allen's temporal intervals theory are not (extendable to) models of BFO.

Werner has it right that we haven't committed to the open vs closed interval distinction.

This, I would say, is only mostly true: though it is an admittedly not really important point, if I am not wrong, BFO cannot talk about cosed adjacent intervals (meaning that the end of one is the start of the other, they meet, using Allen's relations), while it can talk about adjacent open intervals. Allen's time interval theory should, instead, admit models in which there are adjacent closed intervals, though I cannot formally prove it right now.

[wceusters]

@kataph , You say ":Indeed, it must be false, or we get a contradiction: as per your reasoning, we get that t12 precedes t23. But, this is impossible, since t12 and t23 have t2 as common point, and, therefore, t12 does NOT precede t23, as per axiom [aou-1]," Now I do see it and why you say BFO can't talk about such situations. Thanks for your patience. To make talk about both types of intervals possible, I believe it is not suk-1 that should disappear, but [aou-1] (or perhaps weekend). I need to put some more thought in that.

[alanruttenberg]

@kataph, @wceusters OK, I see it too. Can't have a model in which two regions overlap at an instant. At the moment I am thinking the fix is to modify suk-1 to exclude that case.

The situation with the Allen relations is that they don't pay attention to whether temporal instants are parts at all. So the overlap relation doesn't mean the same thing in Allen as it does in the mereology sense. As I understand it, Allen doesn't have the concept of open/closed intervals, just the relations. I'm not sure whether Allen can have the same meaning of overlaps as in mereology, but I haven't thought it completely through. Maybe if meets is defined so that it only obtains between one interval that is open and one closed at the middle?

The definition of overlaps in Allen I have is

    (:forall (?x ?y)
      (:iff (overlaps ?x ?y)
      (:and
       (:exists (?xs ?xe ?ys ?ye)
         (:and
          (instance-of ?x temporal-interval ?x)
          (instance-of ?y temporal-interval ?y)
          (has-first-instant ?x ?xs)
          (has-first-instant ?y ?ys)
          (has-last-instant ?x ?xe)
          (has-last-instant ?y ?ye)
          (precedes ?xs ?ys)
          (precedes ?ys ?xe)
          (precedes ?xe ?ye)
          )))))