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

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

# On Relational Lattice complements, pseudocomplements, distributivity and Boolean algebras

PreviousPage 2 of 2

#### Axioms sufficient to prove uniqueness of R00 aka DUM, based on complements and pseudocomplements.

Addit: dang it, fail again. The proof turns out to rely on a contradiction. Subtle, because it took a long time for the prover to figure it out. Removing the contradiction (def'n of relPCompl( ) ) leaves the goal undecidable -- or at least if it's going to be provable I need to divert the power feed from NZ's Aluminium smelter. I think the problem is the def'n doesn't require the relative top/bottom to form a convex sublattice. The counter-case is relPCompl(R01, R11, R1half), which doesn't exist (although Mace doesn't find it), because the complement should be R00 but that's outside the sublattice.

Approach: define two DUM's -- R00, R002. For each axiom that mentions R00, make sure there's a parallel axiom using R002. If that axiom is introducing additional entities, make sure to introduce parallels for that: R11, R112, mtchg( ), mtchg2( ) etc.

• There's no need to introduce parallel lattice top R01 aka DEE nor lattice bottom R10 aka Dumpty, because their definitions mention only NatJoin, InnerUnion.
• Nor parallel absPCompl( ) (absolute pseudocomplement), because its definition mentions only R01, R10, plus those operators.
• mtchg( ) is Tutorial D MATCHING. Introducing it as a function in effect says: there exists a unique semijoin for any two relation values. There's two equations: mtchg(x, y) = (x ^ y) v (x ^ R00) . mtchg(x, y) = x ^ (y v (x ^ R00)). Both mention R00; neither alone 'fixes' mtchg( ) as unique. So the fact they introduce an equality, and assert it exists and is unique contributes to the definition of R00. Specifically, they're asserting you can 'push project through join'.
• A definition of NOT MATCHING seems not required to fix R00, but I've left the definition in the code for interest, commented out.
• Also for interest/commented out are some of my workings/proofs I obtained (or not) along the way.

Goal: R00 = R002.

x ^ y = y ^ x.                           % commutative
x ^ (y ^ z) = (x ^ y) ^ z.               % associative
x ^ x = x.                               % idempotent

x ^ R01 = x.
% x ^ R012 = x.                          % R01 = R012 proven pronto
x ^ R10 = R10.
% x ^ R102 = R102.                       % R10 = R102 proven pronto

(x = (x ^ z) & y = (y ^ z))              % can prove v is commut, assoc, idemp
<-> ((x v y) = (x v y) ^ z).            % x v (x ^ y) = x.  % absorb 1, 2 proven

% x ^ R00 != x <-> x v R00 = R01.          % 'Fundamental Empty Relations Axiom'

% useful for investigating large lattices
cover (y, x) <-> y ^ x = x & y != x & -(exists z (y ^ z = z & z ^ x = x & y != z & z != x)).

% Pseudocomplement axioms
% exists z (x ^ z = R10 & x v z = R01).    % every element has a complement
% not nec. unique, but pseudoCompl is unique
x ^ absPCompl(x) = R10.                 % so define as a function
x v absPCompl(x) = R01.
x ^ z = R10 & x v z = R01 -> absPCompl(x) ^ z = z.  % PCompl is max of candidate complements
absPCompl(absPCompl(absPCompl(x))) = absPCompl(x).
absPCompl(x v y) = absPCompl(x) ^ absPCompl(y).   % not proven, no counter
% absPCompl(absPCompl(x ^ y)) = absPCompl(absPCompl(x)) ^ absPCompl(absPCompl(y)).
%                                        % not true in general: (x ^ y) empty, but neither x, y empty
absPCompl(absPCompl(x ^ R00))  = x ^ R00.
absPCompl(absPCompl(x ^ R002)) = x ^ R002.

% x ^ absPCompl2(x) = R10.                 % proven equiv
% x v absPCompl2(x) = R01.
% x ^ z = R10 & x v z = R01 -> absPCompl2(x) ^ z = z.  % PCompl is max of candidate complements

%%% x1 ^ y = y & y ^ x2 = x2                           %%% contradiction in here, see Addit
%%% <-> relPCompl(x1, y, x2) ^ y = x2 & relPCompl(x1, y, x2) v y = x1.
%%% x1 ^ y = y & y ^ x2 = x2 & y ^ z = x2 & y v z = x1
%%% -> relPCompl(x1, y, x2) ^ z = z.

x v R00  = R01 <-> R00  ^ absPCompl(x) = absPCompl(x).
x v R00  = R01 <-> x ^ R00  != x.        % Fundamental Empty Relations axiom
x v R002 = R01 <-> R002 ^ absPCompl(x) = absPCompl(x).
x v R002 = R01 <-> x ^ R002 != x.

hCompl(x) ^ (x ^ R00) = R10.             % convex sublattice between [R00, R10]
hCompl(x) v (x ^ R00) = R00.             % is uniquely complemented/Boolean algebra
(x ^ R00) v ((y ^ R00) ^ (z ^ R00)) = ((x ^ R00) v (y ^ R00)) ^ ((x ^ R00) v (z ^ R00)).
% distrib1 a ? (b ? c) = (a ? b) ? (a ? c)
(x ^ R00) ^ ((y ^ R00) v (z ^ R00)) = ((x ^ R00) ^ (y ^ R00)) v ((x ^ R00) ^ (z ^ R00)).
% distrib2 a ? (b ? c) = (a ? b) ? (a ? c)

hCompl2(x) ^ (x ^ R002) = R10.             % convex sublattice between [R00, R10]
hCompl2(x) v (x ^ R002) = R002.            % is uniquely complemented/Boolean algebra
(x ^ R002) v ((y ^ R002) ^ (z ^ R002)) = ((x ^ R002) v (y ^ R002)) ^ ((x ^ R002) v (z ^ R002)).
% distrib1 a ? (b ? c) = (a ? b) ? (a ? c)
(x ^ R002) ^ ((y ^ R002) v (z ^ R002)) = ((x ^ R002) ^ (y ^ R002)) v ((x ^ R002) ^ (z ^ R002)).
% distrib2 a ? (b ? c) = (a ? b) ? (a ? c)

% complements of R00
R11 = absPCompl(R00).
absPCompl(R1half) = R00.
R11 ^ R1half = R1half.                   % ½ Prover9 says is illegal char
R11 != R1half.                           % != in axioms seems to require extra proofs
%% R1half != R10.                           % proven pronto

R112 = absPCompl(R002).
absPCompl(R1half2) = R002.
R112 ^ R1half2 = R1half2.                   % ½ Prover9 says is illegal char
R112 != R1half2.                           % != in axioms seems to require extra proofs

% 'top' face Boolean algebra
mCompl(x) ^ (x v R11) = R11.             % convex sublattice between [R01, R11]
mCompl(x) v (x v R11) = R01.             % is uniquely complemented/Boolean algebra
(x v R11) v ((y v R11) ^ (z v R11)) = ((x v R11) v (y v R11)) ^ ((x v R11) v (z v R11)).
% distrib1 a ? (b ? c) = (a ? b) ? (a ? c)
(x v R11) ^ ((y v R11) v (z v R11)) = ((x v R11) ^ (y v R11)) v ((x v R11) ^ (z v R11)).
% distrib2 a ? (b ? c) = (a ? b) ? (a ? c)
mCompl(hCompl(x)) = x v R11.           % not proven, no counter, make axiom

mCompl2(x) ^ (x v R112) = R112.             % convex sublattice between [R01, R11]
mCompl2(x) v (x v R112) = R01.             % is uniquely complemented/Boolean algebra
(x v R112) v ((y v R112) ^ (z v R112)) = ((x v R112) v (y v R112)) ^ ((x v R112) v (z v R112)).
% distrib1 a ? (b ? c) = (a ? b) ? (a ? c)
(x v R112) ^ ((y v R112) v (z v R112)) = ((x v R112) ^ (y v R112)) v ((x v R112) ^ (z v R112)).
% distrib2 a ? (b ? c) = (a ? b) ? (a ? c)
mCompl2(hCompl2(x)) = x v R112.           % not proven, no counter, make axiom

% x ^ z1 = R10 & x v z1 = R01 & x ^ z2 = R10 & x v z2 = R01     % if there are multiple complements
% -> z1 ^ R00 = z2 ^ R00.                  % they all have same heading

% x v R00 = R01 -> (x ^ z = R10 & x v z = R01 -> z ^ R00 = z).
% if x is non-empty, its complement is empty
% x v R00 = R01                            % if x is non-empty, its complement is unique
% -> (x ^ z1 = R10 & x v z1 = R01 & x ^ z2 = R10 & x v z2 = R01
%     -> z1 = z2).

% R00 ^ z1 = R10 & R00 v z1 = R01          % complement of R00 is not unique
% -> exists z2 (R00 ^ z2 = R10 & R00 v z2 = R01 & z1 != z2).

% x ^ z1 = R10 & x v z1 = R01 & x ^ z2 = R10 & x v z2 = R01
% & z1 != z2 -> R00 ^ x = x.               % R00 is max element with non-unique compl

% x1 ^ y = y & y ^ x2 = x2 & y ^ z1 = x2 & y v z1 = x1 & y ^ z2 = x2 & y v z2 = x1
% -> z1 ^ R00 = z2 ^ R00.                  % relative complements have same hdg

% x1 ^ y1 = y1 & y1 ^ x2 = x2 & y1 ^ z1 = x2 & y1 v z1 = x1
% & x1 ^ y2 = y2 & y2 ^ x2 = x2 & y2 ^ z2 = x2 & y2 v z2 = x1
% & y1 ^ R00 = y2 ^ R00
% -> z1 ^ R00 = z2 ^ R00.                  % for elems of same heading, their relative complements have same hdg

% x ^ z1 = R10 & x v z1 = R01 & x ^ z2 = R10 & x v z2 = R01     % if there are multiple complements
% -> z1 ^ R002 = z2 ^ R002.                  % they all have same heading

% x v R002 = R01 -> (x ^ z = R10 & x v z = R01 -> z ^ R002 = z).
% if x is non-empty, its complement is empty
% x v R002 = R01                            % if x is non-empty, its complement is unique
% -> (x ^ z1 = R10 & x v z1 = R01 & x ^ z2 = R10 & x v z2 = R01
%     -> z1 = z2).

% R002 ^ z1 = R10 & R002 v z1 = R01          % complement of R00 is not unique
% -> exists z2 (R002 ^ z2 = R10 & R002 v z2 = R01 & z1 != z2).

% x ^ z1 = R10 & x v z1 = R01 & x ^ z2 = R10 & x v z2 = R01
% & z1 != z2 -> R002 ^ x = x.

% MATCHING
mtchg(x, y) = (x ^  y) v (x ^ R00) .     % proven same heading as x
mtchg(x, y) =  x ^ (y  v (x ^ R00)).     % ?? has counter 11 elems, make axiom

mtchg2(x, y) = (x ^  y) v (x ^ R002) .     % ?? makes R002 unique
mtchg2(x, y) =  x ^ (y  v (x ^ R002)).     %

% NOTMATCHING (\)
% (x \ y) = relTCompl( x v R11, mtchg(x, y)).
% (x ^ y) v (x \ y) = x.                 % } proven from def'n
% (x ^ y) ^ (x \ y) = (x ^ y) ^ R00.     % } using compl of mtchg( )
% mtchg(x, y) = x \ (x \ y).             % }
% mtchg(x, y) v (x \ y) = x.
% mtchg(x, y) ^ (x \ y) = x ^ R00.

