Re: completeness of the relational lattice
Date: Wed, 27 Jun 2007 20:42:20 -0000
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) \/
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