Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

first instant of and last instant of textual definitions are incorrect #127

Open
michaelrabenberg opened this issue Feb 6, 2025 · 9 comments
Open

first instant of and last instant of textual definitions are incorrect #127

michaelrabenberg opened this issue Feb 6, 2025 · 9 comments

Comments

@michaelrabenberg
Copy link

This problem was pointed out by someone else the other day; wanted to post it before it was forgotten. (I take no credit for the counterexample!)

Here's the definition of first-instant-of (more about last-instant-of below):

t first instant of t' =Def t is a temporal instant & t' is a temporal region t' & t precedes all temporal parts of t' other than t

Let R be the temporal interval spanning 1pm to 3pm, inclusive, and let R- be the temporal interval spanning 1pm to 2pm, inclusive. R- and R are both temporal regions, R- is a temporal part of R, and 1pm does not precede R-, so this definition implies that 1pm is not the first instant of R. But that's false, so the definition is wrong.

Here's a revised definition that avoids the counterexample:

t first instant of t' =Def t is a temporal instant & t' is a temporal region and t is a temporal part of t' & t precedes all temporal parts of t' that do not have t for temporal parts.

This captures the intuitive idea that the first instant of a region precedes everything in the region that doesn't include the instant, not just everything in the region other than the instant.

Unsurprisingly, a parallel issue arises for the last-instant-of definition.

There might be other relations that suffer from similar problems. Haven't had the time to check.
@alanruttenberg
Copy link
Contributor

This is #110 striking again.
The definition in the original source is does not make the same mistake.

Temporal instant t first instant of temporal region t' =Def. t precedes all temporal parts of t' that do not have t as a temporal part. [268-BFO]

Nor does the CLIF documentation

The first temporal instant is such that it precedes every part of the interval that doesn't have the first instant as part

That said, I don't believe the definition is correct. The implication forward is correct, but the backwards is too weak.

Consider the RHS:

t precedes all temporal parts of t' that do not have t as a temporal part.

This could be satisfied if we had

t precedes t2 precedes t'

In that case even though t2 is closer to the start of t', t satisfies the expression and so would be determined to be first instant, as would t2 as would all other instants back in history.

Those models are prevented by other axioms.

So 3 choices:

  1. Leave it as is. It gets the right idea across

  2. Weaken it to:

Temporal instant t first instant of temporal region t' implies t precedes all temporal parts of t' that do not have t as a temporal part.

  1. Strengthen it:

Temporal instant t first instant of temporal region t' =def t precedes all temporal parts of t' that do not have t as a temporal part and there is no temporal instant t'' such that t'' first instant of t' and t precedes t''

I'd probably change the variables t'->tr, t->ti, t''->ti'

Any preferences?

And let's deal with #110, ok?

@alanruttenberg
Copy link
Contributor

@michaelrabenberg, also the revised definition asserts that the first instant is part of the region, but we don't commit to that.

@michaelrabenberg
Copy link
Author

Is the, uh, recursiveness, or circularity, or whatever it'd best be called, in (3) a problem given the lack of a specified base case? I understand that the motivation for the last boldfaced material in (3) is partly to avoid the commitment to a first instant's being part of the relevant region. I was vaguely aware of that matter but ignored it in my original post, as you note.

I'm with you on the objection to the clif definition on the assumption that first instants need not be parts of the regions of which they're first instants.

Would it work to say that ti first instant of tr iff EITHER ti is a part of tr and precedes all non-ti-including parts of tr OR nothing is like that, but ti immediately precedes tr? More formally:

ti first instant of tr =def. (a) ti is a temporal instant and (b) tr is a temporal region and (c) EITHER (c1) ti occurrent part of tr & ti precedes all occurrent parts of tr that don't have ti for occurrent parts OR (c2) there does not exist a temporal instant, ti', such that ti' occurrent part of tr & ti' precedes all occurrent parts of tr that don't have ti' for occurrent parts, but ti precedes tr and there does not exist a temporal instant, ti'', such that ti precedes ti' and ti' precedes tr.

