Uniqueness of Dum (R00)
Quote from Vadim on August 5, 2019, 6:25 pmQuote from AntC on August 5, 2019, 1:32 pmTake this list as a program of work to prove the lattice algebra correctly implements Appendix A's model of relations. Note none of these are quasi-equational, so presumably Litak et al is not interested in them, and that's why they're getting such weak results within their quasi-equational straitjacket -- as is revealed more in their 2015 paper that has been conceded previously:
* R00 != R01. That is: DUM is distinct from DEE.
It is not derivable from the relational lattice axioms. In the universe [database] consisting of a single relation, it would be both R00 and R01. Such universe consisting of one very lonely relation is vacuous, of course, but this is besides the point.
Very much the point is to capture the logic of the Relational Model, as specified in TTM + Appendix A. A universe consisting of a single relation (whatever you call it) fails to do that: RM Pro 5.
For any workable set of relation values, we need to embed counterparts to logical True, False. Then lattice meet ≡ NaturalJOIN implements logical AND; lattice join ≡ InnerUnion implements logical OR; DEE NOTMATCHING x implements logical NOT x. So any set of values that claims to model relations must have at least two distinct values; and one must model True, one False. We don't have a workable NOTMATCHING (because it's defined in terms of R00, which isn't unique).
* forall x [(x NatJOIN R00 != x) EQUIV (x InnerUnion R00 = R01)]
The latex is right there, supported on the forum. I understand, this is not a peer reviewed publication, but if you make some effort, you'll draw satisfaction from neatly written formulas.
Tell that to the thunderstorm and the dodgy wifi.
Am I correctly understanding that you proposed the above as an axiom with the goal to derive
R_{00} \neq R_{01}
from it?
You can derive that inequality from it. As an axiom, it leaves a lot to be desired. For example it doesn't fix R00. I'd hope for some more powerful axiom from which we can derive both.
Gloss: relation x being non-empty can be expressed in two ways: emptified x not equal x; x InnerUnion DUM is Dee. Notice the corollary of that, viz: relation x being empty can be expressed in two ways: emptified x = x; x InnerUnion DUM is DUM *is* a theorem, but only because this is inferrable from the lattice axioms:
* forall z forall x [(x NatJoin z = x) EQUIV (x InnerUnion z = z)]
Substituting R00 for z in there is not telling us anything about R00. This is a symptom of R00's definitions (so far) being unable to fix R00.
* forall x [(x NatJoin R00 = R00) EQUIV (x = R00 OR x = R01)]
There's a stronger form of that (which is uglier to express, so I'll do it in English): for any two relations, their NatJOIN being DUM is equivalent to either one or both being DUM, and the other being DEE (i.e. if it's not DUM).
Are you trying to assert that there is no other relations in the lattice interval between R00 and R01?
Yes that's what my next para goes on to say.
This has been discussed at page 10 of Relational Lattice foundation for Algebraic Logic
This seems like it's a special property of DUM; but no: we could substitute any constant q in place of R00; then all this is requiring is that DUM/R00/q be displacement 1/along a single edge in the lattice from DEE. I.e. there is no relation 'between' DEE and DUM/R00/q. Again this is a symptom of R00's definitions (so far) being unable to fix R00.
OK I could just make all of the above axioms. I could add in Litak et al's two axioms mentioning R00 (their H). Does that give R00 all the needed properties? No! We don't get
* distributivity of NatJOIN over InnerUnion; and distributivity of InnerUnion over NatJOIN; for
* both combs of all three relations same heading; and all three relations empty.
The Litak axioms get us some of those, but not all.
The fact that their axiom system is not quite complete is quite easy to establish.
I could have sworn that's what I just said. I don't need an incomprehensible demonstration, thanks.
Quote from dandl on August 6, 2019, 12:21 am
I suppose you could apply that name to R01, but roo (lower case) is a shortening of kangaroo used in Australia.
You don't say. I thought they were all called Skippy (unless they're boomers or joeys of course).
Yet another deadpan snarker from Oz (but I repeat myself). They're everywhere, it seems.
Quote from Vadim on August 5, 2019, 6:25 pmQuote from AntC on August 5, 2019, 1:32 pm* forall x [(x NatJoin R00 = R00) EQUIV (x = R00 OR x = R01)]
There's a stronger form of that (which is uglier to express, so I'll do it in English): for any two relations, their NatJOIN being DUM is equivalent to either one or both being DUM, and the other being DEE (i.e. if it's not DUM).
Are you trying to assert that there is no other relations in the lattice interval between R00 and R01?
This has been discussed at page 10 of Relational Lattice foundation for Algebraic Logic
Yes that's one interpretation of that formula, as my next para says (and as I said in just previous message). I can't see that your page 10 is saying that. It asks:
How many relations with empty attribute sets exist?
That's not a question you can even ask: the lattice system has no notion of number of attributes. You can ask a question: does relation x have the same number of attributes as R01? I.e. heading(x) = heading(R01). In which heading(x) =df x NatJOIN R00. Except we haven't fixed R00. You can ask if there exists xx whose heading is a subset of the heading of R01? Except guess what?
The goal you set at top of page 10: (x InnerUnion R00 = R00) OR (x InnerUnion R00 = negate(R00)).
negate(R00) is R11, not R01. I don't see what "translates directly" to that goal. R11 is not a candidate to have an empty heading.
This seems like it's a special property of DUM; but no: we could substitute any constant q in place of R00; then all this is requiring is that DUM/R00/q be displacement 1/along a single edge in the lattice from DEE. I.e. there is no relation 'between' DEE and DUM/R00/q. Again this is a symptom of R00's definitions (so far) being unable to fix R00.
To expand this explanation further: there are an infinity of relations q such that there are no other relations in the interval between R01 and q. For example any relation with exactly one attribute and all possible values for that attribute. We can express 'q has exactly one attribute' in the lattice algebra -- except guess what? it needs R00 and R00 isn't fixed. We can express 'there is no relation qq that has the same heading as q but whose content is a superset of q's' -- except guess what?
Also there are an infinity of relations qqq such that there are no other relations in the interval between R00 and qqq. For example any empty relation with exactly one attribute. Guess what?