Re: completeness of the relational lattice

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.

Of course, you might also try to proof this yourself. The tactic would be to show that there are enough axioms to rewrite any expression to either an expression r without W or to the form r * W where r contains no W. If you can show this then completeness of the algebra with W follows from the completeness of the current algebra.

• Jan Hidders