# Re: completeness of the relational lattice

Date: Wed, 27 Jun 2007 21:17:11 GMT

Message-ID: <rtAgi.7101$Rw1.5485_at_newssvr25.news.prodigy.net>

"Vadim Tropashko" <vadimtro_invalid_at_yahoo.com> wrote in message
news:1182964456.876858.28340_at_g37g2000prf.googlegroups.com...

> 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
**>
*

While it is true that

exists x: (P \/ Q) implies exists x: P \/ exists x: Q
and

exists x: P \/ exists x: Q implies exists x: (P \/ Q),

isn't it true that

exists x: (P /\ Q) implies exists x: P /\ exists x: Q
but

exists x: P /\ exists x: Q does not imply exists x: (P /\ Q)?

Consequently,

exists x: (P /\ Q) is not equivalent to 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 - 23:17:11 CEST