PROV-ISSUE-578 (equivalence): Use of "equivalent" incompatible with common uses of the term in logic/mathematics [prov-dm-constraints]

PROV-ISSUE-578 (equivalence):  Use of "equivalent" incompatible with common uses of the term in logic/mathematics  [prov-dm-constraints]

http://www.w3.org/2011/prov/track/issues/578

Raised by: James Cheney
On product: prov-dm-constraints

A sub-issue of ISSUE-576.

>From Antoine Zimmermann's email:
http://lists.w3.org/Archives/Public/public-prov-comments/2012Oct/0004.html

To give an example before getting into the details, let us examine the notion of PROV-equivalence, in Section 2.4. Equivalence is a well known and understood notion in maths and logics, which is necessarily reflexive. In PROV, equivalence isn't reflexive! For X to be PROV-equivalent to Y, it is required that both X and Y are PROV-valid, which is the PROV term used to say "consistent".
...


"""
[...] to be considered equivalent, the two instances must also be valid
"""

This is very strange, as "equivalence" is defined as a non-reflexive relationship. Again, the definition of equivalence would simply follow from a proper formalisation in FOL or model theory.

Moreover, again, the paragraph strongly suggests relying on "applying" normalisation to check equivalence.

See comments on Section 6.1.

...

In this section, "equivalence" does not require validity, as opposed to Section 2.4.

Equivalence is defined according to the notion of isomorphic normal form, which is never normatively defined (the only definition being in the non-normative Section 2.4). In any case, there is no reason to rely on isomorphims at all, if only the logic of PROV was properly defined.

Unfortunately, since equivalence is given in terms of normal forms, and normal forms are given purely in procedural terms, there can be no sensible justification for 2 instances to be non-equivalent. The justification would be "because the procedure gave us different results", which isn't satisfactory at all. This is again a drawback of not providing an appropriate logical account of PROV statements.

Received on Thursday, 25 October 2012 16:15:16 UTC