Re: completeness of the relational lattice

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> = (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)

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 as

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