Is there a convergent extended rewrite system for ternary boolean algebra, in which certain equations hold?
The source page states the original problem together with its recorded qualifications and progress updates as follows.
Is there a convergent extended rewrite system for ternary boolean algebra, for which the following permutative equations hold:
See [Zhang, 1995].
Recorded update.
Submitted by Hansj"org Lehner on Wed Dec 20 17:46:07 MET 2000.
\begin{verbatim}
The following permutative equations hold for every ternary boolean algebra:
f(f(x, y, z), u, x) = f(x, y, f(z, u, x)) f(x, y, z) = f(x, z, y) = f(y, x, z) = f(y, z, x) = f(z, x, y) = f(z, y, x)
Consider the following set of axioms:
Axiom 1: f(f(x1,x2,x3),x4,f(x1,x2,x5)) = f(x1,x2,f(x3,x4,x5)) Axiom 2: f(x1,x1,x2) = x1
This theorem holds true:
Theorem 1: f(f(A,B,C),D,A) = f(A,B,f(C,D,A))
Proof:
Lemma 1: z = f(z,x4,z)
z
= by Axiom 2 RL f(z,z,f(y,x4,x5)) = by Axiom 1 RL f(f(z,z,y),x4,f(z,z,x5)) = by Axiom 2 LR f(z,x4,f(z,z,x5)) = by Axiom 2 LR f(z,x4,z)
Theorem 1: f(f(A,B,C),D,A) = f(A,B,f(C,D,A))
f(f(A,B,C),D,A)
= by Lemma 1 LR f(f(A,B,C),D,f(A,B,A)) = by Axiom 1 LR f(A,B,f(C,D,A))
Consider the following set of axioms:
Axiom 1: x1 = f(x2,x1,x1) Axiom 2: x1 = f(x1,x2,g(x2)) Axiom 3: f(x1,x2,f(x3,x4,x5)) = f(f(x1,x2,x3),x4,f(x1,x2,x5))
This theorem holds true:
Theorem 1: f(A,B,C) = f(B,A,C)
Proof:
Lemma 1: f(f(g(x1),x0,q),x0,x1) = f(g(x1),x0,x1)
f(f(g(x1),x0,q),x0,x1)
= by Axiom 2 LR f(f(f(g(x1),x0,q),x1,g(x1)),x0,x1) = by Axiom 1 LR f(f(f(g(x1),x0,q),x1,g(x1)),x0,f(f(g(x1),x0,q),x1,x1)) = by Axiom 3 RL f(f(g(x1),x0,q),x1,f(g(x1),x0,x1)) = by Axiom 3 RL f(g(x1),x0,f(q,x1,x1)) = by Axiom 1 RL f(g(x1),x0,x1)
Lemma 2: f(g(g(y)),y,q) = g(g(y))
f(g(g(y)),y,q)
= by Axiom 2 LR f(f(g(g(y)),y,q),y,g(y)) = by Lemma 1 LR f(g(g(y)),y,g(y)) = by Axiom 2 RL g(g(y))
Lemma 3: g(g(z)) = z
g(g(z))
= by Lemma 2 RL f(g(g(z)),z,z) = by Axiom 1 RL z
Lemma 4: f(y,y,q) = y
f(y,y,q)
= by Lemma 3 RL f(g(g(y)),y,q) = by Lemma 2 LR g(g(y)) = by Lemma 3 LR y
Lemma 5: f(g(x1),y,x1) = y
f(g(x1),y,x1)
= by Lemma 1 RL f(f(g(x1),y,y),y,x1) = by Axiom 1 RL f(y,y,x1) = by Lemma 4 LR y
Lemma 6: f(v,u,x4) = f(u,x4,v)
f(v,u,x4)
= by Lemma 5 RL f(v,u,f(g(v),x4,v)) = by Axiom 3 LR f(f(v,u,g(v)),x4,f(v,u,v)) = by Axiom 1 LR f(f(v,u,g(v)),x4,f(f(v,v,v),u,v)) = by Axiom 1 LR f(f(v,u,g(v)),x4,f(f(v,v,v),u,f(v,v,v))) = by Axiom 3 RL f(f(v,u,g(v)),x4,f(v,v,f(v,u,v))) = by Lemma 4 LR f(f(v,u,g(v)),x4,v) = by Lemma 3 RL f(f(g(g(v)),u,g(v)),x4,v) = by Lemma 5 LR f(u,x4,v)
Theorem 1: f(A,B,C) = f(B,A,C)
f(A,B,C)
= by Lemma 6 RL f(C,A,B) = by Lemma 5 RL f(C,A,f(g(A),B,A)) = by Axiom 3 LR f(f(C,A,g(A)),B,f(C,A,A)) = by Axiom 1 RL f(f(C,A,g(A)),B,A) = by Axiom 2 RL f(C,B,A) = by Lemma 6 LR f(B,A,C)
Consider the following set of axioms:
Axiom 1: x1 = f(x2,x1,x1) Axiom 2: x1 = f(x1,x2,g(x2)) Axiom 3: f(x1,x2,f(x3,x4,x5)) = f(f(x1,x2,x3),x4,f(x1,x2,x5))
This theorem holds true:
Theorem 1: f(A,B,C) = f(A,C,B)
Proof:
Lemma 1: f(v,u,f(g(u),x4,u)) = f(v,x4,u)
f(v,u,f(g(u),x4,u))
= by Axiom 3 LR f(f(v,u,g(u)),x4,f(v,u,u)) = by Axiom 1 RL f(f(v,u,g(u)),x4,u) = by Axiom 2 RL f(v,x4,u)
Lemma 2: f(f(g(x1),x0,q),x0,x1) = f(g(x1),x0,x1)
f(f(g(x1),x0,q),x0,x1)
= by Lemma 1 RL f(f(g(x1),x0,q),x1,f(g(x1),x0,x1)) = by Axiom 3 RL f(g(x1),x0,f(q,x1,x1)) = by Axiom 1 RL f(g(x1),x0,x1)
Lemma 3: f(g(g(y)),y,q) = g(g(y))
f(g(g(y)),y,q)
= by Axiom 2 LR f(f(g(g(y)),y,q),y,g(y)) = by Lemma 2 LR f(g(g(y)),y,g(y)) = by Axiom 2 RL g(g(y))
Lemma 4: g(g(z)) = z
g(g(z))
= by Lemma 3 RL f(g(g(z)),z,z) = by Axiom 1 RL z
Lemma 5: f(y,y,q) = y
f(y,y,q)
= by Lemma 4 RL f(g(g(y)),y,q) = by Lemma 3 LR g(g(y)) = by Lemma 4 LR y
Lemma 6: f(v,u,x4) = f(v,x4,u)
f(v,u,x4)
= by Lemma 5 RL f(v,u,f(x4,x4,u)) = by Axiom 1 LR f(v,u,f(f(g(u),x4,x4),x4,u)) = by Lemma 2 LR f(v,u,f(g(u),x4,u)) = by Lemma 1 LR f(v,x4,u)
Theorem 1: f(A,B,C) = f(A,C,B)
f(A,B,C)
= by Lemma 6 LR f(A,C,B) \end{verbatim}