Quote from tobega on June 18, 2021, 2:03 pm

Quote from AntC on June 18, 2021, 10:41 am

Quote from tobega on June 18, 2021, 4:56 am

Quote from AntC on June 18, 2021, 2:39 am

Quote from Vadim on June 17, 2021, 8:33 pm

Which is why I have asked you for your definition of "NOT MATCHING".

From here (from one of Vadim's papers)

• (r1 NatJoin r2) InnerUnion (r1 NotMatching r2) = r1;
• (r1 NatJoin r2) NatJoin    (r1 NotMatching r2) = DUM NatJoin (r1 NatJoin r2); = emptify( r1 NatJoin r2 );

Note that is for all r1, r2: NotMatching, like NatJoin, InnerUnion must produce a well-defined result for any relation operands. There's no expectation the operands need have any attributes in common, nor tuples in common (after projecting on to attributes in common).

Vadim's paper claims those two simultaneous equations 'fix' NotMatching uniquely. But since he fails to fix DUM, that demo is moot.

True, in the general case. But I could propose a value in a particular case that "works like DUM".

So let's go with the set of all relations that have attribute A and that all contain the TUPLE {A=1}. We could also if we wish restrict A's set of possible values to 1, 2 and 3.

So I propose that the element that acts like DUM is RELATION{TUPLE{A=1}}, lets call it Aum

Now we want to see what Aum NOT MATCHING Aum is. So from above then, we get:

• (Aum NatJoin Aum) InnerUnion (Aum NotMatching Aum) = Aum
• (Aum NatJoin Aum) NatJoin (Aum NotMatching Aum) = Aum NatJoin (Aum NatJoin Aum)

So pretty clear that (Aum NotMatching Aum) = Aum works

Let A2 = RELATION{TUPLE{A=1}, TUPLE{A=2}}

• (A2 NatJoin A2) InnerUnion (A2 NotMatching A2) = A2
• (A2 NatJoin A2) NatJoin (A2 NotMatching A2) = Aum NatJoin (A2 NatJoin A2)

Again we see that (A2 NotMatching A2) = Aum fits the bill. So this may work, with Aum playing the role of DUM.

But there could be more worrying deviant sets that also conform to the rules of the model as stated, taking an example from wikipedia (and please let me know if there is a rule in the model I'm contradicting):

• We have some elements with opaque structure: I think I'll try the positive integers.
• We have an operation called InnerUnion that returns the supremum of two elements: I'll choose GCD as my InnerUnion operation
• We have an operation called NatJoin that returns the infimum of two elements: I'll choose LCM for that.
• Lattice top is called DEE: looks like that corresponds to 1

So far so good? Now we want to find an element corresponding to DUM?

Quote from Vadim on June 18, 2021, 4:50 pm

Quote from AntC on June 18, 2021, 2:39 am

Hi Vadim, your demo doesn't look right to me. DUMPTY is the relation with all atributes, empty body. That's your R10. Your demo 1 uses R01 -- that's DEE; and emptify(R01) = R01 is not a theorem for DEE, in fact it's always false.

Your demos 3, 4, 5 use uppercase R, R1, R2; so that's skolems/existentially quantified, whereas @tobega's axioms require forall quantified.

I agree that I made a sloppy copy-and-paste job over there, but still, those assertions are quite easy to prove (even manually).

I also partially agree that it might be possible to introduce the axioms step-by-step. For example, if we have "the fixed" lattice meet operation, then the lattice join is uniquely defined (infix "v", versus functional style "v1"):

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.41 (+ 0.01) seconds.
% Length of proof is 25.
% Level of proof is 6.
% Maximum clause weight is 13.
% Given clauses 189.

1 v1(x,y) = x v y # label(non_clause) # label(goal).  [goal].
2 x ^ y = y ^ x.  [assumption].
4 x ^ (x v y) = x.  [assumption].
5 x v y = y v x.  [assumption].
6 (x v y) v z = x v (y v z).  [assumption].
7 x v (x ^ y) = x.  [assumption].
8 v1(x,y) = v1(y,x).  [assumption].
9 v1(v1(x,y),z) = v1(x,v1(y,z)).  [assumption].
10 v1(x,x ^ y) = x.  [assumption].
11 x ^ v1(x,y) = x.  [assumption].
12 v1(c1,c2) != c1 v c2.  [deny(1)].
17 x ^ (y v x) = x.  [para(5(a,1),4(a,1,2))].
18 (x v y) ^ (x v (y v z)) = x v y.  [para(6(a,1),4(a,1,2))].
21 x v (y ^ x) = x.  [para(2(a,1),7(a,1,2))].
28 v1(x,v1(y,z)) = v1(y,v1(x,z)).  [para(8(a,1),9(a,1,1)),rewrite([9(2)])].
29 v1(x,y ^ x) = x.  [para(2(a,1),10(a,1,2))].
36 x ^ v1(y,x) = x.  [para(8(a,1),11(a,1,2))].
63 x v v1(x,y) = v1(x,y).  [para(11(a,1),21(a,1,2)),rewrite([5(2)])].
67 v1(x,x v y) = x v y.  [para(4(a,1),29(a,1,2)),rewrite([8(2)])].
71 v1(x,y v x) = y v x.  [para(17(a,1),29(a,1,2)),rewrite([8(2)])].
78 x v v1(y,x) = v1(y,x).  [para(36(a,1),21(a,1,2)),rewrite([5(2)])].
153 (x v y) ^ (x v v1(y,z)) = x v y.  [para(63(a,1),18(a,1,2,2))].
3862 (x v y) ^ v1(y,x) = x v y.  [para(78(a,1),153(a,1,2))].
3899 v1(x,y) = y v x.  [para(3862(a,1),29(a,1,2)),rewrite([8(3),28(3),8(2),67(2),71(2)]),flip(a)].
4092 $F.  [back_rewrite(12),rewrite([3899(3),5(3)]),xx(a)].

============================== end of proof ==========================

However, there is implicit assumption in this step-by-step approach: the meet semilattice is considered as fixed or, in other words, that the relational natural join is unique.

The related issue is of an axiom system "completeness". Intuitively, if a theory has less assertions, it allows more freedom in the models. This might definitely cause ambiguity; for example, remove the absorption laws, and the lower semilattice becomes independent of the upper one.

There are actually the two parts of the issue: the completeness of the algebraic signature, and the completeness of the axioms in a given signature. Consider the Litak et.al. system

x ^ (y v z) = (x ^ (z v (R00 ^ y))) v (x ^ (y v (R00 ^ z))).
(x ^ y) v (x ^ z) = x ^ ( ((x v z) ^ y) v ((x v y) ^ z) ).
(R00 ^ (x ^ (y v z))) v (y ^ z) = ((R00 ^ (x ^ y)) v z) ^ ((R00 ^ (x ^ z)) v y).

Even if we agree on the [latex]\{\wedge,\vee,R_{00}\}[/latex] signature (which is admittedly quite limited), it captures some relational database theory semantics but not all of it. Here is a conditional assertion from page 10 of Yannakakis&Papadimitou "Algebraic dependencies" paper:

a v b=R00 &
b v c=R00 &
a v c=R00
->
(a^c)v(((a^b)v r)^( (b^c)v( ((a^c)v r)
^
((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) )) ) ) )=
(a^c)v( ((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) ))
^
( (b^c)v(((a^b)v r)^((a^c)v r)) ) ).

