question about relation algebra (eliminating variables)

[YKY (Yan King Yin, 甄景贤)]

Look at this formula in first-order logic:

    f(X,Y) /\ f(W,Z) -> g(X,Z)

(for all X,Y,W,Z).

How can this be expressed in a bound-variable-free way?

I have looked at relation algebra, ie the following system with signature (2,2,1,2,1):

​

So I can write:

    grandfather = father ∘ father

or

    g = f ∘ f

which in first-order logic would be:

    g(X,Z) = f(X,Y) /\ f(W,Z), Y = W

But if I remove the Y=W condition, is it still possible to express

   g(X,Z) = f(X,Y) /\ f(W,Z)

in relation algebra?  Or combinatory logic?  (I can introduce new combinators or relational operators as long as they do not involve quantified first-order logic variables).

[Ivan Vodišek]

why not:

g (X, Z) = f (X, Y) /\ f (Y, Z)

[YKY (Yan King Yin, 甄景贤)]

On Mon, Jul 21, 2014 at 7:57 PM, Ivan Vodišek <ivan....@gmail.com> wrote:

why not:

g (X, Z) = f (X, Y) /\ f (Y, Z)

Cylindric algebra provides an operator, called the diagonal set, denoted D_xy, that ​is the set of all elements in the universe such that x=y.

Using this operator, I suppose we can avoid explict substitution of bound variables by using purely algebraic operations.  But so far I cannot work it out algebraically.

I have asked it on Stack Exchange Mathematics:

http://math.stackexchange.com/questions/874485/simple-exercise-in-cylindric-algebra