Re: Relational lattice completeness

Marshall Spight wrote:
> Jan Hidders wrote:
> > Mikito Harakiri wrote:
> > >
> > > AFIR you mentioned long time ago that there is some kind of
> > > incompleteness result for RA. Do you have any reference? (Then it would
> > > be clear for me what kind of completeness you have in mind.)
> >
> > I'm not sure I said that, but there is a strongly related result about
> > the undecidability of equivalence of two relational algebra
> > expressions. But I suspect that is not going to help you much.
>
> I would like to second Mikito's request for a citation for this.
> For one thing, I now have this idea in my head that the
> equivalence of two RA expressions is undecidable, but
> no actual way to back that idea up.

It's a direct consequence of the fact that the satisfiability of a first-order logic formula over finite structures is undecidable. Just ask if it is not clear to you why this is a consequence. The usual references for the FOL result may not be what you wanted but I'll give them anyway:

W. Craig. Incompletability, with respect to validity in every finite nonempty domain, of first ­order functional calculus. In Proceedings of the International Congress of
Mathematicians, page 721, Cambridge, Mass., 1950.

B.A. Trakhtenbrot. The impossibility of an algorithm for the decision problem for
finite models. Dokl. Akad. Nauk SSSR, 70:596--572, 1950. English translation in:
AMS Transl. Ser. 2, vol.23 (1063), 1--6.

• Jan Hidders