It is independent of the Litak et.al. axioms (Mace4 generates counterexample of order 31 which fails to be interpreted as relational universe).

Quote from AntC on June 19, 2021, 4:31 am

Quote from tobega on June 18, 2021, 2:03 pm

Quote from AntC on June 18, 2021, 10:41 am

Quote from tobega on June 18, 2021, 4:56 am

Quote from AntC on June 18, 2021, 2:39 am

Quote from Vadim on June 17, 2021, 8:33 pm

Which is why I have asked you for your definition of "NOT MATCHING".

From here (from one of Vadim's papers)

• (r1 NatJoin r2) InnerUnion (r1 NotMatching r2) = r1;
• (r1 NatJoin r2) NatJoin    (r1 NotMatching r2) = DUM NatJoin (r1 NatJoin r2); = emptify( r1 NatJoin r2 );

Note that is for all r1, r2: NotMatching, like NatJoin, InnerUnion must produce a well-defined result for any relation operands. There's no expectation the operands need have any attributes in common, nor tuples in common (after projecting on to attributes in common).

Vadim's paper claims those two simultaneous equations 'fix' NotMatching uniquely. But since he fails to fix DUM, that demo is moot.

True, in the general case. But I could propose a value in a particular case that "works like DUM".

So let's go with the set of all relations that have attribute A and that all contain the TUPLE {A=1}.

Oh good grief you've 'discovered' a Boolean Algebra with a complement operation. And the thing that "works like DUM" (no it doesn't) is lattice bottom -- that is, the absorbing element for NaturalJoin. So we have a simpler definition for complement:

