Re: Relational lattice completeness
Date: 23 Apr 2006 12:41:58 -0700
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
finite models. Dokl. Akad. Nauk SSSR, 70:596--572, 1950. English translation in:
AMS Transl. Ser. 2, vol.23 (1063), 1--6.
- Jan Hidders