Comment of [csk-1] a tiny bit inadequate

[wceusters]

  (cl:comment "If a occurrent-part-of b then if a is an instance of process then b is an instance of process [csk-1]"
    (forall (p q)
     (if (occurrent-part-of p q)
      (if (exists (t) (instance-of p process t))
       (exists (t) (instance-of q process t))))))

To reflect the axiom accurately, the comment should be: If a occurrent-part-of b then if a is an instance of process at some time, then b is an instance of process at some time.
Although for both instantiation assertions the existentially quantified variable 't' is used, FOL does not require these variables to have the same individual as values. The comment reflects nevertheless a fact in light of (at least) [ayr-1] which states: No occurrent changes type during its existence.

[alanruttenberg]

what is inadequate about it

[wceusters]

You probably read the comment just after I posted it without the explanation just to check whether I got the trick with the back quotes correct to keep the indentations. When I saw it worked, I edited the post further. You were too fast this time :-)

[michaelrabenberg]

Werner, is it that you want this instead?

"If a occurrent-part-of b then if there's a time at which a is an instance of process then there's a time at which b is an instance of process [csk-1]"

I think many axioms' comments don't make that sort of temporal existential quantification stuff explicit.

EDIT: Just saw your edit.

[wceusters]

Werner, is it that you want this instead?

"If a occurrent-part-of b then if there's a time at which a is an instance of process then there's a time at which b is an instance of process [csk-1]"

I think many axioms' comments don't make that sort of temporal existential quantification stuff explicit.

EDIT: Just saw your edit.

Also too fast! :-)
Well, I know many people just read the Excel files with the comments, and not the axioms. If the comments don't cover the axioms exactly and vice versa, then that may create wrong assumptions. I have been on the wrong track too many times by being lazy in that way, so therefore just this remark.

[alanruttenberg]

Stating the axiom in that way, IMO, will confuse things more than clarify. That there are two temporal regions is irrelevant and distracting. Occurrents don't change type. The (:exists(t) (instance-of instance class t)) pattern is the only way to check a type, if there's no specific time that is relevant. Maybe if I did it again I would use a time-independent instance-of predicate. I suppose it could also be rewritten as

  (forall (p q t)
    (if (occurrent-part-of p q)
      (if (instance-of p process t))
         (instance-of q process t)))))

As it happens the snippet is generated by a macro. In the source code it is

(relation-argument-implication (occurrent-part-of process process) :kind :occurrent-mereology)

What you see is the macro expansion. The macro expands differently if called between two temporal regions because we don't have to introduce a new temporal region. The macro is used in a few places, so it would take work to make sure this rewrite is done only when appropriate since I'd have to review each use.

(relation-argument-implication (temporal-part-of one-dimensional-temporal-region one-dimensional-temporal-region) :kind :temporal-region)

Expands to

(:forall (?p ?q)
  (:implies (temporal-part-of ?p ?q)
      (:implies
          (instance-of ?p one-dimensional-temporal-region ?p)
          (instance-of ?q one-dimensional-temporal-region ?q))))

[wceusters]

I suppose it could also be rewritten as

  (forall (p q t)
    (if (occurrent-part-of p q)
      (if (instance-of p process t))
         (instance-of q process t)))))

The third line would then have a condition without a consequence.
But when corrected as such:

 (forall (p q t)
    (if (occurrent-part-of p q)
      (if (instance-of p process t)
         (instance-of q process t))))

then it is indeed better (to my taste at least) because transformation to CNF does not change the semantics as no skolems ought to be generated.

Maybe if I did it again I would use a time-independent instance-of predicate.

You mean only for occurrents, I hope. Doing it also for continuants would be a sin and I would toss BFO in the garbage.

[alanruttenberg]

You mean only for occurrents, I hope. Doing it also for continuants would be a sin and I would toss BFO in the garbage.

Yes of course. I resisted using both (instance-of x ) and (instance-of x t) because I thought it clearer if there were not predicate names meant different things depending on their arity. That's something that I might reconsider.

We can keep this issue open as a reminder that it would be nice to do the universal vs existential for of this and similar axioms

[wceusters]

Good. One might also consider to do that for all relations which have at least one continuant as argument.