Re: completeness of the relational lattice

On 29 jun, 22:40, Jan Hidders <hidd..._at_gmail.com> wrote:
> On 29 jun, 18:20, Vadim Tropashko <vadimtro_inva..._at_yahoo.com> wrote:
>
> > On Jun 28, 3:41 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
>
> > > > > I invite you to challenge me to show that it can prove an equation
> > > > > that holds. Of course you should also check if all these equations can
> > > > > be derived by you.
>
> > One more challenge:
>
> > <xy> + S + Q = <xy> + S
>
> > where S * [] = [z], and Q header is unconstrained. (I don't see axioms
> > about the lattice bottom element:-)
>
> Sorry. The rules axiomatize the algebra for relations with finite
> headers. When I redid parts of the completeness proof with the
> corrected distribution rule new axioms for W kept on popping up, so I
> decided to do the proof first without W. Once it's completely done I
> might try to put it back in.

I had a brief look and perhaps it's not so bad. It seems only the following rules are required for the introduction of W:

(32a)  W + [] = <>
(32b)  W + [x] = <x>             with x a single attribute
(55)   W * <x> = W               with x a single attribute
(56)   W + (r * s) = (W + r) * (W + s)

• Jan Hidders