%A finite axiomatization of G_n.
%H. Andreka, Sept.2, 1995. (Tex version: April 1996.)
%te -hez kell:

\input amstex1
\documentstyle{amsppt1}
\input amsppt.mor
\input amssym.def
\input amssym.tex

\magnification=\magstep1
\nologo
\hsize=17truecm
\vsize=24truecm
%\overfullrule=0pt

\topmatter

\centerline{\bf A FINITE AXIOMATIZATION OF LOCALLY SQUARE}
\centerline{\bf CYLINDRIC-RELATIVIZED SET ALGEBRAS\footnote{This work 
has been supported by the Hungarian National Foundation for Scientific 
Research Grants No T16448, T7255.}}

\centerline{Preliminary draft version.}
\medskip

\author 
H. Andr\'eka
\endauthor

\address{H. Andr\'eka : \ Mathematical\ Institute of the Hungarian Acad\. of 
Sci\., Budapest, Pf.127, H--1364, Hungary}
\date{September, 1995.}
\abstract{We give a finite set of equations defining the class $G_n$ 
of locally square cylindric-relativized set algebras (of dimension $n$)
if $n$ is 
finite. For infinite $n$, we give an axiomatization of the equational 
theory of $G_n$. Here $G_n$ denotes the class of all cylindric-relativized 
set algebras of dimension $n$ with unit a union of Cartesian spaces.}
\thanks{}
\keywords{}
\subjclass{03G15, 06, 08}

\endtopmatter

\def\sij{s^i_j}
\def\sji{s^j_i}
\def\ski{s^k_i}
\def\sjk{s^j_k}
\def\el{\ell}

\def\b{\smallsetminus}


\def\at{AT}
\def\nd{N86}
\def\agon{AGN} %Andreka-Goldblatt-Nemeti 1996
\def\mv{MV} %Marx-Venema book
\def\n2{N95} %Logic Coll'92
\def\nm{N96} %Arrow Logic Volume
\def\nc{N85} %NJSL
\def\hmtan{HMTAN}
\def\hmt{HMTII}
\def\m{M95} %Monk Banach


\document


Let $n$ be an ordinal. We will deal with algebras of $n$-ary relations. A 
cylindric-relativized set algebra of dimension $n$ is an algebra of $n$-ary 
relations, we do not recall its definition here. $Crs_n$ denotes the class of 
all cylindric-relativized set algebras of dimension $n$, and $Gs_n\subseteq 
G_n\subseteq D_n\subseteq Crs_n$ are subclasses of $Crs_n$ defined by making 
restrictions on the biggest element (unit) of the algebra, we briefly recall 
their definitions below.
\smallskip

Let $\goth A$ be a cylindric-relativized set algebra of dimension $n$ with 
unit $V$. Then
\roster
\item"{}"
$\goth A\in D_n$ iff for every $s\in V$ and every finite nonpermutational 
transformation $\tau$ of $n$, also $s\circ\tau$ is in $V$.
\item"{}"
$\goth A\in G_n$ iff $V$ is a union of Cartesian spaces.
\item"{}"
$\goth A\in Gs_n$ iff $V$ is a disjoint union of Cartesian spaces.
\endroster
For a class $K$ of algebras, $IK$ denotes the class of all isomorhic copies of 
elements of $K$.
\smallskip

