# ISSUE-578: Use of "equivalent" incompatible with common uses of the term in logic/mathematics

## Use of "equivalent" incompatible with common uses of the term in logic/mathematics

State:
CLOSED
Product:
prov-dm-constraints
Raised by:
James Cheney
Opened on:
2012-10-25
Description:
A sub-issue of ISSUE-576.

From Antoine Zimmermann's email:

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.

...

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.
Related Actions Items:
No related actions
Related emails:
1. Re: PROV-WG response to comments on constraints (from jcheney@inf.ed.ac.uk on 2012-11-06)
2. Re: PROV-WG response to comments on constraints (from jcheney@inf.ed.ac.uk on 2012-11-01)
3. Re: PROV-WG response to comments on constraints (from antoine.zimmermann@emse.fr on 2012-11-01)
4. PROV-WG response to comments on constraints (from jcheney@inf.ed.ac.uk on 2012-11-01)
5. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from l.moreau@ecs.soton.ac.uk on 2012-11-01)
6. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from jcheney@inf.ed.ac.uk on 2012-11-01)
7. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from l.moreau@ecs.soton.ac.uk on 2012-11-01)
8. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from jcheney@inf.ed.ac.uk on 2012-11-01)
9. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from p.t.groth@vu.nl on 2012-11-01)
10. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from jcheney@inf.ed.ac.uk on 2012-10-31)
11. Re: Reminder: Review of responses to PROV-CONSTRAINTS public comments (from l.moreau@ecs.soton.ac.uk on 2012-10-31)
12. Reminder: Review of responses to PROV-CONSTRAINTS public comments (from jcheney@inf.ed.ac.uk on 2012-10-31)
13. Review of PROV-CONSTRAINTS issues (ISSUE-576, ISSUE-580, ISSUE-577, ISSUE-578, ISSUE-581) (from jcheney@inf.ed.ac.uk on 2012-10-29)
14. PROV-ISSUE-578 (equivalence): Use of 'equivalent' incompatible with common uses of the term in logic/mathematics [prov-dm-constraints] (from sysbot+tracker@w3.org on 2012-10-25)