- From: Graham Klyne <GK@ninebynine.org>
- Date: Thu, 29 Sep 2011 14:01:23 +0100
- To: public-prov-wg@w3.org

James, Thanks for pointing out this to me. #g -- On 29/09/2011 12:07, James Cheney wrote: >> <aside> >> My suggested definition of IVPof might be something like this: >> >> A IVPof B iff forall p : (Entity -> Bool) . p(B) => p(A) >> >> where A, B are Entities, and the values of p are predicates on Entities. >> </aside> >> > > Hi Graham, > > Just to pick on this specifically, this definition may be too strong. In ordinary higher-order logic or type theory, the right-hand side of the above definition is called "Leibniz equality" - it is reflexive, symmetric and transitive. The non-obvious part is symmetry. Suppose A IVPof B. Take p = \lambda x. B IVPof x. Then since B IVPof B, clearly also B IVPof A. > > One way to avoid this is to be more careful about what p can be , since the symmetry above results from instantiating p with a predicate involving IVPof. For example, if p : Entity -> Bool is restricted to, say, Boolean combinations of formulas involving attributes and values, then this would be fine. > > --James

Received on Thursday, 29 September 2011 14:34:49 UTC