Expressing FDs without RENAME (nor COUNT)
Quote from AntC on July 30, 2019, 3:14 pmAlso as you said earlier:
One axiom is not enough to unambiguously define an operation.
Then I'm not seeing that one axiom for NOT MATCHING and one for REMOVE fixes anything.
It doesn't fix everything. What I need to demonstrate is that it fixes the constant R00 with very weak assumptions. Actually, one binary operation satisfying one axiom would suffice:
(x ^ y) ^ (x - y) = (x ^ y) ^ 0.
This operation fits NOT MATCHING. Formally, it can be defined (in terms of unsafe NOT) as:
x - y := x ^ <NOT>(y v (x ^ 0))
Again, this formula is just for illustrative purposes, because this binary minus is domain independent operation.
Now, the proof is really simple. Assuming there exists constant 1 satisfying the same identity we derive:
(x ^ y) ^ 0 = (x ^ y) ^ 1.
which is essentially
z ^ 0 = z ^ 1.
The 2 substitutions -- z:=0 and z:=1 -- produce
0 = 0 ^ 1. 1 = 0 ^ 1.
Now, onto your original question about NOT MATCHING itself, this sole axiom doesn't define it uniquely. Also, it doesn't define it uniquely together with:
(x ^ y) v (x - y) = x.
Now, with three additional relational lattice axioms from the aforementioned paper by Litak et.al. both Prover9 and Mace4 are busy for 10 minutes already...
P.S. I have trouble with binary minus in Prover9/Mace4 (because by default it is a unary operation?). I'm using forward and backward slashes instead.
Quote from Vadim on July 30, 2019, 5:15 pmQuote from AntC on July 30, 2019, 3:14 pmAlso as you said earlier:
One axiom is not enough to unambiguously define an operation.
Then I'm not seeing that one axiom for NOT MATCHING and one for REMOVE fixes anything.
...
Now, the proof is really simple. ...
Vadim, your posts on this thread have been a parade of misunderstandings, false claims, and downright dumb errors. You have not acknowledged that, nor shown you are reflecting on what I'm saying.
I'm travelling and not easily able to respond. On the balance of probability when someone who's been consistently wrong throughout claims "the proof is really simple" -- on a topic which I know isn't simple; and more to the point Tadeusz Litak has said [private correspondence to you] he has no proofs; I'm just not going to waste any more time.
Quote from Vadim on July 30, 2019, 5:15 pm
P.S. I have trouble with binary minus in Prover9/Mace4 (because by default it is a unary operation?). I'm using forward and backward slashes instead.
Yes, overriding the default operator binding/precedence doesn't work -- especially not for the logical connectives; despite what the manual claims. I've experienced various combos of it going OK in Prover9 but not Mace4 and/or not displaying properly in proofs and/or confusing the syntax-checker in the formula editor.
Prover9 is not a programming language, so there's no point in making the formulas look pretty. I would use prefix function form rather than trying to steal operators: remv(y, x).
And on the forum I use Tutorial D style, because it's not reasonable to expect readers to understand Prover9 nor QBQL.