(It's entirely possible that that's just equivalent to (3) and I'm not smart enough to see that.)

I'll note that the "nothing is like that" part of the second disjunct is important, because without it the definition would imply that if time is discrete then a temporal region has two first instants (the one that's the "first part" and the one that immediately precedes the region).

@phismith
Copy link

phismith commented Feb 14, 2025 via email

@alanruttenberg
Copy link
Contributor

@michaelrabenberg we don't have 'immediately precedes' as a relation. If we did have it, we wouldn't allow it for instants because that would commit to discrete time, and we're leaving it open. For regions it would only obtain for regions whose last instant is the same as the first instant of the next, as long as only one has that instant as part. Better to use the Allen relations I contributed the CLIF for.

For 3, I don't think the recursive nature is a problem. Why do you? A reasonable argument against would be conflicting, or nonsensical or model in which it is ambiguous as to whether a particular instant is a first instant. Can you provide one? The definition you offer is hard to follow, and I'm not sure what it gains. Perhaps it is time to switch to CLIF so we can get a clearer idea of what's going on and do things like check for equivalence with a reasoner.

I'm mixed about whether we need a biconditional and should let the axiom just be a necessary condition, leaving an elucidation rather than a definition. The term and its axiom don't exist in isolation, and along with other axioms disallows models we don't want. However, 3 would allow for =def and in that case I don't think the axiom has to match, just that the definition is provable from the theory.

Anyways, I'll scrutinize your definition when I have some more time to think about it. In the meantime, providing a counter-model, like you did in the issue post, is most useful.

@phismith yes, I commented so about the definition he offered in the first post of this discussion.

@alanruttenberg
Copy link
Contributor

@phismith (personal email) says first and last instant are part of temporal region. It seems this would imply no open (temporally) occurrent, since occupies spatial region and temporally-projects-onto are exact. It also conflicts with #127 (comment) and it would require work on the model since the current model isn't consistent with that change.

@michaelrabenberg
Copy link
Author

michaelrabenberg commented Feb 18, 2025 •
edited
Loading

Hi Alan, I tried writing up the definition I proposed in clif. I wrote this a few days ago and haven't proofread it but I think I got it right the first time...

(cl:comment "first instant of defined [fiod-1]
      (forall (ti tr)
            (iff  (first-instant-of ti tr)
                  (and  (instance-of ti temporal-instant ti)
                        (instance-of tr temporal-region tr)
                        (or   (and  (occurrent-part-of ti tr)
                                    (forall (ti1)
                                          (if   (and  (occurrent-part-of ti1 tr)
                                                      (not  (occurrent-part-of ti ti1)))
                                                (precedes ti ti1))))
                              (and  (not  (exists (ti2)
                                                (and  (occurrent-part-of ti2 tr)
                                                      (forall (ti3)
                                                            (if   (and  (occurrent-part-of ti3 tr)
                                                                        (not  (occurrent-part-of ti2 ti3)))
                                                                  (precedes ti2 ti3))))))
                                    (precedes ti tr)
                                    (not  (exists (ti4)
                                                (and  (instance-of ti4 temporal-instant ti4)
                                                      (precedes ti ti4)
                                                      (precedes ti4 tr)))))))))"
)

@wceusters
Copy link

wceusters commented Feb 18, 2025 •
edited
Loading

Michael,

I converted your axiom to CNF and noticed this one as one of the generated clauses:

[[-1,'first-instant-of',B,C],[-1,'instance-of',A,'temporal-instant',A],[-1,precedes,A,C],[-1,precedes,B,A],[0,'occurrent-part-of',B,C]]

(you can read the '-1' 4-tuples as IF 3-tuples and the '0' as THEN 3-tuple)

So I gave as input for the reasoner, replacing the variables by constants:

t([0,first-instant-of,b,c]).
t([0,instance-of,a,temporal-instant,a]).
t([0,precedes,a,c]).
t([0,precedes,b,a]).

(you can read the '0' in these tuples: it is the case that ... 3-tuple)

The result is an inconsistency. Here is the proof (note: 'BFO-m127' is the index I gave to your axiom):

