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 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 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).orx ^ (y v z) != (x ^ y) v (x ^ z).x v (y ^ z) = (x v y) ^ (x v z).orx 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 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.
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.