An Algebra of R00, R01, R10, and R11
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 theoremr1 NatJoin DUM = r2 NatJoin DUM.has a counter-example in Mace4, in which alleged-DUMhas the same value asDEE/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
N5sub-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].
...