% rel'ns with same heading form a Boolean algebra 'descending' from a given x:
% complemented, distributive
x ^ y = y & y ^ (x ^ R00) = (x ^ R00) -> relTCompl(x, y) v y = x.              %% needs x^R00 =< y =< x
x ^ y = y & y ^ (x ^ R00) = (x ^ R00) -> relTCompl(x, y) ^ y = x ^ R00.        %% same
x ^ y1 = y1 & y1 ^ (x ^ R00) = x ^ R00 & x ^ y2 = y2 & y2 ^ (x ^ R00) = x ^ R00 & x ^ y3 = y3 & y3 ^ (x ^ R00) = x ^ R00
-> y1 ^ (y2 v y3) = (y1 ^ y2) v (y1 ^ y3).  % same hdg distrib sub-lattice

x ^ y = y & y ^ (x ^ R002) = (x ^ R002) -> relTCompl2(x, y) v y = x.              %% needs x^R00 =< y =< x
x ^ y = y & y ^ (x ^ R002) = (x ^ R002) -> relTCompl2(x, y) ^ y = x ^ R002.        %% same
x ^ y1 = y1 & y1 ^ (x ^ R002) = (x ^ R002) & x ^ y2 = y2 & y2 ^ (x ^ R002) = (x ^ R002) & x ^ y3 = y3 & y3 ^ (x ^ R002) = (x ^ R002)
-> y1 ^ (y2 v y3) = (y1 ^ y2) v (y1 ^ y3).  % same hdg distrib sub-lattice