254	CRT	ERROR	inconsistency				<--	244	 BFO-hew-1	 inc	163			
163	CRT	TRUE	precedes	sk8	sk8		<--	269	 BFO-wff-1	 mpp	58	58	148	
148	CRT	TRUE	precedes	a	a		<--	245	 BFO-ctz-1	 mpp	7	84		
84	CRT	TRUE	precedes	a	b		<--	249	 BFO-wix-1	 mpp	6	26	51	
58	CRT	TRUE	'temporally-projects-onto'	sk8	a		<--	367	 BFO-xco-2	 mpp	14			
51	CRT	TRUE	'occurrent-part-of'	a	a		<--	185	 BFO-hbj-1	 mpp	21			
26	CRT	TRUE	'occurrent-part-of'	b	c		<--	169	 BFO-m127	 mpp	7	6	4	1
21	CRT	TRUE	'instance-of'	a	occurrent	a	<--	684	 BFO-ayr-1	 mpp	10	4	4	
14	CRT	TRUE	'instance-of'	a	'temporal-region'	a	<--	72	 BFO-lqn-1	 mpp	4			
10	CRT	TRUE	'instance-of'	a	occurrent	sk1	<--	247	 BFO-sen-1	 mpp	7			
7	CRT	TRUE	precedes	b	a		<--	0	 unmarked	 input				
6	CRT	TRUE	precedes	a	c		<--	0	 unmarked	 input				
4	CRT	TRUE	'instance-of'	a	'temporal-instant'	a	<--	0	 unmarked	 input				
1	CRT	TRUE	'first-instant-of'	b	c		<--	0	 unmarked	 input

So if this axiom is to be accepted, something else in the BFO2020-FOL axiomatization has to change to remove the inconsistency.

@alanruttenberg
Copy link
Contributor

Hi Alan, I tried writing up the definition I proposed in clif. I wrote this a few days ago and haven't proofread it but I think I got it right the first time...

(cl:comment "first instant of defined [fiod-1]
      (forall (ti tr)
            (iff  (first-instant-of ti tr)
                  (and  (instance-of ti temporal-instant ti)
                        (instance-of tr temporal-region tr)
                        (or   (and  (occurrent-part-of ti tr)
                                    (forall (ti1)
                                          (if   (and  (occurrent-part-of ti1 tr)
                                                      (not  (occurrent-part-of ti ti1)))
                                                (precedes ti ti1))))
                              (and  (not  (exists (ti2)
                                                (and  (occurrent-part-of ti2 tr)
                                                      (forall (ti3)
                                                            (if   (and  (occurrent-part-of ti3 tr)
                                                                        (not  (occurrent-part-of ti2 ti3)))
                                                                  (precedes ti2 ti3))))))
                                    (precedes ti tr)
                                    (not  (exists (ti4)
                                                (and  (instance-of ti4 temporal-instant ti4)
                                                      (precedes ti ti4)
                                                      (precedes ti4 tr)))))))))"
)

The model fails with it. Not sure if its the axiom's fault or the model's fault. The below basically finds a counterexample and substitutes it in the formula, showing how the counterexample plays out.

(:forall-false (0dt3 01dt)
 (:iff-false (:false (has-first-instant 01dt 0dt3))
  (:and-true (:true (instance-of 0dt3 temporal-instant 0dt3))
   (:true (instance-of 01dt temporal-region 01dt))
   (:or-true
    (:and-false (:false (occurrent-part-of 0dt3 01dt))
     (:forall-true (0dt2)
      (:implies-true
       (:and-false (:false (occurrent-part-of 0dt2 01dt))
        (:not-true (:false (occurrent-part-of 0dt3 0dt2))))
       (:false (precedes 0dt3 0dt2)))))
    (:and-true (:true (precedes 0dt3 01dt))
     (:not-true
      (:exists-false (?ti4)
       (:and (instance-of ?ti4 temporal-instant ?ti4)
        (precedes 0dt3 ?ti4) (precedes ?ti4 01dt)))))))))

If you look at the model you can try to figure it out, but Werner's comment suggests it might be the axiom.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@alanruttenberg @phismith @wceusters @michaelrabenberg