An Algebra of R00, R01, R10, and R11

#1 · May 23, 2021, 5:13 pm

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₃ and the pentagon lattice N₅. (I'm actually not sure if I ever encountered the M₃ in my Mace4 ventures, so interpreting elements of M₃ 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.

#2 · May 23, 2021, 10:47 pm

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

#3 · May 24, 2021, 3:02 am

Quote from AntC on May 24, 2021, 3:02 am

Quote from Vadim on May 23, 2021, 5:13 pm

When 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₃ and the pentagon lattice N₅. (I'm actually not sure if I ever encountered the M₃ in my Mace4 ventures, so interpreting elements of M₃ as database relations is a worthy exercise).

No, an M₃ sub-lattice can't appear in a relational lattice. An N₅ 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 pm

When 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₃ and the pentagon lattice N₅. (I'm actually not sure if I ever encountered the M₃ in my Mace4 ventures, so interpreting elements of M₃ as database relations is a worthy exercise).

No, an M₃ sub-lattice can't appear in a relational lattice. An N₅ 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.)

#4 · May 24, 2021, 4:26 am

Quote from AntC on May 24, 2021, 4:26 am

Quote from AntC on May 24, 2021, 3:02 am

Quote from Vadim on May 23, 2021, 5:13 pm

When 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₃ and the pentagon lattice N₅. (I'm actually not sure if I ever encountered the M₃ in my Mace4 ventures, so interpreting elements of M₃ as database relations is a worthy exercise).

No, an M₃ sub-lattice can't appear in a relational lattice. An N₅ 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 am

Quote from Vadim on May 23, 2021, 5:13 pm

When 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₃ and the pentagon lattice N₅. (I'm actually not sure if I ever encountered the M₃ in my Mace4 ventures, so interpreting elements of M₃ as database relations is a worthy exercise).

No, an M₃ sub-lattice can't appear in a relational lattice. An N₅ 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;

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

#5 · May 24, 2021, 3:58 pm

(redundant)

#6 · May 24, 2021, 4:04 pm

Quote from AntC on May 24, 2021, 4:26 am

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.

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.

#7 · May 24, 2021, 6:36 pm

Quote from Vadim on May 24, 2021, 6:36 pm
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...

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

#8 · May 25, 2021, 12:49 am

Quote from Vadim on May 24, 2021, 4:04 pm

Quote from AntC on May 24, 2021, 4:26 am

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.

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.

#9 · May 25, 2021, 1:06 am

Quote from AntC on May 25, 2021, 1:06 am

Quote from Vadim on May 24, 2021, 6:36 pm

Here 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 24, 2021, 6:36 pm

Here 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?

#10 · May 25, 2021, 2:10 am

Quote from AntC on May 25, 2021, 12:49 am

Quote from Vadim on May 24, 2021, 4:04 pm

Quote from AntC on May 24, 2021, 4:26 am

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.

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 identifiableN₅ 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

TTM Forum

The Forum for Discussion about The Third Manifesto and Related Matters

An Algebra of R00, R01, R10, and R11