#86 is a theorem in the 2x2 system $\{\wedge,\vee,',\}$:

1 mCompl(hCompl(x)) = x v R11  [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].
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 hCompl(x) = (R00 ^ x) .  [assumption].
27 mCompl(x) = (R11 v x) .  [assumption].
...

where definition #26 and #27 above are found by QBQL expression search satisfying axioms 45,46, 72, 73 from your post.

Here is attribute inversion expressed via your operations:

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

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

Quote from Vadim on July 3, 2021, 6:19 pm

#86 is a theorem in the 2x2 system $\{\wedge,\vee,',\}$:

1 mCompl(hCompl(x)) = x v R11 [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].
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 hCompl(x) = (R00 ^ x) . [assumption].
27 mCompl(x) = (R11 v x) . [assumption].
...
1 mCompl(hCompl(x)) = x v R11 [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]. 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 hCompl(x) = (R00 ^ x) . [assumption]. 27 mCompl(x) = (R11 v x) . [assumption]. ...
1 mCompl(hCompl(x)) = x v R11  [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].
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 hCompl(x) = (R00 ^ x) .  [assumption].
27 mCompl(x) = (R11 v x) .  [assumption].
...

where definition #26 and #27 above are found by QBQL expression search satisfying axioms 45,46, 72, 73 from your post.

