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

**Page 2 of 2**

Quote from AntC on July 2, 2021, 1:41 am## 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( )`

isTutorial 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 % 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

#### 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 % 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

Quote from Vadim on July 3, 2021, 6:19 pm#86 is a theorem in the 2x2 system [latex]\{\wedge,\vee,',`\}[/latex]:

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

#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 AntC on July 7, 2021, 7:42 amQuote from Vadim on July 3, 2021, 6:19 pm#86 is a theorem in the 2x2 system [latex]\{\wedge,\vee,',`\}[/latex]:

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 N

_{5}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 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]....

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 N_{5} 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 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

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 N

_{5 }is a Relational Lattice in the [latex]\{\wedge,\vee,R_{00}\}[/latex] signature that LMH use. Unfortunately, the direct product [latex]N_5 \times N_5 [/latex] doesn't seem to be representable as relational lattice. Therefore, by Birkhoff theorem it is not a variety.

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 N_{5 }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 AntC on July 8, 2021, 3:04 amQuote 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

lotstronger. 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 N

_{5 }is a Relational Lattice in the [latex]\{\wedge,\vee,R_{00}\}[/latex] signature that LMH use. Unfortunately, the direct product [latex]N_5 \times N_5 [/latex] 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

`N`

_{5}`x N`

_{5}? 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 M

_{3}sublattice or abenzeneN_{6}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.

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.

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 N

_{5 }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 `N`

_{5}` x N`

_{5}? 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 M_{3} sublattice or a *benzene* N_{6} 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.

**Page 2 of 2**