## The Forum for Discussion about The Third Manifesto and Related Matters

Forum breadcrumbs - You are here:
Please or Register to create posts and topics.

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

PreviousPage 2 of 2
Quote from Vadim on 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 identifiableN5 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.

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

...

PreviousPage 2 of 2