simple exercise in Cylindric algebra I am trying to gain a better understanding of cylindric algebra, so I made up this example.
Given a general rule that someone's father's father is his/her grandfather:
$\forall_X ~ \forall_Y ~ \forall_Z ~~ \{ ~ f(X,Y) \wedge f(Y,Z) \rightarrow g(X,Z) ~ \} $
And given that Albert is Bob's father and Bod is Carol's father:
$ f(a,b) $
$ f(b,c) $
I want to derive that Albert is Carol's grandfather:
$ \vdash g(a,c) $ 
This set of axioms for cylindric algebra is worked out by Tarski in 1959:


*

*$\left< A, +, \cdot, \neg \right>$ is a boolean algebra

*$\exists_\kappa 0 = 0$

*$x \cdot \exists_\kappa \; x = x$

*$\exists_\kappa (x \cdot \exists_\kappa ~ y) = \exists_\kappa ~ x \cdot \exists_\kappa ~ y$

*$\exists_\kappa \exists_\lambda ~ x = \exists_\lambda \exists_\kappa ~ x$

*$D_{\kappa\kappa} = 1$

*$D_{\kappa\lambda} = \exists_\mu (D_{\kappa\mu} \cdot D_{\mu\lambda}) $ for all $\kappa, \lambda \neq \mu$

*$\exists_\kappa (D_{\kappa\lambda}\cdot x) \cdot \exists_\kappa (D_{\kappa\lambda}\cdot \neg x) = 0$ for all $\kappa \neq \lambda$

*for each $x$ there exists $\mu < \omega$ such that $\exists_\nu ~ x$ for every $\nu$ where $\mu < \nu < \omega$


where $\exists$ denotes cylindrification and $D_{\kappa\lambda}$ is the diagonal set (ie, the set of the entire domain where $\kappa = \lambda$).
Attempted solution:
First I try to make the equating of variables explicit:
$\forall_x ~ \forall_y ~ \forall_w ~ \forall_z ~~ \{ ~ f(x,y) \wedge f(w,z) \wedge (y=w) \rightarrow g(x,z) ~ \} $
(This is because $D_{\kappa\lambda}$ seems to be for this purpose.  I can also make the equality of x's and z's on both sides explicit, but I wonder what is to be gained by this?)
Then I convert the $\forall~$'s to $\exists~$'s and I get this formula:
$ \neg ~ \exists_x ~\exists_y ~ \exists_w ~ \exists_z ~  D_{yw} ~~ \{ f(x,y) \wedge f(w,z) \wedge \neg g(x,z) \}$
But now I need to make some substitutions like {$john/x$} but I'm not sure if that is what I'm supposed to do in cylindric algebra.  I suppose the point of cylindric algebra is to avoid explicit substitutions by performing algebraic operations only?
 A: Maybe I can try to answer my own question:
Suppose our universe are people in the family, ie, the set $\{john,\; pete, \; paul, \; mary, \; jane, \; ...\}$.
Use small letters $x,y,z,w...$ to represent variables of objects in the universe, ie, $x$ may be instantiated to $john$, etc.
Use capital letters $X,Y,Z,W,...$ to represent infinite sequences of variable instantiations.  For example, sequence $X$ may denote that $x$ is instantiated to $john$, $y$ is instantiated to $mary$, ... and so on.
The cylindrification operator ($C_i$) applies to sequence variables.  When $C_i$ is applied to a class of sequences, all the original sequences plus the sequences obtained by ringing changes in the $i$-th index will be included.
For example a formula $\phi$ may contain the variable $y$.  Let $X$ denote the class of sequences that satisfies $\phi$.  What sequences will satisfy $(\exists y)\phi$?  They are all the original sequences plus the ones obtained by ringing changes in $y$ (because the existence of any $y$ already suffices to make the formula true, what $y$ was instantiated to doesn't matter).  Thus, the existential operator $\exists_x$ is the same as the cylindrification $C_x$.
The diagonal element $D_{xy}$ is the (constant) class of infinite sequences whose $x$th and $y$th places match.
I need to prove that:
$ \neg ~ \exists_x ~\exists_y ~ \exists_w ~ \exists_z ~  D_{yw} ~~ [ f(x,y) \wedge f(w,z) \wedge \neg g(x,z) ]$.
Inside the []'s are 3 infinite sequences that make each of the 3 conjuncts true.  So $f(x,y)$ is an infinite sequence that makes $father(x,y)$ true.  For example, $\{x = john, \; y=pete, \; ...\}$ is one such sequence.  We can do the conjunction (ie, intersection) of such sequences, treating these sequences as volumes in the 4-dimensional $x$-$y$-$z$-$w$ space.  We can also obtain the complement of the volumes (sequences).
To understand, say, the formula
$ D_{yw} ~ \exists_x ~\exists_y ~ \exists_w ~ \exists_z ~~ [ f(x,y) \wedge f(w,z) ]$, first apply the cylindrifications and then intersect with the diagonal element, what we get is the volume that satisfies the $g(x,z)$ grandfather relation.
Then the negation of this volume intersected with the $g(x,z)$ volume will be the null set, whose negation is the universe.  This is the geometric interpretation of why the original formula should be true.
It remains to be shown how the result can be gotten algebraically...
