# Re: completeness of the relational lattice

Date: Tue, 26 Jun 2007 10:55:50 -0700

Message-ID: <1182880550.168211.271670_at_g37g2000prf.googlegroups.com>

On Jun 26, 12:53 am, Jan Hidders <hidd..._at_gmail.com> wrote:

> On Jun 26, 12:29 am, Vadim Tropashko <vadimtro_inva..._at_yahoo.com>

*> > So you have axiom schemas, instead of a single axiom system? I don't
**> > challenge this approach, but think that a single axiom system is
**> > workable as well (see below).
**>
**> It's a schema anyway because you still have relation variables.
**> Although I agree that I need two types of variables, or three if you
**> count the singleton attributes, and you have one (or two if you have
**> special ones for singleton sets, as you suggest later). On the other
**> hand, I only have equations, and you need propositional formulas over
**> equation.
*

I'm not sure I understand. I see "if" all over the place in your axiom system -- you must have propositions there as well. I had a quantifier in one place where I wanted to introduce atomic attribute, but this can be avoided (see below).

> > > Your suggestion might work, but you would have to first formalize what

*> > > your inference mechanism is before we can start thinking about it.
**> > > Right now my formalism is quite simple. It derives r = s iff it can
**> > > rewrite r to s with the given axioms. Yours would probably be much
**> > > more complicated than that. Can you give a formal definition of yours?
**>
**> > OK, I have relation variables, 5 constants 00, 01, 10, 11, 1E, and two
**> > binary operations \/, /\, and the inequlity Y <= X abbreviation for X /
**> > \ Y = X. Axioms:
**>
**> > 1-8. Lattice axioms
**> > 9. Spight criteria:
**> > (R/\00) \/ (S/\00) <= Q/\00 and (R/\00) \/ (Q/\00) <= S/\00 implies
**> > (R /\ S) \/ (R /\ Q) = R /\ (S \/ Q)
**> > 10. (R/\00) \/ (Q/\00) <= R/\00 implies
**> > (R /\ S) /\ (R \/ Q) = R \/ (S /\ Q)
**> > 11. 01 <= R <= 10
**> > 12. R = (00 /\ R) \/ (11 /\ R)
**> > 13. Universal equality relation 1E axioms.
**>
**> You found those already?
*

Let's translate your axioms 26-31 in terms of 1E (no special meaning of square brackets in my notation other than easy reading):

<H> + [S] = (def) (1E \/ [H /\ 00]) \/ [S /\ 00] = (distr) (1E \/ [(H \/ S) /\ 00] = (def)

<H * S>

[H] * <S> = (def)

[H /\ 00] /\ (1E \/ [S /\ 00]) = (idemp, assoc)
H /\ 00 /\ (00 /\ (1E \/ [S /\ 00])) = ( A -> 00 /\ A homomorhism )
[H /\ 00] /\ [00 /\ 1E] \/ [S /\ 00])) = ( A -> 00 /\ A homomorhism,
again )

00 /\ (H \/ 1E \/ S) = (axiom 13a see below) 00 /\ (H /\ S)] = (def)

[H + S]

Axiom 13a: 1E /\ 00 = 10

Axiom #31 is the only fundamental property of equality, which translated in my notation becomes (no special meaning for angled brackets either!)

13b: S /\ 00 = S and H /\ 00 = H and S \/ H != 00 and S /\ H = H'
imply

((R /\ <S \/ 1E>) \/ H) /\ <S \/ 1E> = (R /\ <S \/ 1E>) \/ H'

> > Do you imply that I can't reduce both sides of the expression R = S to

*> > the Union Normal Form in this system?
**>
**> I don't know, you've onlly given axioms and not the inference
**> mechanism. Since they are propositional formulas I assume you want to
**> use propositional calculus.
*

What is the inference mechanism? I thought that we prove equalities by writing down a chain of equations where each step is supported by some axiom.

I'm not sure I understand your comment about propositional calculus -- sure your system have implications and therefore derives equalities by rules of propositional calculus as well.

> If you add this you can no longer claim

*> that you have a pure algebraic axiomatization, which makes the
**> completeness claim less interesting. But is propositional calculus all
**> you allow, or are you also allowing reasoning by rewriting? The latter
**> can be captured in either your inference mechanism or by adding adding
**> extra axioms (e.g. the rules "if R = R' and S = S' then R /\ S = R' /\
**> S'" and "if R = S and S= T then S = T" and ... ). There is the usual
**> trade off between putting your inference in the axioms or in the
**> inference mechanism.
*

Again as soon as propositional claculus is used implicitly I don't see the difference between your and my systems. Perhaps you can reveal inference rules of your system so that I can see the difference?

> Btw. what I did wonder about is how you would derive "if R1(x,y) /\ 00

*> = R1(x,y) and R2(x,y) /\ 00 = R2(x,y) then R1(x,y) /\ [] = R2(x,y) /\
**> []".
*

R1 /\ 00 = X /\ Y /\ 00 (R1 has a set of attributes X and Y) R2 /\ 00 = X /\ Y /\ 00 (R2 has a set of attributes X and Y aswell)

therefore

R1 /\ 00 = R2 /\ 00

The fact that R1 /\ 00 = R1 is irrelevant, although can be leveraged to further derive R1 = R2.

> > > Yes, but again this means that you extend your inference mechanism,

*> > > namely with first order logic inference.
**>
**> > OK, if this is a critical showstopper, then I would have to introduce
**> > single attribute relations, conveniently designated with small letters
**> > r,s,t etc. Your rule #28, for example becomes
**>
**> > 28. x /\ 00 <= R /\ 00 implies
**> > R /\ ((x /\ 00) \/ 1E) = R
**>
**> Ok. I think that would work. But also here you have to say how the
**> inference deals with this. How does it know what and what not to match
**> x with when it rewrites? This is solvable, but again it adds
**> complexity to the inference mechanism.
*

Actually, there is no need for explicit single attribute relations (see below).

> > Can you please derive

*>
**> > (((R(x,y) * <yz>) + [xz]) * <yz>) + [xy] = R(x,y)
**>
**> > in your system?
**>
**> Sure. (I'm skipping rewrites involving shifting brackets):
**>
**> (((R(x,y) * <yz>) + [xz]) * <yz>) + [xy]
**> = (((R(x,y) * <yz>) + [xz]) * <yz> * <yz>) + [xy] (1)
**> = (((R(x,y) * <yz>) + [xyz]) * <yz>) + [xy] (31)
**> = (R(x,y) * <yz> * <yz>) + ([xyz] * <yz>) + [xy] (8)
**> = (R(x,y) * <yz>) + ([xyz] * <yz>) + [xy] (1)
**> = ((R(x,y) * <yz>) + [xyz] + [xy] (29)
**> = ((R(x,y) * <yz>) + [xy] (12)
**> = (R(x,y) + [xy]) * (<yz> + [xy]) (9)
**> = (R(x,y) + [xy]) * <y> (26)
**> = R(x,y) * <y>
**> (10)
**> =
**> R(x,y)
**> (28)
*

OK now you earned your notation. If you also derive (R /\ 00) \/ (R /\ 11) = R, I would be totally sold out.

I admit that generalizing your axiom #31 getting rid of the single attribute condition is quite clever. Leveraging on this idea a little bit more, can we just define single attribute relation "x" as the one satisfying the following constraint:

<x> /\ R = R if x*[R]=[R] (in your notation)

(x /\ 1E) \/ (x /\ 00) = x (in my notation)

Again, there is no single attribute relation premise in my system! Received on Tue Jun 26 2007 - 19:55:50 CEST