DTV — CLIF Logic Errors

Various logical errors in the CLIF axioms need correction:

1. In clause E.1.2, the axiom under concept "sequence is of concept" reads:

(forall ((member thing) (s sequence))
(exists ((c concept))
(iff ("sequence is of concept" s c)
(if "member participates in sequence" member s)
("concept corresponds to instance" c member)))))

and should probably read:

(forall (s sequence)
(exists (c concept)
(iff ("sequence is of concept" s c)
(forall (member thing)
(if ("member participates in sequence" member s)
("concept corresponds to instance" c
member))))))
2. Several of the verb concepts in clause E.1.5 range specifically over "unique sequences". In several cases, the axioms are not written to match the concept types that the roles range over.

The formulations in (1) are logically equivalent, but neither is the definition of ‘sequence is of concept’. Issue 17225 points out that the structure of the definitions in Annex D is generally poor. The text that resolves this issue is included in that resolution.

Revised Text:
none.

Disposition: Merged with Issue 17225