Quote from AntC on May 20, 2021, 8:00 am

Quote from tobega on May 16, 2021, 8:41 am

I'll give a second reply, as a hook to report on further research (which has only elaborated the ineffability) ...

IIUC, Dee is the identity for natural join, but Dum would be the zero. Also, it seems Dum might be the identity for inner union, and Dee would be the zero. Or is it? Does the identity for inner union need to be the empty relation with maximum heading? Could/should Dum have the maximum heading (oh, that's Dumpty)? Yes, I think so, Dumpty is also the true zero for natural join, not Dum.

The closest (simplish) analogue I can think of is the role of zero in multiplication of Naturals:

• 1 × x = x, for all x, so 1 is the identity for ×, as DEE is the identity for NatJoin.
• 0 × x = 0, for all x, so 0 is the absorbing element for ×. So its effect is 'sideways' relative to 1.
• DUM's effect is sideways in the sense: DUM InnerUnion x yields DUM if x is empty, otherwise DEE. (Compare a sign function signum on Naturals that returns 0 or 1.)
• There's a handy corollary: DUM NatJoin x yields x if x is empty, otherwise something not equal x. (Unfortunately, stipulating that corollary as an equivalence is not sufficient to 'fix' DUM. I can't say the 'something not equal x' is emptify(x), because I haven't independently defined what is an empty relation.)
• But the analogue breaks down fairly quickly: there's a minimal Natural, but not a maximal; and
• we can build the Naturals by starting at 0 and applying a successor function; similarly we can 'unbuild' the Naturals by applying a predecessor that's the inverse of successor.
• There's no 'definite procedure' to build all relation values starting from some seed: we could start from DUM and add a tuple, = DEE, but we can't add any more tuples with that heading; we could start from DUM and add an attribute (the choice of attribute is not definite, I suppose we could apply some ordering to attribute names and pick the least); perhaps we take next the empty relation at that heading; but now we need to add a tuple (at least one), and what attribute value do we pick -- again the choice is not definite.
• Equally there's no definite procedure to 'unbuild' relations: remove some tuple arbitrarily? remove some attribute arbitrarily? We want that we could do those in either order and arrive at the same answer -- but in what sense are we removing the 'same' tuple if we first remove some attribute: projecting the attribute away might have reduced cardinality by more than one, IOW squished several tuples into one.

So that's why I'm taking the 'Universe' of relation values as given -- as lattice theory takes its set, and it's entirely happy if the set is infinite, providing we can identify the minimal and maximal. DEE (maximal/top), Dumpty (minimal/lowest), DUM('leftmost' ?) are in there somewhere, I just have to specify how to find them, and in sufficient detail that's unique.

If we start with Dee and Dumpty (it perhaps remains to be proven that the algebra from that is sane), ...

Yes it's sane that far. Because all we need to identify them uniquely is a single operation NaturalJoin, acting as lattice meet, with a (provably unique) identity value and a (provably unique) absorbing value.

we can never create Dum by natural join and inner union.

Correct. But my hope was to introduce additional operations that were well-behaved (NotMatching, Project, Remove, emptify( )) then fix DUM in terms of them -- it's variously the identity or absorbing or idempotent (kinda) element for those -- but be careful they're not commutative. That approach presumed those other operations could be 'fixed' in terms of NatJoin, InnerUnion. And/or I could specify a bunch of properties about those operations, and a bunch of properties of DUM, then 'nail' all of them together with

• DUM = emptify(DEE)
• emptify(x) = x NatJoin DUM
• As I have it, either of those as axioms implies the other; but neither is sufficient to 'fix' enough.
• The handy corollary I mentioned above: x NatJoin DUM ≠ x ≡ x InnerUnion DUM = DEE does greatly limit what DUM could be, but not sufficient to 'fix' it.

It's not as if counter-examples need be anything very weird or degenerate. So if Vadim is still listening ... There's a counter-example with just 4 elements: suppose in this Universe there's only one attribute, and its type has only value, then there's a single relation with non-empty heading (degree 1) and non-empty body (cardinality 1), call it R11; the 4 elements DEE, DUM, Dumpty, R11. The axioms and operators all work if we take R11 as a false DUM, and leave the true DUM  as just some other element.

It's not that I've introduced a contradiction. There's no counter-examples to the properties I expect for DUM and the operators. It's just that neither are those properties inferable. Or at least inferable in any reasonable timescale -- if we had all of mathematical time ... maybe. If I (for example) had a proof of the Collatz Conjecture, I could plug that in and derive stuff effortlessly. (This position is not unprecedented: PLT higher-order type inference for possibly-non-terminating function definitions needs the same trick.)

I could write those expected properties as axioms. (That wouldn't be wrong, provided I didn't introduce contradictions.) But still it doesn't derive equivalences between what should be equivalent queries. These theorems aren't provable:

• r1 project r2 = r1 Remove (r1 Remove r2)
• r1 Remove (s1 NatJoin s2) = (r1 Remove s1) Remove s2 -- required by Appendix A: I can <REMOVE> a bunch of attributes by successively removing each one, IOW <REMOVE> attribute-comma-list must be equivalent to a nesting of ((r <REMOVE> A1) <REMOVE> A2 ...). I'm taking s1 as a relation with attribute A1 only; s2 as the relation with all other attributes that'll be successively unpeeled as A2, ...; s1 NatJoin s2 is Cartesian product, where we're only interested in the resulting heading.

I haven't yet gone as far as running inference over a set-up with all four operators defined along with DUM; perhaps that'll magically fix it all together. To solve a set of simultaneous equations in 5 variables, how many equations does it take? And what if 4 of the 'variables' are functions that must be defined for all elements in the 'Universe'? Note that project, NotMatching (say) must be defined even if the headings of the operands are disjoint -- just as NatJoin degnerates to Cartesian product, or if an operand is DUM -- which is kinda disjoint (no attributes in common) but actually a subset.

Quote from Vadim on May 20, 2021, 3:08 pm

Quote from AntC on May 20, 2021, 8:00 am

 

There's a counter-example with just 4 elements: suppose in this Universe there's only one attribute, and its type has only value, then there's a single relation with non-empty heading (degree 1) and non-empty body (cardinality 1), call it R11; the 4 elements DEE, DUM, Dumpty, R11. The axioms and operators all work if we take R11 as a false DUM, and leave the true DUM  as just some other element.

Another example: take the universe inhabited by 4 unary relations [latex] X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle [/latex], [latex] Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle [/latex], [latex] X \wedge Y [/latex], [latex] X \vee Y [/latex]. Some may argue that there are "genuine" DUM and DEE hidden somewhere in that universe, but I'd think their roles can perfectly be played by unary relations, so that those 4 relations is all that you will ever see.

Again, there is "definition" of DEE  and DUM in set theoretic terms, but my faith in the curly brackets and the membership symbol has been compromized lately. Perhaps, the best way to proceed is, as you have mentioned before, not to pretend that  [latex]R_{00} = DUM[/latex], [latex]R_{01} = DEE[/latex] .

I could write those expected properties as axioms. (That wouldn't be wrong, provided I didn't introduce contradictions.) But still it doesn't derive equivalences between what should be equivalent queries. These theorems aren't provable:

• r1 project r2 = r1 Remove (r1 Remove r2)
• r1 Remove (s1 NatJoin s2) = (r1 Remove s1) Remove s2 -- required by Appendix A: I can <REMOVE> a bunch of attributes by successively removing each one, IOW <REMOVE> attribute-comma-list must be equivalent to a nesting of ((r <REMOVE> A1) <REMOVE> A2 ...). I'm taking s1 as a relation with attribute A1 only; s2 as the relation with all other attributes that'll be successively unpeeled as A2, ...; s1 NatJoin s2 is Cartesian product, where we're only interested in the resulting heading.

I haven't yet gone as far as running inference over a set-up with all four operators defined along with DUM; perhaps that'll magically fix it all together. To solve a set of simultaneous equations in 5 variables, how many equations does it take? And what if 4 of the 'variables' are functions that must be defined for all elements in the 'Universe'? Note that project, NotMatching (say) must be defined even if the headings of the operands are disjoint -- just as NatJoin degnerates to Cartesian product, or if an operand is DUM -- which is kinda disjoint (no attributes in common) but actually a subset.

Is your version of <REMOVE> total? Also, by project do you mean classic project, or inner union?

P.S. I'm using the total unary version of <REMOVE> called <INVERSE>. The axioms for <INVERSE> are the dual versions of the axioms for the <NOT> . I agree that perhaps a binary incarnation of the <INVERSE> operation,  which would be domain and attribute set independent, might have its merits, but it would certainly make the axiom system more complex.

Quote from AntC on May 21, 2021, 12:44 am

Quote from Vadim on May 20, 2021, 3:08 pm

Quote from AntC on May 20, 2021, 8:00 am

 

There's a counter-example with just 4 elements: suppose in this Universe there's only one attribute, and its type has only value, then there's a single relation with non-empty heading (degree 1) and non-empty body (cardinality 1), call it R11; the 4 elements DEE, DUM, Dumpty, R11. The axioms and operators all work if we take R11 as a false DUM, and leave the true DUM  as just some other element.

Another example: take the universe inhabited by 4 unary relations [latex] X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle [/latex], [latex] Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle [/latex], [latex] X \wedge Y [/latex], [latex] X \vee Y [/latex]. Some may argue that there are "genuine" DUM and DEE hidden somewhere in that universe, but I'd think their roles can perfectly be played by unary relations, so that those 4 relations is all that you will ever see.

Edit: some mistakes here, I'll expand more in my reply to Vadim's reply:

There is a DEE -- that is, a relation whose heading is a subset of every other relation (not necessarily proper), and content a subset superset of every other relation projected on that heading. That is X ^ Y.

There isn't a DUM -- that is a relation whose headings is the subset of every other relation, and content a subset of every other relation projected on that heading. (Neither X's nor Y's body are a subset of the other.) [Correction: there is a relation like that subset, subset -- but that one is Dumpty= lattice bottom. But it's not DUM because it isn't immediately adjacent to DEE. ] But I suspect my definitions would work 'fine' (as well/badly as I'm currently experiencing) by interpreting DUM = X. But equally well/badly by interpreting DUM = Y. The choice is arbitrary -- which is the problem.

