Quote from p c on August 23, 2019, 10:23 pm

 

 

Quote from AntC on August 24, 2019, 6:47 am

Quote from Vadim on August 23, 2019, 9:10 pm

Vadim, I don't know who you think you're trying to persuade, or why you think it's persuasive. You've written precisely this before; and I've rebuffed it before. Mace4 rejects that this could be a definition of R00 within a few seconds, in multiple ways.

I'll say again: we need R00 fixed uniquely in terms of lattice meet/join. And the definition you present fails. This is nothing to do with introducing domain-dependent operations. (By the way, you're using "unsafe" incorrectly.)

I presume you intend R00 defined as the identity element for operation + -- which you want to be equivalent to Appendix A's <OR>. For the purposes of the following disproofs, I'll also define R11 as the absorbing element for +. I have R01 defined as the identity element for lattice meet (^) i.e. lattice top; and R10 defined as the absorbing element for ^ i.e. lattice bottom. Note that to define a lattice we only need one operation that is idempotent, commutative, associative; so I'll ignore your *. I'll also avoid the issue of whether this makes R00 the 'sideways' lattice's top or bottom.

We know a lot about the inter-relations of the four 'cardinal points' of a relational lattice. I'm using 'relational lattice' in the sense defined by Litak et al; and I shall ignore your 'galaxy'.

• R00 = R10 v (R10 ^ R00). % gloss: projecting lattice bottom (the empty relation of all attributes) on to the heading of lattice top gives R00.

Prover9 is happy to prove that. In the proof you can see it reduces the goal to x = R10 v x., which merely amounts to R10 is the identity element for v, so that's not at all specific to R00.

For the following equations involving the cardinal points, Mace4 finds counter-examples in less than a second each:

• R00 ^ R11 = R10. % gloss: taking the heading-only of the relation with all attributes, all possible tuples gives lattice bottom.
• R00 v R11 = R01. % gloss: taking the relation with all attributes, all possible tuples projected on to degree zero gives lattice top.
• R00 ^ x != x <-> x v R00 = R01. % gloss: x being non-empty is equivalent to x InnerUnion R00 being lattice top.

So introducing domain-dependent operations and potentially-infinite relation constants is no help. Yes, you've defined an 'alternative lattice' over the same set of elements; No you haven't fixed how the elements correspond to the lattice fixed by ^  -- which is to say that in the alternative lattice defined by +, there are many candidates for R01, R10.

And although those equations amongst the four cardinal points are sufficient to reject your definitions very quickly, they're not sufficient to fix R00. That's where I'm stuck.

I agree that there is subtle distinction between R00 and Dum. The first one is defined purely algebraically, while the second one is defined in database/set theoretic means.  And with the axioms that we have we can't guarantee that R00 can be interpreted as a relation with the empty set of attributes and empty set of tuples.

Yet, R00 is uniquely defined with rudimentary set of axioms. I will leverage the unary complement operation (AKA TTM <NOT>). Those readers whose religion doesn't admit domain unsafe operations are welcome to translate the proof replacing the complement with binary MINUS (AKA <NOT MATCHING>) operation, which is domain independent.

Formally, we use the algebraic system which is the standard lattice amended with unary complement with only one extra axiom -- the law of double complement:

(x') ' = x.

Next we define the two binary operations:

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

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

Informally, the first operation -- + -- can be interpreted as the familiar TTM <OR>. The second one -- *-- is less intuitive and, as Anthony noticed, is of questionable practical value. Yet, it is not hard to prove this pair of operations forms an alternative lattice structure, which lattice bottom is R00.

I anticipate certain readers being not quite satisfied with my approach to uniqueness. Here it has been proven that R00 is fixed with respect to a galaxy (that is lattice structure considered as universal algebra). Can we compare R00 constants (AKA "galaxy centers") in different galaxies; after all, they all are supposedly interpreted as DUM, so they should be the same? Certainly not, because different galaxies are not comparable by purely algebraic means.

 

 

 

 

 

 

 

 

 

Quote from AntC on August 24, 2019, 11:38 am

Quote from Vadim on August 23, 2019, 9:10 pm

Ah, a couple of follow-ups to show your model is not what you think it is.

Yet, R00 is uniquely defined with rudimentary set of axioms. I will leverage the unary complement operation (AKA TTM <NOT>). Those readers whose religion doesn't admit domain unsafe operations ...

... will be quite happy with the following model:

Formally, we use the algebraic system which is the standard lattice amended with unary complement with only one extra axiom -- the law of double complement:

(x') ' = x.

That's consistent with ' being the identity operation. Then ...

Next we define the two binary operations:

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

That's consistent with + being the same as ^.

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

And that's consistent with * being the same as v.

So these axioms (with the usual lattice axioms) have a two-element model in which R00 is indeed fixed -- as R01, and R11 is indeed fixed -- as R10.

I could (rather clunkily -- our quasiequational friends wouldn't be happy) add an axiom x' != x. Now we get a two-element model with the operations flipped round and R00 = R10.

Quote from Vadim on October 14, 2019, 7:41 pm

Here is another attempt which doesn't produce immediate counter examples in Mace4 (while Prover9 is still working on the proof).

I was unsuccessful trying to prove uniqueness of tuple complement in an axiom system with reduced signature (^,v,'). Therefore, I have to use the full system (^,v,',`).  There, both binary lattice operations are well established as unique, and it is the uniqueness of both unary operations that has to be proven. Therefore, for tuple complement -- postfix ' -- we introduce duplicate operation in functional notation not(), and for attribute inversion -- postfix back quote ` -- we introduce another duplicate inv().

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

x = (x ^ y') v (x ^ y`).
x = (x ^ not(y)) v (x ^ inv(y)).

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

(y` ^ x') v (y' ^ x `) = (y' v x') ^ (y` v x `).
(inv(y) ^ not(x)) v (not(y) ^ inv(x)) = (not(y) v not(x)) ^ (inv(y) v inv(x)).

x' ^ x = x ^ ((x' ^ x)` ^ x)`.
not(x) ^ x = x ^ inv(inv(not(x) ^ x) ^ x).

x' v x = x v (x' v x`)`.
not(x) v x = x v inv(not(x) v inv(x)).

x` ^ x = (x' v x`)` ^ x.
inv(x) ^ x = inv(not(x) v inv(x)) ^ x.

x` v x = ((x' ^ x)` ^ x)` v x.
inv(x) v x = inv(inv(not(x) ^ x) ^ x) v x.

((x' ^ x)` ^ x)` = inv(inv(not(x) ^ x) ^ x).
(x' v x`)`=inv(not(x) v inv(x)).

Theorem (well, conjecture, at the moment):

x' = not(x).

In the above axiom system, both R00 and R11 are expressed in terms of (^,v,',`) signature, and the last two  identities equate each constant in duplicate notation.

 

Quote from AntC on October 15, 2019, 10:49 am

Quote from Vadim on October 14, 2019, 7:41 pm

Here is another attempt which doesn't produce immediate counter examples in Mace4 (while Prover9 is still working on the proof).

Thank you Vadim.

I was unsuccessful trying to prove uniqueness of tuple complement in an axiom system with reduced signature (^,v,'). Therefore, I have to use the full system (^,v,',`).  There, both binary lattice operations are well established as unique, and it is the uniqueness of both unary operations that has to be proven.

Therein is the reason Mace4 can't find a counter-example; and the reason Prover9 is still working. Assuming all of your axioms are needed to 'fix' both operators, then '/not is defined partially in terms of `/inv, and `/inv is defined partially in terms of '/not. So Prover9 can't infer that x' = not(x). unless until it can infer x` = inv(x)., and vice versa. I think Prover9 will never finish.

A useful exercise would be to give no goals, and get Mace4 to produce a model. That is, any model consistent with the axioms. I suspect that for any model beyond the trivial 4 elements, it'll either fail or produce a function table you won't be happy with.

Therefore, for tuple complement -- postfix ' -- we introduce duplicate operation in functional notation not(), and for attribute inversion -- postfix back quote ` -- we introduce another duplicate inv().

The axiom system:

...

Theorem (well, conjecture, at the moment):

x' = not(x).

In the above axiom system, both R00 and R11 are expressed in terms of (^,v,',`) signature, and the last two  identities equate each constant in duplicate notation.

 

If I'm wrong and those operators are fixed (can be inferred to be fixed), we should have R00 = R01'. R00 = R10`. R11 = R10'. R11 = R01`. ? Can the system infer R01' = R10`. R10' = R01`.?

Quote from Vadim on October 15, 2019, 5:14 pm

Quote from AntC on October 15, 2019, 10:49 am

Therein is the reason Mace4 can't find a counter-example; and the reason Prover9 is still working. Assuming all of your axioms are needed to 'fix' both operators, then '/not is defined partially in terms of `/inv, and `/inv is defined partially in terms of '/not. So Prover9 can't infer that x' = not(x). unless until it can infer x` = inv(x)., and vice versa. I think Prover9 will never finish.

Any axiom defines one operation partially in terms of the others. ("Constrain" would be better but still quite sloppy wording). For example, absorption "defines" lattice meet in terms of join. However, why stop at one level of dependency? But then, transitive closure of the operation dependencies would quickly infer the full dependency graph.

Another way to see it is adding x` = inv(x).to the list of axioms (or inlining inv(x) everywhere). It appears to change nothing as far as model search or proving is concerned...

Automatic theorem proving is well known to be NP-complete or even worse, and this is the real reason why Prover9 hangs. Forget about computational complexity, even decideability of relational lattices is not clear. Santocanale has published series of papers on this topic; but man, if you think Litak&Mikulas&Hidders paper were tough to digest, this one is next level...

A useful exercise would be to give no goals, and get Mace4 to produce a model. That is, any model consistent with the axioms. I suspect that for any model beyond the trivial 4 elements, it'll either fail or produce a function table you won't be happy with.

From your earlier postings and this comment I infer that you doubt my axiom system. Let's call it 2x2 for future reference, where the first number refers to two binary operations, while the second one refers to two unary ones. Which axiom in the 2x2 system

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

x' ^ x = x ^ R00.
x' v x = x v R11.

x` ^ x = R11 ^ x.
x` v x = R00 v x.

do you suspect is wrong?

Here are several alternative definitions for the constants

R00 = ((x' ^ x)` ^ x)`.
R00 = ((x` v x)' v x)'
R00 = (x' v x`)``'.
R11 = (x' v x`)`.
R11 = ((x` ^ x)' ^ x)'.

but in my experience Prover9 is faster (when it finishes a proof) with explicit constants, versus when their definitions are inlined into main axioms.

If I'm wrong and those operators are fixed (can be inferred to be fixed), we should have R00 = R01'. R00 = R10`. R11 = R10'. R11 = R01`. ? Can the system infer R01' = R10`. R10' = R01`.?

Those are proved instantaneously:

1 R00 = R01'. [goal].
2 x ^ y = y ^ x. [assumption].
3 x' ^ x = x ^ R00. [assumption].
4 x ^ x' = x ^ R00. [para(2(a,1),3(a,1))].
5 R01 ^ x = x. [assumption].
6 R01' != R00. [deny(1)].
7 x = x ^ R01. [para(5(a,1),2(a,1))].
8 x ^ R01 = x. [copy(7),flip(a)].
9 R01' = R01 ^ R00. [para(5(a,1),4(a,1))].
10 R01' = R00 ^ R01. [para(2(a,1),9(a,2))].
11 R01' = R00. [para(8(a,1),10(a,2))].
12 $F. [resolve(11,a,6,a)].

Quote from Vadim on October 15, 2019, 10:39 pm

Actually, my comment that assuming x` = inv(x). doesn't change anything was too hasty. After 25 minutes it it proved the uniquiness of negation. (For comparison, I killed the prior attempt after 3 hours.)

% -------- Comments from original proof --------
% Proof 1 at 1533.36 (+ 26.19) seconds.
% Length of proof is 424.
% Level of proof is 40.
% Maximum clause weight is 40.
% Given clauses 8548.

1 x' = not(x) # label(non_clause) # label(goal). [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),rewrite([5(5)]),flip(a)].
10 x = (x ^ not(y)) v (x ^ y `). [assumption].
11 (x ^ y `) v (x ^ not(y)) = x. [copy(10),rewrite([5(5)]),flip(a)].
12 x ^ (y' ^ z')' = ((x ^ y)' ^ (x ^ z)')'. [assumption].
13 ((x ^ y)' ^ (x ^ z)')' = x ^ (y' ^ z')'. [copy(12),flip(a)].
14 x ^ not(not(y) ^ not(z)) = not(not(x ^ y) ^ not(x ^ z)). [assumption].
15 not(not(x ^ y) ^ not(x ^ z)) = x ^ not(not(y) ^ not(z)). [copy(14),flip(a)].
20 x' ^ x = x ^ ((x' ^ x) ` ^ x) `. [assumption].
21 x ^ (x ^ (x ^ x') `) ` = x ^ x'. [copy(20),rewrite([2(2),2(4),2(6)]),flip(a)].
22 not(x) ^ x = x ^ ((not(x) ^ x) ` ^ x) `. [assumption].
23 x ^ (x ^ (x ^ not(x)) `) ` = x ^ not(x). [copy(22),rewrite([2(2),2(4),2(6)]),flip(a)].
24 x' v x = x v (x' v x `) `. [assumption].
25 x v (x ` v x') ` = x v x'. [copy(24),rewrite([5(2),5(5)]),flip(a)].
26 not(x) v x = x v (not(x) v x `) `. [assumption].
27 x v (x ` v not(x)) ` = x v not(x). [copy(26),rewrite([5(2),5(5)]),flip(a)].
28 x ` ^ x = (x' v x `) ` ^ x. [assumption].
29 x ^ (x ` v x') ` = x ^ x `. [copy(28),rewrite([2(2),5(5),2(7)]),flip(a)].
36 ((x' ^ x) ` ^ x) ` = ((not(x) ^ x) ` ^ x) `. [assumption].
37 (x ^ (x ^ not(x)) `) ` = (x ^ (x ^ x') `) `. [copy(36),rewrite([2(2),2(4),2(7),2(9)]),flip(a)].
38 (x' v x `) ` = (not(x) v x `) `. [assumption].


...

I cut out the rest, but you can see all the assumptions made from this snippet. The effort involved prompts the conclusion that uniqueness of tuple complement (and, consequently, R00) is nontrivial matter.

 

Quote from AntC on October 16, 2019, 4:07 am

Quote from Vadim on October 15, 2019, 10:39 pm

Actually, my comment that assuming x` = inv(x). doesn't change anything was too hasty. After 25 minutes it it proved the uniquiness of negation.

And you might find that if you instead add an assumption x' = not(x). you can 'prove the uniqueness' of inversion. No that's not a proof of uniqueness in either case, because you no longer have independent parallel definitions of the operators.

...

I cut out the rest, but you can see all the assumptions made from this snippet. The effort involved prompts the conclusion that uniqueness of tuple complement (and, consequently, R00) is nontrivial matter.

 

I agree the uniqueness of tuple complement is problematic. I disagree that necessarily intrudes on R00. Because I think there's another way to fix R00  that doesn't involve complements or inversions at all. That is, by using its unique position in N₅ sub-lattices that have uppermost element R01. I'm just not able to put any time into trying, for the moment.

From your previous message wrt R00:

Here are several alternative definitions for the constants

R00 = ((x' ^ x)` ^ x)`.
R00 = ((x` v x)' v x)'
R00 = (x' v x`)``'.
R11 = (x' v x`)`.
R11 = ((x` ^ x)' ^ x)'.

but in my experience Prover9 is faster (when it finishes a proof) with explicit constants, versus when their definitions are inlined into main axioms.

> If I'm wrong and those operators are fixed (can be inferred to be fixed), we should have R00 = R01'. R00 = R10`. R11 = R10'. R11 = R01`. ?

> Can the system infer R01' = R10`. R10' = R01`.?

Those are proved instantaneously:

1 R00 = R01'. [goal]. ...

No that goal is not one of "those" I was asking about. Those last two equations from me use only lattice top and bottom, not R00. If they're provable, it tells us something about tuple negation and header inversion, not about R00.

Quote from AntC on October 16, 2019, 5:00 am

Quote from Vadim on October 15, 2019, 5:14 pm

Quote from AntC on October 15, 2019, 10:49 am

Therein is the reason Mace4 can't find a counter-example; and the reason Prover9 is still working. Assuming all of your axioms are needed to 'fix' both operators, then '/not is defined partially in terms of `/inv, and `/inv is defined partially in terms of '/not. So Prover9 can't infer that x' = not(x). unless until it can infer x` = inv(x)., and vice versa. I think Prover9 will never finish.

Any axiom defines one operation partially in terms of the others.

No. The way to build up axioms is to first fully define one operator. Then use it to define another. The trouble with your negation/inversion definitions is they're mutually recursive. Now you can solve 'simultaneous equations' for variables. As I understand it for functions, you need some advanced form of solving with second-order logic (so beyond Prover9). For an example of a tractable way to build up, here's a non-standard definition of lattice operators.

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

R01 ^ x = x.
R10 ^ x = R10.

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

Firstly define lattice meet as idempotent, commutative, associative. That's sufficient to fix ^ as unique. Therefore its identity element and absorbing element (R01, R10) are fixed unique.

Then use the absorption law (in effect) to define lattice join as the dual of lattice meet. From that definition can be proven:

• v is uniquely defined (prove that by a parallel definition of the operator).
• v is idempotent, commutative, associative.
• The standard form of absorption laws x ^ (x v y) = x.  y ^ (x v y) = y.

 

Automatic theorem proving is well known to be NP-complete or even worse, and this is the real reason why Prover9 hangs.

To be precise: there's three possible reasons Prover9 hangs. Yes one is that theorem proving is NP-complete. Another is Gödel incompleteness: given a bunch of axioms, there are always theorems that are neither implied by the axioms nor is their negation implied. Thirdly there are theorems that need higher-order unification to prove from the axioms. Prover9 (SAT solvers in general) don't do that. I think it's the third that's biting in case of your negation/inversion operators.

 

...

From your earlier postings and this comment I infer that you doubt my axiom system.

If by "doubt" you mean I think some axioms are false or inconsistent: no I haven't looked in enough detail. What I mean is your equations are in a form they're not tractable for inference: in the third, both operators appear (and multiple times) on both sides of the =; in the second only ' appears, but again it appears multiply on both sides of =; in the first both operators appear once only, attached to y which isn't 'anchored' on the other side of the =.

Contrast that in my above definition for v: the definiendum appears on only one side of <->; it appears twice but with the same operands each time; those operands are anchored on the other side of the <->; the other univ quantified variable also appears on both sides. Now of course I could give equivalent definitions not using <->, but they'd still have those 'anchoring' characteristics. So I remain perplexed why Litak et al want to limit themselves to quasiequational forms of axioms.

Let's call it 2x2 for future reference, where the first number refers to two binary operations, while the second one refers to two unary ones. Which axiom in the 2x2 system

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

x' ^ x = x ^ R00.
x' v x = x v R11.

x` ^ x = R11 ^ x.
x` v x = R00 v x.

do you suspect is wrong?