# An Algebra of R00, R01, R10, and R11

**Page 1 of 2**Next

Quote from Vadim on May 23, 2021, 5:13 pmWhen running Mace4 with RL axioms it often outputs the 2 and 4 element models. Anthony suggested that we need to exclude from consideration the lattices which honor distributive property, and impose some restrictions onto sublattice bounded between [latex]R_{00}[/latex] and [latex]R_{01}[/latex]. In other words, the minimal admissible universes are considered to be the diamond lattice

M_{3}and the pentagon latticeN_{5}. (I'm actually not sure if I ever encountered theM_{3}in my Mace4 ventures, so interpreting elements ofM_{3}as database relations is a worthy exercise).Consider the universe of the 4 relations (forgive me, galaxies) [latex]R_{00}, R_{01}, R_{10},[/latex] and [latex]R_{11}[/latex]. Even though it is distributive lattice, it is legitimate universe, as witnessed by the following interpretation:

[latex]R_{10} = \langle \{p\}, \emptyset \rangle[/latex]

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

(The interpretation of the other two is standard).

Here is the list of equalities among these elements:

R00' = R01. R10' = R11. R00 = R01'. R10 = R11'. R00` = R10. R01` = R11. R00 = R10`. R01 = R11`. R10 = R00 ^ R11. R01 = R00 v R11.In this universe the attribute inversion operation honors the law of double negation:

`x``=x.`

P.S. Finding all those equalities became kind of sport activity. Therefore, for those readers who ask the question: "What is there for me?", I'd suggest that discovering a mathematical identity is often rewarded with your name attached to it. And those attachements last for a very long time, arguably outliving anything in programming area, or even in computer science.

When running Mace4 with RL axioms it often outputs the 2 and 4 element models. Anthony suggested that we need to exclude from consideration the lattices which honor distributive property, and impose some restrictions onto sublattice bounded between R_{00} and R_{01}. In other words, the minimal admissible universes are considered to be the diamond lattice *M*_{3} and the pentagon lattice *N*_{5}. (I'm actually not sure if I ever encountered the *M*_{3} in my Mace4 ventures, so interpreting elements of *M*_{3} as database relations is a worthy exercise).

Consider the universe of the 4 relations (forgive me, galaxies) R_{00}, R_{01}, R_{10}, and R_{11}. Even though it is distributive lattice, it is legitimate universe, as witnessed by the following interpretation:

R_{10} = \langle \{p\}, \emptyset \rangle

R_{11} = \langle \{p\}, \{0\} \rangle

(The interpretation of the other two is standard).

Here is the list of equalities among these elements:

R00' = R01. R10' = R11. R00 = R01'. R10 = R11'. R00` = R10. R01` = R11. R00 = R10`. R01 = R11`. R10 = R00 ^ R11. R01 = R00 v R11.

In this universe the attribute inversion operation honors the law of double negation:

`x``=x.`

P.S. Finding all those equalities became kind of sport activity. Therefore, for those readers who ask the question: "What is there for me?", I'd suggest that discovering a mathematical identity is often rewarded with your name attached to it. And those attachements last for a very long time, arguably outliving anything in programming area, or even in computer science.

Quote from AntC on May 23, 2021, 10:47 pmThere's no universe of 4 elements that models a set of relations. It's a lattice; it's not a

relationallattice.

There's no universe of 4 elements that models a set of relations. It's a lattice; it's not a *relational* lattice.

Quote from AntC on May 24, 2021, 3:02 amQuote from Vadim on May 23, 2021, 5:13 pmWhen running Mace4 with RL axioms it often outputs the 2 and 4 element models.

All the models I'm getting have an element count that is a power of 2. I smell a rat.

Anthony suggested that we need to exclude from consideration the lattices which honor distributive property, and impose some restrictions onto sublattice bounded between [latex]R_{00}[/latex] and [latex]R_{01}[/latex]. In other words, the minimal admissible universes are considered to be the diamond lattice

M_{3}and the pentagon latticeN_{5}. (I'm actually not sure if I ever encountered theM_{3}in my Mace4 ventures, so interpreting elements ofM_{3}as database relations is a worthy exercise).No, an

`M`

_{3}sub-lattice can't appear in arelationallattice. An`N`

_{5}sub-lattice certainly should appear, but your axioms prevent it. I smell a rat.Consider the universe of the 4 relations (forgive me, galaxies) [latex]R_{00}, R_{01}, R_{10},[/latex] and [latex]R_{11}[/latex]. Even though it is distributive lattice, it is legitimate universe, as witnessed by the following interpretation:

[latex]R_{10} = \langle \{p\}, \emptyset \rangle[/latex]

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

There's also an interpretation from those axioms (2-, 4- 8- or 16-elements) with

`Fullest = Emptiest`

aka`R11 = R10`

/lattice bottom. In those models`DUM = DEE`

aka`R00 = R01`

/lattice top. So

- your axioms do not give a unique/stable model;
- your axioms can put
`DUM/R00`

in a ridiculous place;- your axioms (I suspect) generate only Boolean Algebras, not elements that correspond to relations with differing headings.
- I generated those models by asking Mace4 to counter
`r1 NatJoin DUM = r2 NatJoin DUM`

.

(For those following along at home, there's an implicit`forall r1 r2.`

I was expecting this to provide counters I could interpret as`r1, r2`

having differing headings. But because the axiom's`R00`

is not`DUM`

,`r1 NatJoin R00`

does not correspond to getting a heading-only empty`r1`

.)- Of course the Fundamental Empty Relation Axiom doesn't hold. Because
`R00`

is not modelling`DUM`

.In this universe the attribute inversion operation honors the law of double negation:

`x``=x.`

That's probably because the axioms generate only Boolean Algebras.

P.S. Finding all those equalities became kind of sport activity.

You're doing the typical end-user testing 'confirmation bias': looking only for models that behave the way you want.

Therefore, for those readers who ask the question: "What is there for me?", I'd suggest that discovering a mathematical identity is often rewarded with your name attached to it. And those attachements last for a very long time, arguably outliving anything in programming area, or even in computer science.

Testers rarely get acknowledged. The mark of well-tested software is that it works across a wide range of circumstances/models that were not envisaged by the original designers. Or at least that it degrades gracefully when encountering out-of-band circumstances.

Or of course that the software never gets to see the light of day. Which is what should happen to your axioms. (As a tester, I don't count that as 'success'; but I do count it as better than releasing software that isn't fit for purpose.)

Quote from Vadim on May 23, 2021, 5:13 pmWhen running Mace4 with RL axioms it often outputs the 2 and 4 element models.

All the models I'm getting have an element count that is a power of 2. I smell a rat.

Anthony suggested that we need to exclude from consideration the lattices which honor distributive property, and impose some restrictions onto sublattice bounded between R_{00} and R_{01}. In other words, the minimal admissible universes are considered to be the diamond lattice

M_{3}and the pentagon latticeN_{5}. (I'm actually not sure if I ever encountered theM_{3}in my Mace4 ventures, so interpreting elements ofM_{3}as database relations is a worthy exercise).

No, an `M`

_{3} sub-lattice can't appear in a *relational* lattice. An `N`

_{5} sub-lattice certainly should appear, but your axioms prevent it. I smell a rat.

Consider the universe of the 4 relations (forgive me, galaxies) R_{00}, R_{01}, R_{10}, and R_{11}. Even though it is distributive lattice, it is legitimate universe, as witnessed by the following interpretation:

R_{10} = \langle \{p\}, \emptyset \rangle

R_{11} = \langle \{p\}, \{0\} \rangle

There's also an interpretation from those axioms (2-, 4- 8- or 16-elements) with `Fullest = Emptiest`

aka `R11 = R10`

/lattice bottom. In those models `DUM = DEE`

aka `R00 = R01`

/lattice top. So

- your axioms do not give a unique/stable model;
- your axioms can put
`DUM/R00`

in a ridiculous place; - your axioms (I suspect) generate only Boolean Algebras, not elements that correspond to relations with differing headings.
- I generated those models by asking Mace4 to counter
`r1 NatJoin DUM = r2 NatJoin DUM`

.

(For those following along at home, there's an implicit`forall r1 r2.`

I was expecting this to provide counters I could interpret as`r1, r2`

having differing headings. But because the axiom's`R00`

is not`DUM`

,`r1 NatJoin R00`

does not correspond to getting a heading-only empty`r1`

.) - Of course the Fundamental Empty Relation Axiom doesn't hold. Because
`R00`

is not modelling`DUM`

.

In this universe the attribute inversion operation honors the law of double negation:

`x``=x.`

That's probably because the axioms generate only Boolean Algebras.

P.S. Finding all those equalities became kind of sport activity.

You're doing the typical end-user testing 'confirmation bias': looking only for models that behave the way you want.

Therefore, for those readers who ask the question: "What is there for me?", I'd suggest that discovering a mathematical identity is often rewarded with your name attached to it. And those attachements last for a very long time, arguably outliving anything in programming area, or even in computer science.

Testers rarely get acknowledged. The mark of well-tested software is that it works across a wide range of circumstances/models that were not envisaged by the original designers. Or at least that it degrades gracefully when encountering out-of-band circumstances.

Or of course that the software never gets to see the light of day. Which is what should happen to your axioms. (As a tester, I don't count that as 'success'; but I do count it as better than releasing software that isn't fit for purpose.)

Quote from AntC on May 24, 2021, 4:26 amQuote from AntC on May 24, 2021, 3:02 amQuote from Vadim on May 23, 2021, 5:13 pmWhen running Mace4 with RL axioms it often outputs the 2 and 4 element models.

All the models I'm getting have an element count that is a power of 2. I smell a rat.

Confirmed: this is merely a distributive lattice.

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

is a theorem. The weird inverse operator doesn't model what you think it models. It just produces an obfuscated Boolean Algebra.Anthony suggested that we need to exclude from consideration the lattices which honor distributive property, and impose some restrictions onto sublattice bounded between [latex]R_{00}[/latex] and [latex]R_{01}[/latex]. In other words, the minimal admissible universes are considered to be the diamond lattice

M_{3}and the pentagon latticeN_{5}. (I'm actually not sure if I ever encountered theM_{3}in my Mace4 ventures, so interpreting elements ofM_{3}as database relations is a worthy exercise).No, an

`M`

_{3}sub-lattice can't appear in arelationallattice. An`N`

_{5}sub-lattice certainly should appear, but your axioms prevent it. I smell a rat.Consider the universe of the 4 relations (forgive me, galaxies) [latex]R_{00}, R_{01}, R_{10},[/latex] and [latex]R_{11}[/latex]. Even though it is distributive lattice, it is legitimate universe, as witnessed by the following interpretation:

[latex]R_{10} = \langle \{p\}, \emptyset \rangle[/latex]

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

There's also an interpretation from those axioms (2-, 4- 8- or 16-elements)

Also 32-elements, but no number of elements that isn't a power of 2.

with

`Fullest = Emptiest`

aka`R11 = R10`

/lattice bottom. In those models`DUM = DEE`

aka`R00 = R01`

/lattice top. So

- your axioms do not give a unique/stable model;
- your axioms can put
`DUM/R00`

in a ridiculous place;- your axioms (I suspect) generate only Boolean Algebras, not elements that correspond to relations with differing headings.
- I generated those models by asking Mace4 to counter
`r1 NatJoin DUM = r2 NatJoin DUM`

.

(For those following along at home, there's an implicit`forall r1 r2.`

I was expecting this to provide counters I could interpret as`r1, r2`

having differing headings. But because the axiom's`R00`

is not`DUM`

,`r1 NatJoin R00`

does not correspond to getting a heading-only empty`r1`

.)- Of course the Fundamental Empty Relation Axiom doesn't hold. Because
`R00`

is not modelling`DUM`

.In this universe the attribute inversion operation honors the law of double negation:

`x``=x.`

That's probably because the axioms generate only Boolean Algebras.

Confirmed. That's a theorem (Prover9 proves in less than a minute). You don't need the triple-negation business.

P.S. Finding all those equalities became kind of sport activity.

You're doing the typical end-user testing 'confirmation bias': looking only for models that behave the way you want.

Therefore, for those readers who ask the question: "What is there for me?", I'd suggest that discovering a mathematical identity is often rewarded with your name attached to it. And those attachements last for a very long time, arguably outliving anything in programming area, or even in computer science.

Testers rarely get acknowledged. The mark of well-tested software is that it works across a wide range of circumstances/models that were not envisaged by the original designers. Or at least that it degrades gracefully when encountering out-of-band circumstances.

Or of course that the software never gets to see the light of day. Which is what should happen to your axioms. (As a tester, I don't count that as 'success'; but I do count it as better than releasing software that isn't fit for purpose.)

Quote from AntC on May 24, 2021, 3:02 amQuote from Vadim on May 23, 2021, 5:13 pmWhen running Mace4 with RL axioms it often outputs the 2 and 4 element models.

All the models I'm getting have an element count that is a power of 2. I smell a rat.

Confirmed: this is merely a distributive lattice. `x ^ (y v z) = (x ^ y) v (x ^ z).`

is a theorem. The weird inverse operator doesn't model what you think it models. It just produces an obfuscated Boolean Algebra.

Anthony suggested that we need to exclude from consideration the lattices which honor distributive property, and impose some restrictions onto sublattice bounded between R_{00} and R_{01}. In other words, the minimal admissible universes are considered to be the diamond lattice

M_{3}and the pentagon latticeN_{5}. (I'm actually not sure if I ever encountered theM_{3}in my Mace4 ventures, so interpreting elements ofM_{3}as database relations is a worthy exercise).`M`

_{3}sub-lattice can't appear in arelationallattice. An`N`

_{5}sub-lattice certainly should appear, but your axioms prevent it. I smell a rat.Consider the universe of the 4 relations (forgive me, galaxies) R_{00}, R_{01}, R_{10}, and R_{11}. Even though it is distributive lattice, it is legitimate universe, as witnessed by the following interpretation:

R_{10} = \langle \{p\}, \emptyset \rangle

R_{11} = \langle \{p\}, \{0\} \rangle

There's also an interpretation from those axioms (2-, 4- 8- or 16-elements)

Also 32-elements, but no number of elements that isn't a power of 2.

with

`Fullest = Emptiest`

aka`R11 = R10`

/lattice bottom. In those models`DUM = DEE`

aka`R00 = R01`

/lattice top. So

- your axioms do not give a unique/stable model;
- your axioms can put
`DUM/R00`

in a ridiculous place;- I generated those models by asking Mace4 to counter
`r1 NatJoin DUM = r2 NatJoin DUM`

.

(For those following along at home, there's an implicit`forall r1 r2.`

I was expecting this to provide counters I could interpret as`r1, r2`

having differing headings. But because the axiom's`R00`

is not`DUM`

,`r1 NatJoin R00`

does not correspond to getting a heading-only empty`r1`

.)- Of course the Fundamental Empty Relation Axiom doesn't hold. Because
`R00`

is not modelling`DUM`

.In this universe the attribute inversion operation honors the law of double negation:

`x``=x.`

That's probably because the axioms generate only Boolean Algebras.

Confirmed. That's a theorem (Prover9 proves in less than a minute). You don't need the triple-negation business.

P.S. Finding all those equalities became kind of sport activity.

Quote from Vadim on May 24, 2021, 3:58 pm(redundant)

(redundant)

Quote from Vadim on May 24, 2021, 4:04 pmQuote from AntC on May 24, 2021, 4:26 amConfirmed: this is merely a distributive lattice.

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

is a theorem. The weird inverse operator doesn't model what you think it models. It just produces an obfuscated Boolean Algebra.Can you please post the axioms that you have used? I repeat mine (in better font setting):

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.Or, better yet, post your proof of distributivity, and I will point which assumption is wrong.

Quote from AntC on May 24, 2021, 4:26 am`x ^ (y v z) = (x ^ y) v (x ^ z).`

is a theorem. The weird inverse operator doesn't model what you think it models. It just produces an obfuscated Boolean Algebra.

Can you please post the axioms that you have used? I repeat mine (in better font setting):

**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.**

Or, better yet, post your proof of distributivity, and I will point which assumption is wrong.

Quote from Vadim on May 24, 2021, 6:36 pmHere is more evidence that

`<NotMatching>`

can be considered as derived operation. (The definition and the assumptions are in the proof).% -------- Comments from original proof --------

% Proof 1 at 750.62 (+ 11.53) seconds.

% Length of proof is 369.

% Level of proof is 46.

% Maximum clause weight is 61.

% Given clauses 5233.1

(x ^ y) v NotMatching(x,y) = x# label(non_clause) # label(goal). [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) v (x ^ R11). [assumption].

9 (x ^ R00) v (x ^ R11) = x. [copy(8),flip(a)].

10 x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'. [assumption].

11 ((x ^ y)' ^ (x ^ z)')' = x ^ (y' ^ z')'. [copy(10),flip(a)].

12 (x' ^ (y ^ z)')' = (x' ^ y')' ^ (x' ^ z')'. [assumption].

13 x ^ (y v z) = (x ^ (z v (R00 ^ y))) v (x ^ (y v (R00 ^ z))). [assumption].

14 (x ^ (y v (R00 ^ z))) v (x ^ (z v (R00 ^ y))) = x ^ (z v y). [copy(13),flip(a)].

15 (x ^ y) v (x ^ z) = x ^ (((x v z) ^ y) v ((x v y) ^ z)). [assumption].

16 x ^ (((x v y) ^ z) v ((x v z) ^ y)) = (x ^ z) v (x ^ y). [copy(15),flip(a)].

17 (R00 ^ (x ^ (y v z))) v (y ^ z) = ((R00 ^ (x ^ y)) v z) ^ ((R00 ^ (x ^ z)) v y). [assumption].

18 (x ^ y) v (R00 ^ (z ^ (x v y))) = ((R00 ^ (z ^ x)) v y) ^ ((R00 ^ (z ^ y)) v x). [copy(17),rewrite([5(6)])].

19 x' ^ x = x ^ R00. [assumption].

20 x ^ x' = x ^ R00. [copy(19),rewrite([2(2)])].

21 x' v x = x v R11. [assumption].

22 x v x' = x v R11. [copy(21),rewrite([5(2)])].

23 NotMatching(x,y) = (x' v (y ^ x))'. [assumption]....

The other equality is proven instantaneously:

% -------- Comments from original proof --------

% Proof 1 at 0.06 (+ 0.01) seconds.

% Length of proof is 16.

% Level of proof is 5.

% Maximum clause weight is 17.

% Given clauses 79.1

(x ^ y) ^ NotMatching(x,y) = (x ^ y) ^ R00# label(non_clause) # label(goal). [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].

19 x' ^ x = x ^ R00. [assumption].

20 x ^ x' = x ^ R00. [copy(19),rewrite([2(2)])].

23 NotMatching(x,y) = (x' v (y ^ x))'. [assumption].

24 (c1 ^ c2) ^ NotMatching(c1,c2) != (c1 ^ c2) ^ R00. [deny(1)].

25 c1 ^ (c2 ^ ((c1 ^ c2) v c1')') != R00 ^ (c1 ^ c2). [copy(24),rewrite([23(6),2(8),5(9),3(11),2(16)])].

28 x ^ (y ^ z) = y ^ (x ^ z). [para(2(a,1),3(a,1,1)),rewrite([3(2)])].

29 x ^ ((x v y) ^ z) = x ^ z. [para(4(a,1),3(a,1,1)),flip(a)].

150 x ^ (y ^ (x v z)) = y ^ x. [para(4(a,1),28(a,1,2)),flip(a)].

242 x ^ (x v y)' = R00 ^ x. [para(20(a,1),29(a,1,2)),rewrite([2(3),150(4)]),flip(a)].

1057 x ^ (y ^ ((x ^ y) v z)') = R00 ^ (x ^ y). [para(242(a,1),3(a,1)),flip(a)].

1058 $F. [resolve(1057,a,25,a)].

It is also provable without Litak et.al. axioms (takes a little longer):

% -------- Comments from original proof --------

% Proof 1 at 2567.78 (+ 48.27) seconds.

% Length of proof is 320.

% Level of proof is 37.

% Maximum clause weight is 31.

% Given clauses 13100.1

(x ^ y) v NotMatching(x,y) = x# label(non_clause) # label(goal). [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 ^ y') v (x ^ y `). [assumption].

9 (x ^ y') v (x ^ y `) = x. [copy(8),flip(a)].

10 x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'. [assumption].

11 ((x ^ y)' ^ (x ^ z)')' = x ^ (y' ^ z')'. [copy(10),flip(a)].

12 (x' ^ (y ^ z)')' = (x' ^ y')' ^ (x' ^ z')'. [assumption].

13 (x ` ^ y') v (x' ^ y `) = (x' v y') ^ (x ` v y `). [assumption].

14 R00 = ((x' ^ x) ` ^ x) `. [assumption].

15 (x ^ (x ^ x') `) ` = R00. [copy(14),rewrite([2(3),2(5)]),flip(a)].

16 x' ^ x = x ^ R00. [assumption].

17 x ^ x' = x ^ R00. [copy(16),rewrite([2(2)])].

18 x' v x = x v R11. [assumption].

19 x v x' = x v R11. [copy(18),rewrite([5(2)])].

22 x ` ^ x = R11 ^ x. [assumption].

23 x ^ x ` = R11 ^ x. [copy(22),rewrite([2(2)])].

24 x ` v x = R00 v x. [assumption].

25 x v x ` = R00 v x. [copy(24),rewrite([5(2)])].

26 NotMatching(x,y) = (x' v (y ^ x))'. [assumption]....

I wonder if adding this identity to the axiom system would simplify it...

Here is more evidence that `<NotMatching>`

can be considered as derived operation. (The definition and the assumptions are in the proof).

% -------- Comments from original proof --------

% Proof 1 at 750.62 (+ 11.53) seconds.

% Length of proof is 369.

% Level of proof is 46.

% Maximum clause weight is 61.

% Given clauses 5233.

1 **(x ^ y) v NotMatching(x,y) = x** # label(non_clause) # label(goal). [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) v (x ^ R11). [assumption].

9 (x ^ R00) v (x ^ R11) = x. [copy(8),flip(a)].

10 x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'. [assumption].

11 ((x ^ y)' ^ (x ^ z)')' = x ^ (y' ^ z')'. [copy(10),flip(a)].

12 (x' ^ (y ^ z)')' = (x' ^ y')' ^ (x' ^ z')'. [assumption].

13 x ^ (y v z) = (x ^ (z v (R00 ^ y))) v (x ^ (y v (R00 ^ z))). [assumption].

14 (x ^ (y v (R00 ^ z))) v (x ^ (z v (R00 ^ y))) = x ^ (z v y). [copy(13),flip(a)].

15 (x ^ y) v (x ^ z) = x ^ (((x v z) ^ y) v ((x v y) ^ z)). [assumption].

16 x ^ (((x v y) ^ z) v ((x v z) ^ y)) = (x ^ z) v (x ^ y). [copy(15),flip(a)].

17 (R00 ^ (x ^ (y v z))) v (y ^ z) = ((R00 ^ (x ^ y)) v z) ^ ((R00 ^ (x ^ z)) v y). [assumption].

18 (x ^ y) v (R00 ^ (z ^ (x v y))) = ((R00 ^ (z ^ x)) v y) ^ ((R00 ^ (z ^ y)) v x). [copy(17),rewrite([5(6)])].

19 x' ^ x = x ^ R00. [assumption].

20 x ^ x' = x ^ R00. [copy(19),rewrite([2(2)])].

21 x' v x = x v R11. [assumption].

22 x v x' = x v R11. [copy(21),rewrite([5(2)])].

23 NotMatching(x,y) = (x' v (y ^ x))'. [assumption].

...

The other equality is proven instantaneously:

% -------- Comments from original proof --------

% Proof 1 at 0.06 (+ 0.01) seconds.

% Length of proof is 16.

% Level of proof is 5.

% Maximum clause weight is 17.

% Given clauses 79.

1 **(x ^ y) ^ NotMatching(x,y) = (x ^ y) ^ R00** # label(non_clause) # label(goal). [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].

19 x' ^ x = x ^ R00. [assumption].

20 x ^ x' = x ^ R00. [copy(19),rewrite([2(2)])].

23 NotMatching(x,y) = (x' v (y ^ x))'. [assumption].

24 (c1 ^ c2) ^ NotMatching(c1,c2) != (c1 ^ c2) ^ R00. [deny(1)].

25 c1 ^ (c2 ^ ((c1 ^ c2) v c1')') != R00 ^ (c1 ^ c2). [copy(24),rewrite([23(6),2(8),5(9),3(11),2(16)])].

28 x ^ (y ^ z) = y ^ (x ^ z). [para(2(a,1),3(a,1,1)),rewrite([3(2)])].

29 x ^ ((x v y) ^ z) = x ^ z. [para(4(a,1),3(a,1,1)),flip(a)].

150 x ^ (y ^ (x v z)) = y ^ x. [para(4(a,1),28(a,1,2)),flip(a)].

242 x ^ (x v y)' = R00 ^ x. [para(20(a,1),29(a,1,2)),rewrite([2(3),150(4)]),flip(a)].

1057 x ^ (y ^ ((x ^ y) v z)') = R00 ^ (x ^ y). [para(242(a,1),3(a,1)),flip(a)].

1058 $F. [resolve(1057,a,25,a)].

It is also provable without Litak et.al. axioms (takes a little longer):

% -------- Comments from original proof --------

% Proof 1 at 2567.78 (+ 48.27) seconds.

% Length of proof is 320.

% Level of proof is 37.

% Maximum clause weight is 31.

% Given clauses 13100.

1 **(x ^ y) v NotMatching(x,y) = x** # label(non_clause) # label(goal). [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 ^ y') v (x ^ y `). [assumption].

9 (x ^ y') v (x ^ y `) = x. [copy(8),flip(a)].

10 x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'. [assumption].

11 ((x ^ y)' ^ (x ^ z)')' = x ^ (y' ^ z')'. [copy(10),flip(a)].

12 (x' ^ (y ^ z)')' = (x' ^ y')' ^ (x' ^ z')'. [assumption].

13 (x ` ^ y') v (x' ^ y `) = (x' v y') ^ (x ` v y `). [assumption].

14 R00 = ((x' ^ x) ` ^ x) `. [assumption].

15 (x ^ (x ^ x') `) ` = R00. [copy(14),rewrite([2(3),2(5)]),flip(a)].

16 x' ^ x = x ^ R00. [assumption].

17 x ^ x' = x ^ R00. [copy(16),rewrite([2(2)])].

18 x' v x = x v R11. [assumption].

19 x v x' = x v R11. [copy(18),rewrite([5(2)])].

22 x ` ^ x = R11 ^ x. [assumption].

23 x ^ x ` = R11 ^ x. [copy(22),rewrite([2(2)])].

24 x ` v x = R00 v x. [assumption].

25 x v x ` = R00 v x. [copy(24),rewrite([5(2)])].

26 NotMatching(x,y) = (x' v (y ^ x))'. [assumption].

...

I wonder if adding this identity to the axiom system would simplify it...

Quote from AntC on May 25, 2021, 12:49 amQuote from Vadim on May 24, 2021, 4:04 pmQuote from AntC on May 24, 2021, 4:26 am`x ^ (y v z) = (x ^ y) v (x ^ z).`

is a theorem. The weird inverse operator doesn't model what you think it models. It just produces an obfuscated Boolean Algebra.Can you please post the axioms that you have used? I repeat mine (in better font setting):

Vadim you can do the work. Especially if you continue to post code indistinguishable from line noise. Recap:

- The distributivity conditions are a theorem. Code quoted above.
`x``=x.`

double-weirdinverse = identity is a theorem`r1 NatJoin DUM = r2 NatJoin DUM.`

has a counter-example in Mace4, in which alleged-`DUM`

has the same value as`DEE`

/lattice top.

Quote from Vadim on May 24, 2021, 4:04 pmQuote from AntC on May 24, 2021, 4:26 am`x ^ (y v z) = (x ^ y) v (x ^ z).`

is a theorem. The weird inverse operator doesn't model what you think it models. It just produces an obfuscated Boolean Algebra.Can you please post the axioms that you have used? I repeat mine (in better font setting):

Vadim you can do the work. Especially if you continue to post code indistinguishable from line noise. Recap:

- The distributivity conditions are a theorem. Code quoted above.
`x``=x.`

double-weirdinverse = identity is a theorem-
`r1 NatJoin DUM = r2 NatJoin DUM.`

has a counter-example in Mace4, in which alleged-`DUM`

has the same value as`DEE`

/lattice top.

Quote from AntC on May 25, 2021, 1:06 amQuote from Vadim on May 24, 2021, 6:36 pmHere is more evidence that

`<NotMatching>`

can be considered as derived operation.Nobody's denying

`NotMatching`

should be definable in terms of other operations. In fact it must be, if we're going to be able to prove equivalence of queries using`NotMatching`

.But all definitions of

`NotMatching`

rely on`DUM`

. What you haven't shown is that`DUM`

is unique/stable. Indeed I have shown it isn't.One thought: If

`NotMatching`

is definable uniquely/is stable, then we have in effect required that the sub-lattice descending from each lattice element`r`

to`emptify( r ) = r NatJoin DUM`

is uniquely complemented: within that sub-lattice,`NotMatching`

is the (unique) lattice-complement of`Matching`

. It's no surprise that holds with your axioms, because your axioms produce a Boolean Algebra,nota relational lattice.Similarly: If

`Remove`

is definable uniquely/is stable, then we have in effect required that the sub-lattice descending from`DUM`

to`emptify( r )`

is uniquely complemented: within that sub-lattice,`emptify( r Remove s)`

is the (unique) lattice-complement of`emptify( r project s )`

. It's no surprise that holds with your axioms, because your axioms produce a Boolean Algebra with only one empty element:`emptify( r )`

=`emptify( r Remove s)`

=`emptify( r project s )`

= fake-`DUM`

=`Dumpty`

aka`R10`

. (I'm supposing the model hasn't taken the equally-valid position that`DUM`

=`DEE`

=`Fullest`

aka`R11`

.) Your axioms do not produce a relational lattice.I wonder if adding this identity to the axiom system would simplify it...

I'm thinking that adding the definition of

`NotMatching`

(and`Remove`

) in effect declares a restriction that sub-lattices`r`

to`emptify( r )`

must be uniquely complemented. (Andmutatis mutandisfor`Remove`

and the sub-lattice`DUM`

to`emptify( r )`

). The trouble might be that`NotMatching, Remove`

and`Matching, project`

are defined for any two operands. Can the axiomatisation see that the heading of`Matching, NotMatching`

in effect ignore 'extraneous' attributes in the r.h. operand, so must be the same as the heading of its left operand? Can it see that the headings of`project, Remove`

ignore 'extraneous' attributes in the r.h. operand, so are subsets of the heading of its left operand?

Quote from Vadim on May 24, 2021, 6:36 pmHere is more evidence that

`<NotMatching>`

can be considered as derived operation.

Nobody's denying `NotMatching`

should be definable in terms of other operations. In fact it must be, if we're going to be able to prove equivalence of queries using `NotMatching`

.

But all definitions of `NotMatching`

rely on `DUM`

. What you haven't shown is that `DUM`

is unique/stable. Indeed I have shown it isn't.

One thought: If `NotMatching`

is definable uniquely/is stable, then we have in effect required that the sub-lattice descending from each lattice element `r`

to `emptify( r ) = r NatJoin DUM`

is uniquely complemented: within that sub-lattice, `NotMatching`

is the (unique) lattice-complement of `Matching`

. It's no surprise that holds with your axioms, because your axioms produce a Boolean Algebra, *not* a relational lattice.

Similarly: If `Remove`

is definable uniquely/is stable, then we have in effect required that the sub-lattice descending from `DUM`

to `emptify( r )`

is uniquely complemented: within that sub-lattice, `emptify( r Remove s)`

is the (unique) lattice-complement of `emptify( r project s )`

. It's no surprise that holds with your axioms, because your axioms produce a Boolean Algebra with only one empty element: `emptify( r )`

= `emptify( r Remove s)`

= `emptify( r project s )`

= fake-`DUM`

= `Dumpty`

aka `R10`

. (I'm supposing the model hasn't taken the equally-valid position that `DUM`

= `DEE`

= `Fullest`

aka `R11`

.) Your axioms do not produce a relational lattice.

I wonder if adding this identity to the axiom system would simplify it...

I'm thinking that adding the definition of `NotMatching`

(and `Remove`

) in effect declares a restriction that sub-lattices `r`

to `emptify( r )`

must be uniquely complemented. (And *mutatis mutandis* for `Remove`

and the sub-lattice `DUM`

to `emptify( r )`

). The trouble might be that `NotMatching, Remove`

and `Matching, project`

are defined for any two operands. Can the axiomatisation see that the heading of `Matching, NotMatching`

in effect ignore 'extraneous' attributes in the r.h. operand, so must be the same as the heading of its left operand? Can it see that the headings of `project, Remove`

ignore 'extraneous' attributes in the r.h. operand, so are subsets of the heading of its left operand?

Quote from Vadim on May 25, 2021, 2:10 amQuote from AntC on May 25, 2021, 12:49 amQuote from Vadim on May 24, 2021, 4:04 pmQuote from AntC on May 24, 2021, 4:26 am`x ^ (y v z) = (x ^ y) v (x ^ z).`

is a theorem. The weird inverse operator doesn't model what you think it models. It just produces an obfuscated Boolean Algebra.Can you please post the axioms that you have used? I repeat mine (in better font setting):

Vadim you can do the work. Especially if you continue to post code indistinguishable from line noise. Recap:

- The distributivity conditions are a theorem. Code quoted above.
`x``=x.`

double-weirdinverse = identity is a theorem`r1 NatJoin DUM = r2 NatJoin DUM.`

has a counter-example in Mace4, in which alleged-`DUM`

has the same value as`DEE`

/lattice top.

Please show me the proof of distributivity, is it too hard to copy and paste? Because I don't see it. The Mace4 exhibits the 6 element model, with easily identifiable

`N`

_{5}sub-lattices:% Interpretation of size 6

^ :

| 0 1 2 3 4 5

---+------------

0 | 0 4 4 0 4 4

1 | 4 1 2 1 4 5

2 | 4 2 2 2 4 4

3 | 0 1 2 3 4 5

4 | 4 4 4 4 4 4

5 | 4 5 4 5 4 5v :

| 0 1 2 3 4 5

---+------------

0 | 0 3 3 3 0 3

1 | 3 1 1 3 1 1

2 | 3 1 2 3 2 1

3 | 3 3 3 3 3 3

4 | 0 1 2 3 4 5

5 | 3 1 1 3 5 5' :

0 1 2 3 4 5

----------------

3 4 5 0 1 2R00 : 0

R11 : 1

c1 : 1

c2 : 0

c3 : 2

` :

0 1 2 3 4 5

----------------

4 3 3 1 0 3

Quote from AntC on May 25, 2021, 12:49 amQuote from Vadim on May 24, 2021, 4:04 pmQuote from AntC on May 24, 2021, 4:26 am`x ^ (y v z) = (x ^ y) v (x ^ z).`

is a theorem. The weird inverse operator doesn't model what you think it models. It just produces an obfuscated Boolean Algebra.Can you please post the axioms that you have used? I repeat mine (in better font setting):

- The distributivity conditions are a theorem. Code quoted above.
`x``=x.`

double-weirdinverse = identity is a theorem`r1 NatJoin DUM = r2 NatJoin DUM.`

has a counter-example in Mace4, in which alleged-`DUM`

has the same value as`DEE`

/lattice top.

Please show me the proof of distributivity, is it too hard to copy and paste? Because I don't see it. The Mace4 exhibits the 6 element model, with easily identifiable`N`

_{5} sub-lattices:

% Interpretation of size 6

^ :

| 0 1 2 3 4 5

---+------------

0 | 0 4 4 0 4 4

1 | 4 1 2 1 4 5

2 | 4 2 2 2 4 4

3 | 0 1 2 3 4 5

4 | 4 4 4 4 4 4

5 | 4 5 4 5 4 5

v :

| 0 1 2 3 4 5

---+------------

0 | 0 3 3 3 0 3

1 | 3 1 1 3 1 1

2 | 3 1 2 3 2 1

3 | 3 3 3 3 3 3

4 | 0 1 2 3 4 5

5 | 3 1 1 3 5 5

' :

0 1 2 3 4 5

----------------

3 4 5 0 1 2

R00 : 0

R11 : 1

c1 : 1

c2 : 0

c3 : 2

` :

0 1 2 3 4 5

----------------

4 3 3 1 0 3

**Page 1 of 2**Next