Uniqueness of Dum (R00)

#1 · July 22, 2019, 3:33 am

Quote from Vadim on July 22, 2019, 3:33 am

Here is formal proof of [latex]R_{00} [/latex] uniqueness:

1 (x v (x v x `)')' = R00. [goal].
2 x ^ y = y ^ x. [assumption].
3 (x ^ y) ^ z = x ^ (y ^ z). [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 x' ^ x = R00 ^ x. [assumption].
9 x ^ x' = R00 ^ x. [para(2(a,1),8(a,1))].
10 x' v x = R00' ` v x. [assumption].
11 x v x' = R00' ` v x. [para(5(a,1),10(a,1))].
12 R00' ` v x = x v x'. [copy(11),flip(a)].
13 x ` ^ x = R00' ` ^ x. [assumption].
14 x ^ x ` = R00' ` ^ x. [para(2(a,1),13(a,1))].
15 R00' ` ^ x = x ^ x `. [copy(14),flip(a)].
16 x ` v x = R00 v x. [assumption].
17 x v x ` = R00 v x. [para(5(a,1),16(a,1))].
18 x = (x ^ y') v (x ^ y `). [assumption].
19 (x ^ y') v (x ^ y `) = x. [copy(18),flip(a)].
20 (c1 v (c1 v c1 `)')' != R00. [deny(1)].
21 (c1 v (R00 v c1)')' != R00. [para(17(a,1),20(a,1,1,2,1))].
22 x ^ (y v x) = x. [para(5(a,1),4(a,1,2))].
23 (x v y) v z = y v (x v z). [para(5(a,1),6(a,1,1))].
24 x v (y v z) = y v (x v z). [para(6(a,1),23(a,1))].
25 x v (y ^ x) = x. [para(2(a,1),7(a,1,2))].
26 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(3(a,1),7(a,1,2))].
27 x ^ x = x. [para(7(a,1),4(a,1,2))].
28 x v x = x. [para(4(a,1),7(a,1,2))].
29 x v x' = x v R00' `. [para(12(a,1),5(a,1))].
30 x v R00' ` = x v x'. [copy(29),flip(a)].
31 x ^ x ` = x ^ R00' `. [para(15(a,1),2(a,1))].
32 x ^ R00' ` = x ^ x `. [copy(31),flip(a)].
33 (R00 v x) v y = x v (x ` v y). [para(17(a,1),6(a,1,1))].
34 R00 v (x v y) = x v (x ` v y). [para(6(a,1),33(a,1))].
35 x v (x ` v y) = R00 v (x v y). [copy(34),flip(a)].
36 (x' ^ y) v (y ^ x `) = y. [para(2(a,1),19(a,1,1))].
37 (x ^ y) ^ y = x ^ y. [para(27(a,1),3(a,2,2))].
38 x ^ (y ^ x) = y ^ x. [para(2(a,1),37(a,1))].
39 x ` ^ (R00 v x) = x `. [para(17(a,1),22(a,1,2))].
40 (R00 v x) ^ x ` = x `. [para(2(a,1),39(a,1))].
41 x' v (R00 ^ x) = x'. [para(9(a,1),25(a,1,2))].
42 (R00 ^ x) v x' = x'. [para(5(a,1),41(a,1))].
43 R00 ^ R00 ` = R00 `. [para(28(a,1),40(a,1,1))].
44 R00' ` ^ R00 = R00 `. [para(43(a,1),15(a,2))].
45 R00 ^ R00' ` = R00 `. [para(2(a,1),44(a,1))].
46 R00' ` v R00 ` = R00' `. [para(45(a,1),25(a,1,2))].
47 R00 ` v R00' ` = R00' `. [para(5(a,1),46(a,1))].
48 R00' ` ^ R00 ` = R00 ^ R00' `. [para(45(a,1),38(a,1,2))].
49 R00 ` ^ R00' ` = R00 ^ R00' `. [para(2(a,1),48(a,1))].
50 R00 ` ^ R00' ` = R00 `. [para(45(a,1),49(a,2))].
51 (R00' ` ^ R00) v R00 `' = R00 `'. [para(15(a,2),42(a,1,1))].
52 (R00 ^ R00' `) v R00 `' = R00 `'. [para(2(a,1),51(a,1,1))].
53 R00 ` v R00 `' = R00 `'. [para(45(a,1),52(a,1,1))].
54 R00 v R00' = R00'. [para(27(a,1),42(a,1,1))].
55 R00 v (x v R00)' = (x v R00)'. [para(22(a,1),42(a,1,1))].
56 R00' ` v R00 = R00'. [para(54(a,1),12(a,2))].
57 R00 v R00' ` = R00'. [para(5(a,1),56(a,1))].
58 R00' v R00'' = R00 v R00'. [para(30(a,1),17(a,1))].
59 R00' v R00'' = R00'. [para(54(a,1),58(a,2))].
60 R00'' ^ R00' = R00''. [para(59(a,1),22(a,1,2))].
61 R00' ^ R00'' = R00''. [para(2(a,1),60(a,1))].
62 R00 ^ R00' = R00''. [para(9(a,1),61(a,1))].
63 R00 ^ R00 = R00''. [para(9(a,1),62(a,1))].
64 R00 = R00''. [para(27(a,1),63(a,1))].
65 R00'' = R00. [copy(64),flip(a)].
66 R00 ` ^ R00 ` ` = R00 `. [para(32(a,1),50(a,1))].
67 R00 ` ` v R00 ` = R00 ` `. [para(66(a,1),25(a,1,2))].
68 R00 ` v R00 ` ` = R00 ` `. [para(5(a,1),67(a,1))].
69 R00 v R00 ` = R00 ` `. [para(17(a,1),68(a,1))].
70 R00 v R00 = R00 ` `. [para(17(a,1),69(a,1))].
71 R00 = R00 ` `. [para(28(a,1),70(a,1))].
72 R00 ` ` = R00. [copy(71),flip(a)].
73 R00' ` = R00 ` v R00 `'. [para(47(a,1),30(a,1))].
74 R00' ` = R00 `'. [para(53(a,1),73(a,2))].
75 R00 v R00 `' = R00'. [para(74(a,1),57(a,1,2))].
76 R00 `' v x = x v x'. [para(74(a,1),12(a,1,1))].
77 R00 ` v (R00 ` ` v R00 `') = R00 v R00 `'. [para(53(a,1),35(a,2,2))].
78 R00 ` v (R00 v R00 `') = R00 v R00 `'. [para(72(a,1),77(a,1,2,1))].
79 R00 ` v R00' = R00 v R00 `'. [para(75(a,1),78(a,1,2))].
80 R00' v R00 ` = R00 v R00 `'. [para(5(a,1),79(a,1))].
81 R00' v R00 ` = R00'. [para(75(a,1),80(a,2))].
82 R00 ` ^ R00' = R00 `. [para(81(a,1),22(a,1,2))].
83 R00' ^ R00 ` = R00 `. [para(2(a,1),82(a,1))].
84 x v R00' = R00' v (x v R00 `). [para(81(a,1),24(a,1,2))].
85 R00' v (x v R00 `) = x v R00'. [copy(84),flip(a)].
86 (x ^ R00') v (x ^ R00 `) = x ^ R00'. [para(83(a,1),26(a,1,2,2))].
87 x = x ^ R00'. [para(19(a,1),86(a,1))].
88 x ^ R00' = x. [copy(87),flip(a)].
89 x = R00' ^ x. [para(88(a,1),2(a,1))].
90 R00' ^ x = x. [copy(89),flip(a)].
91 R00' v x = R00'. [para(88(a,1),25(a,1,2))].
92 R00' = x v R00'. [para(91(a,1),85(a,1))].
93 x v R00' = R00'. [copy(92),flip(a)].
94 x' v (R00' ^ x `) = R00'. [para(88(a,1),36(a,1,1))].
95 x' v x ` = R00'. [para(90(a,1),94(a,1,2))].
96 x v R00' = y' v (x v y `). [para(95(a,1),24(a,1,2))].
97 R00' = y' v (x v y `). [para(93(a,1),96(a,1))].
98 x' v (y v x `) = R00'. [copy(97),flip(a)].
99 R00' = (x v R00 ` `) v (x v R00 ` `)'. [para(98(a,1),76(a,1))].
100 R00' = (x v R00) v (x v R00 ` `)'. [para(72(a,1),99(a,2,1,2))].
101 R00' = (x v R00) v (x v R00)'. [para(72(a,1),100(a,2,2,1,2))].
102 R00' = x v (R00 v (x v R00)'). [para(6(a,1),101(a,2))].
103 R00' = x v (x v R00)'. [para(55(a,1),102(a,2,2))].
104 x v (x v R00)' = R00'. [copy(103),flip(a)].
105 x v (R00 v x)' = R00'. [para(5(a,1),104(a,1,2,1))].
106 R00'' != R00. [para(105(a,1),21(a,1,1))].
107 R00 != R00. [para(65(a,1),106(a,1))].
108 $F. [copy(107),xx(a)].

The unary postfix single quote operation is the Appendix A <NOT>. The unary backquote is negation applied to relation attributes which we'll call inversion.

Assumptions:

#8: Negated relation is disjoint with the original one

#10: The negated relation is complement to the original one

#13,16. Conditions for inversion

#18: Fundamental decomposition identity. It is generalized version of:

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

which informally asserts that any relation is an inner union of relation’s
content and header.

Now you may object, that uniqueness of negation and inversion is not proven. However, with the supplied axioms you'll be able to derive the above formula [latex]R_{00} = (x \vee (x \vee \grave{x})^\prime)^\prime[/latex]. If you argue that there might be a different constant [latex]R_{00}^* [/latex], then you'll be able to derive same formula for it.

Here is formal proof of $R_{00}$ uniqueness:

1 (x v (x v x `)')' = R00. [goal].
2 x ^ y = y ^ x. [assumption].
3 (x ^ y) ^ z = x ^ (y ^ z). [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 x' ^ x = R00 ^ x. [assumption].
9 x ^ x' = R00 ^ x. [para(2(a,1),8(a,1))].
10 x' v x = R00' ` v x. [assumption].
11 x v x' = R00' ` v x. [para(5(a,1),10(a,1))].
12 R00' ` v x = x v x'. [copy(11),flip(a)].
13 x ` ^ x = R00' ` ^ x. [assumption].
14 x ^ x ` = R00' ` ^ x. [para(2(a,1),13(a,1))].
15 R00' ` ^ x = x ^ x `. [copy(14),flip(a)].
16 x ` v x = R00 v x. [assumption].
17 x v x ` = R00 v x. [para(5(a,1),16(a,1))].
18 x = (x ^ y') v (x ^ y `). [assumption].
19 (x ^ y') v (x ^ y `) = x. [copy(18),flip(a)].
20 (c1 v (c1 v c1 `)')' != R00. [deny(1)].
21 (c1 v (R00 v c1)')' != R00. [para(17(a,1),20(a,1,1,2,1))].
22 x ^ (y v x) = x. [para(5(a,1),4(a,1,2))].
23 (x v y) v z = y v (x v z). [para(5(a,1),6(a,1,1))].
24 x v (y v z) = y v (x v z). [para(6(a,1),23(a,1))].
25 x v (y ^ x) = x. [para(2(a,1),7(a,1,2))].
26 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(3(a,1),7(a,1,2))].
27 x ^ x = x. [para(7(a,1),4(a,1,2))].
28 x v x = x. [para(4(a,1),7(a,1,2))].
29 x v x' = x v R00' `. [para(12(a,1),5(a,1))].
30 x v R00' ` = x v x'. [copy(29),flip(a)].
31 x ^ x ` = x ^ R00' `. [para(15(a,1),2(a,1))].
32 x ^ R00' ` = x ^ x `. [copy(31),flip(a)].
33 (R00 v x) v y = x v (x ` v y). [para(17(a,1),6(a,1,1))].
34 R00 v (x v y) = x v (x ` v y). [para(6(a,1),33(a,1))].
35 x v (x ` v y) = R00 v (x v y). [copy(34),flip(a)].
36 (x' ^ y) v (y ^ x `) = y. [para(2(a,1),19(a,1,1))].
37 (x ^ y) ^ y = x ^ y. [para(27(a,1),3(a,2,2))].
38 x ^ (y ^ x) = y ^ x. [para(2(a,1),37(a,1))].
39 x ` ^ (R00 v x) = x `. [para(17(a,1),22(a,1,2))].
40 (R00 v x) ^ x ` = x `. [para(2(a,1),39(a,1))].
41 x' v (R00 ^ x) = x'. [para(9(a,1),25(a,1,2))].
42 (R00 ^ x) v x' = x'. [para(5(a,1),41(a,1))].
43 R00 ^ R00 ` = R00 `. [para(28(a,1),40(a,1,1))].
44 R00' ` ^ R00 = R00 `. [para(43(a,1),15(a,2))].
45 R00 ^ R00' ` = R00 `. [para(2(a,1),44(a,1))].
46 R00' ` v R00 ` = R00' `. [para(45(a,1),25(a,1,2))].
47 R00 ` v R00' ` = R00' `. [para(5(a,1),46(a,1))].
48 R00' ` ^ R00 ` = R00 ^ R00' `. [para(45(a,1),38(a,1,2))].
49 R00 ` ^ R00' ` = R00 ^ R00' `. [para(2(a,1),48(a,1))].
50 R00 ` ^ R00' ` = R00 `. [para(45(a,1),49(a,2))].
51 (R00' ` ^ R00) v R00 `' = R00 `'. [para(15(a,2),42(a,1,1))].
52 (R00 ^ R00' `) v R00 `' = R00 `'. [para(2(a,1),51(a,1,1))].
53 R00 ` v R00 `' = R00 `'. [para(45(a,1),52(a,1,1))].
54 R00 v R00' = R00'. [para(27(a,1),42(a,1,1))].
55 R00 v (x v R00)' = (x v R00)'. [para(22(a,1),42(a,1,1))].
56 R00' ` v R00 = R00'. [para(54(a,1),12(a,2))].
57 R00 v R00' ` = R00'. [para(5(a,1),56(a,1))].
58 R00' v R00'' = R00 v R00'. [para(30(a,1),17(a,1))].
59 R00' v R00'' = R00'. [para(54(a,1),58(a,2))].
60 R00'' ^ R00' = R00''. [para(59(a,1),22(a,1,2))].
61 R00' ^ R00'' = R00''. [para(2(a,1),60(a,1))].
62 R00 ^ R00' = R00''. [para(9(a,1),61(a,1))].
63 R00 ^ R00 = R00''. [para(9(a,1),62(a,1))].
64 R00 = R00''. [para(27(a,1),63(a,1))].
65 R00'' = R00. [copy(64),flip(a)].
66 R00 ` ^ R00 ` ` = R00 `. [para(32(a,1),50(a,1))].
67 R00 ` ` v R00 ` = R00 ` `. [para(66(a,1),25(a,1,2))].
68 R00 ` v R00 ` ` = R00 ` `. [para(5(a,1),67(a,1))].
69 R00 v R00 ` = R00 ` `. [para(17(a,1),68(a,1))].
70 R00 v R00 = R00 ` `. [para(17(a,1),69(a,1))].
71 R00 = R00 ` `. [para(28(a,1),70(a,1))].
72 R00 ` ` = R00. [copy(71),flip(a)].
73 R00' ` = R00 ` v R00 `'. [para(47(a,1),30(a,1))].
74 R00' ` = R00 `'. [para(53(a,1),73(a,2))].
75 R00 v R00 `' = R00'. [para(74(a,1),57(a,1,2))].
76 R00 `' v x = x v x'. [para(74(a,1),12(a,1,1))].
77 R00 ` v (R00 ` ` v R00 `') = R00 v R00 `'. [para(53(a,1),35(a,2,2))].
78 R00 ` v (R00 v R00 `') = R00 v R00 `'. [para(72(a,1),77(a,1,2,1))].
79 R00 ` v R00' = R00 v R00 `'. [para(75(a,1),78(a,1,2))].
80 R00' v R00 ` = R00 v R00 `'. [para(5(a,1),79(a,1))].
81 R00' v R00 ` = R00'. [para(75(a,1),80(a,2))].
82 R00 ` ^ R00' = R00 `. [para(81(a,1),22(a,1,2))].
83 R00' ^ R00 ` = R00 `. [para(2(a,1),82(a,1))].
84 x v R00' = R00' v (x v R00 `). [para(81(a,1),24(a,1,2))].
85 R00' v (x v R00 `) = x v R00'. [copy(84),flip(a)].
86 (x ^ R00') v (x ^ R00 `) = x ^ R00'. [para(83(a,1),26(a,1,2,2))].
87 x = x ^ R00'. [para(19(a,1),86(a,1))].
88 x ^ R00' = x. [copy(87),flip(a)].
89 x = R00' ^ x. [para(88(a,1),2(a,1))].
90 R00' ^ x = x. [copy(89),flip(a)].
91 R00' v x = R00'. [para(88(a,1),25(a,1,2))].
92 R00' = x v R00'. [para(91(a,1),85(a,1))].
93 x v R00' = R00'. [copy(92),flip(a)].
94 x' v (R00' ^ x `) = R00'. [para(88(a,1),36(a,1,1))].
95 x' v x ` = R00'. [para(90(a,1),94(a,1,2))].
96 x v R00' = y' v (x v y `). [para(95(a,1),24(a,1,2))].
97 R00' = y' v (x v y `). [para(93(a,1),96(a,1))].
98 x' v (y v x `) = R00'. [copy(97),flip(a)].
99 R00' = (x v R00 ` `) v (x v R00 ` `)'. [para(98(a,1),76(a,1))].
100 R00' = (x v R00) v (x v R00 ` `)'. [para(72(a,1),99(a,2,1,2))].
101 R00' = (x v R00) v (x v R00)'. [para(72(a,1),100(a,2,2,1,2))].
102 R00' = x v (R00 v (x v R00)'). [para(6(a,1),101(a,2))].
103 R00' = x v (x v R00)'. [para(55(a,1),102(a,2,2))].
104 x v (x v R00)' = R00'. [copy(103),flip(a)].
105 x v (R00 v x)' = R00'. [para(5(a,1),104(a,1,2,1))].
106 R00'' != R00. [para(105(a,1),21(a,1,1))].
107 R00 != R00. [para(65(a,1),106(a,1))].
108 $F. [copy(107),xx(a)].

The unary postfix single quote operation is the Appendix A <NOT>. The unary backquote is negation applied to relation attributes which we'll call inversion.

Assumptions:

#8: Negated relation is disjoint with the original one

#10: The negated relation is complement to the original one

#13,16. Conditions for inversion

#18: Fundamental decomposition identity. It is generalized version of:

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

which informally asserts that any relation is an inner union of relation’s
content and header.

Now you may object, that uniqueness of negation and inversion is not proven. However, with the supplied axioms you'll be able to derive the above formula $R_{00} = (x \vee (x \vee \grave{x})^\prime)^\prime$ . If you argue that there might be a different constant $R_{00}^*$ , then you'll be able to derive same formula for it.

#2 · July 22, 2019, 1:27 pm

Quote from AntC on July 22, 2019, 1:27 pm

Quote from vadim tropashko on July 22, 2019, 3:33 am

Many results, such as Armstrong transitivity and reflexivity follow from premises that have little to do with [latex]R_{00}[/latex] uniqueness.

Sorry, "little to do with" is not a distinction recognised in logic. All logical differences are big differences. The premises mention R00, therefore they're totally reliant on it.

What I said in the other thread was

a shortcoming which as far as I can see is a total block to any further algebraisation: there is no definition of R00 in terms of lattice meet/join that fixes the value.

What you've provided is wrong in so many ways, I don't know where to start. That is not a proof of uniqueness of R00; it's not a technique for proving uniqueness of any (alleged) constant. And I don't really see the TTM Forum is the place for a tutorial about proving stuff in Prover9/Mace4.

Expressing R00 in terms of some other operation (negation/<NOT>), as you do here (I've elided) does not help fix it in terms of lattice meet/join. The fact that you can't prove uniqueness of negation or 'inversion' is an additional shortcoming.

As a comparison, defining R00 as the identity element for <OR> also appears to make R00 unique; what it fails to do is define <OR> in terms of lattice meet; so what you get is just some other lattice structure defined over the same elements; with an indeterminate orientation wrt lattice top aka DEE.

This is why this thread is dedicated to the issue. Also, the old forum posts can be edited. For example, I removed the citation, that you criticized that I was not replying to. Then, rather than adding yet another post to the dependency thread, can I ask you, Anthony, to clean up/amend your replies there?

That'll be difficult/impossible for another month. I'm travelling and surviving off hotel/cafe wifi on an iPad. This WordPress editor seems not to be coping at all with the combination. (I suspect that's down to the browser (lack of) emulation on the iPad.)

...

You can convince yourself that those assumptions are not blatantly erroneous the following way. Add 3 Litak et.al. identities, and try to find a counterexample for lattice distributivity. The Mace4 will exhibit 6 element model. Then, interpret those elements as database relations.

The assumptions are blatantly irrelevant.

Here's a challenge for you (with whatever definition of R00). Try to prove the uniqueness of generalised difference aka NOT MATCHING -- which one of your papers defines using R00. There is a proof (Appendix K from memory) which is completely bogus. That's what alerted me in the first place that what you're doing is not legitimate. I tried to make a proper proof and after a great deal of stirring around, discovered that R00 is not fixed.

Quote from vadim tropashko on July 22, 2019, 3:33 am

Many results, such as Armstrong transitivity and reflexivity follow from premises that have little to do with $R_{00}$ uniqueness.

Sorry, "little to do with" is not a distinction recognised in logic. All logical differences are big differences. The premises mention R00, therefore they're totally reliant on it.

What I said in the other thread was

a shortcoming which as far as I can see is a total block to any further algebraisation: there is no definition of R00 in terms of lattice meet/join that fixes the value.

What you've provided is wrong in so many ways, I don't know where to start. That is not a proof of uniqueness of R00; it's not a technique for proving uniqueness of any (alleged) constant. And I don't really see the TTM Forum is the place for a tutorial about proving stuff in Prover9/Mace4.

Expressing R00 in terms of some other operation (negation/<NOT>), as you do here (I've elided) does not help fix it in terms of lattice meet/join. The fact that you can't prove uniqueness of negation or 'inversion' is an additional shortcoming.

As a comparison, defining R00 as the identity element for <OR> also appears to make R00 unique; what it fails to do is define <OR> in terms of lattice meet; so what you get is just some other lattice structure defined over the same elements; with an indeterminate orientation wrt lattice top aka DEE.

This is why this thread is dedicated to the issue. Also, the old forum posts can be edited. For example, I removed the citation, that you criticized that I was not replying to. Then, rather than adding yet another post to the dependency thread, can I ask you, Anthony, to clean up/amend your replies there?

That'll be difficult/impossible for another month. I'm travelling and surviving off hotel/cafe wifi on an iPad. This WordPress editor seems not to be coping at all with the combination. (I suspect that's down to the browser (lack of) emulation on the iPad.)

...

You can convince yourself that those assumptions are not blatantly erroneous the following way. Add 3 Litak et.al. identities, and try to find a counterexample for lattice distributivity. The Mace4 will exhibit 6 element model. Then, interpret those elements as database relations.

The assumptions are blatantly irrelevant.

Here's a challenge for you (with whatever definition of R00). Try to prove the uniqueness of generalised difference aka NOT MATCHING -- which one of your papers defines using R00. There is a proof (Appendix K from memory) which is completely bogus. That's what alerted me in the first place that what you're doing is not legitimate. I tried to make a proper proof and after a great deal of stirring around, discovered that R00 is not fixed.

#3 · July 22, 2019, 1:36 pm

Quote from AntC on July 22, 2019, 1:27 pm

I'm travelling and surviving off hotel/cafe wifi on an iPad. This WordPress editor seems not to be coping at all with the combination. (I suspect that's down to the browser (lack of) emulation on the iPad.)

Try the Chrome browser app, maybe?

I'm the forum administrator and lead developer of Rel. Email me at dave@armchair.mb.ca with the Subject 'TTM Forum'. Download Rel from https://reldb.org

#4 · July 22, 2019, 2:02 pm

Quote from Dave Voorhis on July 22, 2019, 1:36 pm

Quote from AntC on July 22, 2019, 1:27 pm

I'm travelling and surviving off hotel/cafe wifi on an iPad. This WordPress editor seems not to be coping at all with the combination. (I suspect that's down to the browser (lack of) emulation on the iPad.)

Try the Chrome browser app, maybe?

Thank Dave (I wasn't expecting such prompt or indeed any support ;-). It's Chrome I'm using. Safari seems to suffer the same difficulties, so I suspect Apple's browser engine and/or the clip-on Bluetooth keyboard.

Specifically, any cursor movement key does move the cursor, but also jumps the view to bottom of page, so wherever the cursor's gone is now out of sight. Also the Shortcut keys don't work, hence I've given up trying to format R00 or <OR> as <>Code in the above messages.

#5 · July 22, 2019, 2:12 pm

Quote from AntC on July 22, 2019, 2:02 pm

Quote from Dave Voorhis on July 22, 2019, 1:36 pm

Quote from AntC on July 22, 2019, 1:27 pm

I'm travelling and surviving off hotel/cafe wifi on an iPad. This WordPress editor seems not to be coping at all with the combination. (I suspect that's down to the browser (lack of) emulation on the iPad.)

Try the Chrome browser app, maybe?

Thank Dave (I wasn't expecting such prompt or indeed any support ;-). It's Chrome I'm using. Safari seems to suffer the same difficulties, so I suspect Apple's browser engine and/or the clip-on Bluetooth keyboard.

Specifically, any cursor movement key does move the cursor, but also jumps the view to bottom of page, so wherever the cursor's gone is now out of sight. Also the Shortcut keys don't work, hence I've given up trying to format R00 or <OR> as <>Code in the above messages.

How annoying. I'm away from my iPad at the moment, but will try it (along with a clip-on BT keyboard) tomorrow and see if I can find a fix or workaround.

I suppose in the mean time you could use the $\LaTeX$ facility instead of Code Insert or similar.

I'm the forum administrator and lead developer of Rel. Email me at dave@armchair.mb.ca with the Subject 'TTM Forum'. Download Rel from https://reldb.org

#6 · July 23, 2019, 6:56 am

BTW, I think D&D could reasonably take umbrage at the title of this thread: The uniqueness of DUM is perfectly clear, defined using the set-theoretic basis for relations as Prescribed in TTM.

Furthermore we know how useful DUM is for reasoning about operations on relations, because we can apply the setbuilder specifications from Appendix A's FORMAL DEFINITIONS. (And we can extend those specifications to give setbuilder for the dual of relational JOIN, aka 'inner union'.)

So the difficulties are all to do with R00:

* We can't (yet) define it uniquely in terms of lattice meet/join.

* We can't (yet) derive all the properties for R00 that would prove it's the lattice/algebraicised counterpart of DUM.

I've said "yet" because I haven't tried throwing the kitchen sink at the exercise. I'd got to the point of nailing down that R00 wasn't uniquely defined (and therefore Vadim's definition of generalised difference/NOT MATCHING wasn't unique); and raised the 'quiz' thread when entirely by coincidence Vadim emailed on another matter, and started posting to the forum.

Litak et al's papers seem to be taking it that R00 (their H) is a primitive. Their axioms give some of its properties (enough for their purposes), but not all. Indeed they seem to be unconcerned it's not unique (private correspondence with Vadim). I just don't get what species of logic they're doing.

Something else puzzles me: when Vadim started posting about the lattice approach on c.d.t. there were plenty of logicians/algebraicists partaking in the discussion, including Philip Kelly & Erwin. (Why) didn't somebody point out R00 was ill-defined? Did everybody just presume that because the lattice structure needed a counterpart to DUM, it was sufficient to merely assert "R00 aka DUM"?

#7 · July 23, 2019, 2:36 pm

Quote from AntC on July 23, 2019, 6:56 am

Something else puzzles me: when Vadim started posting about the lattice approach on c.d.t. there were plenty of logicians/algebraicists partaking in the discussion, including Philip Kelly & Erwin. (Why) didn't somebody point out R00 was ill-defined? Did everybody just presume that because the lattice structure needed a counterpart to DUM, it was sufficient to merely assert "R00 aka DUM"?

Can't speak for others but as for me, the most likely reason is I'm not really an algebraicist let alone a logician. I never understood what he was up to or where he was headed or what problems he thought needed addressing. Still don't BTW.

Author of SIRA_PRISE

#8 · July 23, 2019, 2:40 pm

Quote from AntC on July 23, 2019, 6:56 am

BTW, I think D&D could reasonably take umbrage at the title of this thread: The uniqueness of DUM is perfectly clear, defined using the set-theoretic basis for relations as Prescribed in TTM.

Well, one of them was a bit puzzled by the rubric and decided not to bother the other with it. I didn't understand the initial post anyway. Was it a (needless) proof of uniqueness, or a questioning thereof? Or was it just attempting to equate it with something else? The only Roo I know of (spelled slightly differently) is the one that lives in Kanga's pouch in Winnie The Pooh. I hope I'm not going to rue chipping in like this.

Apologies to Vadim Tropashko.

Hugh

Coauthor of The Third Manifesto and related books.

#9 · July 24, 2019, 1:49 am

Quote from AntC on July 24, 2019, 1:49 am

Quote from Hugh on July 23, 2019, 2:40 pm

Quote from AntC on July 23, 2019, 6:56 am

BTW, I think D&D could reasonably take umbrage at the title of this thread: The uniqueness of DUM is perfectly clear, defined using the set-theoretic basis for relations as Prescribed in TTM.

... Was it [the initial post] a (needless) proof of uniqueness, or a questioning thereof? Or was it just attempting to equate it with something else?

True that DUM needs no proof of uniqueness. What had been questioned (at first in other places) was: a) the uniquess of R00 (given definitions appearing in Vadim/Marshall's and Litak et al's papers); then b) equating R00 with DUM.

Quote from Erwin on July 23, 2019, 2:36 pm
... I'm not really an algebraicist let alone a logician. I never understood what he was up to or where he was headed or what problems he thought needed addressing. Still don't BTW.

Then as one non-algebraicist to another ...

The appeal is an equivalent to the A algebra, but with fewer primitive concepts. (I think the appeal of having fewer primitive operators is a rather pointless parlour game.) Specifically, the A algebra still requires attribute name literals (for <REMOVE>); and their being literals only means we can't treat them as first-class; so we can't express theorems about equivalences between A expressions. For example we can't express the conditions under which you can 'push project through <AND>' in any form that allows deriving proofs.

Then the appeal of the 'inner union' operator is that it can express projection as a relational operation taking only relations as operands; and we can express 'r1 has no attributes in common with r2' as an equiequation: (r1 INNERUNION r2) JOIN DUM = DUM . DUM plays a critical role as the relational value that enables taking relations as headings for these proofs. We must have an equational definition of DUM in terms of JOIN and InnerUnion to drive inference; and that's what we do not have.

We do have some equations around a thing called R00 -- which we'd like to be equivalent to DUM. So far those equtions aren't sufficient to fix all the needed properties of R00.

A further appeal of 'inner union' (speaking more as an implementor/programmer than algebraicist) is that it is domain-independent, as opposed to <OR>, <NOT>. Then for Vadim's opening gambit on this thread to define R00 in terms of two domain-dependent operators has no appeal. This criticism is additional to the point about not defining R00 in terms of JOIN/InnerUnion. Indeed I'm not sure if 'domain dependent' is the correct term for 'inversion'/the unary postfix backquote operator. It requires an absolute complement of the set of attribute names. That seems worse than domain dependent -- schema dependent?

Does the underpinning algebra make a difference to the surface programming language/D? Not necessarily. It at least suggests 'blessing' the technique of using relation(al expression)s to denote a heading. That's already available in Rel, as it turns out, with ATTRIBUTES_OF( ). It remains an annoyance in Rel that the return value from ATTRIBUTES_OF( ) is not first-class/can only appear where syntactically an attribute-commalist is expected.

Quote from Hugh on July 23, 2019, 2:40 pm

Quote from AntC on July 23, 2019, 6:56 am

BTW, I think D&D could reasonably take umbrage at the title of this thread: The uniqueness of DUM is perfectly clear, defined using the set-theoretic basis for relations as Prescribed in TTM.

... Was it [the initial post] a (needless) proof of uniqueness, or a questioning thereof? Or was it just attempting to equate it with something else?

True that DUM needs no proof of uniqueness. What had been questioned (at first in other places) was: a) the uniquess of R00 (given definitions appearing in Vadim/Marshall's and Litak et al's papers); then b) equating R00 with DUM.

Quote from Erwin on July 23, 2019, 2:36 pm
... I'm not really an algebraicist let alone a logician. I never understood what he was up to or where he was headed or what problems he thought needed addressing. Still don't BTW.

Then as one non-algebraicist to another ...

The appeal is an equivalent to the A algebra, but with fewer primitive concepts. (I think the appeal of having fewer primitive operators is a rather pointless parlour game.) Specifically, the A algebra still requires attribute name literals (for <REMOVE>); and their being literals only means we can't treat them as first-class; so we can't express theorems about equivalences between A expressions. For example we can't express the conditions under which you can 'push project through <AND>' in any form that allows deriving proofs.

Then the appeal of the 'inner union' operator is that it can express projection as a relational operation taking only relations as operands; and we can express 'r1 has no attributes in common with r2' as an equiequation: (r1 INNERUNION r2) JOIN DUM = DUM . DUM plays a critical role as the relational value that enables taking relations as headings for these proofs. We must have an equational definition of DUM in terms of JOIN and InnerUnion to drive inference; and that's what we do not have.

We do have some equations around a thing called R00 -- which we'd like to be equivalent to DUM. So far those equtions aren't sufficient to fix all the needed properties of R00.

A further appeal of 'inner union' (speaking more as an implementor/programmer than algebraicist) is that it is domain-independent, as opposed to <OR>, <NOT>. Then for Vadim's opening gambit on this thread to define R00 in terms of two domain-dependent operators has no appeal. This criticism is additional to the point about not defining R00 in terms of JOIN/InnerUnion. Indeed I'm not sure if 'domain dependent' is the correct term for 'inversion'/the unary postfix backquote operator. It requires an absolute complement of the set of attribute names. That seems worse than domain dependent -- schema dependent?

Does the underpinning algebra make a difference to the surface programming language/D? Not necessarily. It at least suggests 'blessing' the technique of using relation(al expression)s to denote a heading. That's already available in Rel, as it turns out, with ATTRIBUTES_OF( ). It remains an annoyance in Rel that the return value from ATTRIBUTES_OF( ) is not first-class/can only appear where syntactically an attribute-commalist is expected.

#10 · July 24, 2019, 3:20 am

Quote from Erwin on July 23, 2019, 2:36 pm

Quote from AntC on July 23, 2019, 6:56 am

Something else puzzles me: when Vadim started posting about the lattice approach on c.d.t. there were plenty of logicians/algebraicists partaking in the discussion, including Philip Kelly & Erwin. (Why) didn't somebody point out R00 was ill-defined? Did everybody just presume that because the lattice structure needed a counterpart to DUM, it was sufficient to merely assert "R00 aka DUM"?

Can't speak for others but as for me, the most likely reason is I'm not really an algebraicist let alone a logician. I never understood what he was up to or where he was headed or what problems he thought needed addressing. Still don't BTW.

Ditto. It would be nice to think there is some problem worth solving before heading down this rabbit hole. A later post points to attribute names...tbc

Andl - A New Database Language - andl.org

The Forum for Discussion about The Third Manifesto and Related Matters

Uniqueness of Dum (R00)