On Relational Lattice complements, pseudocomplements, distributivity and Boolean algebras
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
R01akaDEEnor lattice bottomR10akaDumpty, because their definitions mention onlyNatJoin, InnerUnion. - Nor parallel
absPCompl( )(absolute pseudocomplement), because its definition mentions onlyR01, R10, plus those operators. mtchg( )is Tutorial DMATCHING. 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 mentionR00; neither alone 'fixes'mtchg( )as unique. So the fact they introduce an equality, and assert it exists and is unique contributes to the definition ofR00. Specifically, they're asserting you can 'push project through join'.- A definition of
NOT MATCHINGseems not required to fixR00, 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
% shadow R00
% 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 R00 , R11 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 pmQuote 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.