# Re: completeness of the relational lattice

Date: Wed, 27 Jun 2007 20:42:20 -0000

Message-ID: <1182976940.199959.74900_at_w5g2000hsg.googlegroups.com>

On 27 jun, 19:14, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:

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

Indeed. And you can also verify that it is the criterium that allows exactly all correct rewrites by checking all remaining variables that are not in there:

- Having a variable that is in B and C and not in A gives a counterexample.

A() \/ (B(u) /\ C(u)) != (A() \/ B(u)) /\ (A() \/ C(u))

- Having a variable that is in A and C and not in B gives a counterexample.

A(v) \/ (B() /\ C(v)) != (A(v) \/ B()) /\ (A(v) \/ C(v))

- Having a variable that is in A and B and not in C gives a counterexample.

A(w) \/ (B(w) /\ C()) != (A(w) \/ B()) /\ (A(w) \/ C())

And these were all the types of variables that were not already in the criterium, so it is provably exactly right.

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

Fair enough. Although I'm beginning to suspect it might require a new axiom. :-(

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

Ok. That is very good to hear, of course.

I'm currently busy with checking in proofs that I already had if I falsely used the incorrect distribution law. Especially to see if I need new axioms because of that.

- Jan Hidders