Re: Some thoughts about the revised provenance Model document

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