Note that for a sub-lattice to be a Boolean Algebra needs distributivity as well as unique complementation. (How) are you expressing distributivity? (#47, #49 and #74, #76 in my post.)

Here is attribute inversion expressed via your operations:

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

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

I haven't seen any proof from you that R00R11 are unique -- which is the only part of the exercise I'm interested in. Without that, I think you don't have as strong a result as you seem to think.

It needs the overall structure to allow N5 sub-lattices, and for them to appear only in a configuration where all the candidate non-unique complements have the same heading; and that heading is 'wider' than the unique element they're complementing.

I've specified that as axioms; but it seems not enough to fix R00.

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

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

#49 is a weaker version of Eq1 from the LMH paper (Table 1 at p.8 (547))

#47  is also easily proven in their AxRH1+AxRH2 (+dependent RL1) system

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

Again, I conjectured that the 2x2 system is at least as strong as LMH AxRH1+AxRH2. Admittedly, having extra operations slows down Prover9 considerably.

Distributivity in 2x2 system holds for natural join over the TTM Algebra A <OR>:

x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'.
(x' ^ (y ^ z)')' = (x' ^ y')' ^ (x' ^ z')'.

All the conditional versions, like the ones that you exhibited, follow from them.

P.S. There is a different argument why there can't be finite set of equational axioms for Relational Lattice. The N5 is a Relational Lattice in the $\{\wedge,\vee,R_{00}\}$ signature that LMH use. Unfortunately, the direct product $N_5 \times N_5$ doesn't seem to be representable as relational lattice. Therefore, by Birkhoff theorem it is not a variety.

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

#49 is a weaker version of Eq1 from the LMH paper (Table 1 at p.8 (547))

#47  is also easily proven in their AxRH1+AxRH2 (+dependent RL1) system

Thanks Vadim. What I'm learning is that to be a Relational Algebra (or for a sublattice to be a Relational Algebra), not only must distributivity hold but also unique complementation. The LMH paper is so dense I plain can't tell whether it captures unique complementation, but I suspect not, because that would need introducing an existential quantification ('for every element there exists a complement s.t. ...') or a function -- neither of which they do. (Or of course you could express the existential as a negation of a nested universal quant -- but latticists seem to have a horror of that.)

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

R11 is easily expressed as the (unique) pseudcomplement of DUM aka R00 aka LMH's H. But they presumably don't want to define pseudocomplement for the same reasons.

Again, I conjectured that the 2x2 system is at least as strong as LMH AxRH1+AxRH2. Admittedly, having extra operations slows down Prover9 considerably.

The LMH axioms are just not adequate. I'd go so far as saying their paper is just a waste of time. We need a system a lot stronger. Never mind that it becomes difficult/slow to prove anything.

Distributivity in 2x2 system holds for natural join over the TTM Algebra A <OR>:

x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'.
(x' ^ (y ^ z)')' = (x' ^ y')' ^ (x' ^ z')'.

All the conditional versions, like the ones that you exhibited, follow from them.

Again this is useless if you can't define <OR> purely in terms of NatJoin, InnerUnion; or (equivalently) prove your complement operator is uniquely defined from those. All you've achieved is defining two (vaguely) orthogonal/non-identical lattice systems over the same set of elements. R00 is the identity element for <OR>, but it could be almost any element in the lattice. In fact IIRC there's a valid model where R00 === R10 (lattice bottom).

P.S. There is a different argument why there can't be finite set of equational axioms for Relational Lattice. The N5 is a Relational Lattice in the $\{\wedge,\vee,R_{00}\}$ signature that LMH use. Unfortunately, the direct product $N_5 \times N_5$ doesn't seem to be representable as relational lattice. Therefore, by Birkhoff theorem it is not a variety.

What is an example of a direct product N5 x N5`? Does it occur as a set of relation values for some 'universal heading'? Why should I care whether Birkhoff's theorem applies/whether a Relational Lattice structure forms a variety? Are you just gratuitously throwing terms around?

I want to exclude the possibility of an M3 sublattice or a benzene N6 sublattice. It seems the LMH axioms don't achieve that. By saying every element has a unique pseudocomplement, and properties of complements-of-complements, I am at least capturing those exclusions.

PreviousPage 2 of 2