• r NatJoin compl(r) = DUMPTY;
• r InnerUnion compl(r) = DEE;

This is well-defined and unique within a Boolean Algebra (follows from the definition of Boolean Algebra). And because within a relational lattice you get a sub-lattice that is a Boolean Algebra for all relations with the same heading, you're only demonstrating what we already know within such a sub-lattice.

A lattice having all elements (all relation values) with same heading is not a relational lattice. It can't express 'Suppliers and Parts'; it can't express 'Employees and Departments'.

We could also if we wish restrict A's set of possible values to 1, 2 and 3.

So I propose that the element that acts like DUM is RELATION{TUPLE{A=1}}, lets call it Aum

Now we want to see what Aum NOT MATCHING Aum is. So from above then, we get:

• (Aum NatJoin Aum) InnerUnion (Aum NotMatching Aum) = Aum
• (Aum NatJoin Aum) NatJoin (Aum NotMatching Aum) = Aum NatJoin (Aum NatJoin Aum)

So pretty clear that (Aum NotMatching Aum) = Aum works

Because Aum is lattice bottom; and r NatJoin Aum = Aum for all r. You're not finding anything specific to Aum. Note that with a relational lattice r NotMatching DUM = r = r NotMatching DUMPTY for all r. r NotMatching r does not equal DUM in general, neither does it equal DUMPTY. As would be evident if you actually studied what I said about NotMatching not making restrictions on its arguments.

Let A2 = RELATION{TUPLE{A=1}, TUPLE{A=2}}

• (A2 NatJoin A2) InnerUnion (A2 NotMatching A2) = A2
• (A2 NatJoin A2) NatJoin (A2 NotMatching A2) = Aum NatJoin (A2 NatJoin A2)

Again we see that (A2 NotMatching A2) = Aum fits the bill. So this may work, with Aum playing the role of DUM.

