Quote from Vadim on July 8, 2021, 10:34 pm

Quote from Vadim on July 7, 2021, 5:29 pm

Quote from AntC on July 7, 2021, 7:42 am

(How) are you expressing distributivity? (#47, #49 and #74, #76 in my post.)

Unfortunately, LMH algebra doesn't feature R11 constant to express #74 and 76.

The last statement warrants some clarification. It is quite easy to add one equation to LMH so that both #74 and #76 become theorems. I hope the summary below of the axioms that are already known would help to quickly dismiss weaker proposals, while continue working on extending the equational basis discovering genuine independent axioms. Which might someday help fixing the operations, such as R00.

 

1. We start with the most basic signature [latex]\{\wedge,\vee,R_{00}\}[/latex]. (LMH consider even more restrictive pure lattice signature[latex]\{\wedge,\vee \}[/latex], but we'll ignore it here.) The equational basis is:

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

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

As you might have already noticed, I sloppily referred to it as LMH, while little more precise term for it is  AxRH1+AxRH2.

There are the two more candidates, discussed here and here.

In this basis various conditional distributivity assertions such as distributivity of the headers sublattice are theorems.

 

2. [latex]\{\wedge,\vee,R_{00},R_{11}\}[/latex]. The axiomatization for it is AxRH1+AxRH2+FDI

x = (x ^ R00) v (x ^ R11).

The aforementioned conditional distributivity assertions #74 and 76 are theorems:

% -------- Comments from original proof --------
% Proof 1 at 8.31 (+ 0.14) seconds.
% Length of proof is 314.
% Level of proof is 27.
% Maximum clause weight is 65.
% Given clauses 346.

1 (x v R11) v ((y v R11) ^ (z v R11)) = ((x v R11) v (y v R11)) ^ ((x v R11) v (z v R11)) # 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 ^ (y v z) = (x ^ (z v (R00 ^ y))) v (x ^ (y v (R00 ^ z))).  [assumption].
9 (x ^ (y v (R00 ^ z))) v (x ^ (z v (R00 ^ y))) = x ^ (z v y).  [copy(8),flip(a)].
10 (x ^ y) v (x ^ z) = x ^ (((x v z) ^ y) v ((x v y) ^ z)).  [assumption].
11 x ^ (((x v y) ^ z) v ((x v z) ^ y)) = (x ^ z) v (x ^ y).  [copy(10),flip(a)].
12 (R00 ^ (x ^ (y v z))) v (y ^ z) = ((R00 ^ (x ^ y)) v z) ^ ((R00 ^ (x ^ z)) v y).  [assumption].
13 (x ^ y) v (R00 ^ (z ^ (x v y))) = ((R00 ^ (z ^ x)) v y) ^ ((R00 ^ (z ^ y)) v x).  [copy(12),rewrite([5(6)])].
14 x = (x ^ R00) v (x ^ R11).  [assumption].
...

 

1 (x v R11) ^ ((y v R11) v (z v R11)) = ((x v R11) ^ (y v R11)) v ((x v R11) ^ (z v R11)) # 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 ^ (y v z) = (x ^ (z v (R00 ^ y))) v (x ^ (y v (R00 ^ z))).  [assumption].
9 (x ^ (y v (R00 ^ z))) v (x ^ (z v (R00 ^ y))) = x ^ (z v y).  [copy(8),flip(a)].
10 (x ^ y) v (x ^ z) = x ^ (((x v z) ^ y) v ((x v y) ^ z)).  [assumption].
11 x ^ (((x v y) ^ z) v ((x v z) ^ y)) = (x ^ z) v (x ^ y).  [copy(10),flip(a)].
12 (R00 ^ (x ^ (y v z))) v (y ^ z) = ((R00 ^ (x ^ y)) v z) ^ ((R00 ^ (x ^ z)) v y).  [assumption].
13 (x ^ y) v (R00 ^ (z ^ (x v y))) = ((R00 ^ (z ^ x)) v y) ^ ((R00 ^ (z ^ y)) v x).  [copy(12),rewrite([5(6)])].
14 x = (x ^ R00) v (x ^ R11).  [assumption].
...

where in both proofs step #10 is the dependent RL1 equality from the LMH paper.

 

3. [latex]\{\wedge,\vee,',`\}[/latex] which I call the 2x2 system:

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

x' ^ x = x ^ R00.
x' v x = x v R11.

x` ^ x = R11 ^ x.
x` v x = R00 v x.

The following expressions for the [latex]R_{00},R_{01},R_{10}[/latex] and [latex]R_{11}[/latex] are theorems:

R00 = (x' v x`)'.

R01 = (x' v x`).

R10 = (x' v x`)'`.

R11 = (x' v x`)`.

Conjecture, AxR1 and AxR2 are theorems in this system:

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