Re: TRUE and FALSE values in the relational lattice

From: Jan Hidders <hidders_at_gmail.com>
Date: Thu, 21 Jun 2007 10:14:23 -0000

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.

```- 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
```
the empty set)
```- 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)

```

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
Received on Thu Jun 21 2007 - 12:14:23 CEST

Original text of this message