Re: TRUE and FALSE values in the relational lattice

On 19 jun, 22:32, Marshall <marshall.spi..._at_gmail.com> wrote:
>
>
>
> I am thinking about formalizing the lattice logic. That would
> involve a formal statement of the axioms and the rules of
> inference. We would then want a soundness proof, and
> a proof of consistency. We would also want to understand
> how complete such a logic would be, and how strong it
> was relative to FOL. And how decidable. My hope is
> that it is decidable even if that means it is weaker than
> FOL. We also have to think about what else besides
> & and | we're putting in to it. Clearly 00 is a strong
> candidate. I'm currently thinking that the negation
> operator I defined a week or two ago is *not* a good idea.
> The scary one is division/group by.

I would assume the following operations: (in yet another notation)

- E * E : natural join
- E + E : generalized union
- {()} : the relation with empty header and a single empty tuple
- [A,B,..D] : the empty relation with header {A, B, ..., D} (possibly

- A=B : the equality relation with header {A, B}
- A=c : the relation with header {A} and tuple (A:c)
- R : a relation with name R (and known header)

That would be roughly equivalent with unions of conjunctive queries, for which equivalence is known to be decidable. Adding the set difference or division would make it relationally complete (so, FOL) and make this undecidable.

Actually, a (sound and complete) axiomatization would be a small but publishable result. It doesn't seem that impossible either. You could start with showing that you have enough rules to bring the thing into some union normal form, and then show that you also have enough rules to show a homomorfisme over the conjuncts. Quite interesting indeed. Anyone interested in thinking about a paper on that?

• Jan Hidders