# On uniqueness of R00

Quote from Vadim on July 9, 2021, 6:53 pmThis development hinges on well known uniqueness of the lattice top [latex]R_{01}[/latex] and bottom [latex]R_{10}[/latex]. We investigate the uniqueness of the unary operation of tuple set complement, also known as TTM appendix A <NOT>. We use, however, postfix single quote -- the choice influenced by Prover9

already having a built-in operation with that name. In this notation

R00 = R01'.Therefore, if uniqueness of tuple complement is established, then the uniqueness of [latex]R_{00}[/latex] follows.

To formally investigate the uniqueness, we need a second version of this operation, which we'll use (

for this article only) the back quote:

op(300, postfix, "`" ).Our axiom system:

x ^ y = y ^ x.

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

x ^ (x v y) = x.

x v y = y v x.

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

x v (x ^ y) = x.

R10 = x ^ R10.

R01 = x v R01.

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

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

x ^ (y v z) = (x ^ (z v (R01` ^ y))) v (x ^ (y v (R01` ^ z))).

(R01` ^ (x ^ (y v z))) v (y ^ z) = ((R01` ^ (x ^ y)) v z) ^ ((R01` ^ (x ^ z)) v y).

x = (x ^ R10') v (x ^ R01').

x = (x ^ R10`) v (x ^ R01`).

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

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

x' ^ x = x ^ R01'.

x' v x = x v R10'.

x` ^ x = x ^ R01`.

x` v x = x v R10`.and the goal:

x'=x`.In this form the system eagerly exhibits counterexample models, starting with cardinality 2. An interesting development happens when we add explicit non-distributivity condition:

exists x exists y exists z x ^ (y v z) != (x ^ y) v (x ^ z).

Now the model checker minimal counterexample domain size is 12! This is remarkable, because the minimal non-distributive relational lattice with complement operation is of size 6.

Anthony, what is the minimal domain size in your approach when you add this non-distributivity condition?

This development hinges on well known uniqueness of the lattice top R_{01} and bottom R_{10}. We investigate the uniqueness of the unary operation of tuple set complement, also known as TTM appendix A <NOT>. We use, however, postfix single quote -- the choice influenced by Prover9 *already having a built-in operation with that name*. In this notation

**R00 = R01'.**

Therefore, if uniqueness of tuple complement is established, then the uniqueness of R_{00} follows.

To formally investigate the uniqueness, we need a second version of this operation, which we'll use (**for this article only**) the back quote:

**op(300, postfix, "`" ).**

Our axiom system:

**x ^ y = y ^ x.**

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

**x ^ (x v y) = x.**

**x v y = y v x.**

**(x v y) v z = x v (y v z).**

**x v (x ^ y) = x.**

**R10 = x ^ R10.**

**R01 = x v R01.**

**x ^ (y v z) = (x ^ (z v (R01' ^ y))) v (x ^ (y v (R01' ^ z))).**

**(R01' ^ (x ^ (y v z))) v (y ^ z) = ((R01' ^ (x ^ y)) v z) ^ ((R01' ^ (x ^ z)) v y).**

**x ^ (y v z) = (x ^ (z v (R01` ^ y))) v (x ^ (y v (R01` ^ z))).**

**(R01` ^ (x ^ (y v z))) v (y ^ z) = ((R01` ^ (x ^ y)) v z) ^ ((R01` ^ (x ^ z)) v y).**

**x = (x ^ R10') v (x ^ R01').**

**x = (x ^ R10`) v (x ^ R01`).**

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

**x ^ (y` ^ z`)` = ((x ^ y)` ^ (x ^ z)`)`.**

**x' ^ x = x ^ R01'.**

**x' v x = x v R10'.**

**x` ^ x = x ^ R01`.**

**x` v x = x v R10`.**

and the goal:

**x'=x`.**

In this form the system eagerly exhibits counterexample models, starting with cardinality 2. An interesting development happens when we add explicit non-distributivity condition:

exists x exists y exists z x ^ (y v z) != (x ^ y) v (x ^ z).

Now the model checker minimal counterexample domain size is 12! This is remarkable, because the minimal non-distributive relational lattice with complement operation is of size 6.

Anthony, what is the minimal domain size in your approach when you add this non-distributivity condition?

Quote from AntC on July 10, 2021, 2:14 amQuote from Vadim on July 9, 2021, 6:53 pmThis development hinges on well known uniqueness of the lattice top [latex]R_{01}[/latex] and bottom [latex]R_{10}[/latex]. We investigate the uniqueness of the unary operation of tuple set complement, also known as TTM appendix A <NOT>. We use, however, postfix single quote -- the choice influenced by Prover9

already having a built-in operation with that name.No Prover9 doesn't have a function. What's built in is the syntax. That doesn't make it a function until you've defined it (by giving equations). Suffixed graphics are unreadable. It looks like a caterpillar has fallen into the inkwell then crawled across the page. I've asked before for you not to use this unreadable stuff. Please use meaningful names like I do --

`absPCompl( )`

or`absolutePseudoComplement( )`

. It's like you (and LMH) don't want to communicate. So I won't.

Quote from Vadim on July 9, 2021, 6:53 pmThis development hinges on well known uniqueness of the lattice top R_{01} and bottom R_{10}. We investigate the uniqueness of the unary operation of tuple set complement, also known as TTM appendix A <NOT>. We use, however, postfix single quote -- the choice influenced by Prover9

already having a built-in operation with that name.

No Prover9 doesn't have a function. What's built in is the syntax. That doesn't make it a function until you've defined it (by giving equations). Suffixed graphics are unreadable. It looks like a caterpillar has fallen into the inkwell then crawled across the page. I've asked before for you not to use this unreadable stuff. Please use meaningful names like I do -- `absPCompl( )`

or `absolutePseudoComplement( )`

. It's like you (and LMH) don't want to communicate. So I won't.

Quote from AntC on July 10, 2021, 2:49 amQuote from Vadim on July 9, 2021, 6:53 pmexists x exists y exists z x ^ (y v z) != (x ^ y) v (x ^ z).

Now the model checker minimal counterexample domain size is 12! This is remarkable, because the minimal non-distributive relational lattice with complement operation is of size 6.

Anthony, what is the minimal domain size in your approach when you add this non-distributivity condition?

With that as goal, and my axioms (which are not yours), Mace hits a memory limit at model size 17, after ~20 seconds. Changing the

`!=`

to`=`

hits the memory limit also at size 17. Either of these forms:

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

or`x ^ (y v z) != (x ^ y) v (x ^ z).`

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

or`x v (y ^ z) != (x v y) ^ (x v z).`

Mace finds a counter-model size 6 (the same model in each case).

That corresponds to the first model here, for a single attribute

`B Bool`

other than`Dee, Dum`

.function(R00, [0]),

function(R002, [0]),

function(R01, [1]),

function(R10, [3]),

function(R11, [4]),

function(R112, [4]),

function(R1half, [2]),

function(R1half2, [2]),relation(cover(_,_), [ % see definition in my axioms in previous thread

0,0,0,1,0,0,

1,0,0,0,1,0,

0,0,0,1,0,0,

0,0,0,0,0,0,

0,0,1,0,0,1,

0,0,0,1,0,0])

Quote from Vadim on July 9, 2021, 6:53 pmexists x exists y exists z x ^ (y v z) != (x ^ y) v (x ^ z).

With that as goal, and my axioms (which are not yours), Mace hits a memory limit at model size 17, after ~20 seconds. Changing the `!=`

to `=`

hits the memory limit also at size 17. Either of these forms:

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

or`x ^ (y v z) != (x ^ y) v (x ^ z).`

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

or`x v (y ^ z) != (x v y) ^ (x v z).`

Mace finds a counter-model size 6 (the same model in each case).

That corresponds to the first model here, for a single attribute `B Bool`

other than `Dee, Dum`

.

function(R00, [0]),

function(R002, [0]),

function(R01, [1]),

function(R10, [3]),

function(R11, [4]),

function(R112, [4]),

function(R1half, [2]),

function(R1half2, [2]),

relation(cover(_,_), [ % see definition in my axioms in previous thread

0,0,0,1,0,0,

1,0,0,0,1,0,

0,0,0,1,0,0,

0,0,0,0,0,0,

0,0,1,0,0,1,

0,0,0,1,0,0])

Quote from AntC on July 10, 2021, 3:00 amQuote from Vadim on July 9, 2021, 6:53 pmThis development hinges on well known uniqueness of the lattice top [latex]R_{01}[/latex] and bottom [latex]R_{10}[/latex]. We investigate the uniqueness of the unary operation of tuple set complement, also known as TTM appendix A <NOT>. We use, however, postfix single quote -- the choice influenced by Prover9

already having a built-in operation with that name. In this notation

R00 = R01'.Some of your axioms use

`R10'`

. That's tuple complement of lattice bottom; which should be`R11`

. Is it? That is, is tuple complement sufficiently defined to prove that? I don't follow your caterpillar-scratchings, but I guess if you're failing to fix tuple complement; you're also failing to fix`R00`

or`R11`

.

Quote from Vadim on July 9, 2021, 6:53 pmThis development hinges on well known uniqueness of the lattice top R_{01} and bottom R_{10}. We investigate the uniqueness of the unary operation of tuple set complement, also known as TTM appendix A <NOT>. We use, however, postfix single quote -- the choice influenced by Prover9

already having a built-in operation with that name. In this notation

R00 = R01'.

Some of your axioms use `R10'`

. That's tuple complement of lattice bottom; which should be `R11`

. Is it? That is, is tuple complement sufficiently defined to prove that? I don't follow your caterpillar-scratchings, but I guess if you're failing to fix tuple complement; you're also failing to fix `R00`

or `R11`

.

Quote from Vadim on July 10, 2021, 4:04 pmYou can increase Mace 4 memory. However, if model search progresses too fast and runs out of memory, that is likely to be an error in the input. For example, if I remove existential quantification in the non-distributivity condition above then the model checker quickly goes up to domain size 76 running out of memory.

After analyzing the aforementioned model of size 12 I have added the condition that the interval between

`R00`

and`R01`

doesn't contain any other lattice elements

x = x v R01' -> x = R01' | x = R01.

x = x v R01` -> x = R01` | x = R01.Currently, the model checker runs for 16 hours, up to the model size 15.

You can increase Mace 4 memory. However, if model search progresses too fast and runs out of memory, that is likely to be an error in the input. For example, if I remove existential quantification in the non-distributivity condition above then the model checker quickly goes up to domain size 76 running out of memory.

After analyzing the aforementioned model of size 12 I have added the condition that the interval between `R00`

and `R01`

doesn't contain any other lattice elements

**x = x v R01' -> x = R01' | x = R01.**

**x = x v R01` -> x = R01` | x = R01.**

Currently, the model checker runs for 16 hours, up to the model size 15.

Quote from AntC on November 12, 2023, 9:21 amQuote from Vadim on July 9, 2021, 6:53 pm... An interesting development happens when we add explicit non-distributivity condition:

exists x exists y exists z x ^ (y v z) != (x ^ y) v (x ^ z).

I agree the (non-)distributivity characteristics are critical to describing relational lattice(s). This previous post illustrates a

`N`

_{5}non-distributive lattice. Your axiom here merely saying there must be some non-distributivity isn't specific enough. I've tried a combination of these:

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

- The Litak et al three axioms. Note two of them mention
`R00`

.- An axiom spec'ing that the sub-lattice of empty relvals form a distributive lattice:

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

In which`(x ^ R00)`

etc means some arbitrary relval`x`

, 'emptified'.- An axiom spec'ing that any sub-lattice of relvals with the same heading form a distributive lattice:

`x ^ R00 = y ^ R00 & y ^ R00 = z ^ R00 -> x v (y ^ z) = (x v y) ^ (x v z).`

In which`x ^ R00 = y ^ R00`

etc means 'emptified'`x`

equals 'emptified'`y`

-- that is, they have the same Heading.

(This axiom is implied by the Litak et al's.)- What I've added is an axiom stating for all relvals other than
`DEE, DUM`

/`R01, R00`

: there must be at least two other distinct relvals with the same Heading [**]:

`x ^ R00 != R00 -> (exists y (exists z ( (y ^ R00 = x ^ R00 & z ^ R00 = x ^ R00) & ((x != y & x != z) & y != z ) ) ) ).`

Again`x ^ R00 = y ^ R00`

etc means 'emptified'`x`

equals 'emptified'`y`

; but`x != y`

means they're distinct relvals. [***]Litak et al would hate these axioms: they use implications, they use existential quant, they use disequalities.

Although I'd experimented previously with those (or something like them); I'd assumed they wouldn't be effective until I'd 'fixed'

`R00/DUM`

. Instead now, I've taken the attitude: they're all part of the properties of`R00`

; perhaps in combination they'll constrain the model enough to be useful.So, standard tactic: take a copy of the six axioms mentioning

`R00`

; change`R00`

to`R002`

throughout, so we've 'competing' definitions;_{get a proof that R00 = R002. (whisper it)}Given my track record of messing up proofs and prematurely announcing results, I'm very hesitant. Furthermore, using

`R00`

to define follow-on operators like`NotMatching, Remove`

is failing to yield proofs of uniqueness. (But not finding counter-models either.)Would somebody like to reproduce my results, please.

Notes:

- [**] The requirement all relvals with non-empty Heading must have at least three relvals -- that is, an Attribute type with at least two values -- is pragmatically not an annoyance:
`Bool`

is the smallest cardinality type. (The worked example I linked to has a single attribute`REL {B Bool} {...}`

.) But it offends against the theoretical purity of the model: we should be able to model Attribute types with a single or even no value (`Unit, Void`

). Of course aDcan include such types; it just can't write them to a relval. (`Unit`

's OK providing it's not the only Attribute.)- [***] Note that last axiom
doesn'trequire there to be relvals with non-empty Heading. So just`{DEE, DUM}`

is a valid model -- rather satisfying. It saysifthere's a relval with non-empty Heading, there must be at least two more. [****] (This is less restrictive than Vadim's axiom I quoted.)- [****] For this reason, I don't need/don't define lattice bottom (
`R10`

aka`Dumpty`

the empty relval with all possible Attributes) nor the 'full as possible' relval (`R11`

with all possible Attributes, all possible tuples). It's a big relief not to have to rely on such Domain Dependence.

Quote from Vadim on July 9, 2021, 6:53 pm... An interesting development happens when we add explicit non-distributivity condition:

exists x exists y exists z x ^ (y v z) != (x ^ y) v (x ^ z).

I agree the (non-)distributivity characteristics are critical to describing relational lattice(s). This previous post illustrates a `N`

_{5} non-distributive lattice. Your axiom here merely saying there must be some non-distributivity isn't specific enough. I've tried a combination of these:

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

- The Litak et al three axioms. Note two of them mention
`R00`

. - An axiom spec'ing that the sub-lattice of empty relvals form a distributive lattice:

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

In which`(x ^ R00)`

etc means some arbitrary relval`x`

, 'emptified'. - An axiom spec'ing that any sub-lattice of relvals with the same heading form a distributive lattice:

`x ^ R00 = y ^ R00 & y ^ R00 = z ^ R00 -> x v (y ^ z) = (x v y) ^ (x v z).`

In which`x ^ R00 = y ^ R00`

etc means 'emptified'`x`

equals 'emptified'`y`

-- that is, they have the same Heading.

(This axiom is implied by the Litak et al's.) - What I've added is an axiom stating for all relvals other than
`DEE, DUM`

/`R01, R00`

: there must be at least two other distinct relvals with the same Heading [**]:

`x ^ R00 != R00 -> (exists y (exists z ( (y ^ R00 = x ^ R00 & z ^ R00 = x ^ R00) & ((x != y & x != z) & y != z ) ) ) ).`

Again`x ^ R00 = y ^ R00`

etc means 'emptified'`x`

equals 'emptified'`y`

; but`x != y`

means they're distinct relvals. [***]

Litak et al would hate these axioms: they use implications, they use existential quant, they use disequalities.

Although I'd experimented previously with those (or something like them); I'd assumed they wouldn't be effective until I'd 'fixed' `R00/DUM`

. Instead now, I've taken the attitude: they're all part of the properties of `R00`

; perhaps in combination they'll constrain the model enough to be useful.

So, standard tactic: take a copy of the six axioms mentioning `R00`

; change `R00`

to `R002`

throughout, so we've 'competing' definitions; _{get a proof that R00 = R002. (whisper it)}

Given my track record of messing up proofs and prematurely announcing results, I'm very hesitant. Furthermore, using `R00`

to define follow-on operators like `NotMatching, Remove`

is failing to yield proofs of uniqueness. (But not finding counter-models either.)

Would somebody like to reproduce my results, please.

Notes:

- [**] The requirement all relvals with non-empty Heading must have at least three relvals -- that is, an Attribute type with at least two values -- is pragmatically not an annoyance:
`Bool`

is the smallest cardinality type. (The worked example I linked to has a single attribute`REL {B Bool} {...}`

.) But it offends against the theoretical purity of the model: we should be able to model Attribute types with a single or even no value (`Unit, Void`

). Of course a**D**can include such types; it just can't write them to a relval. (`Unit`

's OK providing it's not the only Attribute.) - [***] Note that last axiom
*doesn't*require there to be relvals with non-empty Heading. So just`{DEE, DUM}`

is a valid model -- rather satisfying. It says*if*there's a relval with non-empty Heading, there must be at least two more. [****] (This is less restrictive than Vadim's axiom I quoted.) - [****] For this reason, I don't need/don't define lattice bottom (
`R10`

aka`Dumpty`

the empty relval with all possible Attributes) nor the 'full as possible' relval (`R11`

with all possible Attributes, all possible tuples). It's a big relief not to have to rely on such Domain Dependence.

Quote from AntC on November 18, 2023, 7:06 amQuote from AntC on November 12, 2023, 9:21 am

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

BTW, the Litak axioms (+ the usual behaviour for

`^, v`

) don't seem sufficient to prove this.I can't see any adequate account of Relational lattices could allow an element in between

`DUM, DEE`

. (Essentially that's how I distinguish`DUM`

: it's the only empty relation immediately adjacent to`DEE`

.)

Quote from AntC on November 12, 2023, 9:21 am

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

BTW, the Litak axioms (+ the usual behaviour for `^, v`

) don't seem sufficient to prove this.

I can't see any adequate account of Relational lattices could allow an element in between `DUM, DEE`

. (Essentially that's how I distinguish `DUM`

: it's the only empty relation immediately adjacent to `DEE`

.)