Again, there is "definition" of DEE  and DUM in set theoretic terms, but my faith in the curly brackets and the membership symbol has been compromized lately. Perhaps, the best way to proceed is, as you have mentioned before, not to pretend that  [latex]R_{00} = DUM[/latex], [latex]R_{01} = DEE[/latex] .

Lattice definitions don't know anything about set contents nor headings. We're given a universe of elements (i.e. relation values -- we assume all possible values for some set of `<attribute name, type>` pairs). Our problem is to identify certain critical elements amongst them.

For comparison: If we start with an unbounded lattice (set of elements), we can always 'invent' a supremum/infimum. If we start with a set of relations without an equivalent to DUM, we can always 'invent' it. Just define it into existence -- if only there were precise enough definitions.

Taking lattice top as DEE is I think fine. D&D don't have a cute name for lattice bottom, but I don't think there's much need to mention it. We take DEE equivalent to TRUE where we have projected away all attributes/obtained a proposition rather than a predicate. (Are there any Suppliers in Leeds? Yes or No.) Then we do need an equivalent to FALSE and it must have as few attributes as TRUE. This is quite apart from the role of DUM in being the possible result of r1 Project r2 (where they have no attributes in common, r1 empty) r1 Remove r1 (where r1 is empty).

I could write those expected properties as axioms. (That wouldn't be wrong, provided I didn't introduce contradictions.) But still it doesn't derive equivalences between what should be equivalent queries. These theorems aren't provable:

• r1 project r2 = r1 Remove (r1 Remove r2)
• r1 Remove (s1 NatJoin s2) = (r1 Remove s1) Remove s2 -- required by Appendix A: I can <REMOVE> a bunch of attributes by successively removing each one, IOW <REMOVE> attribute-comma-list must be equivalent to a nesting of ((r <REMOVE> A1) <REMOVE> A2 ...). I'm taking s1 as a relation with attribute A1 only; s2 as the relation with all other attributes that'll be successively unpeeled as A2, ...; s1 NatJoin s2 is Cartesian product, where we're only interested in the resulting heading.

I haven't yet gone as far as running inference over a set-up with all four operators defined along with DUM; perhaps that'll magically fix it all together. To solve a set of simultaneous equations in 5 variables, how many equations does it take? And what if 4 of the 'variables' are functions that must be defined for all elements in the 'Universe'? Note that project, NotMatching (say) must be defined even if the headings of the operands are disjoint -- just as NatJoin degnerates to Cartesian product, or if an operand is DUM -- which is kinda disjoint (no attributes in common) but actually a subset.

Is your version of <REMOVE> total? Also, by project do you mean classic project, or inner union?

• r1 project r2 =df r1 InnerUnion emptify(r2) (many possible definitions for emptify( ), which ought to be equivalent but aren't provably so.)
• r1 Remove r2 = r1 project s ≡ emptify(r1 InnerUnion s) NatJoin emptify(r1 InnerUnion r2) = emptify(r1) & emptify((s InnerUnion r1) InnerUnion r2) = emptify(DEE). That is, Remove is equivalent to project on any s such that s has at least the attributes of r1 not in r2.

So yes I'm aiming to make project, Remove total (defined for all possible operands). I've added several further axioms for Remove which ought to be implied by that (and aren't countered by Mace4), but aren't provable, it seems.

Why is there that 'at least the attributes' business for s? Because I want an equivalence in the definition, to strengthen inference. See below about headings for the attributes to project/remove.

P.S. I'm using the total unary version of <REMOVE> called <INVERSE>. The axioms for <INVERSE> are the dual versions of the axioms for the <NOT> . I agree that perhaps a binary incarnation of the <INVERSE> operation,  which would be domain and attribute set independent, might have its merits, but it would certainly make the axiom system more complex.

I'm pretty sure using <NOT>, <INVERSE> run into the same problems of non-provability. I think the difficulty is this:

• NatJoin, InnerUnion are well-defined no matter what the headings of their operands. Indeed we deliberately exploit unequal headings for NatJoin: if they're the same, thats INTERSECT; if they don't overlap, that's Cartesian product; if one is a subset, that's WHERE; if there's a partial overlap, that's EXTEND. (To be more precise, the axiom system takes NatJoin to be well-defined; then it follows from the absorption laws that InnerUnion is well-defined. For the other operators, we don't have definitions as strong as the absorption laws.
• We want Matching, NotMatching, project, Remove to be well-defined no matter what the headings of operands. And for Matching, NotMatching that's not too bad, because the heading of the result is to be the heading of the left operand. But the heading of the r.h. operand to project, Remove could include any rubbishy attributes that don't appear in the l.h. operand, they're just ignored/they don't have any influence on the result.
• For Matching, NotMatching, project, Remove the bodies of the r.h. operand could include any rubbishy tuples that don't appear in the l.h. operand, again they're just ignored.
• So you want r1 Remove r2 = r1 project (<INVERSE> r2) = r1 InnerUnion emptify?(<INVERSE> r2). Again that must be well defined if r2 has attributes outside r1, and/or <INVERSE> r2 has attributes outside r1. For emptify?( ) you still need to fix something -- perhaps emptify?(r) = r NatJoin DUM; DUM = <NOT> DEE?
• You can define <INVERSE> (<INVERSE> r) = r; <NOT> (<NOT> r) = r. I think that won't fix either operation to what you want. For example, those are 'solved' if <INVERSE>, <NOT> are merely identity. I've added stupid/ugly axioms like emptify(DEE) ≠ DEE; DUM must be adjacent to DEE. That's not enough to fix anything. (So in your 4-element model, it merely fixes that R00 is the element 'opposite' R11 -- either could be X, Y, the choice is arbitrary.)

Quote from AntC on May 21, 2021, 4:54 am

Quote from AntC on May 21, 2021, 12:44 am

Quote from Vadim on May 20, 2021, 3:08 pm

Quote from AntC on May 20, 2021, 8:00 am

 

There's a counter-example with just 4 elements: suppose in this Universe there's only one attribute, and its type has only value, then there's a single relation with non-empty heading (degree 1) and non-empty body (cardinality 1), call it R11; the 4 elements DEE, DUM, Dumpty, R11. The axioms and operators all work if we take R11 as a false DUM, and leave the true DUM  as just some other element.

 

Is your version of <REMOVE> total? Also, by project do you mean classic project, or inner union?

• r1 project r2 =df r1 InnerUnion emptify(r2) (many possible definitions for emptify( ), which ought to be equivalent but aren't provably so.)
• r1 Remove r2 = r1 project s ≡ emptify(r1 InnerUnion s) NatJoin emptify(r1 InnerUnion r2) = emptify(r1) & emptify((s InnerUnion r1) InnerUnion r2) = emptify(DEE). That is, Remove is equivalent to project on any s such that s has at least the attributes of r1 not in r2.

So yes I'm aiming to make project, Remove total (defined for all possible operands). I've added several further axioms for Remove which ought to be implied by that (and aren't countered by Mace4), but aren't provable, it seems.

Why is there that 'at least the attributes' business for s? Because I want an equivalence in the definition, to strengthen inference. See below about headings for the attributes to project/remove.

P.S. I'm using the total unary version of <REMOVE> called <INVERSE>. The axioms for <INVERSE> are the dual versions of the axioms for the <NOT> . I agree that perhaps a binary incarnation of the <INVERSE> operation,  which would be domain and attribute set independent, might have its merits, but it would certainly make the axiom system more complex.

I'm pretty sure using <NOT>, <INVERSE> run into the same problems of non-provability. I think the difficulty is this:

• NatJoin, InnerUnion are well-defined no matter what the headings of their operands. Indeed we deliberately exploit unequal headings for NatJoin: if they're the same, thats INTERSECT; if they don't overlap, that's Cartesian product; if one is a subset, that's WHERE; if there's a partial overlap, that's EXTEND. (To be more precise, the axiom system takes NatJoin to be well-defined; then it follows from the absorption laws that InnerUnion is well-defined. For the other operators, we don't have definitions as strong as the absorption laws.
• We want Matching, NotMatching, project, Remove to be well-defined no matter what the headings of operands. And for Matching, NotMatching that's not too bad, because the heading of the result is to be the heading of the left operand. But the heading of the r.h. operand to project, Remove could include any rubbishy attributes that don't appear in the l.h. operand, they're just ignored/they don't have any influence on the result.
• For Matching, NotMatching, project, Remove the bodies of the r.h. operand could include any rubbishy tuples that don't appear in the l.h. operand, again they're just ignored.
• So you want r1 Remove r2 = r1 project (<INVERSE> r2) = r1 InnerUnion emptify?(<INVERSE> r2). Again that must be well defined if r2 has attributes outside r1, and/or <INVERSE> r2 has attributes outside r1. For emptify?( ) you still need to fix something -- perhaps emptify?(r) = r NatJoin DUM; DUM = <NOT> DEE?
• You can define <INVERSE> (<INVERSE> r) = r; <NOT> (<NOT> r) = r. I think that won't fix either operation to what you want. For example, those are 'solved' if <INVERSE>, <NOT> are merely identity. I've added stupid/ugly axioms like emptify(DEE) ≠ DEE; DUM must be adjacent to DEE. That's not enough to fix anything. (So in your 4-element model, it merely fixes that R00 is the element 'opposite' R11 -- either could be X, Y, the choice is arbitrary.)

Ah, that was easy to prove. Or are there some extra axioms I need? My definition above for <INVERSE> is wrong, a better guess below.

• <NOT>(<NOT> r1)) = r1.
• r1 ≠ <NOT> r1.
• Does not fix <NOT>. I can see this is pointless anyway, because there's no mention of NatJoin, InnerUnion that are really what defines the lattice. Try that ...
• emptify(r1) = r1 NatJoin (<NOT> r1).
• emptify(DEE) = <NOT>(DEE). i.e. two definitions for DUM not proven equal, neither is there a counter-model; so this has rapidly reached the position I'm in. (For full disclosure, Prover9 gives a strange message: 'not all the required proofs were found' -- even though I'm asking for only one proof. I don't think it's this problem. And that's weird because expanding the emptify ⇒ DEE NatJoin (<NOT> DEE) and DEE NatJoin r = r, then lhs reduces to same as rhs.

Well perhaps it'll all fix itself if I go on to <INVERSE>. My guess <INVERSE> (<INVERSE> r) = r must be wrong, because the heading of <INVERSE>'s result must be the absolute complement of the heading of r; which throws away the content of r; so double-inverting can't restore it. I'll better-guess that <INVERSE> returns the maximum content for that complemented heading. That'll give an opportunity to introduce the lattice operators into the equations.

• <INVERSE>(<INVERSE)(r1)) = r1 InnerUnion <NOT> r1.
<INVERSE> r1 ≠ r1.
<INVERSE>(<NOT> r1) = <INVERSE> r1.
<INVERSE> Dumpty = DEE. ( Dumpty =df the identity for InnerUnion aka lattice bottom aka Tropashko's R10.)
• Those definitions don't fix <INVERSE> unique.
• I don't see a definition for DUM that would use <INVERSE> without also using <NOT> to emptify.

Perhaps it'll magically come together if we tie the loose ends with NotMatching?

• r1 NotMatching r2 = (r1 NatJoin <NOT> r2) InnerUnion (r1 NatJoin <NOT> DEE). -- writing out emptify in full -- no, not unique
• (r1 NatJoin r2) InnerUnion (r1 NotMatching r2) = r1.
(r1 NatJoin r2) NatJoin (r1 NotMatching r2) = (r1 NatJoin r2) ^ <NOT> DEE.  Adding both those doesn't make NotMatching unique.

So this approach ('total unary'/absolute complements) is just as ineffable as my avoiding domain-dependent operators.

Quote from Vadim on May 21, 2021, 2:45 pm

Quote from AntC on May 21, 2021, 12:44 am

Quote from Vadim on May 20, 2021, 3:08 pm

Quote from AntC on May 20, 2021, 8:00 am

 

There's a counter-example with just 4 elements: suppose in this Universe there's only one attribute, and its type has only value, then there's a single relation with non-empty heading (degree 1) and non-empty body (cardinality 1), call it R11; the 4 elements DEE, DUM, Dumpty, R11. The axioms and operators all work if we take R11 as a false DUM, and leave the true DUM  as just some other element.

Another example: take the universe inhabited by 4 unary relations [latex] X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle [/latex], [latex] Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle [/latex], [latex] X \wedge Y [/latex], [latex] X \vee Y [/latex]. Some may argue that there are "genuine" DUM and DEE hidden somewhere in that universe, but I'd think their roles can perfectly be played by unary relations, so that those 4 relations is all that you will ever see.

There is a DEE -- that is, a relation whose heading is a subset of every other relation (not necessarily proper), and content a subset of every other relation projected on that heading. That is X ^ Y.

There isn't a DUM -- that is a relation whose headings is the subset of every other relation, and content a subset of every other relation projected on that heading. (Neither X's nor Y's body are a subset of the other.) But I suspect my definitions would work 'fine' (as well/badly as I'm currently experiencing) by interpreting DUM = X. But equally well/badly by interpreting DUM = Y. The choice is arbitrary -- which is the problem.

I don't see any arbitrarines. We have

[latex] X = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle [/latex],

[latex] Y = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle [/latex],

[latex] X \wedge Y  = R_{10} [/latex]  (lattice bottom),

[latex] X \vee Y = R_{01} [/latex]  (lattice top).

Then, we have the operation of tuple set complement. I'd prefer to use the quote symbol notation as a postfix operation, rather than TTM prefix <NOT> , because the later can be easily confused with boolean algebra negation. (In the relational lattice the analog of boolean negation is the composition of the attribute set complement (AKA inversion) and tuple set complement). The calculation of the tuple set complement of the each unverse inhabitant is straightforward:

[latex] X ' = \langle \{ p \}, \{ \langle 0 \rangle \}\rangle ' = \langle \{ p \}, \{ \langle 1 \rangle \}\rangle = Y [/latex]

[latex] Y ' = X [/latex]

[latex] R_{01} ' = R_{10} [/latex]

[latex] R_{10} ' = R_{01} [/latex]

Then, by definition

[latex] R_{00} = R_{10}' [/latex]

This fixes [latex] R_{00}  [/latex] uniquely in our universe as [latex] \langle \{ p \}, \emptyset \rangle [/latex]

• You can define <INVERSE> (<INVERSE> r) = r; <NOT> (<NOT> r) = r. I think that won't fix either operation to what you want. For example, those are 'solved' if <INVERSE>, <NOT> are merely identity. I've added stupid/ugly axioms like emptify(DEE) ≠ DEE; DUM must be adjacent to DEE. That's not enough to fix anything. (So in your 4-element model, it merely fixes that R00 is the element 'opposite' R11 -- either could be X, Y, the choice is arbitrary.)

Unlike tuple set complement honoring the law of double negation

x'' = x

the law for repetitive attribute inversion is more subtle:

x``` = x`

This makes attribute inversion less intutive compared to tuple set complement.

P.S. I see you made correction post, but the correspondence could have been clearer if you had edited the predecessor post. You can always temporarily delete/ mark the content of your post while in the process of editing so that people would not reply to it.

Quote from Vadim on May 21, 2021, 3:36 pm

Quote from AntC on May 21, 2021, 4:54 am

• I don't see a definition for DUM that would use <INVERSE> without also using <NOT> to emptify.

I have a system with 4 operation signature and 8 additional axioms:

% Language Options

op(300, postfix, "`" ).


formulas(assumptions).

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

x = (x ^ y') v (x ^ y`).
x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'.
(x' ^ (y ^ z)')' = (x' ^ y')' ^ (x' ^ z')'.
(y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `).

R00 = ((x' ^ x)` ^ x)`.
x' ^ x = x ^ R00.
x' v x = x v R11.

R11 = (x' v x`)`.
x` ^ x = R11 ^ x.
x` v x = R00 v x.

end_of_list.

formulas(goals).

%R00 = ((x` v x)' v x)'.
%R00 = (x' v x`)``'.
%R11 = ((x` ^ x)' ^ x)'.

end_of_list.

Comments:

Axiom at line 15 is the generalization of FDA: x = (x ^ R00) v (x ^ R11)

Axiom at line 16 is distributivity of the <OR> over <AND> from TTM Appendix A

Axiom at line 17 is the dual

Axiom at line 18 has been discovered by expression search in QBQL

Theorems like double tuple set complement, or triple attribute inversion are easily provable.  The axioms from the Litak et.al. system are less so (but not refuted by Mace4 either).

Quote from tobega on May 21, 2021, 8:06 pm

I'll take the liberty to waffle on with some further thoughts from my limited understanding.

I'm still thinking of some kind of analogy to field extensions in Galois theory (which I don't really pretend to understand despite passing a class in it long ago), so I'll play with that:

We start with the lattice with no attributes, say D, with elements DUM and DEE. Then we extend with an attribute, say A1, to form the lattice D(A₁) with elements DUM(A₁) which is heading A₁ no tuples, and DEE(A₁) which has all possible values of A₁. We can extend more to D(A₁..A_n), giving DUM(A₁..A_n) and DEE(A₁..A_n). An extension can be characterized as DEE(A₁..A_n) join DEE(A_n+1)

For any relation in D(A₁..A_n), any DEE(B₁..B_k) where B₁..B_k is a subset of A₁..A_n works as identity for join, and any DUM(C₁..C_m) where C₁..C_m is a superset of A₁..A_n works as an identity for inner union.

Don't know if that gets us anywhere, but it gives the thought that DUM and DEE could be functions (emptify and fullify). It seems be enough to have just DUM and the biggest possible DEE, call it F (I was going to call it DOLLY but that's probably not PC), the others are easily derived from them and the relation we are looking at.

Quote from AntC on May 21, 2021, 10:34 pm

Quote from Vadim on May 21, 2021, 3:36 pm

Quote from AntC on May 21, 2021, 4:54 am

• I don't see a definition for DUM that would use <INVERSE> without also using <NOT> to emptify.

I have a system with 4 operation signature and 8 additional axioms:

Are these axioms sufficient to fix your operators uniquely (in terms of lattice meet, join)? Do you have a proof of that uniqueness?

Anybody can go around inventing operators and giving some equations mentioning them. And inventing constants like R00, R11. Without proofs of uniqueness, we don't have an algebra.

 

Quote from AntC on May 21, 2021, 10:57 pm

Quote from tobega on May 21, 2021, 8:06 pm

 

We start with the lattice with no attributes, say D, with elements DUM and DEE.

To count as a lattice, we need a (partial) ordering. Or (equivalently as it turns out) a pair of operators that operate on any two elements to produce a third (not necessarily distinct), and that are commutative, associative, idempotent, and mutually dual such that they absorb each other. Read the wiki page on Lattice (ordering), it's simple algebra, unlike Galois theory.

You seem to be building a set of elements. Not every set of elements is a lattice. You seem to have an ordering only amongst relations of the same heading. That's not a lattice: you need an (partial) ordering amongst relations of different headings.

Then we extend with an attribute, say A1, to form the lattice D(A₁) with elements DUM(A₁) which is heading A₁ no tuples, and DEE(A₁) which has all possible values of A₁. We can extend more to D(A₁..A_n), giving DUM(A₁..A_n) and DEE(A₁..A_n). An extension can be characterized as DEE(A₁..A_n) join DEE(A_n+1)

How do we generate non-empty relations with less than all possible tuples for that heading? How to prove that subtracting one tuple from DEE(A₁) then subtracting another yields the same relation as subtracting in the reverse ordering? (How to prove that adding tuples to DUM(A1) likewise produces the same yield? How to prove that if you add enough tuples to DUM(A₁) you'll arrive at DEE(A₁)? And inversely subtracting? ) That'll be true if DEE(A₁) is a set, but you haven't given any axioms saying it's a set. Neither have you given axioms saying how the set contents relate to the ordering.

For any relation in D(A₁..A_n), any DEE(B₁..B_k) where B₁..B_k is a subset of A₁..A_n works as identity for join, and any DUM(C₁..C_m) where C₁..C_m is a superset of A₁..A_n works as an identity for inner union.

I don't understand "works as an identity for ...". The consequence of the lattice structure, and characteristics of the lattice operators, is there is exactly one identity element. It must work as identity for NatJoin to any element of any heading.

Don't know if that gets us anywhere, but it gives the thought that DUM and DEE could be functions (emptify and fullify). It seems be enough to have just DUM and the biggest possible DEE, call it F (I was going to call it DOLLY but that's probably not PC), the others are easily derived from them and the relation we are looking at.

To repeat for the umpteenth time: there is no problem with DEE, it's easy to define, and define uniquely. The 'biggest possible' relation -- that is, with all possible attributes and all possible tuples for those attributes (let's call it Fullest) is emphatically not DEE -- because DEE is greater than Fullest in the lattice ordering, because Fullest is not identity for NatJoin for all possible relations/all headings.