Let $n$ be finite. In this paper we give a finite equational axiom 
system for $G_n$. It was already known that $IG_n$ is a variety (N\'emeti 
\cite{\nd}), moreover it is a canonical variety, i.e\. it is closed under 
perfect extensions (Andr\'eka-Goldblatt-N\'emeti \cite{\agon}). These will 
also follow from the theorem in the present paper because the axiomatization 
we give contains only positive equations. If $n$ is infinite, then we do not 
know weather $IG_n$ is a variety or not. More on $IG_n$ can be found in 
\cite{\agon, \mv, \nd, \n2, \nm}.
\smallskip

We note that $ICrs_n, ID_n, IGs_n$ are all varieties, $ICrs_n$ and $IGs_n$ 
are not finitely axiomatizable for $n\ge 3$, and a finite axiomatization for 
$ID_n$ is given in \cite{\at}. These are all distinct classes, equations 
distinguishing them are given in \cite{\nd, \n2}. A rich material on these 
classes can be found besides the above cited references e.g\. in \cite{\hmtan, 
\hmt, \m,\nc}.

%Definition of $G_n$.
%Definition of $D_n, Crs_n, Gs_n$.
%What do we know about them [$IG_n$ is a variety if $n$ is finite 
%(\cite{\nd}), for infinite $n$ we do not know whether $IG_n$ is a variety.
%Let $n$ be finite. $IG_n$ is a canonical variety (\cite{\agon}), i.e\. it is 
%closed under perfect extensions. This will also follow from the present
%theorem, because our axioms are positive in the wider sense, so they are
%preserved by perfect extensions. In \cite{\agon} we use very different methods.
%The varieties $ICrs_n, ID_n, IG_n, IGs_n$ are all distinct, equations
%distinguishing them can be found in \cite{\nd}. The distinguishing equation
%in \cite{\nd} is equivalent with the axiom we give for $n=2$ here (though it has
%a different form in \cite{\nd}). $ICrs_n, IGs_n$ are not finitely %axiomatizable.]
\bigskip

Let $n$ be a finite number and let $i,j< n$.
Let $Ax_{ij}$ be the following equation:
$$
x\le c_ic_j(\sij c_jx\cdot \sji c_ix\cdot \prod_{k<n, 
k\ne i,j}\ski\sij\sjk c_kx).
$$ 
In the above, $\prod$ is the grouped version of $\cdot$, and 
$\sij(x)=c_i(d_{ij}\cdot x)$ if $i\ne j$ and $s^i_i(x)=x$.
We will see from the 
proof of the next theorem that $Ax_{ij}$ intuitively says that for any sequence 
in the unit, we can also put into the unit the sequence we obtain from it by 
interchanging its $i$'th and $j$'th elements. 
From the equation $Ax_{ij}$ we will only use its following consequence:
$$
x\ne 0\quad\rightarrow\quad \sij c_jx\cdot \sji c_ix\cdot \prod_{k<n, 
k\ne i,j}\ski\sij\sjk c_kx\ne 0.
$$
Intuitively, this ensures that if a sequence is in $x$, then its permuted 
version can be put into $\sij c_ix \cdot \dots$.
\smallskip

To extend these equations for infinite $n$, assume now that $n$ is any 
ordinal, possibly infinite. For all $i,j<n$ and 
all finite subsets $\Gamma$ of $n$ let $Ax_{ij\Gamma}$ denote the following 
equation:
$$
x\le c_ic_j(\sij c_jx\cdot \sji c_ix\cdot \prod_{k\in \Gamma, 
k\ne i,j}\ski\sij\sjk c_kx).
$$ 
Let $Ax_n$ be the set of all $Ax_{ij}$, for $i,j<n$, and let $Ax'_n
=\{ Ax_{ij\Gamma} : i,j< n, \Gamma\subseteq n, \Gamma\text{ finite 
}\}.$ We will simply write $Ax$ and $Ax'$ if there is no danger of confusion.
$IG_n, HG_n$ denote the classes of all isomorphic copies and all homomorphic 
images of elements of $G_n$, respectively.

\proclaim{\bf THEOREM}
\roster
\item"{(i)}" 
$IG_n=\{\goth A\in ID_n : \goth A\models Ax\},$ if $n$ is finite, $n\ge 3$.
\item"{(ii)}"
$HG_n=\{\goth A\in ID_n : \goth A\models Ax'\}$ for all $n\ge 3$.
\item"{(iii)}"
$IG_2=\{\goth A\in ID_n : \goth A\models 
x-d_{01}\le c_0c_1(-d_{01}\cdot s^0_1c_1x\cdot s^1_0c_0x) \}$.
\endroster
\endproclaim

\demo{\bf Proof} Let $n\ge 2$.
\smallskip
First we show that $G_n\models Ax'$. Let $\goth A\in G_n$ with unit $V$, 
$x\in A$ and let $s\in x$. Let $i,j,k< n$. Let $z=s\circ [i,j]$, 
where $[i,j]:n\to n$ is the permutation of the set $n=\{k: k<n\}$
which interchanges $i$ and $j$ and leaves all the other elements fixed.
Then 
$z\in V$ and it is easy to check that $s\in c_ic_j(\{ z\})$, $z\in \sij c_jx$, 
$z\in \sji c_ix$, $z\in\ski\sij\sjk c_kx$. This shows that 
$\goth A\models Ax_{ij\Gamma}$ for all $i,j<n$ and for all finite 
$\Gamma\subseteq n$. This shows $G_n\models Ax'$.
The same argument shows that $G_2$ satisfies the indicated equation
(notice that if $s\in x-d_{01}$, then $s_0\ne s_1$, and so $z$ also is
in $-d_{01}$).
\medskip

To show the other direction of (i)-(iii), we first assume that $n$ is finite
$n\ge 2$.
Let $\goth A\in D_n$ with unit $V$, and assume that $\goth A\models Ax$.
\smallskip

By the proof of the representation theorem in \cite{\at}, we may assume 
that $V$ satisfies the following
\roster
\item"{(*)}"
For all repetition-free sequences $s,z\in V$, the ranges of 
$s$ and $z$ are different.
\endroster
This means, in other words, that if $s\in V$, then no other permuted version 
of $s$ is in $V$. We note that for any $D_n$-unit $V$ it is true that
\roster
\item"{(**)}"
If $s\in V$ is not repetition-free and $i,j\in n$, then $s\circ [i,j]\in V$.
\endroster
This means, in other words, that if $s\in V$ has a repetition (i.e\. is not 
repetition-free), then all permuted versions of $s$ are in $V$. Using that 
$V$ is a $D_n$-unit, this also means that  $s\circ\tau\in V$ for all 
$\tau : n\to n$, or still in other words, ${}^nRgn(s)\subseteq n$ 
(if $s\in V$ has repetitions).
\smallskip

The idea of the following proof is that we can ``throw in'' the permuted 
versions of the repetition-free sequences in $V$ such that  ``$\goth A$ will 
not change''. $Ax_{ij}$ will tell us ``where to put the new sequence 
$s\circ [i,j]$''.
\smallskip

Assume that $\goth A\in D_n$ has unit $V$ such that the following holds:
\roster
\item"{(***)}"
For all repetition-free sequences $s\in V$, either $s\circ\tau\in V$ for 
all bijections $\tau :n\to n$ or else $s\circ\tau\notin V$ for all bijections 
$\tau :n\to n$ which are not the identity on $n$.
\endroster
Of course, (*) implies (***).

Let $s\in V$ be a repetition-free sequence such that ``no permuted version of 
$s$ is in $V$''. Let $S=\{ z_0,z_1,\dots ,z_N\}$ be a listing of all the 
permuted versions of $s$---i.e\. $S=\{ s\circ\tau : \tau\text{ is a bijection 
of }n \}$--- such that
\roster
\item"{}"
$z_0=s$
\item"{}"
$z_i=z_j\circ [k,\el ]$ for some $j<i,\  k,\el< n$.
\item"{}"
$z_i\ne z_j$ if $i\ne j$.
\endroster

Such a listing is possible. Then $V\cup S$ also satisfies (***). We will 
``represent'' $\goth A$ on $V\cup S$, i.e\. we will show that $\goth A$ is 
isomorphic to an $\goth A'$ with unit $V\cup S$. Then we will be done by an 
induction.
\medskip

We may assume that $\goth A$ is atomic and every repetition-free sequence 
in the unit of $\goth A$ is in an atom, because of the following. All 
the axioms listed here are positive in the wider sense (i.e\. complementation 
$-$ occurs only in front of some constant terms) and the defining axioms of 
$D_n$ are also positive, so we may pass on to the perfect extension and 
represent that. Also, the representation for $D_n$ 
given in \cite{\at} is such that 
every sequence in the unit is in some atom (i.e\. the unit is the union---and 
not only the supremum---of the atoms).
\smallskip

We say that an atom of $\goth A$ is repetition-free if it is below no 
$d_{ij}$ (i.e\. if it is below $\prod_{i<j<n}-d_{ij}$). Let $a$ be an 
arbitrary repetition-free atom of $\goth A$ and let $i,j< n,\  i\ne j$.
\smallskip

Let now $n\ge 3$ and let
$$
b\le \sij c_ja\cdot \sji c_ia\cdot \prod_{k\ne i,j}\ski\sij\sjk c_ka
$$
be an atom. Such an atom exists by $\goth A\models Ax$. We will show that 
$b$ is repetition-free.
\smallskip

We will work in the atom-structure of $\goth A$ for a while. I.e\. let $At$ 
be the set of all atoms of $\goth A$, let $E_{ij}=\{ x\in At : x\le d_{ij}\}$ 
and let $T_i = \{ \langle x,y\rangle : x,y\in At, c_ix=c_iy\}$. Let 
$E_{ijk}=E_{ij}\cap E_{jk}$. 
We will freely use the following properties of atom-structures:
\roster
\item"{}"
$a\in E_{ij}, a T_k b$ imply $b\in E_{ij}$ if $k\ne i,j$.
\item"{}"
$a,b\in E_{ij}, a T_i b$ imply $a=b$.
\item"{}"
$E_{ij}\cap E_{jk}\subseteq E_{ik} = E_{ki}$.
\item"{}"
For any $a\in At$ and $i,j<n,\ i\ne j$ there is a unique $b\in At$ 
such that $a T_i b\in E_{ij}$.
\endroster
\smallskip

\noindent
First we show that $b\in E_{ij}$ would imply that $a\in E_{ij}$.
Let $k< n,\  k\ne i,j$. Then $b\le \ski\sij\sjk c_ka$, and this means that 
there are atoms $x,y,z$ of $\goth A$ such that $b T_k x, x\in E_{ik}, 
x T_i y, y\in E_{ij}, y T_j z, z\in E_{jk}, z T_k a$, see Figure 1.

$$
\matrix
               & b&  &\ \ & &\ \ &  &a&   \\
               & |&  &    & &    &  &|&   \\
               & |&k &    & &    & k&|&   \\
               & |&  &    & &    &  &|&   \\
\quad E_{ik}\ni& x&  &    & &    &  &z&\in E_{jk}  \\
               &\b&  &    & &    &  &/&            \\
               &  &\b i&  & &    &j/& &            \\
               &  &    &\b& &  / &  & &            \\
               &  &  &    &y&    &  & &      \\
               &  &  &  &E_{ij}& &  & &      \\
\endmatrix
$$

\centerline{Figure 1}

Now, $b\in E_{ij}$ implies $x\in E_{ijk}$, which implies that $y=x, 
\ y\in E_{ijk}$ which imply that $z=y,\  z\in E_{ijk}$, which imply that 
$a\in E_{ij}$. 
\smallskip

\noindent
Next we show that $b\in E_{ik}$ would imply that $a\in E_{jk}$. By 
$b\le \sji c_ia$ there is an atom $x$ such that $b T_j x\in E_{ij}, x T_i a$, 
see Figure 2.

\bigskip

$$
\matrix
%\hskip 3truecm &  &  &\ \ & &\ \ &  &a&   \\
%               & |&  &    & &    &  &|&   \\
%               & |&k &    & &    & k&|&   \\
%               & |&  &    & &    &  &|&   \\
                & b&  &    & &    &  &a&    \\
                &\b&  &    & &    &  &/&            \\
                &  &\b j&  & &    &i/& &            \\
                &  &    &\b& &  / &  & &            \\
                &  &  &    &x&    &  & &      \\
                &  &  &  &E_{ij}& &  & &      \\
\endmatrix
$$

\centerline{Figure 2}


Now $b\in E_{ik}$ implies $x\in E_{ijk}$ which implies that $a\in E_{jk}$.
\smallskip

\noindent
Finally we show that $b\in E_{k\el}$  would imply $a\in E_{k\el}$ for all 
$k\ne\el,\ \  j,i\ne k,\el$. Let $x$ be an atom as in Figure 2. Then 
$b\in E_{k\el}$ implies that $x\in E_{k\el}$ which implies that 
$a\in E_{k\el}$.

\noindent
Thus $b$ is repetition-free, because $a$ is repetition-free.
\smallskip

Assume now that $n\ge 2$ and $i,j\le n,\  i\ne j$. For any repetition-free atom 
$a$ choose a repetition-free atom $b$ below 
$\sij c_ja\cdot \sji c_ia\cdot\prod_{k\ne i,j}\ski\sij\sjk c_ka$ and let
$$
f_{ij}(a) = b.
$$
Such a $b$ exists, because if $n\ge 3$, then we have seen this above, and if 
$n=2$, then this holds by the axiom we required to hold.
\smallskip

Let now $s$ be the repetition-free sequence we chose at the beginning of this 
proof, and recall the definition of $S=\{ z_0,z_1,\dots , z_N\}$. We will 
define a sequence $a_0,a_1,\dots ,a_N$ of repetition-free atoms. Let $a$ be 
an atom such that $s\in a$. Such an atom exists by our assumption.
\smallskip

Let 
$$
a_0 = a.
$$
Assume that $a_\el$ has been defined for all $\el <i$. Let $\el <i$ and 
$m\ne j$ be such that $z_i=z_\el\circ [m,j]$. 
(If there are several such $\el, m, j$, then we just select one such triple.)
Now we define
$$
a_i = f_{mj}(a_\el).
$$

We are ready to define the new representation of $\goth A$.: For any $x\in A$ 
define $x'$ as
$$
x' = x\cup \{ z_i : a_i\le x,\  i<N\}.
$$
(Intuitively, this means that ``we put the sequences $z_i$ into the atoms $a_i$''.)

Then $V' = V\cup S$, so the unit of the new representation will be $V\cup S$ 
as desired. We have to show that the function $x\mapsto x'$ is an embedding 
of $\goth A$ into the full set algebra with unit $V\cup S$. Let us denote 
this function $x\mapsto x'$ by $h$.
\smallskip

Clearly, $h$ is a one-to-one Boolean embedding,
 and $h(d_{ij})=d_{ij}$ for all $i,j<n$. To show 
that $h$ respects the cylindrifications $c_k$, first we prove an auxiliary 
statement.
\enddemo
\smallskip

\noindent
\underbar{\bf Notation:} If $z$ is an $n$-sequence and $k,\el <n$, then 
$z(k/z_\el)$ denotes the sequence which agrees everywhere with $z$ except on 
$k$, where it is the same as $z_\el$.
\smallskip

\proclaim{\bf LEMMA} Assume that $z\in S$ and $z\in x'$, $x\in At$. Let 
$k,\el <n,\  k\ne\el$. Then for all $b\in At$ we have that
\roster
\item"{(*)}"
\qquad $z(k/z_\el)\in b\ \ \text{ iff }\ \  x T_k b\in E_{k\el}.$
\endroster
\endproclaim

\demo{\bf Proof}
By $z\in S$ there is an $m\le N$ such that $z=z_m$. We will prove by 
induction on $m$.
\smallskip

Assume that $m=0$. Then by $z_0=s\in V$,\ (*) is true 
because $\goth A$ is a set 
algebra on $V$.
\smallskip

Assume that (*) is true for all $k,\el <n$ and for all $m<p$. We will show 
that (*) is true for $p$, too. Let $z_p = z_m\circ [i,j]$
be such that $m<p$ and $a_p=f_{ij}(a_m)$. There are such $m,i,j$ by 
the definition of $a_p$. Then 
$x=a_p$ by $z_p\in x'$, and also $z_m\in a_m$.
\smallskip

First we prove that $x T_k b \in E_{k\el}$ imply that $z(k/z_\el)\in b$.
\bigskip

\noindent
\underbar{Case 1} $k\ne i,j$ and $\el=i$ or $\el=j$.
Assume first that $\el=j$.

By $a_p=f_{ij}(a_m)$ we have that $a_p\le \ski\sij\sjk c_k(a_m)$.
Since in $D_n$ the so called Merry Go Round equation $\ski\sij\sjk c_kx=
s^k_js^j_is^i_kc_kx$ is true, then we also have that 
$x=a_p\le s^k_js^j_is^i_kc_k(a_m)$. Thus there are atoms $d,e,b^+$ such that 
$x T_k b^+, b^+\in E_{kj}, b^+ T_j e, e\in E_{ij}, e T_i d, d\in E_{ki},
d T_k a_m$. By $x T_k b \in E_{kj}$ then $b^+=b$ (by the basic properties of
atomstructures).
See Figure 3.
\bigskip

$$
\matrix
      w=z_m\ni & a_m&  &\ \ & &\ \ &  &x&\in z_m\circ [i,j]=z_p=z   \\
               & |&  &    & &    &  &|&   \\
               & |&k &    & &    & k&|&   \\
               & |&  &    & &    &  &|&   \\
\quad E_{ki}\ni& d&  &    & &    &  &b&\in E_{kj}  \\
               &\b&  &    & &    &  &/&            \\
               &  &\b i&  & &    &j/& &            \\
               &  &    &\b& &  / &  & &            \\
               &  &  &    &e&    &  & &      \\
               &  &  &  &E_{ij}& &  & &      \\
\endmatrix
$$

\centerline{Figure 3}


Let $w=z_m$ and recall that $z=z_p$. 
Then $w(k/w_i)\in d$ by our induction hypothesis, and therefore 
$w(k/w_i)(i/w_j)\in e$ because $\goth A$ is a set algebra. But then 
$w(k/w_i)(i/w_j)(j/w_i)\in b$, again because $\goth A$ is a 
set algebra (notice that $w_i$ is the $k$'th member of the sequence 
$w(k/w_i)(i/w_j)$). Finally notice that $z(k/z_j) = w(k/w_i)(i/w_j)(j/w_i)$.
\medskip

The case $\el=i$ is completely similar, except that we do not have to use the
Merry Go Round equation.
\bigskip

\noindent
\underbar{Case 2} $k\ne i,j$ and $\el\ne i,j$.

Then $z(k/z_\el) = z(k/z_j)(k/z_\el)$ and therefore we will use the
previous case. Let $b^+\in E_{kj}$ be such that $x T_k b^+$. Such a $b^+$ 
exists by basic properties of atomstructures. Then by Case 1 we have that 
$z(k/z_j)\in b^+$, and then $z(k/z_j)(k/z_\el)\in b$, because $\goth A$ is 
a set algebra, $z(k/z_j)\in V$ and $b^+ T_k b \in E_{k\el}$.

% Now $z(k/z_j)\in b'\in E_{kj}$ and 
%$b' T_k x'$  imply that $z(k/z_j)(k/z_\el)\in b\in E_{k\el}$ and $b T_k b'$. 
%(Summing up: by using the notation that $t^i_j(y)$ is the unique atom in 
%$E_{ij}$ which is in $T_i$-relation with $y$ we have that 
%$t^k_\el = t^k_\el t^k_j$, and $t^k_j$ brings us to ``the old 
%representation''.)
\bigskip
\eject

\noindent
\underbar{Case 3} $k=i$ and $\el=j$. 

By $a_p\le f_{ij}(a_m)$ we have that $a_m\le \sij c_i(a_p)$, see Figure 4.
\bigskip

$$
\matrix
        w\ni&a_m&  &\ \ & &\ \ &  &x&=a_p   \\
%               & |&  &    & &    &  &|&   \\
%               & |&k &    & &    & k&|&   \\
%               & |&  &    & &    &  &|&   \\
%\quad E_{ik}\ni& x&  &    & &    &  &z&\in E_{jk}  \\
                &\;\b&  &    & &    &  &/&            \\
                &  &\;\b j&  & &    &i/& &            \\
                &  &    &\;\b& &  / &  & &            \\
                &  &  &    &\;b&    &  & &      \\
                &  &  &  &\;E_{ij}& &  & &      \\
\endmatrix
$$

\centerline{Figure 4}


Now, $w\in a_m$ implies, by the induction hypothesis, that $w(j/w_i)\in b$. 
But $w(j/w_i)=z(i/z_j)$.
\bigskip

\noindent
The case $k=i,\ \el\ne i,j$ is as above. The case $k=j$ is completely
analogous.
\medskip

Thus we have seen that $x T_k b\in E_{k\el}$ imply that $z(k/z_\el)\in b$. 
To see the other direction, assume that $z(k/z_\el)\in b$. There is a $b^+$ 
such that $x T_k b^+ \in E_{k\el}$, and we have seen that  $z(k/z_\el)\in b^+$ 
for this $b^+$. Then $b=b^+$ because distinct atoms are disjoint from 
each other, and 
so $b T_k x$ since $b^+ T_k x$.
\noindent
{\bf QED(Lemma)}
\enddemo

Now we are ready to show that $h$ is a homomorphism w.r.t\. $c_i$. 
Let $j<n,\ j\ne i$. We will use that two sequences $z$ and $w$ differ only 
at $i$ if and only if $z(i/z_j)=w(i/w_j)$.
\smallskip

To show that $h$ is a homomorphism w.r.t\. $c_i$  
amounts to showing (i)-(ii) below for all atoms $a,b$ and sequences 
$z,w\in V\cup S$:

\roster
\item"{(i)}"
$z\in a,\ w\in b$ and $z(i/z_j)=w(i/w_j)$ imply that $a T_i b$
\item"{(ii)}"
$z\in a$ and $a T_i b$ imply that $z(i/z_j)=w(i/w_j)$ for some $w\in b$.
\endroster

To prove (i)-(ii), let $a,b$ be two atoms, and let $a T_i  a^+ \in E_{ij}$, 
$b T_i b^+\in E_{ij}$. Then $z\in a$ implies $z(i/z_j)\in a^+$ if $z\in S$ by 
the previous lemma, and if $z\in V$, then this is so since $\goth A$ is a set 
algebra and $z(i/z_j)\in V$. Similarly, $w\in b$ implies $w(i/w_j)\in b^+$ for 
all $w\in V\cup S$.
\smallskip

Proof of (i): Assume $z\in a,\ w\in b,\ z(i/z_j)=w(i/w_j)$. Then 
$z(i/z_j)\in a^+$ and $w(i/w_j)\in b^+$ by the above, hence $a^+=b^+$, which 
implies that $a T_i b$ by the definition of $a^+, b^+$.

Proof of (ii): Assume $z\in a,\ a T_i b$. Then $z(i/z_j)\in a^+$. Further, 
$a T_i b$ implies that $a^+=b^+$. So $z(i/z_j)\in b^+$. Now since $b^+ T_i b$, 
$z(i/z_j)\in V$, and since $\goth A$ is a set algebra, $z(i/z_j)\in b^+$ 
implies that $w(i/w_j)=z(i/z_j)$ for some $w\in b$.
\medskip

By the above we have see that $h$ is an embedding of $\goth A$ into the full 
set algebra on $V\cup S$, i.e\. $\goth A$ ``can be represented on $V\cup S$.''
Now repeating the above procedure along a transfinite induction we get a 
representation of $\goth A$ on $G(V) = \{ {}^nRng(s) : s\in V\}$. Since $G(V)$ 
is a union of Cartesion spaces, this shows that $\goth A\in IG_n$.
\medskip

Let $n$ be infinite. Now \cite{\n2 , Lemma 4.13(ii)} implies that $Ax'$ is an 
axiomatization of the equational theory of $G_n$, as follows. Let $e$ be an 
equation that holds in $G_n$. We want to show that it follows from $Ax'$. Let 
$\Gamma$ be a finite subset of $n$ which strictly contains all the indices 
occurring in $e$ (i.e\. $\Gamma$ contains some other index, too). By \cite{\n2, 
Lemma 4.13(ii)} then $G_\Gamma\models e$. Then $Ax_\Gamma\models e$, since 
$\Gamma$ is finite. By $Ax_\Gamma\subseteq Ax'$ then $Ax'\models e$. Since 
$IG_n$ is closed under subalgebras and direct products, the variety generated 
by $G_n$ is $HG_n$.

\noindent
{\bf QED(Theorem)}


\Refs

\ref\no\agon
\by Andr\'eka,H. Goldblatt,R. N\'emeti,I.
\paper Relativised quantification: some canonical varieties of sequence-set 
algebras
\finalinfo Submitted.
\endref

\ref\no\at
\by Andr\'eka,H. and Thompson,R.J.
\paper
A Stone-type representation theorem for algebras of relations of higher rank
\jour Trans\. Amer\. Math\. Soc\.\vol 309,2 \yr1988\pages671-682
\endref

\ref\no\hmt
\by Henkin,L. Monk,J.D. and Tarski,A.
\paper Cylindric Algebras. Part II
\finalinfo North-Holland, 1985.
\endref

\ref\no\hmtan
\by Henkin,L. Monk,J.D. Tarski,A. Andr\'eka,H. and N\'emeti,I.
\book
Cylindric Set Algebras
\publ
Lecture Notes in Mathematics Vol 883, Springer-Verlag 
\publaddr Berlin 
\yr1981 \pages vi + 323
\endref

\ref\no\mv
\by Marx.M. and Venema.Y.
\paper Multi-dimensional Modal Logic
\finalinfo Kluwer Academic Publisher, to appear.
\endref

\ref\no\m
\by Monk,J.D.
\paper Lectures on cylindric set algebras
\finalinfo In: Algebraic Methods in Logic and in Computer Science,
(Proc\. Banach Semester Fall' 1991).
Banach Center Publications Vol 28, Institute of Mathematics, 
Polish Academy of Sciences, Warsaw 1993. Ed: C. Rauszer. pp.253-290.
\endref

\ref\no\nc
\by N\'emeti,I.
\paper Cylindric-relativized set algebras have strong amalgamation
\jour J\. Symbolic Logic \vol50 \yr1985\pages689-700
\endref

\ref\no\nd
\by N\'emeti,I.
\paper Free algebras and decidability in algebraic logic
\finalinfo Doctoral Dissertation with the Academy, Budapest,
1986. (In Hungarian.)
\endref

\ref\no\n2
\by N\'emeti,I.
\paper Decidable versions of first order logic and cylindric-relativized
set algebras
%\by N\'emeti,I.
\finalinfo In: Logic Colloquium'92 (Proc\. Veszpr\'em, Hungary 1992),
eds: Csirmaz,L\. and Gabbay,D\. M.  and de Rijke, M.,
Studies in Logic, Language and Computation,
CSLI Publications, 1995. pp.177-241.
\endref

\ref\no\nm
\by N\'emeti,I.
\paper Fine-structure analysis of first order logic
\finalinfo Arrow Logic and Multi-Modal Logic, M\. Marx, L\. Polos, 
and M\. Masuch eds, CSLI Publications, Stanford, California, 1996.
pp.221-247.
\endref


\enddocument