But there could be more worrying deviant sets that also conform to the rules of the model as stated, taking an example from wikipedia (and please let me know if there is a rule in the model I'm contradicting):

• We have some elements with opaque structure: I think I'll try the positive integers.

So you don't have a bottom value? That is, a maximum possible Integer? wikipedia does have an example using 'divisors of 60' Pic 2. Note it is a bounded lattice. The consequence is not all Integers between 1, 60 can appear as elements.

• We have an operation called InnerUnion that returns the supremum of two elements: I'll choose GCD as my InnerUnion operation
• We have an operation called NatJoin that returns the infimum of two elements: I'll choose LCM for that.

No these don't correspond whatsoever to InnerUnion, NatJoin. Use the terms from lattice theory meet, join.

• Lattice top is called DEE: looks like that corresponds to 1

So far so good? Now we want to find an element corresponding to DUM?

Nothing good so far. Please just stop wasting everybody's time. You've picked another example of a symmetric structure -- this time it's a semi-lattice, because there's no bottom (maximum Integer) . So there's nothing corresponding to DUM and for any operation you try to claim is 'relative complement', there'll be either a non-unique result, or no valid result -- for example you don't include rationals in your elements. Or indeed there might be non-unique results for some arguments and no valid result for other arguments. I just can't be bothered to work it out.

Just stop.

Quote from tobega on June 19, 2021, 5:10 am

Quote from AntC on June 19, 2021, 4:31 am

Quote from tobega on June 18, 2021, 2:03 pm

Quote from AntC on June 18, 2021, 10:41 am

Quote from tobega on June 18, 2021, 4:56 am

Quote from AntC on June 18, 2021, 2:39 am

Quote from Vadim on June 17, 2021, 8:33 pm

Which is why I have asked you for your definition of "NOT MATCHING".

From here (from one of Vadim's papers)

• (r1 NatJoin r2) InnerUnion (r1 NotMatching r2) = r1;
• (r1 NatJoin r2) NatJoin    (r1 NotMatching r2) = DUM NatJoin (r1 NatJoin r2); = emptify( r1 NatJoin r2 );

Note that is for all r1, r2: NotMatching, like NatJoin, InnerUnion must produce a well-defined result for any relation operands. There's no expectation the operands need have any attributes in common, nor tuples in common (after projecting on to attributes in common).

Vadim's paper claims those two simultaneous equations 'fix' NotMatching uniquely. But since he fails to fix DUM, that demo is moot.

True, in the general case. But I could propose a value in a particular case that "works like DUM".

So let's go with the set of all relations that have attribute A and that all contain the TUPLE {A=1}.

Oh good grief you've 'discovered' a Boolean Algebra with a complement operation. And the thing that "works like DUM" (no it doesn't) is lattice bottom -- that is, the absorbing element for NaturalJoin. So we have a simpler definition for complement:

• r NatJoin compl(r) = DUMPTY;
• r InnerUnion compl(r) = DEE;

This is well-defined and unique within a Boolean Algebra (follows from the definition of Boolean Algebra). And because within a relational lattice you get a sub-lattice that is a Boolean Algebra for all relations with the same heading, you're only demonstrating what we already know within such a sub-lattice.

A lattice having all elements (all relation values) with same heading is not a relational lattice. It can't express 'Suppliers and Parts'; it can't express 'Employees and Departments'.

We could also if we wish restrict A's set of possible values to 1, 2 and 3.

So I propose that the element that acts like DUM is RELATION{TUPLE{A=1}}, lets call it Aum

Now we want to see what Aum NOT MATCHING Aum is. So from above then, we get:

• (Aum NatJoin Aum) InnerUnion (Aum NotMatching Aum) = Aum
• (Aum NatJoin Aum) NatJoin (Aum NotMatching Aum) = Aum NatJoin (Aum NatJoin Aum)

So pretty clear that (Aum NotMatching Aum) = Aum works

Because Aum is lattice bottom; and r NatJoin Aum = Aum for all r. You're not finding anything specific to Aum. Note that with a relational lattice r NotMatching DUM = r = r NotMatching DUMPTY for all r. r NotMatching r does not equal DUM in general, neither does it equal DUMPTY. As would be evident if you actually studied what I said about NotMatching not making restrictions on its arguments.

Let A2 = RELATION{TUPLE{A=1}, TUPLE{A=2}}

• (A2 NatJoin A2) InnerUnion (A2 NotMatching A2) = A2
• (A2 NatJoin A2) NatJoin (A2 NotMatching A2) = Aum NatJoin (A2 NatJoin A2)

Again we see that (A2 NotMatching A2) = Aum fits the bill. So this may work, with Aum playing the role of DUM.

But there could be more worrying deviant sets that also conform to the rules of the model as stated, taking an example from wikipedia (and please let me know if there is a rule in the model I'm contradicting):

• We have some elements with opaque structure: I think I'll try the positive integers.

So you don't have a bottom value? That is, a maximum possible Integer? wikipedia does have an example using 'divisors of 60' Pic 2. Note it is a bounded lattice. The consequence is not all Integers between 1, 60 can appear as elements.

• We have an operation called InnerUnion that returns the supremum of two elements: I'll choose GCD as my InnerUnion operation
• We have an operation called NatJoin that returns the infimum of two elements: I'll choose LCM for that.

No these don't correspond whatsoever to InnerUnion, NatJoin. Use the terms from lattice theory meet, join.

• Lattice top is called DEE: looks like that corresponds to 1

So far so good? Now we want to find an element corresponding to DUM?

Nothing good so far. Please just stop wasting everybody's time. You've picked another example of a symmetric structure -- this time it's a semi-lattice, because there's no bottom (maximum Integer) . So there's nothing corresponding to DUM and for any operation you try to claim is 'relative complement', there'll be either a non-unique result, or no valid result -- for example you don't include rationals in your elements. Or indeed there might be non-unique results for some arguments and no valid result for other arguments. I just can't be bothered to work it out.

Just stop.

You're still entirely missing the point.

Your model only reflects the aspects that are encoded in it. Mathematically there is absolutely no connection between relational algebra and your model, other than that your model reflects the mathematical aspects of relational algebra that they have in common.

For your model to work, it needs to work for ANY choice of values and functions that are consistent with the rules you lay out.

Quote from tobega on June 19, 2021, 5:52 am

Even though your mind is still resisting what I'm saying, I'll give you a possible way (if your prover allows it) to introduce the structure we expect a relational lattice to have (and I have no illusion that this might be perfect or complete yet):

Lets define a lattice (or a semi-lattice depending on whether "the set of all attributes" is finite or infinte, I don't see it really matters) called H, with a supremum called Intersect and an infimum Union (and in our minds the elements work like sets)

Also define our lattice (or semi-lattice) of relations, R, with supremum InnerUnion and infimum NatJoin such that there exists a surjection (called heading) from R to H, i.e. for all Rn in R there exists an Hk in H such that heading(Rn) = Hk.

Further, heading(R1 InnerUnion R2) = heading(R1) Intersect heading(R2) and heading(R1 NatJoin R2) = heading(R1) Union heading(R2) for all R1,R2

For each Hk, the elements of Rn of R where heading(Rn) = Hk must form a (semi-)lattice under InnerUnion and NatJoin, call it RHk

Let the lattice-top of H be H0, then we let the lattice-bottom of RH0 be DUM and the lattice-top of RH0 be DEE

Now I'll stop (maybe).

Quote from AntC on June 19, 2021, 12:01 pm

Quote from Vadim on June 18, 2021, 4:50 pm

 

I also partially agree that it might be possible to introduce the axioms step-by-step. For example, if we have "the fixed" lattice meet operation, then the lattice join is uniquely defined (infix "v", versus functional style "v1"):

Yes, it's the absorption law(s) that fixes them together.

However, there is implicit assumption in this step-by-step approach: the meet semilattice is considered as fixed or, in other words, that the relational natural join is unique.

Commutative, idempotent, associative is sufficient to fix the 'meet'. wikipedia  says the idempotence is usually derived as a consequence of the absorption laws. But I take idempotence as axiomatic for meet === NaturalJoin, and can then derive uniqueness of meet, as you show for lattice join === InnerUnion.

The related issue is of an axiom system "completeness". Intuitively, if a theory has less assertions, it allows more freedom in the models. This might definitely cause ambiguity; for example, remove the absorption laws, and the lower semilattice becomes independent of the upper one.

Beware saying that with untutored ears in this discussion: it's very possible to add gazillions of assertions without changing/limiting the model at all. That is, if the assertions are merely consequences of the axioms already adopted. @tobega seems to have a small cottage industry of adding unhelpful assertions (unhelpful because already consequences).

There are actually the two parts of the issue: the completeness of the algebraic signature, and the completeness of the axioms in a given signature. Consider the Litak et.al. system

x ^ (y v z) = (x ^ (z v (R00 ^ y))) v (x ^ (y v (R00 ^ z))).
(x ^ y) v (x ^ z) = x ^ ( ((x v z) ^ y) v ((x v y) ^ z) ).
(R00 ^ (x ^ (y v z))) v (y ^ z) = ((R00 ^ (x ^ y)) v z) ^ ((R00 ^ (x ^ z)) v y).

Even if we agree on the [latex]\{\wedge,\vee,R_{00}\}[/latex] signature (which is admittedly quite limited), it captures some relational database theory semantics but not all of it.

Specifically, it fails to fix DUM aka R00 -- so from previous discussions with Litak, he conceded those axioms are incomplete. But he wouldn't consider non-positive axioms (like asserting DUM ≠ DEE) so we seem to be stuck. If we could fix DUM in terms of NatJoin, InnerUnion, we wouldn't need to include it in the signature -- as we don't need to include DEE because it's merely the identity for NatJoin.

 

Here is a conditional assertion from page 10 of Yannakakis&Papadimitou "Algebraic dependencies" paper:

Are you sure that's the right link? I see nothing like that on page 10 -- or indeed in the whole paper. They don't seem to have an InnerUnion; they don't seem to have a DUM/R00. 1982 would be before anybody 'discovered' DUM, wouldn't it?

a v b=R00 &
b v c=R00 &
a v c=R00
->
(a^c)v(((a^b)v r)^( (b^c)v( ((a^c)v r)
^
((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) )) ) ) )=
(a^c)v( ((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) ))
^
( (b^c)v(((a^b)v r)^((a^c)v r)) ) ).

It is independent of the Litak et.al. axioms (Mace4 generates counterexample of order 31 which fails to be interpreted as relational universe).

The antecedent a v b=R00 & b v c=R00 & a v c=R00 -> ... means that a, b, c are all empty (and have mutually disjoint headings). That's hardly a useful place to start -- especially to generate such a monster consequent. Can't we say that the sub-lattice of empty relations is a Boolean algebra?

Quote from tobega on June 19, 2021, 4:25 pm

Quote from tobega on June 19, 2021, 5:52 am

Even though your mind is still resisting what I'm saying, I'll give you a possible way (if your prover allows it) to introduce the structure we expect a relational lattice to have (and I have no illusion that this might be perfect or complete yet):

Lets define a lattice (or a semi-lattice depending on whether "the set of all attributes" is finite or infinte, I don't see it really matters) called H, with a supremum called Intersect and an infimum Union (and in our minds the elements work like sets)

Also define our lattice (or semi-lattice) of relations, R, with supremum InnerUnion and infimum NatJoin such that there exists a surjection (called heading) from R to H, i.e. for all Rn in R there exists an Hk in H such that heading(Rn) = Hk.

Further, heading(R1 InnerUnion R2) = heading(R1) Intersect heading(R2) and heading(R1 NatJoin R2) = heading(R1) Union heading(R2) for all R1,R2

For each Hk, the elements of Rn of R where heading(Rn) = Hk must form a (semi-)lattice under InnerUnion and NatJoin, call it RHk

Let the lattice-top of H be H0, then we let the lattice-bottom of RH0 be DUM and the lattice-top of RH0 be DEE

Now I'll stop (maybe).

To complete the surjection we also need to specify that for each Hk in H there exists some Rn in R such that heading(Rn) = Hk

Surprisingly, this does not introduce the concept of emptiness that I recently thought might be necessary, but it does introduce more structure. I guess we'll see if emptiness is needed. Certainly, any relationally complete universe will have it, whether it be defined or not.

So this model will still allow us working with the set of all empty relations, where DUM also acts as DEE. This makes some sense, I suppose, since in the world where everything is false, even true must be false.

Just for fun, it turns out that the positive integers with GCD and LCM still work in the model, with H being the set of unique prime factors in the number. But now we know how to find whatever corresponds to "DUM" in that universe, it is 1 (surprisingly, because I tried to use this as an example to illustrate a universe where there was nothing corresponding to DUM). The function "NotMatching", according to definitions given previously, ends up being uniquely defined in that universe as the function that returns its left operand. It doesn't make much sense to us, but mathematically it just calculates.

Quote from tobega on June 19, 2021, 5:12 pm

Quote from tobega on June 19, 2021, 4:25 pm

Quote from tobega on June 19, 2021, 5:52 am

Even though your mind is still resisting what I'm saying, I'll give you a possible way (if your prover allows it) to introduce the structure we expect a relational lattice to have (and I have no illusion that this might be perfect or complete yet):

Lets define a lattice (or a semi-lattice depending on whether "the set of all attributes" is finite or infinte, I don't see it really matters) called H, with a supremum called Intersect and an infimum Union (and in our minds the elements work like sets)

Also define our lattice (or semi-lattice) of relations, R, with supremum InnerUnion and infimum NatJoin such that there exists a surjection (called heading) from R to H, i.e. for all Rn in R there exists an Hk in H such that heading(Rn) = Hk.

Further, heading(R1 InnerUnion R2) = heading(R1) Intersect heading(R2) and heading(R1 NatJoin R2) = heading(R1) Union heading(R2) for all R1,R2

For each Hk, the elements of Rn of R where heading(Rn) = Hk must form a (semi-)lattice under InnerUnion and NatJoin, call it RHk

Let the lattice-top of H be H0, then we let the lattice-bottom of RH0 be DUM and the lattice-top of RH0 be DEE

Now I'll stop (maybe).

To complete the surjection we also need to specify that for each Hk in H there exists some Rn in R such that heading(Rn) = Hk

Surprisingly, this does not introduce the concept of emptiness that I recently thought might be necessary, but it does introduce more structure. I guess we'll see if emptiness is needed. Certainly, any relationally complete universe will have it, whether it be defined or not.

So this model will still allow us working with the set of all empty relations, where DUM also acts as DEE. This makes some sense, I suppose, since in the world where everything is false, even true must be false.

Just for fun, it turns out that the positive integers with GCD and LCM still work in the model, with H being the set of unique prime factors in the number. But now we know how to find whatever corresponds to "DUM" in that universe, it is 1 (surprisingly, because I tried to use this as an example to illustrate a universe where there was nothing corresponding to DUM). The function "NotMatching", according to definitions given previously, ends up being uniquely defined in that universe as the function that returns its left operand. It doesn't make much sense to us, but mathematically it just calculates.

Unfortunately, H is not uniquely defined. Specifically as it stands, we could pick H as R and heading as the identity function, so maybe we're still not much closer to finding DUM. Is it enough to specify that the number of elements in R must be larger than the number of elements in H?

Oh well, now I'll do Anthony a favour and just shut up for a while.

Quote from Vadim on June 21, 2021, 5:57 pm

Quote from AntC on June 19, 2021, 12:01 pm

 

Here is a conditional assertion from page 10 of Yannakakis&Papadimitou "Algebraic dependencies" paper:

Are you sure that's the right link? I see nothing like that on page 10 -- or indeed in the whole paper. They don't seem to have an InnerUnion; they don't seem to have a DUM/R00. 1982 would be before anybody 'discovered' DUM, wouldn't it?

On page 10, Figure 2 there is a tableau, and the two nonequivalent project-join expressions.

a v b=R00 &
b v c=R00 &
a v c=R00
->
(a^c)v(((a^b)v r)^( (b^c)v( ((a^c)v r)
^
((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) )) ) ) )=
(a^c)v( ((a^b)v ( ((b^c)v r)^( (a^c)v(((b^c)v r)^((a^b)v r)) ) ))
^
( (b^c)v(((a^b)v r)^((a^c)v r)) ) ).

It is independent of the Litak et.al. axioms (Mace4 generates counterexample of order 31 which fails to be interpreted as relational universe).

The antecedent a v b=R00 & b v c=R00 & a v c=R00 -> ... means that a, b, c are all empty (and have mutually disjoint headings). That's hardly a useful place to start -- especially to generate such a monster consequent. Can't we say that the sub-lattice of empty relations is a Boolean algebra?

The a, b, and c are empty relations with disjoint set of attributes. Then,  (a^b)v r  is projection of r onto a^b , that is the [latex]\pi_{AB}[/latex] tree node at the diagram fig 2, and so on.

The entire assertion has to be valid in the project-join algebra as argued in the paper. Again, it seems to be independent of the three LMH axioms. Unfortunately, adding it into the system (admittedly making it quasi-variety) still doesn't fix the R00.