The Forum for Discussion about The Third Manifesto and Related Matters

Please or Register to create posts and topics.

On uniqueness of R00

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 Vadim on July 9, 2021, 6:53 pm

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.

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 pm

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?

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 pm

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

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.

 

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.