Re: completeness of the relational lattice

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