Re: completeness of the relational lattice

On Jun 26, 7:03 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
> I suspect that the condition
> for r + (s * t) = (r + s) * (r + t)
> should be A(r) * A(s) = A(r) * A(t) = A(s) * A(t).
> So if two have an attribute, the third must also have it.

This is more powerful condition than in the "First steps..." paper. Indeed, the correct criteria is:

A(x,t) \/ (B(y,t) /\ C(z,t)) = (A(x,t) \/ B(y,t)) /\ (A(x,t) \/ C(z,t))

The proof is by writing down both sides in the set notation. Assuming general relation headers A(x,u,w,t), B(y,u,v,t), C(z,w,v,t) the left hand side works out to be

exists xyzv : A \/ (B /\ C)

The right hand side evaluates to

exists zy : (exists xwv: A \/ B) /\ (exists xuv: A \/ C)

In predicate logic we have

exists x: (P /\ Q) <-> exists x: P /\ exists x: Q

so that attribute x could be moved outside.

So, your proof of (A /\ 00) \/ (A /\ 11) = A is correct, then. Yet, the earlier proof of the equality theorem is not. (So I keep my notation until at least one more spectacular derivation:-)

I agree with your other post. It seems like advancing "the theory of relations with known attributes" is easier at this point than the "theory of general relations". Received on Wed Jun 27 2007 - 19:14:16 CEST