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

**Page 2 of 2**

Quote from AntC on May 25, 2021, 3:17 amQuote 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 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):

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:Ah, I apologise: I had one of your axioms mis-typed. OK I agree the distributivity has a counter-model 6 elems. The double-weirdinverse identity has a counter. The treble-weirdinverse doesn't have a counter, neither is there a proof (so far).

But still

`R00`

is not stable/unique:Attached counter-example for

`x ^ R001 = y ^ R001.`

, showing model with`R00 = R01`

. (it's a Mace4 model file, not .pdf) All counter-models with number of elems a power of two show the same.

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

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:

Ah, I apologise: I had one of your axioms mis-typed. OK I agree the distributivity has a counter-model 6 elems. The double-weirdinverse identity has a counter. The treble-weirdinverse doesn't have a counter, neither is there a proof (so far).

But still `R00`

is not stable/unique:

Attached counter-example for `x ^ R001 = y ^ R001.`

, showing model with `R00 = R01`

. (it's a Mace4 model file, not .pdf) All counter-models with number of elems a power of two show the same.

**Uploaded files:**

Quote from Vadim on May 25, 2021, 3:16 pmYes, purely equational RL axioms can generate models like this. Or the 2-element Boolean algebra. Moreover,

in any Universal Algebrathere is a vacuous model consisting of a single element. All the operations applied to this element return this element. So, how do you specify, that in a ring, or a field [latex]0 \neq 1[/latex]? Well, mathematicians don't seem to care.I'm not sure I did follow your comment (what did you mean by "the treble-weirdinverse"), but here is the proof:

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

% Proof 1 at 11.81 (+ 0.38) seconds.

% Length of proof is 243.

% Level of proof is 30.

% Maximum clause weight is 31.

% Given clauses 1269.1

x ` ` ` = 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)])].

20 R11 = (x' v x `) `. [assumption].

21 (x' v x `) ` = R11. [copy(20),flip(a)].

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

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

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

Yes, purely equational RL axioms can generate models like this. Or the 2-element Boolean algebra. Moreover, *in any Universal Algebra* there is a vacuous model consisting of a single element. All the operations applied to this element return this element. So, how do you specify, that in a ring, or a field 0 \neq 1? Well, mathematicians don't seem to care.

I'm not sure I did follow your comment (what did you mean by "the treble-weirdinverse"), but here is the proof:

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

% Proof 1 at 11.81 (+ 0.38) seconds.

% Length of proof is 243.

% Level of proof is 30.

% Maximum clause weight is 31.

% Given clauses 1269.

1 **x ` ` ` = 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)])].

20 R11 = (x' v x `) `. [assumption].

21 (x' v x `) ` = R11. [copy(20),flip(a)].

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

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

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

...

**Page 2 of 2**