% Sain-Gyuris: Finite Schematizable Algebraic Logic % Preprint 1996, to appear in IGPL % LaTeX % Run it 3 times \documentstyle{article} \newcommand{\version}{5.2} \scrollmode \newcommand{\eproof}{\mbox{}\hfill\rule{1 ex}{1.5 ex}} \newcommand{\edf}{\mbox{}\hfill\framebox[1 ex]{ }} \newcommand{\erm}{} \newcommand{\tores}{\hfill\mbox{}\linebreak} \newcommand{\lbb}[1]{\label{#1}\marginpar{\tt #1}} \newcommand{\bibl}[2]{\bibitem[#1]{#2}\marginpar{\tt #2}} % BIZONYITAS TIPUS \newenvironment{proofof}[1]{\noindent{\bf Proof of #1 }}{\eproof\\\mbox{}} \newenvironment{proof}{\noindent{\bf Proof }}{\eproof\\\mbox{}} % DEFINICIO TIPUS \newtheorem{df_gen}{Definition}[section] \newtheorem{cn_gen}[df_gen]{Convention} \newtheorem{nt_gen}[df_gen]{Notation} \newenvironment{dfn}[2]{\begin{df_gen}[#2]\lbb{#1}\tores\rm}{\edf\end{df_gen}} \newenvironment{df}[1]{\begin{df_gen}\lbb{#1}\rm}{\edf\end{df_gen}} \newenvironment{conn}[2]{\begin{cn_gen}[#2]\lbb{#1}\tores\rm}{\edf\end{cn_gen}} \newenvironment{con}[1]{\begin{cn_gen}\lbb{#1}\rm}{\edf\end{cn_gen}} \newenvironment{ntn}[2]{\begin{nt_gen}[#2]\lbb{#1}\tores\rm}{\edf\end{nt_gen}} \newenvironment{nt}[1]{\begin{nt_gen}\lbb{#1}\rm}{\edf\end{nt_gen}} % TETEL TIPUS \newtheorem{th_gen}[df_gen]{Theorem} \newtheorem{lm_gen}[df_gen]{Lemma} %\newtheorem{cl_gen2}[df_gen]{Claim} \newtheorem{cl_gen}[df_gen]{Claim} \newtheorem{cr_gen}[df_gen]{Corollary} \newtheorem{ex_gen}[df_gen]{Example} \newtheorem{cj_gen}[df_gen]{Conjecture} \newenvironment{thn}[2]{\begin{th_gen}[#2]\lbb{#1}\tores}{\end{th_gen}} \newenvironment{theo}[1]{\begin{th_gen}\lbb{#1}}{\end{th_gen}} \newenvironment{lmn}[2]{\begin{lm_gen}[#2]\lbb{#1}\tores}{\end{lm_gen}} \newenvironment{lm}[1]{\begin{lm_gen}\lbb{#1}}{\end{lm_gen}} \newenvironment{cln}[2]{\begin{cl_gen}[#2]\lbb{#1}\tores}{\end{cl_gen}} \newenvironment{cl}[1]{\begin{cl_gen}\lbb{#1}}{\end{cl_gen}} \newenvironment{crln}[2]{\begin{cr_gen}[#2]\lbb{#1}\tores}{\end{cr_gen}} \newenvironment{crl}[1]{\begin{cr_gen}\lbb{#1}}{\end{cr_gen}} \newenvironment{exn}[2]{\begin{ex_gen}[#2]\lbb{#1}\tores}{\end{ex_gen}} \newenvironment{ex}[1]{\begin{ex_gen}\lbb{#1}}{\end{ex_gen}} \newenvironment{cjn}[2]{\begin{cj_gen}[#2]\lbb{#1}\tores}{\end{cj_gen}} \newenvironment{cj}[1]{\begin{cj_gen}\lbb{#1}}{\end{cj_gen}} % MEGJEGYZES TIPUS \newtheorem{rm_gen}[df_gen]{Remark} \newtheorem{qu_gen}[df_gen]{Open question} \newenvironment{rmkn}[2]{\begin{rm_gen}[#2]\lbb{#1}\tores\rm}{\erm\end{rm_gen}} \newenvironment{rmk}[1]{\begin{rm_gen}\lbb{#1}\rm}{\erm\end{rm_gen}} \newenvironment{qun}[2]{\begin{qu_gen}[#2]\lbb{#1}\tores\rm}{\erm\end{qu_gen}} \newenvironment{qu}[1]{\begin{qu_gen}\lbb{#1}\rm}{\erm\end{qu_gen}} % ENUMERATE VALTOZATAI \newenvironment{arabate}{\renewcommand{\theenumi}{(\arabic{enumi})} \begin{enumerate}}{\end{enumerate}} \newenvironment{romanate}{\renewcommand{\theenumi}{(\roman{enumi})} \begin{enumerate}}{\end{enumerate}} \newenvironment{romanatesym}[1]{\renewcommand{\theenumi}{(#1\roman{enumi})} \begin{enumerate}}{\end{enumerate}} \newenvironment{arabatesym}[1]{ \addtolength{\leftmargini}{1em} \addtolength{\leftmarginii}{1em} \renewcommand{\theenumi}{(#1\arabic{enumi})} \renewcommand{\theenumii}{#1\arabic{enumii}} \begin{enumerate}}{\end{enumerate}} \newenvironment{symbolate}[1]{ \renewcommand{\theenumi}{#1}\addtolength{\leftmargini}{1em} \renewcommand{\theenumii}{#1} \begin{enumerate}}{\end{enumerate}} \newcounter{fn1} % EQUATION VALTOZATAI \newcounter{egyenlet} \newenvironment{eqsym}[1]{\setcounter{egyenlet}{#1} \renewcommand{\theequation}{\fnsymbol{egyenlet}} \begin{equation}}{\end{equation} \renewcommand{\theequation}{\arabic{equation}}} \newenvironment{eqsymbol}[1]{\renewcommand{\theequation}{{#1}} \begin{equation}}{\end{equation} \renewcommand{\theequation}{\arabic{equation}}} % Basic classes \newcommand{\xgws}{\mbox{{\rm Gwdf}}} \newcommand{\xgs}{\mbox{{\rm Gdf}}} \newcommand{\xcs}{\mbox{{\rm Cdf}}} \newcommand{\xgwsp}{\mbox{{\rm Gws}}} \newcommand{\xgsp}{\mbox{{\rm Gs}}} \newcommand{\xcsp}{\mbox{{\rm Cs}}} % Derived classes \newcommand{\xgwsn}{\xgws^{\mbox{\scriptsize\rm{} nm}}} \newcommand{\xgwsc}{\xgws^{\mbox{\scriptsize\rm{} cm}}} \newcommand{\xgsu}{\xgs^{\mbox{\scriptsize\rm{} ec}}} \newcommand{\xcsu}{\xcs^{\mbox{\scriptsize\rm{} ec}}} \newcommand{\xgspu}{\xgsp^{\mbox{\scriptsize\rm{} ec}}} \newcommand{\xigws}{\mbox{{\bf I}\xgws}} \newcommand{\xigwsp}{\mbox{{\bf I}\xgwsp}} \newcommand{\xigsp}{\mbox{{\bf I}\xgsp}} \newcommand{\xigwsn}{\mbox{\bf I}\xgwsn} \newcommand{\xigwsc}{\mbox{\bf I}\xgwsc} \newcommand{\xigs}{\mbox{{\bf I}\xgs}} \newcommand{\xicsu}{\mbox{\bf I}\xcsu} \newcommand{\xigsu}{\mbox{\bf I}\xgsu} \newcommand{\xics}{\mbox{{\bf I}\xcs}} \newcommand{\xhcs}{\mbox{\bf H}\xcs} \newcommand{\xhspcsp}{\mbox{\bf HSP}\xcsp} \newcommand{\xhspcs}{\mbox{\bf HSP}\xcs} \newcommand{\xspcsu}{\mbox{\bf SP}\xcsu} \newcommand{\xpcsp}{\mbox{\bf P}\xcsp} \newcommand{\xhgsp}{\mbox{\bf H}\xgsp} \newcommand{\xhgwsp}{\mbox{\bf H}\xgwsp} \newcommand{\xnsg}{\mbox{\rm nst}\xgwsp} \newcommand{\gunit}{$\mbox{{\rm Gws}}_\omega$--unit} \newcommand{\xid}{\mbox{{\sl Id}}} \newcommand{\xsid}{\mbox{{\sl\scriptsize Id}}} \newcommand{\xrep}{\mbox{{\sl rep}}} \newcommand{\xmin}{\mbox{{\rm min}}} \newcommand{\xbase}{\mbox{{\sl base}}} \newcommand{\xrng}{\mbox{\sl Rng}} \newcommand{\xmod}{\mbox{\sl Mod}} \newcommand{\xp}{\underline{{\cal P}}} \newcommand{\xeq}{\mbox{\sl Eq}} \newcommand{\xqeq}{\mbox{\sl Qeq}} \newcommand{\xax}{\mbox{{\rm Ax}}} \newcommand{\xqx}{\mbox{{\rm Qx}}} \newcommand{\xaxp}{\mbox{$\mbox{\rm Ax}^=$}} \newcommand{\xalg}{\mbox{{\rm Alg}}} \newcommand{\xsg}{\mbox{{\rm SG}}} \newcommand{\xss}{\mbox{{\bf S}}} \newcommand{\xrcan}{\mbox{$\mbox{\rm RCA}_n$}} \newcommand{\xrqpan}{\mbox{$\mbox{\rm RQPA}_n$}} \newcommand{\xrca}{\mbox{$\mbox{\rm RCA}_\omega$}} \newcommand{\xrqpa}{\mbox{$\mbox{\rm RQPA}_\omega$}} \newcommand{\xsurpea}{\mbox{{\bf SUp}{\rm RPEA}}} \newcommand{\xpea}{\mbox{{\rm PEA}}} \newcommand{\xpa}{\mbox{{\rm PA}}} \newcommand{\xrpea}{\mbox{{\rm RPEA}}} \newcommand{\xrpa}{\mbox{{\rm RPA}}} \newcommand{\xba}{\mbox{{\rm BA}}} \newcommand{\xrd}{\mbox{{\bf Rd}}} \newcommand{\xsir}{\mbox{{\bf Sir}}} \newcommand{\xrdca}{\mbox{$\mbox{\bf Rd}_{\mbox{\scriptsize CA}}$}} \newcommand{\xdf}{\stackrel{\mbox{{\rm\scriptsize def}}}} \newcommand{\xsim}{\mbox{$\!\sim$}} \newcommand{\megsz}[2]{#1\lceil\raisebox{-2mm}{$#2$}} \newcommand{\xc}{\mbox{{\bf c}}} \newcommand{\xcd}{\xc^\sigma} \newcommand{\xci}{\mbox{{\scriptsize\bf c}}} \newcommand{\xs}{\mbox{{\bf s}}} \newcommand{\xsi}{\mbox{{\scriptsize\bf s}}} \newcommand{\xpsu}{\mbox{{\scriptsize suc}}} \newcommand{\xppr}{\mbox{{\scriptsize pred}}} \newcommand{\xpsp}{{\mbox{{\scriptsize suc, pred}}}} \newcommand{\xd}[2]{\mbox{$\mbox{\bf d}_{#1#2}$}} \newcommand{\xdv}[2]{\mbox{$\mbox{\bf d}_{#1,#2}$}} \newcommand{\xssu}{\mbox{$\mbox{\bf s}_{\mbox{\scriptsize suc}}$}} \newcommand{\xspr}{\mbox{$\mbox{\bf s}_{\mbox{\scriptsize pred}}$}} \newcommand{\xsre}[2]{\xs_{[#1/#2]}} \newcommand{\xspe}[2]{\xs_{[#1,#2]}} \newcommand{\xsnp}[1]{\xs_{{#1}\mbox{\scriptsize -pred}}} \newcommand{\xpr}{\mbox{{\rm pred}}} \newcommand{\xsu}{\mbox{{\rm suc}}} \newcommand{\xre}[2]{[#1/#2]} \newcommand{\xpe}[2]{[#1,#2]} \newcommand{\bb}[1]{\underline{#1}} \newcommand{\xbpr}{\bb{\xpr}} \newcommand{\xbsu}{\bb{\xsu}} \newcommand{\xbpe}[2]{\bb{\xpe{#1}{#2}}} \newcommand{\xbre}[2]{\bb{\xre{#1}{#2}}} \newcommand{\xbpri}{\bb{\mbox{{\scriptsize pred}}}} \newcommand{\xbsui}{\bb{\mbox{{\scriptsize suc}}}} \newcommand{\xdoub}{\mbox{{\rm doub}}} \newcommand{\xsdoub}{\mbox{$\mbox{\bf s}_{\mbox{\scriptsize doub}}$}} \begin{document} %\pagestyle{headings} \title{Finite Schematizable Algebraic Logic \footnote{This is a pre-publication version of the paper, final version will be prepared later and published elsewhere.}} \author{Ildik\'o Sain\thanks{sain@math-inst.hu}, Viktor Gyuris\thanks{viktor@math.uic.edu or viktor@ludens.elte.hu. Research supported by Hungarian Research Fund, grants F17452, T16448.}} \date{November 25, 1996\\(Version \version)} \maketitle \begin{abstract} In this work, we attempt to alleviate three (more or less) equivalent negative results. These are (i) non-axiomatizability (by any finite schema) of the valid formula schemas of first order logic, (ii) non-axiomatizability (by finite schema) of any propositional logic equivalent with classical first order logic (i.e., modal logic of quantification and substitution), and (iii) non-axiomatizability (by finite schema) of the class of representable cylindric algebras (i.e., of the algebraic counterpart of first order logic). Here we present two finite schema axiomatizable classes of algebras that contain, as a reduct, the class of representable quasi-polyadic algebras and the class of representable cylindric algebras, respectively. We establish positive results in the direction of finitary algebraization of first order logic without equality as well as that with equality. Finally, we will indicate how these constructions can be applied to turn negative results (i), (ii) above to positive ones. \end{abstract} \tableofcontents %MAIN FILE:suc %version 5.1 \section{Introduction} \label{sec-int} Since it was introduced, first order logic became the most frequently used and studied logical system. Its logical connectives and basic concepts are motivated by intuitive ``mathematical'' reasoning. It also plays a fundamental role in logical (formal) investigations of not necessarily mathematical reasoning, cf.\ e.g.\ \cite{philos}, \cite{benthem}. First order logic is only one of the logical systems investigated in modern logic. For many logical systems, or logics for short, the methodology of algebraic logic proved to be very useful. This methodology is summarized e.g.\ in \cite{ansk} and in \cite{nean}. Cf.\ also Blok--Pigozzi \cite{memoirs}. The key step in this methodology is that, to any logic $L$, we associate a class $\xalg(L)$ of algebras, called the algebraic counterpart of the logic $L$. In many cases, investigating $\xalg(L)$ is easier than investigating $L$, e.g.\ because, in the study of $\xalg(L)$, we can use the well developed tools of algebra. A number of problems concerning certain logics $L$ were often solved by translating the problem to $\xalg(L)$, solving the algebraic problem by the methodology of algebra, and then translating the algebraic result back to the logical context in which $L$ was originally investigated. Another equally important value of algebraization is obtaining insights into the essential nature of a logic $L$, via abstraction provided by algebraization. The algebraic counterpart of classical propositional logic is the class of Boolean algebras. Boolean algebras proved immensely useful in studying classical propositional logic, and in understanding its connections with other logical systems. Similarly, for a great number of other logics, studying their algebraic counterparts has proven very useful. One example is propositional modal logic, the algebraic counterpart of which is Boolean algebras with operators. Similar positive examples are most of the non-classical propositional logics, e.g.\ intuitionistic propositional calculus whose algebraic counterpart is the variety of Heyting Algebras. Cf.\ e.g.\ \cite{wojcicki}. In the case of first order logic, when trying to apply the methodology of algebraic logic in the above outlined fashion, we have to face the following problem. As we said, the algebraic counterpart of classical propositional logic is the class of Boolean algebras. This class turns out to be a finitely axiomatizable equational class. The same is true for the other successful examples we referred to. In each case, $\xalg(L)$ is axiomatizable by a finite set of equations or quasi-equations\footnote{Quasi-equations are equational implications.}. As a contrast, in the case of first order logic, all the algebraic counterparts found before 1987 are very far from being finitely axiomatizable. Namely, J.\ D.\ Monk proved in \cite{mo70} that the most thoroughly investigated algebraic counterpart of first order logic with equality, the class $\xrca$ of representable cylindric algebras is not axiomatizable by a finite schema of equations\footnote{ Monk obtained similar negative results for $\mbox{\rm RCA}_3$ already in 1964.}. A similar result was obtained in Sain--Thompson \cite{st} about the class $\xrqpa$ of representable quasi-polyadic algebras (the algebraic counterpart of first order logic without equality)\footnote{ The Sain--Thompson result was preceded by a relevant result of James Johnson \cite{jj} who proved that $\xrqpan$ $(20$ and $\xc_{(\omega)}0=0$. Adding the new operator $\xc_{(\omega)}$ to $\xgs_H$ amounts to adding the formation of {\em existential closure} $\varphi\rightarrow \exists \overline x \varphi$ to the logic being algebraized (where $\overline x$ contains all the variables occuring in $\varphi$). The abbreviation `ec' in $\xgsu_H$ (and in $\xcsu_H$) refers to this fact. \begin{df}{d-g} Throughout this paper, $G$ denotes the following set. $$G\xdf=\{\xre ij \;:\; i,j \in \omega\}\cup\{\xsu,\xpr\}.$$ \end{df} The following theorem summarizes the main results of this section. \begin{theo}{csicsa1} \begin{romanate} \item $\xics_G$ is a finite schema axiomatizable quasi-variety. That is, there is a finite schema $\xqx_G$\footnote{ $\xqx_G$ is presented in Definition \ref{d-qx1} below.} of quasi-equations such that $$ \xics_G = \xmod(\xqx_G)\,. $$ \item $\xigsu_G$ is a finite schema axiomatizable discriminator variety. \item $\xhcs_G$ is a variety axiomatized by a finite set $\xax_G$\footnote{ $\xax_G$ is presented in Definition \ref{d-ax} below.} of equation schemas. Thus, $\xax_G$ axiomatizes $\xeq(\xcs_G)$ i.e.\ $$\xcs_G\models e \;\;\mbox{ iff }\;\; \xax_G\vdash e,$$ for any equation $e$ in the language of $\xcs_G$. \end{romanate} \end{theo} The statements of this theorem are restated in Theorems \ref{th-main}, \ref{cj1}, \ref{t-nemeti} below in a more detailed form. In the following part of this section we present the finite sets of equations and quasi-equations that axiomatize $\xhcs_G$, $\xics_G$ and $\xigsu_G$. Further, the related weak classes are examined and a detailed characterization is given. (Theorem \ref{th-main}) Finally, we show that many of the results remain valid if we replace the set $G$ by an arbitrary set $H$ of transformations provided that $H$ satisfies certain properties. (Theorems \ref{th-nc}, \ref{t-csax}, \ref{t-222}) \begin{df}{d-ax} We define the finite set $\xax_G$ of axiom schemas to be the union of sets (1)--(6) below. \begin{arabate} \item A finite set of equations axiomatizing Boolean algebras. \item For every $\tau\in G$, the following axioms stating that $\xs_\tau$ is a Boolean homomorphism:\\ $\begin{array}{rclrcl} \xs_\tau(x\vee y)&=&\xs_\tau(x)\vee \xs_\tau(y), \;\;\;&\xs_\tau(-x)&=&-\xs_\tau(x). \end{array}$ \item The axioms governing $\xsre ij$'s: for all distinct $i, j, k\in \omega$,\\ $\begin{array}{rclrcl} \xsre ji\xsre ijx&=&\xsre jix,&\;\;\; \xsre jk\xsre ijx&=&\xsre jk\xsre ikx. \end{array}$ \item The axioms describing the connections between $\xsre ij$'s, $\xssu$ and $\xspr$:\\ $\begin{array}[t]{lll} \xspr\xssu x&=&x,\\ \xssu\xspr x&=&\xsre 01x,\\ \xssu\xsre ijx&=&\xsre{\xpsu(i)}{\xpsu(j)}\xssu x \;\;\mbox{ for all distinct $i,j \in \omega$.} \end{array}$ \item Two axiom schemas about $\xc_i$ and the Boolean operations: for all $i\in \omega$,\\ $x\leq \xc_ix$, $\;\;\;\;\xc_i(x\vee y)=\xc_ix\vee\xc_iy.$ \item The axiom schemas describing the connection between $\xsre ij$'s and $\xc_k$'s: for all distinct $i,j,k\in \omega$,\\ $\begin{array}[t]{lll} \xsre ij\xc_ix &=&\xc_ix,\\ \xc_i\xsre ijx &=&\xsre ijx,\\ \xc_k\xsre ijx &=&\xsre ij\xc_kx. \end{array}$ \end{arabate} \end{df} \begin{thn}{th-main}{characterization of $\xigws_G$ and related classes} Let $G$ and $\xax_G$ be as in Definitions \ref{d-g} and \ref{d-ax}. Then statements (1)--(4) below hold. \begin{arabate} \item $\xigws_G$ is axiomatizable by the finite set $\xax_G$ of equation schemas i.e.\ $\xigws_G=\xmod(\xax_G)$. \item $\xigws_G$ is a variety. \item $\xigws_G = \xigwsn_G = \xigwsc_G=\xhcs_G$. \item The set $\xeq(\xcs_G)$ of equations is axiomatizable by the finite set $\xax_G$ of equation schemas i.e.\ $$\xcs_G\models e \;\;\mbox{ iff }\;\; \xax_G\vdash e,$$ for any equation $e$ in the language of $\xcs_G$. \end{arabate} \end{thn} \begin{proof} (2) is a corollary of (1) while (1) is proved in Subsections \ref{subsec-main1} -- \ref{subsec-compr}. To prove (3) we note that statement (3) is a special case of Theorem \ref{th-nc} (ii), (iii). To see that the later is applicable, we need to show that the successor, the predecessor and all the substitutions are bounded transformations of $\omega$ and they have right quasi-inverses in $[G]$. (Consult Definition \ref{d-bounded} for the notion of bounded, quasi-bounded and quasi-invertible transformation.) It easy to verify that the given transformations have the required properties using facts as $\xsu\circ\xpr(i)=\xpr\circ\xsu(i)=i$ whenever $i>0$. Finally, (4) follows from (3) and (1). \end{proof} Later, in Remark \ref{rm-allci}, we show that for a slightly modified version of $\xigws_G$ (where only the 0-th cylindrification is a basic operation, the other cylindrifications are terms of the reduced language) similar results can be achieved. \mbox{} In the proof of the previous theorem we referred to a metatheorem (\ref{th-nc}). There we show that if $H$ satisfies certain requirements then the classes $\xigws_H$ and $\xigwsc_H$ actually coincide with $\xigwsn_H$. \begin{nt}{nt-approx} We will often deal with pairs of sequences that agree on all but finitely many coordinates. If $q_1$ and $q_2$ are sequences then $$q_1\approx q_2\mbox{ iff }|\{i\in \omega\;:\; q_1(i)\neq q_2(i)\}|<\omega.$$ Clearly, $\approx$ is an equivalence relation. \end{nt} \begin{df}{d-bounded} Let $f,g\in {}^\omega\omega$ be arbitrary. \begin{itemize} \item $f$ is said to be {\em bounded} if it does not send infinitely many elements of $\omega$ into the same place, that is, if $|f^{-1}(i)|<\omega$ for all $i\in \omega$. \item $f$ is said to be {\em quasi-bounded} if there is a $k\in \omega$ for which $|f^{-1}(f(k))|<\omega$. \item $g$ is called the {\em right (left) quasi-inverse} of $f$ if $ f\circ g\approx\xid$ ($g\circ f\approx\xid$), where $\xid$ is the identity transformation of $\omega$. $f$ is said to be {\em right (left) quasi-invertible} in $H\subseteq {}^\omega\omega$ if it has a left (right) quasi-inverse in $H$. \end{itemize} \end{df} \begin{dfn}{d-rich}{rich semigroup} Suppose that $i,j,k\in \omega$, $A\subseteq \omega$, $f,g\in {}^\omega\omega$. Then $f[i/j]$ and $f[A/g]$ are transformation of $\omega$ defined as $$f[i/j](k)= \left\{ \begin{array}{cl} j&\mbox{ if $k=i$}\\ f(k)&\mbox{ otherwise} \end{array}\right. \;\;\;\; f[A/g](k)= \left\{ \begin{array}{cl} g(k)&\mbox{ if $k\in A$}\\ f(k)&\mbox{ otherwise.} \end{array}\right.$$ (Note that $f[i/j]$ and $f\circ\xre ij$ are different transformations.)\footnote{ $f[i/j]$ can be distinguished from $f[A/g]$ by noticing that always $|g|\geq\omega>i$.} \\ A semigroup $Q\subseteq {}^\omega\omega$ is called {\em rich} if it satisfies the following two conditions: \begin{itemize} \item $(\forall i,j \in \omega)(\forall f\in Q)\; f[i/j]\in Q$, \item $(\exists \hat s,\hat p\in Q)(\forall f\in Q)$\\ $\;\;\hat p\circ \hat s=\xid\wedge\xrng(\hat s)\neq\omega\wedge (\hat s\circ f\circ \hat p) [(\omega-\xrng(\hat s))/\xid]\in Q$. \end{itemize} \end{dfn} \begin{theo}{th-nc} Let $H$ be an arbitrary set of transformations. \begin{romanate} \item $\xigwsn_H=\xhspcs_H$ is a variety. Thus $\xeq(\xcs_H)=\xeq(\xgwsn_H)$. \item If for all $\sigma\in H$, $\sigma$ is bounded then $$\xigwsn_H = \xigwsc_H = \xhcs_H.$$ \item If for all $\sigma\in H$, $\sigma$ is quasi-bounded and right quasi-invertible in $[H]$, then $$\xigws_H = \xigwsn_H.$$ \item Assume that $[H]$ is a finite schema presented\footnote{ We use the notion of a finite schema presented semigroup in the usual sense. For completeness we will recall this concept in Definition \ref{d-fin-pr} in the `Proofs' section.} rich semigroup. Then, $\xigwsn$ is axiomatizable by a finite schema $\Sigma$ of equations. %I.e.\ $\xigwsn_H=\xmod(\Sigma)$, with $\Sigma$ %finite. \end{romanate} \end{theo} (i) and (iv) are quoted from \cite{gabbay} (Theorem 2.1 (2)), the proof of (ii) and (iii) can be found in Subsection \ref{subsec-compr}. The example below shows that the requirement given in Theorem \ref{th-nc} (iii) cannot be omitted. In some cases $\xeq(\xgws_H)\neq\xeq(\xgwsn_H)$. \begin{ex}{ex0} Let $\xdoub\in {}^\omega\omega$ be defined by $\xdoub(i)=2i$ for every $i\in \omega$, let $H=\{\xdoub\}$ and let $e$ be the equation $\xc_0\xsdoub x=\xsdoub\xc_0 x$. Then $$\xgwsn_H\models e \;\;\mbox{ but }\;\;\xgws_H\not\models e.$$ \end{ex} \begin{proof} Let $V=\mbox{}^\omega 2^{(\langle 0,1,0,1,\ldots\rangle)} \cup \mbox{}^\omega 3^{(\langle 0,0,0,0,\ldots\rangle)}$. Then $\xp(V)\in \xgws_H\setminus\xigwsn_H$ since $e$ fails in $\xp(V)$ (choose $x=\{\langle 2,0,0,0,\dots\rangle \}$) but $e$ is satisfied in every algebra of $\xigwsn_H$. \end{proof} \mbox{} We turn our attention to the study of classes of algebras with square (Cartesian space) unit elements. We prove that the class $\xics_G$ is a finite schema axiomatizable quasi-variety and is strictly smaller than $\xigws_G$. \begin{ex}{ex1} Let $q$ be the quasi-equation $\xspr x=-x\Rightarrow 0=1$. Then\footnote{ For completeness we note connections of Example \ref{ex1} and the theory of polyadic algebras ($\xpa_\omega$'s) and $\xpa$'s with equality ($\xpea_\omega$'s) without recalling these two classes. We use the notation of \cite{hmtii}. Although $\xax_G\not\models q$, we have $\xpa_\omega\models q$ (e.g.\ by the Daigneault--Monk theorem). On the other hand, there are equations $e$ such that $\xpea_\omega\not\models e$ but $\xrpea_\omega\models e$, cf.\ N\'emeti-S\'agi \cite{SagNe95}. } $$ \xgs_G\models q \;\mbox{ but }\;\xigws_G\not\models q.$$ \end{ex} \begin{proof} In a $G$--cylindric generalized set algebra we can pick a constant sequence $s$ in the universe. For any element $x$ of the algebra, the chosen $s$ is in $x$ if and only if it is in $\xspr x$. It implies that $q$ is in the symmetric difference of $-x$ and $\xspr x$ so $\xspr x\neq -x$. On the other hand, if we put $V={}^\omega 2^{(\langle 1,0,1,0,\ldots\rangle )} \cup {}^\omega 2^{(\langle 0,1,0,1,\ldots\rangle )}$ then $e$ fails in $\xp(V)$. (Put $x$ to be ${}^\omega 2^{(\langle 0,1,0,1,\ldots\rangle )}$ and for that $x$, $\xspr x = -x$.)\end{proof} \begin{df}{d-qx1} \begin{romanate} \item Let $n\in \omega$. We define $\xc_{(n)}x\xdf=\xc_0\xc_1\ldots\xc_{n-1} x$. Further, $\xsnp{n} x\xdf=\xspr\xsre 01\xsre 12\ldots\xsre{n-1}n x$. Hence, $\xsnp{n}$ is a term function\footnote{ In set algebras, the term function $\xsnp{n}$ coincides with $\xs_\tau$ for $\tau = \langle0,1,\ldots,n-1,n-1,n,n+1,\ldots\rangle$, that is, $$\tau(i) = (\megsz{\xpr}{\omega -n}) \cup (\megsz{\xid}{n}) =\left\{\begin{array}{ll} i & \mbox{if } i0$ and $\xc_{(\omega)}0=0$ holds. \begin{theo}{t-222} Assume that $H\subseteq {}^\omega\omega\addtolength{\leftmargini}{1em}$ is such that $\xics_H$ is a quasi-variety. Then $\xigsu_H$ is a discriminator variety whose subdirectly irreducible members are exactly the elements of $\xicsu_H$. If all the assumptions of Theorem \ref{t-csax} hold for $H$ then $\xigsu_H$ is axiomatized over $\xigws_H$ by the axioms (i) and (ii) of Theorem \ref{t-nemeti} together with \begin{symbolate}{(iii')} \item axioms corresponding to $\xqx$: for all $m\in \omega,\Gamma_0,\ldots,\Gamma_{n-1}\subseteq_\omega\omega$, $H_i\subseteq_\omega [H]$ such that $(\tau\in H_i\Rightarrow\megsz{\tau}{\Gamma_i}=\megsz{\xid}{\Gamma_i})$ we state\\ $\displaystyle -\xc_{(\omega)}{-(\bigcup_{i\leq m} \xc_{(\Gamma_i)}x_i)} \leq \bigcup_{i\leq m}\xc_{(\omega)}(\bigcap_{\tau\in H_i}\xs_\tau x) $. \end{symbolate} \end{theo} \begin{proof} Let $\Sigma$ be the set equations valid in $\xgsu_H$, that is, $\Sigma=\xeq(\xgsu_H)$. We want to prove $\xigsu_H = \xmod(\Sigma)$. $\xigsu_H\subseteq \xmod(\Sigma)$ is obvious. For proving the other direction, it is enough to show that $$\xsir(\xmod(\Sigma))\subseteq \xicsu_H\subseteq \xigsu_H .$$ Therefore, assume ${\cal A}\in \xsir(\xmod(\Sigma))$. ${\cal A}\models x\neq 0\rightarrow\xc_{(\omega)}x=1$ can be verified as follows. Suppose for contradiction that $\xc_{(\omega)}x\neq 1$ for some element $x$ of ${\cal A}$. Since axioms (i) and (ii) certainly hold in $\xgsu_H$, they are in $\Sigma$. But using axioms (i) and (ii) we can prove that the relativization with $x$ and that with $-x$ decomposes ${\cal A}$ to the subdirect product of the two images. Let ${\cal A} = \langle{\cal B}, \xc_{(\omega)}\rangle$. If $\displaystyle\bigwedge_{i0$, $\xc_i$ can be defined by a term of $\xc_0$ and the other operations as follows. $$ \xc_ix=\xspe i0\xc_0\xspe i0x, $$ where $\xspe ij$ abbreviates the term $\xspr\xsre 0{\xpsu(j)}\xsre{\xpsu(j)}{\xpsu(i)}\xsre{\xpsu(i)}0\xssu$. If we had chosen the smaller set $\{\cup, -, \xs_\tau,\xc_0\}_ {\tau\in H}\xdf=t^*_H\subseteq t_H$ to be the set of basic operations then the class $\xgws^*_H$ of representable algebras would be defined as $$\xgws^*_H=\xss\left\{ \langle {\cal P}(V),\cup,-,\xs_\tau,\xc_0\rangle_{\tau\in H} \;:\; \parbox[c]{35mm}{\small$V$ satisfies the conditions listed in Definition \ref{d-igwsg}}\right\}.$$ With this modified class in place of $\xgws_G$, Theorem \ref{th-main} remains true provided that the set $\xax_G$ is replaced with the following bigger set. For all distinct $i,j,k,l\in \omega$ we state: \begin{arabatesym}{'} \item Same as (1). \item Same as (2). \item (3) together with the following 3 schemas:\\ $\begin{array}[t]{rclrcl} \xsre ik\xsre ijx&=&\xsre ijx,&\;\;\; \xsre kj\xsre ijx&=&\xsre ij\xsre kjx,\\ &&&\;\;\; \xsre kl\xsre ijx&=&\xsre ij\xsre klx. \end{array}$ \item Same as (4). \item (5) restricted to $i=0$, that is, $x\leq \xc_0x$, $\;\;\;\;\xc_0(x\vee y)=\xc_0x\vee\xc_0y$. \item $\begin{array}[t]{lll} \xsre 01\xc_0x &=&\xc_0x,\\ \xc_0\xsre 01x &=&\xsre 01x,\\ \xc_0\xsre ijx &=&\xsre ij\xc_0x. \end{array}$ \end{arabatesym} \end{rmk} \subsection{Finitizing algebras of first order logic with equality} \label{subsec-yeseq} As we said in the Introduction, the present subsection is strongly related to Craig \cite{craig}, and can be viewed as a continuation of the approach initiated therein. Indeed, it is very likely that Theorem \ref{th-rca} below could be proved from Craig's results. However, we show a generalization of these results and in later work we intend to generalize it in various directions, a part of which was indicated in \cite{SaFIN} and \cite{gabbay}. \begin{df}{df-gwsp} Suppose that $H$ is a fixed subset of ${}^\omega\omega$. An algebra is called a {\em generalized weak $H$--cylindric set algebra with equality} (or briefly, a $\xgwsp_H$) if it is of the form $$\langle A,\cup,-,\xs_\tau,\xc_i,\xd ij\rangle_{\tau\in H, i,j\in \omega} $$ where $\langle A,\cup,-,\xs_\tau,\xc_i,\rangle_{\tau\in H,i\in \omega}\in \xgws_H$ and the constants $\xd ij$ are the set theoretic diagonal elements (defined e.g.\ in \cite{hmtii} Def.\ 3.1.1: $\xd ij=\{q\in 1\;:\; q(i)=q(j)\}$ --- where 1 is the unit element of the algebra). The class of all generalized weak $H$--cylindric set algebras with equality is denoted by $\xgwsp_H$. The similarity type of $\xgwsp_H$ is denoted by $t_H^=$. \end{df} Similarly to the case where equality was not present, we define subclasses of $\xgwsp_H$ on the bases of differences between the unit elements of the algebras. \begin{df}{df-norm2} Let $H$ be a subset of ${}^\omega\omega$. The class of all algebras of $\xgwsp_H$, whose unit elements are Cartesian spaces, (generalized Cartesian spaces) is denoted by $\xcsp_H$ ($\xgsp_H$ respectively). \end{df} The class $\xgsp_\emptyset$ is the class of representable cylindric algebras. In the literature (e.g.\ in \cite{hmtii}) it is often denoted by $\xgsp_\omega$ or \xrca. Further parallel notations are $\xgwsp_\emptyset=\xgwsp_\omega$, $\xcsp_\emptyset= \xcsp_\omega$. Since the $t_\emptyset^=$--reduct of a $\xgwsp_H$ is a cylindric algebra, we introduce the notation \xrdca\ to be $\xrd_{t^=_\emptyset}$. \begin{theo}{csicsa2} \begin{romanate} \item $\xhspcsp_\xpsp$ is a variety axiomatized by a finite set $\xaxp$ of equation schemas. Thus, $\xaxp$ axiomatizes $\xeq(\xcsp_\xpsp)$ i.e.\ $$\xcsp_\xpsp\models e \;\;\mbox{ iff }\;\; \xaxp\vdash e,$$ for any equation $e$ in the language of $\xcsp_\xpsp$. \item $\xss\:\xrdca \xhspcsp_\xpsp=\xrca.$ \end{romanate} \end{theo} Theorem \ref{csicsa2} above is a corollary of Theorem \ref{th-rca}. In the latter we give a more detailed description of the classes $\xcsp_\xpsp$ and $\xgwsp_\xpsp$ i.e. we give a set of axioms (Definition \ref{d-ax+}) that axiomatizes them. Results \ref{cj1} and \ref{t-nemeti} have the corollary that\\ {\em $ \xqeq(\xcs_G)$ and $\xeq(\xcsu_G)$ are finite schema axiomatizable.}\hfill (*)\\ In view of the results above, it seems natural to expand some generalization of (*) for the case with equality. This was proved impossible in Craig \cite{craig} Chapter 11. It is proved there (using a result of McKenzie) that neither $\xqeq(\xcsp_\xpsp)$ nor $\xeq(\xgspu_\xpsp)$ is recursively enumerable. Moreover, the following seems to be an even sharper contrast with \ref{cj1} and \ref{t-nemeti}. Let $K$ be the class of algebras that are expansions of elements of $\xcsp_\xpsp$ with the operation $\xc_{(\omega\setminus 2)}$ defined as follows: $$\xc_{(\omega\setminus 2)}x\xdf= \{s\in V\;:\; (\exists s'\in x)\; s(0)=s'(0), s(1)=s'(1)\}.$$ It is proved in \cite{SagNe95} that $\xeq(K)$ is $\Pi_1^1$ complete (i.e.\ highly non-computa\-tional). \begin{df}{d-ax+} We define the finite set \xaxp\ of axiom schemas to be the union of sets (1)--(3) below. \begin{arabate} \item The set of axiom schemas characterizing cylindric algebras with equality (this set is quoted from \cite{hmti} Def.\ 1.1.1 p.162): for all $i,j,k \in \omega$,\\ $\begin{array}{ll} \makebox[0cm][l]{a finite set of equations axiomatizing Boolean algebras}&\\ \xc_i0=0,& x\leq \xc_ix,\\ \xc_i(x\wedge \xc_i y)=\xc_ix\wedge \xc_i y,& \xc_i\xc_j x=\xc_j\xc_i x,\\ \xd ii = 1, &\\ \xd ij=\xc_k(\xd ik\wedge \xd kj)& \mbox{ whenever $k\not\in \{i,j\}$},\\ \xc_i(\xd ij\wedge x)\wedge \xc_i(\xd ij\wedge -x)=0 & \mbox{ whenever $i\neq j$}.\\ \end{array}$ \item The axioms stating that \xssu\ and \xspr are Boolean homomorphisms:\\ $\begin{array}{rclrcl} \xssu(x\vee y)&=&\xssu(x)\vee \xssu(y), \;\;\;&\xssu(-x)&=&-\xssu(x),\\ \xspr(x\vee y)&=&\xspr(x)\vee \xspr(y), \;\;\;&\xspr(-x)&=&-\xspr(x). \end{array}$ \item The axioms describing the connection between $\xssu$, $\xspr$ and the other cylindric operations:\\ $\begin{array}{lll} \xspr\xssu x&=&x,\\ \xssu\xspr x&=&\xc_0(\xd 01\wedge x),\\ \xssu\xc_i x&=&\xc_{\xpsu(i)}\xssu x,\\ \xssu\xd ij &=&\xd{\xpsu(i)}{\xpsu(j)}. \end{array}$ $\xssu(x-\xc_0(-\xd 01))=x-\xc_0(-\xd 01)$. \end{arabate} \end{df} \begin{theo}{th-rca} \begin{arabate} \item $\xrca=\xss\:\xrdca\xmod(\xaxp \mbox{without (4)})$ that is, the equations valid in \xrca\ are exactly those consequences of \xaxp\ \mbox{without (4)} that do not use the new operations $\xssu, \xspr$. \item $\xhgwsp_\xpsp= \xmod(\xaxp)$. \item $\xhspcsp_\xpsp=\xmod(\xaxp)$. \item The set $\xeq(\xcsp_\xpsp)$ of equations valid in $\xcsp_\xpsp$ is axiomatized by the finite set \xaxp\ of equations. I.e.\ $$\xcsp_\xpsp\models e \;\;\mbox{ iff }\;\; \xaxp\vdash e,$$ for any equation $e$ in the language of $\xcsp_\xpsp$. \end{arabate} \end{theo} \begin{proof} We apply the general theorem \ref{t-gen=} to the special case $H=\{\xsu,\xpr\}$. First we note that $[\overline{\xsu,\xpr}]=G$. (See Definition \ref{d-H13} below.) We have already seen that $G$ is rich, the cardinality of $G$ is $\omega$, every element of $G$ is bounded, and right quasi-invertible in $G$. (The right quasi-inverse of $\xre ij$ is $\xid$, while that of $\xsu$ is $\xpr$ and vica versa.) (1) We apply Theorem \ref{t-gen=} (1). Since all the equations valid in $\xigws_G$ --- the equations of H2 --- are consequences of $\xax_G$ (Theorem \ref{th-main} (1)), we need to show that the set \xaxp\ \mbox{without (4)} implies H1 and $\xax_G$. But most of the axioms of H1 and $\xax_G$ is actually listed in \xaxp\ while the rest can be easily derived. (2), (3) and (4) are corollaries of Theorem \ref{t-gen=} (3). (We need only that H3 is also implied by \xaxp.) \end{proof} Clearly, $\xmod(\xaxp)\supset \xgwsp_\xpsp$. We have seen in Theorem \ref{th-rca} (2) that equation (4) is valid in $\xhgwsp_\xpsp$. In the following example we show that it is not a consequence of \xaxp\ giving that the variety generated by $\xgwsp_\xpsp$, that is $\xhgwsp_\xpsp$, is a strictly smaller class than $\xmod(\xaxp)$. \begin{ex}{ex2} Let ${\cal A}$ be the four element Boolean algebra augmented with the unary operations $\xc_i$ $(i\in \omega)$, $\xssu, \xspr$ and the constants $\xd ij$ $(i,j\in \omega)$. $\xssu$ and $\xspr$ interchanges the atoms of ${\cal A}$ and fixes $1$ and $0$ while $\xc_i$ $(i\in \omega)$ are the identity functions. $\xd ij = 1$ for all $(i,j\in \omega)$. Equation (4) of \xaxp\ fails in ${\cal A}$ if we set $x$ to be an atom of ${\cal A}$. \end{ex} Theorem \ref{t-gen=} below states that we can obtain positive results not only for the specific choice $H=\{\xsu,\xpr\}$ but for an arbitrary $H\subseteq {}^\omega\omega$ provided that $H$ satisfies certain conditions. In that sense Theorem \ref{t-gen=} is a metatheorem and Theorem \ref{th-rca} is its special case. In Definition \ref{d-H13} below we define those axioms that are used in the metatheorem \ref{t-gen=}. \begin{df}{d-H13} For any set $H\subseteq {}^\omega\omega$, we define $\bar{H}=H\cup\{\xre ij\;:\; i,j\in \omega\}$. Below we define the sets H1, H2, H3 of equations. \begin{arabatesym}{H} \item The set of all equations valid in $\xgwsn_{\bar{H}}$, that is $\xeq(\xgwsn_{\bar{H}})$. Since $t_{\bar{H}} \not\subseteq t_H^=$, we need to define, how to interpret an equation of $\xgwsn_{\bar{H}}$ in $\xgwsp_H$. If $\xre ij\not\in H$ then the symbol $\xsre ijx$ denotes the term $\xc_i(\xd ij \cap x)$ in the language of $t^=_H$. \item $\begin{array}[t]{lcl} \xsre ijx=\xc_i(\xd ij \cap x) &\mbox{ when }& \xre ij\in H,\\ \xs_\sigma\xd ij=\xd{\sigma(i)}{\sigma(j)} &\mbox{ when }& \sigma\in H,\\ \xc_k\xd ij=\xd ij &\mbox{ when }& i,j,k\in \omega, i\neq k\neq j. \end{array}$ \item $\begin{array}[t]{lcl} \xs_\sigma(x-\xc_0(-\xd01))=x-\xc_0(-\xd01) &\mbox{ when }& \sigma\in H,\\ \xc_i(-\xc_0(-\xd01))=-\xc_0(-\xd01) &\mbox{ when }& i\in \omega,\\ \xc_i\xc_0(-\xd01)=\xc_0(-\xd01) &\mbox{ when }& i\in \omega. \end{array}$ \end{arabatesym} \end{df} \begin{thn}{t-gen=}{general} Let $H$ be a set of transformations of $\omega$. Then (1)--(4) below hold. \begin{arabate} \item If $[{\bar H}]$ is rich, then $\xrca=\xss\:\xrdca\xmod(H1,H2)$. \item If the conditions (a)--(e) are satisfied then $\xeq(\xcsp_H)$ is finitely axiomatizable i.e. there is a finite schema $\Sigma$ of equations such that $$\xcsp_H\models e \;\;\mbox{ iff }\;\; \Sigma\vdash e,$$ for any equation $e$ in the language of $\xcsp_H$. \begin{symbolate}{a} \item $[{\bar H}]$ is rich, \end{symbolate}\vspace{-3mm}\begin{symbolate}{b} \item $|H|\leq \omega$, \end{symbolate}\vspace{-3mm}\begin{symbolate}{c} \item for any $\sigma\in H$, $\sigma$ is bounded, \end{symbolate}\vspace{-3mm}\begin{symbolate}{d} \item for any $\sigma\in H$, $\sigma$ is right quasi-invertible in $[{\bar H}]$, \end{symbolate}\vspace{-3mm}\begin{symbolate}{e} \item $[{\bar H}]$ is a finitely presented semigroup (see Definition \ref{d-fin-pr}). \end{symbolate} \item If the conditions (a)--(c) above and (f) below are satisfied then $\xhgwsp_H=\xmod(H1,H2,H3)$ and therefore, $$\xgwsp_H\models e \;\;\mbox{ iff }\;\; (H1,H2,H3)\vdash e,$$ for any equation $e$ in the language of $\xgwsp_H$. \begin{symbolate}{f} \item for any $\nu, \mu \in [{\bar H}]$ there are $\nu^*, \mu^* \in [{\bar H}]$ with $\nu\circ\nu^*\approx\mu\circ\mu^*$. \end{symbolate} \item If the conditions (a)--(d) are satisfied then $\xhspcsp_H=\xmod(H1,H2,H3)$ and therefore, $$\xcsp_H\models e \;\;\mbox{ iff }\;\; (H1,H2,H3)\vdash e,$$ for any equation $e$ in the language of $\xcsp_H$. Furthermore, if conditions (a)--(d) are satisfied then $\xhgwsp_H=\xhgsp_H=\xhspcsp_H$. \end{arabate} \end{thn} (1) is proved in Subsection \ref{subsec-prrca}. (2) follows from the observation that H2, H3 are already finite schemas of equations, and that by Theorem \ref{th-nc} (iv) above there is a finite schema $\Sigma_0$ such that $\Sigma_0\vdash H1$. Now, $\Sigma=\Sigma_0\cup(H1,H2)$. (3) and (4) is proved in Subsection \ref{wtm}. \subsection{Open Qusetions} The authors would like to collect those questions that where raised in the sections listing the results of the paper. Find simpler axiom schemas aximatizing$\xics_G$ and $\xigs^{ec}_G$, respectively. (Cf.\ Theorem's \ref{cj1}, \ref{t-nemeti} and the definition of $\xqx_G$). Is the quasi-variety $\xgs_{G^\times}$ in Sain \cite{SaFIN}, \cite{S9} (cf.\ e.g.\ Section 4 in \cite{S9}) admits a finite schema axiomatization (perhaps by the techniques of \ref{cj1} or \ref{t-nemeti} herein)? \subsection{Application to logic} \label{appl} Consider the following three types of algebraic results: \begin{romanate} \item $\xigws_H$ is axiomatizable by the finite schema $\xax_H$ of equations (if $H$ satisfies certain conditions). \item $\xigs_H$ is closed under ultraproducts (under some conditions in $H$). \item $\xeq(\xcs_H)$ or $\xeq(\xcsp_H)$ is axiomatizable by a finite set of equation schemas. \end{romanate} In the present work we prove results of type (i)--(iii). A detailed elaboration of some of the logical applications of results of type (i)--(iii) is given in Sain \cite{S9} Section 4. Though therein the explanation is given for a particular choice (denoted by $G^+$) of $H$, the same argument applies to any other choice of $H$ (satisfying the conditions of our theorems). The reader interested in applications to logic and in relevance to the original logic oriented formulation of the finitization problem is referred to Sain \cite{S9} Section 4 and N\'emeti \cite{Ne91}. We plan to elaborate these considerations together with new developments in this direction in a sequel to the present work. \subsection{Comparisons with the polyadic notion of a schema} \label{schema} First half of the material studied in this paper is concerned with algebras of logic {\em without} equality. This half seems to be related to the axiomatization of representable polyadic algebras of infinite dimension ($\xrpa_\omega$). The set of axiom schemas approximating $\xrpa_\omega$ in \cite{hmtii} p225 is denoted by $P_0$--$P_{11}$. A difference between the polyadic approach and ours is that $\xrpa_\omega$ has uncountably many operation symbols, hence the computability or recursive enumerability aspects of, say, a completeness theorem (or equivalently of an axiomatizability theorem) are not automatic consequences of the existence of a finite schema axiomatization provided by the theorem in question. As a contrast, in our approach the basic operation symbols ($\xssu,\xspr,\xsre ij, \xc_i \;\;i,j\in \omega$) are effectively enumerated and hence the finite schemas (e.g.\ $\xax_G$ in Definition \ref{d-ax}) of axioms yield a recursive enumeration of their consequences. To illustrate the computational differences between the two notions of schema we recall the following result of G\'abor S\'agi. There are three primitive recursive functions $\tau_1,\tau_2,\tau_3 \in {}^\omega\omega$ such that the set $E$ of equations of the language of $\xrpa_\omega$ that involve only $\{\xs_{\tau_i}\;:\;i=1,2,3\}$ as operations and are consequences of $P_0$--$P_{11}$ is not recursively enumerable. This seems to mean that there are effective and decidable sublanguages $L$ of the language of $\xrpa_\omega$ such that $E_L=\{e\in L\;:\; \mbox{$P_0$--$P_{11}$}\vdash e\}$ is not recursively enumerable. Cf.\ S\'agi \cite{sagi}. Since $L$ is decidable (as a subset of the full language of $\xrpa_\omega$), this is in contrast with the expected behaviour of finite schema axiomatizations. This observation can be interpreted as saying that the finite schemas $P_0$--$P_{11}$ are less informative from the {\em effective} or {\em constructive} point of view as one would normally expect. This seems to imply that for {\em any} reasonable generalization (from $\omega$ to $L_0$) of the notion of computability the set $\xeq(\xmod(P_0$--$P_{11}))$ will turn non-recursively enumerable. As a contrast, $E_L$ becomes recursively enumerable if we replace $P_0$--$P_{11}$ with any (e.g. $\xax_G$) of {\em our} axiom schemas and $L$ with any decidable (or even recursively enumerable) subset of our equational language. The other half of the present paper, that deals with algebras associated to logics {\em with} equality, does not seem to have a polyadic algebraic ($\xrpa_\omega$--theoretic) counterpart in the literature yet. Such a counterpart would deal with $\xsurpea_\omega$ or $\xeq(\xrpea_\omega)$. (It has been known for long that $\xsurpea_\omega\neq\xrpea_\omega$ hence the subject of study is {\em not} $\xrpea_\omega$ but rather $\xsurpea_\omega$.) In \cite{SagNe95} it is proved about the polyadic notion (or Halmos' notion) of a schema that $\xeq(\xrpea_\alpha)$ is not axiomatizable by any set of polyadic schemas if $\alpha \geq \omega$. Therefore the schema $P_0$--$E_3$ used by Halmos to axiomatize $\xpea_\alpha$ and quoted in \cite[pp.225-6]{hmtii} does not describe $\xeq(\xrpea_\alpha)$, moreover, one cannot add similar schemas to $P_0$--$E_3$ such that the result would axiomatize $\xeq(\xrpea_\alpha)$. %MAIN FILE:suc \section{Proofs} \label{sec-cal} \subsection{An axiomatization of $\xigws_G$ } \label{subsec-main1} To prove Theorem \ref{th-main} (1), we use the method and some theorems described in \cite{gabbay}. \begin{cl}{cl-rich} If the subsemigroup $Q$ of $\langle {}^\omega\omega,\circ\rangle $ is rich then all the finite transformations belong to $Q$. \end{cl} \begin{proof} $\xid\in Q$ since $\xid=\hat p\circ\hat s$. For all $i,j\in \omega$, $\xre ij\in Q$ since $\xre ij=\xid\xre ij$ and $\xpe ij\in Q$ since $\xpe ij=\xre ij\xre ji$. The semigroup of finite transformations is generated by the set of transpositions and replacements. \end{proof} \begin{cl}{cl-g-reach} The semigroup $[ G]$ %(that is, the subsemigroup of $\langle {}^\omega\omega, \circ\rangle $ %generated by the meanings of the elements of $G$) is rich. \end{cl} \begin{proof} All the transpositions belong to $[ G]$, since $$\xpe{i}{j}= \xpr\circ\xre 0j\circ\xre ji\circ\xre i0\circ\xsu.$$ This implies that every finite transformation of $\omega$ belongs to $[G]$. A transformation $f$ of $\omega$ is called {\em $n$-shifted} if $f(x)=x+n$ for all but finitely many members of $\omega$ ($n$ is a given integer). Clearly, $\xsu^n$ is $n$-shifted, $\xpr^n$ is $(-n)$-shifted and $\xid$ is 0-shifted i.e.\ it is a finite transformation. If $f$ is $n$-shifted, $g$ is $(-n)$-shifted then both $f\circ\xpr^n$ and $\xsu^n\circ g$ are finite transformations. (Here $n$ is a natural number.) This implies that $f$ is equal to the composition of a finite transformation (namely $f\circ\xpr^n$) and $\xsu^n$, $g$ is equal to the composition of $\xpr^n$ and a finite transformation (namely $\xsu^n\circ g$). So every $n$-shifted transformation is in $[ G]$. An $f\in {}^\omega\omega$ is called {\em shifted} if it is $n$-shifted for some integer $n$. All shifted transformations belong to $[ G]$ and every member of $[ G]$ is shifted. (The generators of $[ G]$ are shifted, composition of shifted transformations is shifted.) The first condition of Definition \ref{d-rich} is satisfied since if $f$ is shifted then so is $f[i/j]$ and that implies that it belongs to $[ G]$. The elements $\hat s$ and $\hat p$ of $[ G]$ required in the second condition can be $\xsu$ and $\xpr$. $\omega-\xrng(\xsu)=\{0\}$. The previous argument shows that $(\xsu\circ f \circ\xpr)[\{0\}/\xid]$ belongs to $[ G]$. \end{proof} In the definition of $\xgws_H$, $\tau\in H$ plays a double role. Namely, $\xs_\tau$ is a symbol hence $\tau$ itself is also used as a symbol. On the other hand, $\tau$ as an element of ${}^\omega\omega$ is a concrete function i.e.\ it occurs on the semantic side of $\xgws_H$. In the proofs below, it will be most useful to distinguish $\tau$ as a {\em symbol} from $\tau$ as a {\em function}. (The reason for this will be clear e.g.\ in Definition \ref{d-*17} below.) Therefore, from that point on until the end of Subsection \ref{subsec-3.2} we use temporarily $\bb\tau$ when we want to refer to $\tau$ as a concrete {\em transformation} of $\omega$, and we use $\tau$ to refer to the {\em symbol} or {\em name} of the transformation. For example, $\xsu,\xpr,\xre ij, \xpe ij$ are symbols while $\xbsu,\xbpr,\xbre ij, \xbpe ij$ are transformations of $\omega$ $(i,j\in \omega)$. Furthermore, if $\sigma$ is a finite sequence (or word) over $H$, that is $\langle \tau_1,\ldots,\tau_n\rangle=\sigma\in H^*$, then $\bb\sigma$ denotes the transformation $\bb\tau_1 \circ\ldots \circ\bb\tau_n$. If $H$ is a set of symbols then $\bb H=\{\bb\tau\;:\;\tau\in H\}$. It follows that $\bb{H^*}=[\bb H]$. \begin{dfn}{d-*17}{Definition 2.2.2 of \cite{S9}} Let $H$ be a set of names of transformations of $\omega$ with the property that $\xc_i$ and $\xsre ij$ are term definable in $\xigws^*_H$ for every $i,j \in \omega$. Below we define postulates (*1)-(*7). The postulates are stated for all $\sigma,\nu\in H^*$ and for all $i,j \in \omega$. The symbols $\xc_i$ and $\xsre ij$ abbreviate the terms that define $\xc_i$ and $\xsre ij$ respectively. For any word $\sigma\in H^*$, $\sigma=\langle \tau_1\ldots\tau_n\rangle$, $\xs_\sigma(x)$ abbreviates the term $\xs_{\tau_1}\ldots\xs_{\tau_n}(x)$. \begin{arabatesym}{*} \item The finite set of equations axiomatizing Boolean algebras. The axioms stating that $\xc_i$ is an additive complemented closure operation and $\xc_i$, $\xc_j$ commute: $x\leq \xc_ix$, $\xc_ix=\xc_i\xc_ix$, $\xc_i(x\vee y)=\xc_ix\vee\xc_iy$, $\xc_i(-\xc_ix)=-\xc_ix$, $\xc_i\xc_jx=\xc_j\xc_ix$. \item The axioms stating that $\xs_\sigma$ is a Boolean homomorphism:\\ $\xs_\sigma(x\vee y)=\xs_\sigma(x)\vee \xs_\sigma(y)$, $\;\;\xs_\sigma(-x)=-\xs_\sigma(x)$. \item $\xs_\sigma(x)=\xs_\nu(x)$ if $\bb{\sigma}=\bb{\nu}$. \item $\xs_\sigma(x)=x$ if $\bb{\sigma}=\xid$. \item $\xs_\sigma\xc_ix=\xs_\nu\xc_ix$ if $j\neq i\Rightarrow \bb{\nu}(j)=\bb{\sigma}(j)$. \item $\xs_\sigma\xc_ix=\xc_j\xs_\sigma x$ if $\bb{\sigma}^{-1}(j)=\{i\}$. \item $\xc_i\xsre{i}{j}x=\xsre{i}{j}x$ if $i\neq j$. \end{arabatesym} \end{dfn} \begin{thn}{th-*17}{Theorem 2.2.4 of \cite{S9}} Let $H$ be a set as in the previous definition. Assume that $[\bb H]$ is rich. Then $$\xmod_{t^*_H}(\mbox{{\rm (*1)-(*7)}})=\xigwsn_H{}^*.$$ \end{thn} \begin{crl}{cr-*171} Let $H$ be as in the previous theorem. Also assume that the set theoretic operations $\xc_i$ ($i>0$) are term definable in $\xgws^*_H$. Then (*1)-(*7) together with the definition of $\xc_i$ ($i>0$) is a complete axiomatization of $\xigwsn_H$. \end{crl} \begin{crl}{cr-*17} (*1)-(*7) together with the definition of $\xc_i$ ($i>0$) is a complete axiomatization of $\xigwsn_G$. Furthermore, that set is a complete axiomatization of $\xigws_G$ since the two class coincide as it will be proved in Subsection \ref{subsec-compr}. \end{crl} \subsection{Theorem \protect\ref{th-main} (1): finite schema axiomatizing $\xigws_G$} \label{subsec-3.2} The axiom system defined in Definition \ref{d-*17} is not a schema axiomatization since the variable $\sigma$ ranges over $G^*$ and not $G$. In this subsection we will correct the axiom system. In the definition below we recall a standard concept of universal algebra. (See e.g.\ \cite{hmtii}.) \begin{df}{d-fin-pr} An algebra ${\cal A}$ is said to be {\em presented} by a set $\Sigma$ of defining equation in a variety $V$ if all of the following conditions hold. \begin{itemize} \item ${\cal A}$ is generated by some set $H\subseteq A$. \item We denote the expansion of the algebra ${\cal A}$ with constants corresponding to $H$ by ${\cal A}'$. $\Sigma$ is a set of equations of the language of ${\cal A}'$ that contain no variables. \item For every pair of terms $\tau$ and $\nu$ of the language of ${\cal A}'$ that contain no variables $$\;\;{\cal A}'\models\tau=\nu\;\Leftrightarrow \Sigma\cup\xeq(V)\models\tau=\nu.$$ \end{itemize} \end{df} Since the equational logic has a strongly complete and sound inference system, in the case when $V$ is the variety \xsg\ of all semigroups we can simplify the last condition as \begin{itemize} \item $(\forall \tau,\nu\in H^*)\;\;\bb{\tau}=\bb{\nu} \;\Leftrightarrow\; \Sigma\cup\xeq(\xsg)\vdash\tau=\nu$. \end{itemize} \begin{theo}{th-g-pr} $[\bb G]$ is presented by the following set of equations in the variety of all semigroups: \begin{arabatesym}{3.} \item $\xpr\,\xsu=\lambda$ where $\lambda$ is the empty word, \item $\xsu\,\xpr=\xre{0}{1}$, \item $\xsu\xre ij=\xre{i+1}{j+1}\xsu$ for every distinct $i,j\in \omega$, \item $\xre ij\xpr=\xpr\xre{i+1}{j+1}$ for every distinct $i,j\in \omega$ with $i\neq 0$, \item $\xre 0j\xpr=\xpr\xre{0}{j+1}\xre{1}{j+1}$ for every $j\in\omega$. \item Thompson's axioms from \cite{T} that present the semigroup generated by the replacements only. All $i,j,k,l\in \omega$ are distinct. \begin{arabatesym}{B} \item $\xre ik\xre ij=\xre ij$, \item $\xre ji\xre ij=\xre ji$, \item $\xre jk\xre ij=\xre jk\xre ik$, \item $\xre kj\xre ij=\xre ij\xre kj$, \item $\xre kl\xre ij=\xre ij\xre kl$, \item $\xre ij\xre jk \xre ki\xre ij=\xre ik\xre kj\xre ji$, \item $\xre ij\xre jk \xre kl\xre li=\xre ik\xre kl\xre lj\xre ji\xre il$. \end{arabatesym} \end{arabatesym} \end{theo} \begin{proof} We will use Thompsons result saying that the semigroup generated by the replacements is presented by a set of axioms. The set listed in \cite{T} contains three additional axioms but they are derivable from the others:\\ $\xre ij\xre ij=\xre ij\xre i{i+j+1}\xre ij=\xre i{i+j+1}\xre ij=\xre ij$\\ $\xre ij\xre kj\xre ij=\xre ij\xre ij\xre kj=\xre ij\xre kj$ and\\ $\xre ij\xre kl\xre ij=\xre ij\xre ij\xre kl=\xre ij\xre kl$. In this proof we will write $\vdash$ instead of (3.1)-(3.6)$\cup\xeq(\xsg)\vdash$. We say that $\tau\in G^*$ is in {\em normal form} if $\tau=\xpr^n\tau'\xsu^m$ for some $\tau'\in \{\xre ij\}_{i,j\in \omega}^*$ and $n,m \in \omega$. Every word can be reduced to a normal formed word using only (3.1)-(3.5). This implies that $$(\forall \tau\in G^*)(\exists \tau'\in G^*) \;\;\vdash \tau=\tau' \mbox{ and $\tau'$ is in normal form}$$ Let $\tau$ and $\nu$ be arbitrary words from $G^*$, assume that $\bb{\tau}=\bb{\nu}$. There are $n,m,l,k\in \omega$ and $\tau',\nu'\in \{\xre{i}{j}\}_{i,j\in\omega}^*$ for that $\vdash\tau=\xpr^n\tau'\xsu^m$, $\vdash\nu=\xpr^l\nu'\xsu^k$. Since $\bb{\tau}$ is $m-n$-shifted, $\bb{\nu}$ is $k-l$-shifted we can conclude that $m-n=k-l$ or $m=n+k-l$. Without loss of generality we may assume that $l\leq n$. $\vdash\xpr^l\nu'\xsu^k= \xpr^l\xpr^{n-l}\xsu^{n-l}\nu'\xsu^k= \xpr^n\nu''\xsu^{n-l}\xsu^k= \xpr^n\nu''\xsu^m$ can be derived using (3.1), (3.3) and the previous observation. $\vdash\xsu^n\tau\xpr^m=\xre 01^n\tau'\xre 01^m$ and similarly $\vdash\xsu^n\nu\xpr^m=\xre 01^n\nu''\xre 01^m$ using (3.2). $\bb{\tau}=\bb{\nu}$ implies $\xbsu^n\circ\bb{\tau}\circ\xbpr^m= \xbsu^n\circ\bb{\nu}\circ\xbpr^m= \xbre 10^n\circ\bb{\tau'}\circ\xbre 10^m= \xbre 10^n\circ\bb{\nu''}\circ\xbre 10^m$. >From the main result of Thompson \cite{T} we know that $\xbre 10^n\circ\bb{\tau'}\circ\xbre 10^m= \xbre 10^n\circ\bb{\nu''}\circ\xbre 10^m$ imply $\vdash\xre 01^n\tau'\xre 01^m=\xre{0}{1}^n\nu''\xre 01^m$. Collecting all the information we have: $\vdash\xsu^n\tau\xpr^m=\xsu^n\nu\xpr^m$. But this implies $\vdash\xpr^n\xsu^n\tau\xpr^m\xsu^m= \xpr^n\xsu^n\nu\xpr^m\xsu^m$. Using (3.1) again we can conclude $\vdash\tau=\nu$ and this completes the proof. \end{proof} The set of defining equations listed in \ref{th-g-pr} is not independent. Below we show that equations (3.4), (3.5), (B6), (B7) are implied by the others. \begin{cl}{cl-b7} (3.1),(3.2),(3.3),(B1),(B3),(B4),(B5)$\vdash$(B6) \end{cl} \begin{proof} First we prove that the listed B-axioms imply $$\xre ij\xre jk\xre ki\xre ij\xre ab=\xre ik\xre kj\xre ji\xre ab$$ where all $i,j,k,a,b$ are distinct: \begin{eqnarray*} \xre{i}{j}\xre{j}{k}\xre{k}{i}\xre{i}{j}\xre{a}{b} &\stackrel{B1}=& \xre{i}{j}\xre{j}{k}\xre{k}{i}\xre{i}{j}\xre{a}{j}\xre{a}{b}\\ &\stackrel{B4}=& \xre{i}{j}\xre{j}{k}\xre{k}{i}\xre{a}{j}\xre{i}{j}\xre{a}{b}\\ &\stackrel{B1}=& \xre{i}{j}\xre{j}{k}\xre{k}{i}\xre{a}{i}\xre{a}{j}\xre{i}{j}\xre{a}{b}\\ &\stackrel{B3,B4}=& \xre{i}{j}\xre{j}{k}\xre{a}{i}\xre{k}{a}\xre{a}{j}\xre{i}{j}\xre{a}{b}\\ &\stackrel{B5,B3,B4,B1}=& \xre{a}{j}\xre{i}{j}\xre{j}{k}\xre{i}{j}\xre{k}{a}\xre{a}{b}\\ &\stackrel{B3}=& \xre{a}{j}\xre{i}{j}\xre{j}{k}\xre{i}{k}\xre{k}{a}\xre{a}{b}\\ &\stackrel{B4,B1,B3}=& \xre{a}{j}\xre{i}{k}\xre{j}{i}\xre{k}{a}\xre{a}{b}\\ &\stackrel{B5}=& \xre{i}{k}\xre{a}{j}\xre{k}{a}\xre{j}{i}\xre{a}{b}\\ &\stackrel{B3,B4,B5}=& \xre{i}{k}\xre{k}{j}\xre{a}{j}\xre{a}{b}\xre{j}{i}\\ &\stackrel{B1,B5}=& \xre{i}{k}\xre{k}{j}\xre{j}{i}\xre{a}{b}. \end{eqnarray*} Now we can compute: \noindent $\xre{i}{j}\xre{j}{k}\xre{k}{i}\xre{i}{j} \stackrel{3.1}= \xpr\,\xsu\xre{i}{j}\xre{j}{k}\xre{k}{i}\xre{i}{j} \stackrel{3.3,3.1,3.2}=$\\ $\xpr\xre{i+1}{j+1}\xre{j+1}{k+1}\xre{k+1}{i+1}\xre{i+1}{j+1}\xre{0}{1}\xsu=$\\ $\xpr\xre{i+1}{k+1}\xre{k+1}{j+1}\xre{j+1}{i+1}\xre{0}{1}\xsu \stackrel{3.3,3.1,3.2}=$\\ $\xre{i}{k}\xre{k}{j}\xre{j}{i}$. \end{proof} \begin{cl}{cl-b8} (3.1),(3.2),(3.3),(B1),(B3),(B4),(B5)$\vdash$(B7) \end{cl} \begin{proof} First we prove that the listed B-axioms imply $$\xre{i}{k}\xre{k}{l}\xre{l}{j}\xre{j}{i}\xre{i}{l}\xre{a}{b}=\xre{i}{j}\xre{j}{k}\xre {k}{l}\xre{l}{i}\xre{a}{b}$$ where all $i,j,k,l,a,b$ are distinct: \begin{eqnarray*} \xre{i}{k}\xre{k}{l}\xre{l}{j}\xre{j}{i}\xre{i}{l}\xre{a}{b} &\stackrel{B1,B4}=& \xre{i}{k}\xre{k}{l}\xre{l}{j}\xre{j}{i}\xre{a}{l}\xre{i}{l}\xre{a}{b}\\ &\stackrel{B1,B4,B3}=& \xre{i}{k}\xre{k}{l}\xre{l}{j}\xre{a}{i}\xre{j}{a}\xre{a}{l}\xre{i}{l}\xre{a}{b}\\ &\stackrel{B4,B5,B3}=& \xre{a}{k}\xre{i}{k}\xre{k}{l}\xre{l}{j}\xre{i}{l}\xre{j}{a}\xre{a}{b}\\ &\stackrel{B4,B3}=& \xre{a}{k}\xre{i}{k}\xre{k}{l}\xre{i}{j}\xre{l}{i}\xre{j}{a}\xre{a}{b}\\ &\stackrel{B5,B1}=& \xre{a}{k}\xre{i}{j}\xre{k}{l}\xre{l}{i}\xre{j}{a}\xre{a}{b}\\ &\stackrel{B5}=& \xre{i}{j}\xre{a}{k}\xre{j}{a}\xre{k}{l}\xre{l}{i}\xre{a}{b}\\ &\stackrel{B3,B4,B5,B1}=& \xre{i}{j}\xre{j}{k}\xre{a}{k}\xre{a}{j}\xre{k}{l}\xre{l}{i}\xre{a}{b}\\ &\stackrel{B1,B5}=& \xre{i}{j}\xre{j}{k}\xre{k}{l}\xre{l}{i}\xre{a}{b}. \end{eqnarray*} Now we can compute:\\ $\xre{i}{k}\xre{k}{l}\xre{l}{j}\xre{j}{i}\xre{i}{l} \stackrel{3.1}= \xpr\,\xsu\xre{i}{k}\xre{k}{l}\xre{l}{j}\xre{j}{i}\xre{i}{l} \stackrel{3.3,3.1,3.2}=$\\ $\xpr\xre{i+1}{k+1}\xre{k+1}{l+1}\xre{l+1}{j+1}\xre{j+1}{i+1}\xre{i+1}{l+1}\xre{0} {1}\xsu=$\\ $\xpr\xre{i+1}{j+1}\xre{j+1}{k+1}\xre{k+1}{l+1}\xre{l+1}{i+1}\xre{0}{1}\xsu \stackrel{3.3,3.1,3.2}=$\\ $\xre{i}{j}\xre{j}{k}\xre{k}{l}\xre{l}{i}$. \end{proof} \begin{cl}{cl-35} (3.1),(3.2),(3.3),(B3),(B4)$\vdash$(3.5) \end{cl} \begin{proof} $\xre{0}{j}\xpr$ $\stackrel{3.1}=$ $\xpr\,\xsu\xre{0}{j}\xpr$ $\stackrel{3.3}=$ $\xpr\xre{1}{j+1}\xsu\,\xpr$ $\stackrel{3.2}=$\\ $\xpr\xre{1}{j+1}\xre{0}{1}$ $\stackrel{B3,B4}=$ $\xpr\xre{0}{j+1}\xre{1}{j+1}$ \end{proof} \begin{cl}{cl-34} (3.1),(3.2),(3.3),(B4),(B5)$\vdash$(3.4) \end{cl} \begin{proof} $\xre{i}{j}\xpr$ $\stackrel{3.1}=$ $\xpr\,\xsu\xre{i}{j}\xpr$ $\stackrel{3.3}=$ $\xpr\xre{i+1}{j+1}\xsu\,\xpr$ $\stackrel{3.2}=$\\ $\xpr\xre{i+1}{j+1}\xre{0}{1}$ $\stackrel{B4 or B5}=$ $\xpr\xre{0}{1}\xre{i+1}{j+1}$ $\stackrel{3.2}=$\\ $\xpr\,\xsu\,\xpr\xre{i+1}{j+1}$ $\stackrel{3.1}=$ $\xpr\xre{i+1}{j+1}$ \end{proof} We quote an important result of Pinter. \begin{cln}{cl-p}{Lemma 2.2 of \cite{P}} For every distinct $i,j,k,l\in \omega$ we have $\begin{array}[t]{lcl} \xax_G&\vdash&\xsre ik\xsre ij=\xsre ij,\\ \xax_G&\vdash&\xsre kj\xsre ij=\xsre ij\xsre kj,\\ \xax_G&\vdash&\xsre kl\xsre ij=\xsre ij\xsre kl. \end{array}$ \end{cln} We will need the following technical observation that originates from S\'andor Csizmazia: \begin{lm}{lm-uj7} $\xax_G$ together with the equations (*3), (*4), (*5), (*1) without $\xc_i\xc_jx=\xc_j\xc_ix$ implies that for any $\tau\in \{\xre ij\mid i,j\geq 1\}\cup\{\xre 10\xsu,\xpr\xre 12\}$ $$\xs_\tau\xc_0 x=\xc_0 \xs_\tau x$$ %(Note that $\xc_i$, as it was mentioned earlier, is a term in the %language of $\xgws_G$.) \end{lm} \begin{proof} There is nothing to prove in $\xsre ij\xc_0x=\xc_0\xsre ijx$ $(i,j\geq 1)$ since it is included in $\xax_G$. It was formulated in the lemma only for further applications. To prove the other two statements we will need the following claim quoted from Pinter \cite{P}: \begin{cl}{cl-ci} $\xc_ix=\xmin\overbrace{\{y\mid y=\xsre ijy, y\geq x\}}^B$ \end{cl} \begin{proof} $\xc_ix\in B$ since $\xsre ij\xc_ix=\xc_ix$ and $\xc_i x\geq x$ that is (5) and (6) of $\xax_G$. For any $y\in B$ $y\geq \xc_ix$ since $\xc_ix\stackrel{*1}{\leq}\xc_iy=\xc_i\xsre ij y \stackrel{*7}=\xsre ijy=y$. \end{proof} Further observations are needed. \begin{cl}{cl-defci} $\xc_ix=\xspe 0i\xc_0\xspe0ix$ \end{cl} \begin{proof} %Refering back to Using the previous claim, we have to prove that $\xspe 0i\xc_0\xspe0ix\in B\xdf=\{y\mid y=\xsre ijy, y\geq x\}$ and $y\in B\;\Rightarrow \;y\geq \xspe 0i\xc_0\xspe0ix$.\\ $\xsre ij\xspe 0i\xc_0\xspe0ix \stackrel{*3}= \xspe 0i\xsre 0j\xc_0\xspe0ix \stackrel{6}= \xspe 0i\xc_0\xspe0ix.$\\ (5) implies $\xc_0\xspe 0ix\geq \xspe 0ix$, using (2) we have $\xspe 0i\xc_0\xspe0ix \geq \xspe 0i\xspe0ix \stackrel{*4}=x$.\\ $y\in B\;\Rightarrow \;y\geq x \stackrel{*1,2}\Rightarrow \xspe 0i\xc_0\xspe0ix \leq \xspe 0i\xc_0\xspe0iy \stackrel{y\in B}= \xspe 0i\xc_0\xspe0i\xsre ijy \stackrel{*3}= \xspe 0i\xc_0\xsre 0j\xspe0iy \stackrel{6}= \xspe 0i\xsre 0j\xspe0iy \stackrel{*3}= \xsre 0jy \stackrel{y\in B}=y. $ \end{proof} \begin{cl}{cl-c1s01} $\xc_0\xsre 10x = \xc_1\xsre 01x$ \end{cl} \begin{proof} $ \xc_0\xsre 10x \stackrel{*3}= \xc_0\xsre 12\xsre 10x \stackrel{6}= \xsre 12\xc_0\xsre 10x \stackrel{*3}= \xsre 10\xsre 12\xc_0\xsre 10x \stackrel{6}=$\\ $\xsre 10\xc_0\xsre 12\xsre 10x \stackrel{*3}= \xsre 10\xc_0\xsre 10x \stackrel{*3}= \xspe01\xsre 01\xc_0\xspe01\xsre 01x \stackrel{6}=$\\ $\xspe01\xc_0\xspe01\xsre 01x \stackrel{Cl. \ref{cl-defci}}= \xc_1\xsre 01x $ \end{proof} \begin{cl}{cl-cisuc} $\xc_{i+1}\xssu x=\xssu\xc_ix$ \end{cl} \begin{proof}Let $ \begin{array}[t]{lll} B_1 &=& \{ y\mid \xsre{i+1}{i+2}y=y, y\geq \xssu x\},\\ B_{12}&=& \{ y\mid \xsre{i+1}{i+2}y=\xsre01y=y,y\geq \xssu x\},\\ B_{21}&=& \{\xssu y\mid \xsre{i}{i+1} y=y, y\geq x\},\\ B_2 &=& \{ y\mid \xsre{i}{i+1} y=y, y\geq x\}. \end{array}$\\ The following statements prove this claim: $ \begin{array}[t]{lrcl} \mbox{I} & \xc_{i+1}\xssu x &=& \xmin B_1, \\ \mbox{II} & \xmin B_1 &=& \xmin B_{12},\\ \mbox{III} & B_{12} &=& B_{21},\\ \mbox{IV} & \xmin B_{21} &=& \xssu \xmin B_2,\\ \mbox{V} & \xmin B_2 &=& \xssu\xc_i x. \end{array}$. I, V follow from Claim \ref{cl-ci}, IV from the observation that $y\in B_2 \;\leftrightarrow \;\xssu y\in B_{21}$. Similarly to the proof of the previous claim, in II we need to show that $B_{12}\subseteq B_1$ (trivial) and $(\forall y\in B_1)\; -\xc_0(-y)\in B_{12}\wedge -\xc_0(-y)\leq y$.\\ So suppose $y\in B_1$. Then $\xsre{i+1}{i+2}(-\xc_0(-y)) \stackrel{Ax}= -\xc_0(-\xsre{i+1}{i+2}y)=-\xc_0(-y)$,\\ $\xsre01(-\xc_0(-y))= -\xsre01\xc_0(-y)= -\xc_0(-y)$ and\\ $y\geq \xssu x \Rightarrow -\xc_0(-y)\geq -\xc_0(-\xssu x)= -\xc_0\xssu (-x) \stackrel*= -\xssu (-x)=\xssu x$.\\ In * we used that $\xssu x=\xssu\xspr\xssu x=\xsre 01\xssu x= \xc_0\xsre 01\xssu x=\xc_0\xssu x$. Turning to III, suppose that $y\in B_{12}$. Then $y=\xsre01y=\xssu(\xspr y)$.\\ $\xsre i{i+1}(\xspr y)= \xspr\xssu\xsre i{i+1}(\xspr y)= \xspr\xsre{i+1}{i+2}\xssu\xspr y=$\\ $\xspr\xsre{i+1}{i+2}\xsre01 y= \xspr y$,\\ $y\geq \xssu x \Rightarrow \xspr y\geq \xspr\xssu x=x$. On the other hand if we suppose that $\xssu y\in B_{21}$ then\\ $\xsre{i+1}{i+2}\xssu y=\xssu\xsre i{i+1}y=\xssu y$,\\ $\xsre01\xssu y=\xssu\xsre\xssu y=\xssu y$ and\\ $y\geq x \Rightarrow \xssu y \geq \xssu x$. \end{proof} Now we can prove the two statements formulated in the lemma:\\ $\xc_0\xsre 10\xssu x \stackrel{*}= \xssu\xc_0 x \stackrel{6}= \xssu\xsre 01\xc_0 x \stackrel{4}= \xsre 12\xssu\xc_0 x \stackrel{3}=\\ \stackrel{3}= \xsre 10\xsre 12\xssu\xc_0 x= \xsre 10\xssu\xc_0 x$,\\ % $\xc_0\xspr\xsre 12 x \stackrel{4}= \xspr\xssu\xc_0\xspr\xsre 12 x \stackrel{*}= \xspr\xc_0\xsre 01 \xssu\xspr\xsre 12 x=\\ =\xspr\xc_0 \xsre 12 x= \xspr\xsre 12 \xc_0 x$.\\ In * we used $\xc_0\xsre10\xssu x \stackrel{Cl. \ref{cl-c1s01}}= \xc_1\xsre01\xssu x \stackrel{Ax}= \xc_1\xssu\xspr\xssu x \stackrel{Ax}=$\\ $\stackrel{Ax}= \xc_1\xssu x \stackrel{Cl. \ref{cl-cisuc}}= \xssu\xc_0 x$. \end{proof} \begin{proofof}{Theorem \ref{th-main} (1)} Using the result of the previous subsection stated in Corollary \ref{cr-*17} we need to prove only that $\xax_G\vdash$(*1)--(*7) and $\xax_G\vdash\xc_ix=\xspe0i\xc_0\xspe0ix$. (*2) is a trivial consequence of (2). (3) and (4) together imply (*3) and (*4) since if ${\cal A}$ is an algebra of $\xigws_G$ and ${\cal A}^*$ is the semigroup of all polynomials of ${\cal A}$, expanded with the constant symbols $\xre{i}{j}, \xsu, \xpr$ evaluated into the polynomials $\xsre ij, \xssu, \xspr$ then ${\cal A}^*$ is a model of (3.1)--(3.6) ((3) and (4) is the relevant part of the set of equations (3.1)--(3.7) --- see Claim \ref{cl-b7}--\ref{cl-p} --- written in the language of ${\cal A}^*$) and so $\bb{\tau}=\bb{\nu}$ forces ${\cal A}^*\models\tau=\nu$ and that is $\xs_\tau x=\xs_\nu x$. (*7) is included in (6). To prove (*5), suppose $\tau$ and $\nu$ are in $G^*$ and $\bb{\tau}$ and $\bb{\nu}$ agree everywhere but in $i$. Then $\bb{\tau}\circ\xbre{i}{i+1}$ and $\bb{\nu}\circ\xbre{i}{i+1}$ are equal everywhere. \begin{eqnarray*} \xs_\tau\xc_ix&\stackrel{6}=& \xs_\tau\xsre i{i+1}\xc_ix= \xs_{\tau\xre i{i+1}}\xc_ix=\\ &=&\xs_{\nu\xre i{i+1}}\xc_ix= \xs_\nu\xsre i{i+1}\xc_ix \stackrel{6}= \xs_\nu\xc_ix \end{eqnarray*} In (*1) $x\leq \xc_ix$, $\xc_i(x\vee y)=\xc_ix\vee \xc_iy$ follow from (2) and (5). $\xc_i\xc_ix=\xc_ix$ and $\xc_i(-\xc_ix)=-\xc_ix$ is a consequence of (2) and (6): $\xc_i\xc_ix=\xc_i\xsre i{i+1}\xc_ix=\xsre i{i+1}\xc_ix=\xc_ix$ and $\xc_i(-\xc_ix)=\xc_i(-\xsre i{i+1}\xc_ix)=\xc_i\xsre i{i+1}(-\xc_ix)=$\\ $=\xsre i{i+1}(-\xc_ix)= -\xsre i{i+1}\xc_ix=-\xc_ix$ To prove (*6) we will need the following observation: {\em If $T_0=\{f\in [\bb G]\mid f^{-1}(0)=\{0\}\}$ and $G_0=\{\xre ij\mid i,j\geq 1\}\cup\{\xre 10\xsu,\xpr\xre 12\}$ then $T_0$ is generated by the meanings of the elements of $G_0$.} To verify this statement define the function ${}'$ mapping $[\bb G]$ into itself $$f'=(\xbsu\circ f\circ\xbpr)\xre{0}{0}$$ (Since $[\bb G]$ is rich $f'\in [\bb G]$.) It is easy to check that ${}'$ is a homomorphism ($(f\circ g)'=f'\circ g'$), furthermore, the ${}'$ image of $[\bb G]$ is $T_0$ (if $f\in [\bb G]$ then $f'^{-1}(0)=\{0\}$ so $f'\in T_0$ and if $g\in T_0$ then $(\xbpr\circ g\circ\xbsu)'=g$). Finally, we note that the set of transformations named by the elements of $G_0$ coincide with the ${}'$ image of the set of those transformations that are named by the elements of $G$. We note that for any $\tau\in G_0$, $\xs_\tau\xc_0 x=\xc_0 \xs_\tau x$. This follows from Lemma \ref{lm-uj7} since all the extra equations listed in the formulation of the lemma are consequences of $\xax_G$, as it was proved up till this point. In passing, we mention that the same reasoning shows that Claim \ref{cl-defci} proves that the definition of $\xc_i$ ($i>0$) is implied by $\xax_G$. Turning our attention again to (*6), suppose $\tau\in G^*$, $\bb{\tau}^{-1}(j)=\{i\}$. Then $f=\xbpe j0\circ\bb{\tau}\circ\xbpe i0\in T_0$. Using the previous observation, $f$ is a composition of functions named by elements of $G_0$ say, $f=\bb{\nu_1}\circ\ldots\circ\bb{\nu_n}$. (3), (4) and (6) imply that $$\xs_{\xpe j0\tau\xpe i0}\xc_0x= \xs_{\nu_1\ldots\nu_n}\xc_0x= \xs_{\nu_1}\ldots\xs_{\nu_n}\xc_0x= \xc_0\xs_{\nu_1}\ldots\xs_{\nu_n}x= \xc_0\xs_{\xpe j0\tau\xpe i0}x.$$ Finally we derive \begin{eqnarray*} \xs_\tau\xc_ix&\stackrel{\dag}=& \xs_\tau\xspe i0\xc_0\xspe i0x= \xspe j0\xs_{\xpe j0\tau\xpe i0}\xc_0\xspe i0x=\\ &=&\xspe j0\xc_0\xs_{\xpe j0\tau\xpe i0}\xspe i0x\stackrel{\dag}= \xc_j\xs_\tau x. \end{eqnarray*} \noindent (In $\dag$ we used that the definition of $\xc_i$ and $\xc_j$ is already proven from $\xax_G$.) It is left to prove $\xc_i\xc_jx=\xc_j\xc_ix$ in (*1). For that we need $x\leq y\Rightarrow \xc_ix\leq \xc_iy$ and $\xc_i\xc_j\xc_ix=\xc_j\xc_ix$. $\xc_i\xc_j\xc_ix \stackrel{6}= \xc_i\xc_j\xsre ik\xc_ix \stackrel{*6}= \xc_i\xsre ik\xc_j\xc_ix \stackrel{6}= \xsre ik\xc_j\xc_ix \stackrel{*6}= \xc_j\xsre ik\xc_ix \stackrel{6}= \xc_j\xc_ix$.\\ Now $\xc_i\xc_jx\leq \xc_i\xc_j\xc_ix=\xc_j\xc_ix$ and symmetrically $\xc_j\xc_ix\leq \xc_i\xc_jx$ giving $\xc_j\xc_ix=\xc_i\xc_jx$. \end{proofof} In the previous two subsections we distinguished the symbol $\tau$ from the transformation $\bb{\tau}$ denoted by it. This distinction is not necessary anymore since axioms (*3), (*4) of Definition \ref{d-*17} hold in all algebras studied hereafter. %and any pair of symbols %or sequences of symbols have the same meaning in any any algebra %satisfying *3 and *4 provided that they denote the same transformation %in ${}^\omega\omega$. So we return to the original notation where $\tau$ denotes {\em both} the symbol and the corresponding transformation hoping that context will help. \renewcommand{\bb}[1]{{#1}} \subsection{Theorem \protect\ref{th-nc}: compressing the unit element} \label{subsec-compr} \begin{proofof}{Theorem \ref{th-nc} (ii)} $\xigwsc_H=\xhcs_H$ can be verified as follows. Suppose that ${\cal A}\in \xgwsc_H$. Put $V$ to be the unit element, $A$ the universe of ${\cal A}$. Since $V$ is a compressed \gunit, every weak space in $V$ has the same base, say $U$. Put $B=\{x\subseteq {}^\omega U : x\cap V\in A\}$. Clearly, ${\cal B}\xdf=\langle B,\cup,-,\xs_\tau,\xc_k\rangle_{\tau\in H, k\in \omega}$ is in $\xcs_H$ and the relativization of ${\cal B}$ with the set $V$ is a homomorphism from ${\cal B}$ to ${\cal A}$. This gives that ${\cal A}\in \xhcs_H$. We need to show that $\xigwsn_H=\xigwsc_H$. The $\xigwsn_H\supseteq \xigwsc_H$ part is obvious so it is left to check that $\xigwsn_H\subseteq\xigwsc_H$. Let ${\cal A}$ be an algebra from $\xgwsn_H$. The unit element $V$ of ${\cal A}$ is a normal \gunit\ therefore it is a disjoint union of weak spaces. Denote the set of weak spaces building $V$ by $\Lambda$. We put $U$ to be the union of the bases of elements of $\Lambda$. We define an accessibility relation $R$ on $\Lambda$ as: for any $\lambda_1,\lambda_2\in\Lambda$ $$\lambda_1 R \lambda_2\;\;\mbox{ iff }\;\; (\exists q\in \lambda_1)(\exists \sigma\in H)\;q \circ\bb\sigma\in \lambda_2.$$ It follows that $\lambda_1 R \lambda_2\Rightarrow \xbase(\lambda_1)=\xbase(\lambda_2)$. (Here we used that $V$ is a normal \gunit.) Let $R^*$ be the transitive, symmetric, reflexive closure of $R$. Clearly, $R^*$ is an equivalence relation. We have that $\lambda_1 R^* \lambda_2\Rightarrow \xbase(\lambda_1)=\xbase(\lambda_2)$. For each $\chi\in \Lambda/R^*$ we put $U_\chi$ to be $\xbase(\lambda)$ for some $\lambda\in \chi$, and we fix a function $f_\chi: U\rightarrow U_\chi$ that is the identity on $U_\chi$. Now we can map the sequences of $V$ into subsets of ${}^\omega U$ in a following way. For any $q\in \lambda\in \chi\in \Lambda/R^*$ $$m(q)\xdf=\{s\in {}^\omega U\mid f_\chi\circ s=q,\; s\approx q\}.$$ \begin{cl}{cll1} The statements below hold. For all $q,q',s\in V$ \begin{romanate} \item $m(q)$ and $m(q')$ are disjoint if $q$ and $q'$ are distinct. \item $s\in m(q)\Rightarrow s[i/u]\in m(q[i/f_\chi(u)])$ if $u\in U$. \item $s\in m(q)\Rightarrow s \circ \bb\sigma\in m(q \circ \bb\sigma)$ if $\sigma\in H$. \end{romanate} \end{cl} \begin{proof} (i): Suppose that $s\in m(q)\cap m(q')$. Then $q \approx s \approx q'$ so $q$ and $q'$ are in the same weak space of $V$, say in $\lambda$. Since $\lambda\in \chi$ for some $\chi\in \Lambda/R^*$ we infer that $q=f_\chi \circ s=q'$. (ii): Suppose that $s\in m(q)$, $q\in \lambda\in \chi\in \Lambda/R^*$. Since $q \approx q[i/f_\chi(u)]$ we have $q[i/f_\chi(u)]\in \lambda\in \chi$. Now $f_\chi \circ s[i/u]=q[i/f_\chi(u)]$, $s[i/u] \approx s \approx q \approx q[i/f_\chi(u)]$ shows that (ii) holds. (iii): Suppose that $s\in m(q)$, $q\in \lambda\in \chi\in \Lambda/R^*$. If $\lambda'$ is the weak space of $q \circ \bb\sigma$ then $\lambda R \lambda'$ and so $\lambda R^* \lambda'$, $\lambda'\in \chi$. We have $s \approx q$, $f_\chi \circ s=q$ and therefore $f_\chi \circ s \circ \bb\sigma=q \circ \bb\sigma$ and $s \circ \bb\sigma \approx q \circ \bb\sigma$ (we used that $\bb\sigma$ is bounded). \end{proof} We put $V^*=\displaystyle\bigcup_{q\in V}m(q)$. (ii) of the previous claim shows that $V^*$ is a compressed Cartesian space, (iii) gives that $\xs_\sigma(V^*)=V^*$ whenever $\sigma\in H$. \begin{cl}{cll2}The statements below hold. \begin{romanate} \item $\{s\in V^*\mid\exists u\in U\; s[i/u]\in m(q)\}= \displaystyle\bigcup_{q'\in \xci_i\{q\}}m(q')$. \item $\{s\in V^*\mid s \circ \bb\sigma\in m(q)\}= \displaystyle\bigcup_{q'\in \xsi_\sigma\{q\}}m(q')$. \end{romanate} \end{cl} \begin{proof} (i): If $s[i/u]\in m(q)$ then $s=s[i/u][i/s(i)] \stackrel{\ref{cll1}(ii)}\in m(q[i/f_\chi(s(i))])\subseteq \displaystyle\bigcup_{q'\in \xci_i\{q\}}m(q')$. On the other hand, if $s\in m(q')$ for some $q'\in \xc_i\{q\}$ then $s[i/q(i)] \stackrel{\ref{cll1}(ii)}\in m(q'[i/f_\chi(q(i))])=m(q)$ since $f_\chi(q(i))=q(i), q'[i/q(i)]=q$. (ii): If $s\in V^*, s \circ \bb\sigma\in m(q)$ then $s\in m(q')$ for some $q'\in V$. By Claim \ref{cll1} (iii), $s \circ \bb\sigma\in m(q \circ \bb\sigma)$. Claim \ref{cll1} (i) implies $m(q)\cap m(q' \circ \bb\sigma)\neq\emptyset\Rightarrow q' \circ \bb\sigma=q$. So $q'\in \xs_\sigma\{q\}$. On the other hand, if $s\in m(q')$ for some $q'\in \xs_\sigma\{q\}$ then $s \circ \bb\sigma\in m(q' \circ \bb\sigma)=m(q)$. \end{proof} We arrived to the point when the algebra in which ${\cal A}$ is embeddable and the representation function $\xrep$ can be defined: $${\cal A'}=\xp(V^*)\in\xgwsc_H, $$ $$\mbox{for any }a\in A,\;\;\;\xrep(a)=\bigcup_{q\in a}m(q).$$ Clearly, $\xrep$ is a Boolean embedding of ${\cal A}$ into ${\cal A'}$ since $m(q)$ is not empty ($q\in m(q)$), and $m(q)$ and $m(q')$ are disjoint when $q$ and $q'$ are distinct (see Claim \ref{cll1}(i)). To see that $\xrep$ preserves the extra Boolean operations we compute:\\ $\xc_i\xrep(a)= \xc_i\displaystyle\bigcup_{q\in a}m(q)= \bigcup_{q\in a}\xc_i m(q) \stackrel{\ref{cll2}(i)}= \bigcup_{q\in a}\bigcup_{q'\in \xci_i\{q\}}m(q')= \bigcup_{q'\in \xci_ia}m(q')= \xrep(\xc_ia)$.\\ $\xs_\sigma \xrep(a)= \xs_\sigma \displaystyle\bigcup_{q\in a}m(q)= \bigcup_{q\in a}\xs_\sigma m(q) \stackrel{\ref{cll2}(ii)}= \bigcup_{q\in a}\bigcup_{q'\in \xsi_\sigma \{q\}}m(q')= \displaystyle\bigcup_{q'\in \xsi_\sigma a}m(q')= \xrep(\xs_\sigma a)$. \end{proofof} Before proving Theorem \ref{th-nc} (iii) we state an important result. \begin{lm}{l-qb} Let $H$ be a set of quasi-bounded transformations, ${\cal A}$ be a $\xgws_H$, $\lambda_1$ and $\lambda_2$ be weak spaces of ${\cal A}$. If $ (\exists q\in \lambda_1)(\exists \sigma\in H)\;q \circ\bb\sigma\in \lambda_2$, then $\xbase(\lambda_1)\subseteq \xbase(\lambda_2)$. \end{lm} \begin{proof} Suppose that $u\in \xbase(\lambda_1)$, $q\in \lambda_1$, $\sigma\in H$, $|\bb\sigma^{-1}(\bb\sigma(k))|<\omega$ (there is a proper $k\in \omega$ while $\bb\sigma$ is quasi-bounded), $q \circ \bb\sigma\in \lambda_2$. Since $\lambda_1$ is a weak space, $q[\bb\sigma(k)/u]\in \lambda_1$. But then $\{i\in \omega\mid q[\bb\sigma(k)/u]\circ \bb\sigma(i)\neq q \circ \bb\sigma(i)\} \subseteq \bb\sigma^{-1}(\bb\sigma(k))$ is finite so $q[\bb\sigma(k)/u]\circ \bb\sigma \approx q \circ \bb\sigma\in \lambda_2$. The sequence $q[\bb\sigma(k)/u]\circ \bb\sigma$ of $\lambda_2$ takes the value $u$ at $k$ so $u\in \xbase(\lambda_2)$. \end{proof} \begin{proofof}{Theorem \ref{th-nc} (iii)} We need to show that under the conditions formulated in the theorem $\xgws_H\subseteq \xigwsn_H$. Let ${\cal A}$ be an algebra from $\xgws_H$. As we did in the proof of (ii) we put $V$ to be the unit element of ${\cal A}$, $\Lambda$ to be the set of weak spaces of ${\cal A}$, $R$ to be the accessibility relation on $\Lambda$, $R^*$ to be the equivalence relation generated by $R$. We show that $\lambda R \lambda_0\Rightarrow \xbase(\lambda)=\xbase(\lambda_0)$ (and so $\lambda R^*\lambda_0\Rightarrow\xbase(\lambda)=\xbase(\lambda_0)$). Suppose that $\lambda R\lambda_0$. Then $(\exists q\in \lambda)(\exists \sigma_0\in H)\; q\circ\bb{\sigma_0}\in\lambda_0$. We know that $\bb{\sigma_0}$ has a quasi-inverse in $[\bb H]$, say $\bb{\sigma_1} \circ \ldots \circ \bb{\sigma_n}$. For any $i\in n+1$ we put $\lambda_i$ to be the weak space of $q\circ\bb{\sigma_0}\circ\ldots\circ\bb{\sigma_i}$. Lemma \ref{l-qb} implies that $\xbase(\lambda_i)\subseteq \xbase(\lambda_{i+1})$ ($i\in n$). If we note that $\bb{\sigma_0}\circ\bb{\sigma_1}\circ\ldots\circ\bb{\sigma_n}\approx \xid$, and so $\lambda=\lambda_n$ then we have $\xbase(\lambda)\subseteq \xbase(\lambda_0)\subseteq \xbase(\lambda_1)\subseteq \ldots\subseteq \xbase(\lambda_n)=\xbase(\lambda)$. Now we can define the set $U_\chi$ to be $\xbase(\lambda)$ for some $\lambda\in \chi\in\Lambda/R^*$. Surely, the definition is independent from the choice of $\lambda$. We put $f_\chi: U_\chi\rightarrow U_\chi\times\{\chi\}$ to be the natural embedding ($f_\chi(u)=\langle u,\chi\rangle $), and $\chi:V\rightarrow \Lambda/R^*$ to be the function that associates the $R^*$ class of the weak space of $q$ to a $q\in V$. We define \begin{center} $\mbox{for any }a\in A,\;\;\;\xrep(a)=\{f_{\chi(q)} \circ q\mid q\in a\}$\\ $A'=\{\xrep(a)\mid a\in A\}$\\ ${\cal A'}=\langle A',\cup,-,\xs_\tau,\xc_k \rangle_{\tau\in H, k\in \omega}$ \end{center} It is straightforward to verify that ${\cal A'}\in \xgwsn_H$ and $\xrep$ is an isomorphism between ${\cal A}$ and ${\cal A'}$. \end{proofof} \subsection{Quasi-axiomatizing $\xics_H$} \label{subsec-prcsg} To find a proof to Theorem \ref{cj1}, we examine the situation described in Example \ref{ex1}. The key idea is that the presence of a constant sequence can be captured by a quasi-equation. Among those $\xgws_G$'s that have constant sequences in their universes, the simplest in structure are the ones with unit elements of the form $\mbox{}^\omega U^{(q)}$ for some set $U$ and constant sequence $q$. A unit element of this form will be called {\em horizontal}. (It is easy to see that $\xs_\tau(\mbox{}^\omega U^{(q)})= \mbox{}^\omega U^{(q)}$.) Any algebra from $\xgws_H$ that has a constant sequence $q$ in it's universe can be homomorphically mapped into a $\xgws_H$ with horizontal unit element. (Indeed, the relativization with $\mbox{}^\omega U^{(q)}$ --- the function that maps the element $x$ of the algebra into $x\cap \mbox{}^\omega U^{(q)}$ --- will be a satisfactory homomorphism.) So any $\xgws_H$ that is isomorphic to a $\xcs_H$ has a homomorphism into some $\xgws_H$ with horizontal unit element. The next theorem states that this requirement is not only necessary but also sufficient to force a $\xgws_H$ to be isomorphic to a $H$--cylindric set algebra. %We state this result not only for the %specific set $G$, but for an arbitrary set $H$ of %transformations of $\omega$. \begin{theo}{th-csg} Let $H$ be an arbitrary subset of ${}^\omega\omega$ with the property that for any $\sigma\in H$, $\sigma$ is bounded and has a right quasi-inverse in ${}^\omega\omega$. Then any algebra ${\cal A}\in \xgws_H$, that has a homomorphism into some $\xgws_H$ with horizontal unit element, is isomorphic to a $H$--cylindric set algebra. That is, $$(\exists \mbox{ set }U)(\exists u_0\in U)(\exists h:{\cal A}\rightarrow \xp({}^\omega U^{(\langle u_0,u_0,\ldots\rangle )})) \Rightarrow {\cal A}\in \xics_H.$$ \end{theo} Before the proof of the Theorem above we present an important lemma. \begin{lm}{lm-d->s} Suppose $U$ is a set, $u_0\in U$. There is a cardinal $\kappa$ for that if $\xp(W')$ is a full compressed $H$--cylindric set algebra with base $U'$ of cardinality bigger than $\kappa$ then there is a homomorphism $h':\xp({}^\omega U^{(\langle u_0,u_0,\ldots\rangle )}) \rightarrow \xp(W')$. \end{lm} \begin{proof} Let $\kappa$ be a cardinal bigger than $\omega$, the cardinality of $U$ and that of $H$. For the algebra $\xp(W')$, we define the set $\Lambda$ of weak spaces, the accessibility relations $R$ and $R^*$ on $\Lambda$ as we defined in the proof of Theorem \ref{th-nc} (ii). For each weak space $\lambda\in \Lambda$ we fix a sequence $q_\lambda$ in $\lambda$. We put $U_\chi'$ ($\chi\in \Lambda/R^*$) to be the set $\{q_\lambda(i)\mid \lambda\in \chi, i\in \omega\}$. \begin{cl}{cl-card} The cardinality of $|U_\chi'|+|U|$ is less than $\kappa$. \end{cl} \begin{proof} For a given $\lambda_1\in \Lambda$ and $\sigma\in H$ there is exactly one $\lambda_2\in \Lambda$ with $\lambda_1 R \lambda_2$. This can verified by noting that from $q \circ \bb\sigma\in \lambda_2$, $ q\in \lambda_1$ we can infer $q' \circ \bb\sigma\in \lambda_2$ when $q'\in \lambda_1$ ($\bb\sigma$ is bounded so $q \approx q'\Rightarrow q \circ \bb\sigma \approx q' \circ \bb\sigma$ and $q \circ \bb\sigma\in \lambda_2\cap\lambda_2' \Rightarrow \lambda_2=\lambda_2'$). For any $\sigma\in H$, $\bb\sigma$ is right quasi-invertible in ${}^\omega\omega$ so there is a transformation $f_\sigma\in {}^\omega\omega$ with $\bb\sigma \circ f_\sigma \approx\xid$. Suppose for contradiction that there is a $k\in \omega$ for that $|f_\sigma^{-1}(k)|=\omega$. Then the transformation $\bb\sigma \circ f_\sigma$ takes the value $\bb\sigma(k)$ on any coordinate of the infinite set $f_\sigma^{-1}(k)$. But this is impossible since $\bb\sigma \circ f_\sigma$ takes the value $i$ on coordinate $i$ for all but finitely many $i\in \omega$. This reasoning shows that $f_\sigma$ is bounded. For a given $\lambda_2\in \Lambda$ and $\sigma\in H$ there is exactly one $\lambda_1\in \Lambda$ with $\lambda_1 R \lambda_2$. Suppose that $\lambda_1,\lambda_1' \in \Lambda$, $q\in \lambda_1$, $q'\in \lambda_1'$ and $q \circ \bb\sigma\in \lambda_2\ni q' \circ \bb\sigma$. Then $q \circ \bb\sigma \approx q' \circ \bb\sigma$ and $q \circ \bb\sigma \circ f_\sigma \approx q' \circ \bb\sigma \circ f_\sigma$ since $f_\sigma$ is bounded. But this implies that $q \approx q \circ \bb\sigma \circ f_\sigma \approx q' \circ \bb\sigma \circ f_\sigma \approx q'$, $q\in \lambda_1\cap\lambda_1'$ so $\lambda_1=\lambda_1'$. For a given $\lambda\in \Lambda$, $|\{\lambda'\in \Lambda\mid \lambda R\lambda' \mbox{ or }\lambda' R\lambda\}|\leq 2\cdot|H|$. For a given $\lambda\in \Lambda$, we have that $\lambda'\in \Lambda$ and $\lambda$ sit in the same $R^*$ class if and only if there is a finite series $\lambda_0, \ldots \lambda_n$ of weak spaces with $\lambda_0=\lambda$, $\lambda_n=\lambda'$ and $i\in n \Rightarrow (\lambda_i R \lambda_{i+1} \mbox{ or }\lambda_{i+1} R \lambda_i)$. Therefore, the size of a $R^*$ class is less than $1+2\cdot|H|+(2\cdot|H|)^2+\ldots\leq \omega\cdot|H|$. Finally, $|U_\chi'|\leq \omega\cdot|\chi|\leq\omega\cdot\omega\cdot|H|= \omega\cdot|H|$, $|U_\chi'|+|U|<\kappa$. \end{proof} Let $f_\chi$ $(\chi\in \Lambda/R^*)$ be any function mapping $U'$ onto $U$ with the property $$(\forall i\in \omega)(\forall \lambda\in \chi)\;\; f_\chi(q_\lambda(i))=u_0.$$ Such an $f_\chi$ exists since not more than $|U_\chi'|$-many elements of $U'$ are to be mapped on $u_0$ so there are enough elements left to cover the set $U-\{u_0\}$. With the help of $f_\chi$, for each sequence $q$ of ${}^\omega U^{(\langle u_0,u_0,\ldots\rangle )}$ a subset of $W'$ can be associated. $$m(q)=\{s\in W'\mid f_\chi\circ s =q, s\in \lambda\in \chi\in \Lambda/R^*\}.$$ As it was presented in the more complicated situation in the proof of Theorem \ref{th-nc} (ii) the function $h'(a)=\displaystyle\bigcup_{q\in a}m(q)$ is a homomorphism. (Claims \ref{cll1} and \ref{cll2} hold here as well since the original proofs can be adapted to the present situation. ) \end{proof} \begin{proofof}{Theorem \ref{th-csg}} In Theorem \ref{th-nc} (ii) and (iii) $\xigws_H=\xigwsc_H$ was proved under the conditions that for any $\sigma\in H$, $\bb\sigma$ is quasi-bounded and it has a quasi-inverse in $[\bb H]$. This holds in our situation so we may assume that ${\cal A}\in \xgwsc_H$. The unit element of ${\cal A}$ is $V\subseteq {}^\omega U^*$ for some set $U^*$. Let $U'$ be a set with cardinality bigger than the cardinality of $U^*$ and the cardinal that corresponds to the set $U$ according to Lemma \ref{lm-d->s}. Let $f$ be a function mapping $U'$ onto $U^*$. With the help of $f$, for each sequence $q$ of ${}^\omega U^*$ a subset of ${}^\omega U'$ can be associated. $$m(q)=\{s\in {}^\omega U'\mid f \circ s=q\}.$$ Let $V'=\displaystyle\bigcup_{q\in V}m(q)$. As it was presented in the proof of Theorem \ref{th-nc} (ii) the function $r_1:{\cal A}\rightarrow \xp(V'),\;\;\; r_1(a)=\displaystyle\bigcup_{q\in a}m(q)$ is an embedding. Let $W'={}^\omega U' \setminus V'$. Just like $V'$, $W'$ is a \gunit\ and $\xs_\sigma(W')=W'$ for any $\sigma\in H$. So $W'$ can be a unit element of a $\xgwsc_H$. According to Lemma \ref{lm-d->s} there is a homomorphism $h'$ mapping $\xp({}^\omega U^{(\langle u_0,u_0,\ldots\rangle )})$ into $\xp(W')$. Let $r_2$ be the composition of the homomorphisms $h'$ and $h$ ($r_2=h'\circ h$) mapping ${\cal A}$ into $\xp(W')$. Since $\xp({}^\omega U')=\xp(V')\times\xp(W')$ the function $\xrep$ defined as $\xrep(a)=r_1(a)\cup r_2(a)$ is an embedding and it demonstrates that ${\cal A}\in \xics_H$. \end{proofof} In the second part of this subsection we show that if an algebra in $\xgws_H$ satisfies $\xqx$ then it has a homomorphism to $\xgws_H$ with horizontal unit element. We assume that $H$ satisfies the assumption stated in Theorem \ref{t-csax}. \begin{lm}{ll1} If ${\cal A}\in \xgws_H$ and ${\cal A}\models\xqx$ then there is an ultrafilter $U$ of ${\cal A}$ with the property that $-\xc_{(\Gamma)}x\in U$ holds whenever $x\cap\xs_\tau x=0$ for some $\Gamma\subseteq_\omega\omega$ $\tau\in [H]$ with $\megsz{\tau}{\Gamma}=\megsz\xid\Gamma$. \end{lm} \begin{cl}{clll1} $\forall\sigma,\tau_1,\ldots,\tau_n\in [H]\; \exists\sigma',\tau_1',\ldots,\tau_n'\in [H]: \displaystyle\bigwedge_{i\leq n}\sigma'\circ\tau_i=\tau_i'\circ\sigma$. Furthermore, if $\megsz{\sigma}{\Gamma}=\megsz{\tau_1}{\Gamma}= \cdots=\megsz{\tau_n}{\Gamma}=\megsz\xid\Gamma$ then the same holds to $\sigma',\tau_1',\ldots,\tau_n'\; (\Gamma\subseteq_\omega\omega)$. \end{cl} \begin{proof} We prove by induction. If $n=0$ then $\sigma'=\sigma$. Suppose that the statement holds for $n-1$. Let $\sigma'',\tau_1'',\ldots,\tau_{n-1}''$ be associated to $\sigma,\tau_1,\ldots,\tau_{n-1}$. Let $\sigma^*$ and $\tau_n^*$ be the left quasi-inverse of $\sigma''\circ \tau_n$ and $\sigma$ respectively. Since $[H]$ contains all finite transformations we can assume that $\sigma^*\circ\sigma''\circ\tau_n(k)= \left\{\begin{array}{ll} k&\in\Gamma\\ 0&k\in m_0-\Gamma\\ k&m_0\leq k \end{array}\right\}=\tau_n'\circ\sigma(k)$ for some $m_0\in \omega$. Setting $\sigma'=\sigma^*\circ\sigma''$, $\tau_i'=\sigma^*\circ\tau_i''$ $(i=1,\ldots, n)$ gives the required result. \end{proof} \begin{proofof}{Lemma \ref{ll1}} Let $B^*=\{-\xc_{(\Gamma)}x: \Gamma\subseteq_\omega\omega, \exists K\subseteq_\omega [H]\;( \tau\in K\rightarrow \megsz\tau \Gamma=\megsz\xid\Gamma), \displaystyle\bigcap_{\tau\in K}\xs_\tau x=0\}$. $\xqx$ states that $B^*$ has the finite intersection property. We put $B$ to be $B^*$'s filter closure, that is, $B=\{y\in {\cal A}\;:\; \exists X\subseteq_\omega B^* \; y\geq\bigcap X\}$. \begin{cl}{clll2} $B$ is closed under $\xs_\nu$ for all $\nu\in [H]$. \end{cl} \begin{proof} Suppose $-\xc_{(\Gamma)}x\in B^*$, $\displaystyle\bigcap_{\tau\in K}\xs_\tau x=0$ for some $\Gamma\subseteq_\omega\omega, K\subseteq_\omega[H]$, $\tau\in K\rightarrow \megsz\tau \Gamma=\megsz\xid\Gamma$. Let $\Gamma'=\{i\in \omega-\Gamma: \nu(i)\in\Gamma, \forall j\in i-\Gamma\;(\nu(i)\neq\nu(j))\}$. $\nu$ is bounded so $\Gamma'$ is finite. If $\Gamma'=\{\gamma_1,\ldots,\gamma_n\}$ then let $\nu_0=\xpe{\gamma_1}{\nu(\gamma_1)} \circ\ldots\circ\xpe{\gamma_n}{\nu(\gamma_n)}$. Let $\Gamma''=\Gamma'\cup(\Gamma-\{\nu(\gamma): \gamma\in\Gamma'\})$, $\nu_1=(\nu_0\circ\nu)[\Gamma/\xid]$. Now we have that $\megsz{\nu_0\circ\nu_1}{\omega-\Gamma}= \megsz{\nu}{\omega-\Gamma}$ and for all $i\in\Gamma$ $\nu_1^{-1}(i)=\{i\}$. Using Claim \ref{clll1}, we pick corresponding transformations $\nu_1'$ and $\tau'$ to $\nu$ and $\tau$ ($\tau\in K$). Then $0=\xs_{\nu_0}\xs_{\nu_1'} \displaystyle\bigcap_{\tau\in K}\xs_\tau x= \bigcap_{\tau\in K}\xs_{\nu_0}\xs_{\nu_1'}\xs_\tau x= \bigcap_{\tau\in K}\xs_{\nu_0}\xs_{\tau'}\xs_{\nu_1} x= \bigcap_{\tau\in K}\xs_{\nu_0\circ\tau'\circ\nu_0} \xs_{\nu_0}\xs_{\nu_1} x$. Noting that $\megsz{\nu_0\circ\tau'\circ\nu_0}{\Gamma''}= \megsz\xid{\Gamma''}$ we have $-\xc_{(\Gamma'')}\xs_{\nu_0}\xs_{\nu_1} x\in B^*$. So $-\xc_{(\Gamma'')}\xs_{\nu_0}\xs_{\nu_1}x \stackrel{*6}= -\xs_{\nu_0}\xc_{(\Gamma)}\xs_{\nu_1}x \stackrel{*6}= -\xs_{\nu_0}\xs_{\nu_1}\xc_{(\Gamma)}x \stackrel{*5}= -\xs_\nu\xc_{(\Gamma)}x= \xs_\nu(-\xc_{(\Gamma)}x)$ gives $\xs_\nu(-\xc_{(\Gamma)}x)\in B^*$. Finally, suppose that $x\in B$. Then there are $x_1,\ldots ,x_n\in B^*$ with $x\geq\displaystyle\bigcap_1^n x_i$. So $\xs_\nu x\geq\xs_\nu\displaystyle\bigcap_1^n x_i= \bigcap_1^n \xs_\nu x_i\in B$ giving $\xs_\nu x\in B$. \end{proof} Let $U$ be a maximal filter extending $B$ with the property that it is closed under $\xs_\nu$ for all $\nu\in[H]$. We can use Zorn's lemma to construct such a filter. We show that $U$ is indeed an ultrafilter. Suppose not. Then there is a $y$ such that neither $y$ nor $-y$ is in $U$. $y$ cannot be added to $U$ so there are $z\in U$, $K\subseteq_\omega[H]$ such that $z\cap\displaystyle\bigcap_{\tau\in K}\xs_\tau y=0$. Then $0=z\cap\displaystyle\bigcap_{\tau\in K}\xs_\tau y \supseteq \bigcap_{\tau\in K}\xs_\tau (z\cap y)$ giving $-(y\cap z)\in B$. Similarly, $-(-y\cap z')\in B$. Therefore $U\ni -(-y\cap z')\cap-(y\cap z)=-((y\cup z')\cap (z\cup z')\cap(z\cup-y))$. But all the three terms in the last expression are in $U$ so their intersection is in $U$ giving that $U$ contains an element and its complement. \end{proofof} Our algebra ${\cal A}\in\xgws_H$ is a {\em normal Boolean algebra with operators}. (Cf.\ e.g.\ \cite{hmti} Definition 2.7.1.) We can define its {\em canonical embedding algebra} or {\em ultrafilter extension} ${\cal A^*}$ as follows (see Definition 2.7.4.\ in \cite{hmti}). Let $V$ be the set of ultrafilters of ${\cal A}$. If $O$ is any of the operators $\{\xs_\tau:\tau\in H\}\cup \{\xc_i:i\in \omega\}$ and $X\subseteq V$ then we define $$OX=\{U\in V: (\exists S\in X)(\forall x\in U)\; Ox\in S\}.$$ Then ${\cal A^*}$ is $\langle{\cal P}(V),\cup,-,\xs_\tau, \xc_i\rangle_{\tau\in H,i\in\omega}$. As stated in Corollary \ref{cr-*171}, $\xigwsn_H$ is axiomatized by (*1)--(*7) (defined in Definition \ref{d-*17}) together with the definition of $\xc_i$ ($i\in\omega$). All that axioms but $\xc_i(-\xc_ix)=-\xc_ix$ and $\xs_\sigma(-x)=-\xs_\sigma x$ are positive, that is, they do not contain any occurance of the symbol $-$ for complementation. But the two exceptions are equivalent (in the presence of the others) with some positive formulas: \begin{eqnarray*} \xc_i(-\xc_ix)=-\xc_ix&\mbox{ iff } & \xc_i 0=0, \xc_i(x\wedge\xc_iy)=\xc_ix\wedge\xc_iy\\ \xs_\sigma(-x)=-\xs_\sigma x&\mbox{ iff } & \xs_\sigma(x\wedge y)=\xs_\sigma x\wedge \xs_\sigma y. \end{eqnarray*} Since positive equations valid in a Boolean algebra with operators still hold in the ultrafilter extension of the algebra, (see e.g.\ \cite{hmti} Remark 2.7.15) we can conclude that the ultrafilter extension ${\cal A^*}$ of ${\cal A}\in \xgwsn_H$ is in $\xgwsn_H$. Furthermore, under the hypothesis of Theorem \ref{t-csax}, $\xigws_H=\xigwsn_H$ holds, so the conclusion stated above holds to the class $\xgws_H$ as well. Finally, we note that every Boolean algebra with operators is embeddable into its ultrafilter extension. (The map that associates $\{U\in V:x\in U\}$ to an element $x$ in ${\cal A}$ will suffice.) \begin{lm}{ll2} If ${\cal A}\in \xgws_H$ and ${\cal A^*}$ is its ultrafilter extension then the atom $a=\{U\}$ has the property $x\cap\xc_{(\Gamma)}a\subseteq\xs_\tau x$ $(\Gamma\subseteq_\omega\omega, \tau\in[H], \megsz{\tau}{\Gamma}= \megsz{\xid}{\Gamma}, x\in{\cal A^*})$ provided that $U$ is an ultrafilter of ${\cal A}$ that satisfies the property stated in Lemma \ref{ll1}. \end{lm} \begin{proof} It is enough to show that the condition $x\cap\xc_{(\Gamma)}a\subseteq\xs_\tau x$ holds for all atoms of ${\cal A^*}$. Suppose $x=\{F\}$. If $F\not\in \xc_{(\Gamma)}a$ then there is nothing to show. If $F\in \xc_{(\Gamma)}a$ then $\forall y\in F\;\xc_{(\Gamma)}y\in U$. Suppose for contradiction that $x\not\subseteq\xs_\tau x$, that is, $\exists y\in F\; \xs_\tau y\not\in F$. Then $-\xs_\tau y\in F$, $w=y\cap{-\xs_\tau y}\in F$. We can conclude that $\xc_{(\Gamma)}w\in U$. On the other hand, $w\cap\xs_\tau w=0$ gives $-\xc_{(\Gamma)}w\in U$ and that is a contradiction. \end{proof} \begin{lm}{ll3} If ${\cal A^*}\in \xgwsc_H$ and ${\cal A^*}$ has an atom $a$ with $x\cap\xc_{(\Gamma)}a\subseteq\xs_\tau x$ whenever $\Gamma\subseteq_\omega\omega, \tau\in[H], \megsz{\tau}{\Gamma}= \megsz{\xid}{\Gamma}, x\in{\cal A^*}$ then ${\cal A^*}$ has a homomorphism to a $\xgws_H$ with horizontal unit element. \end{lm} \begin{proof} We denote the base of ${\cal A^*}$ by $U'$ and the universe of ${\cal A^*}$ by $A^*$. Let $q$ be a sequence in $a$, $V=\{q\circ\tau:\tau\in[H]\}$, $V^*=\displaystyle\bigcup_{m\in\omega}\xc_{(m)}V$. Put $U_0$ to be the range of $q$. Fix an arbitrary element $u\in U_0$. Denote $U'-U_0\cup\{u\}$ by $U$. Let $f$ be the function that is the identity on $U'-U_0$ and the constant $u$ on $U_0$. \begin{cl}{clll3} $x\in A^*, s,s'\in V^*, s\in x, f\circ s=f\circ s' \rightarrow s'\in x$. \end{cl} \begin{proof} Let $\Gamma=\{i\in \omega:s(i)\not\in U_0\}$. Since $s\approx q\circ\tau$ for some $\tau\in[H]$, $\Gamma$ is finite. Clearly, $\Gamma=\{i\in \omega:s'(i)\not\in U_0\}$ so $\megsz s\Gamma=\megsz{s'}\Gamma$. We have that $s'\approx q\circ\tau'$ for some $\tau'\in[H]$. $s=q\circ\tau[\Gamma/s]$, $s'=q\circ\tau'[\Gamma/s]$. Let $\nu$ and $\nu'$ be the right quasi-inverses of $\tau$ and $\tau'$. Since all the finite transformations are in $[H]$, we can choose $\nu$ and $\nu'$ that they satisfy the following additional properties: $\megsz\nu\Gamma=\megsz{\nu'}\Gamma=\megsz\xid\Gamma$, $\megsz{\tau\circ\nu}{\omega-\Gamma}= \megsz{\tau'\circ\nu'}{\omega-\Gamma}$. Then $s\circ\nu=(q\circ\tau[\Gamma/s])\circ\nu= q\circ\tau\circ\nu[\Gamma/s]= q\circ\tau'\circ\nu'[\Gamma/s]= (q\circ\tau'[\Gamma/s])\circ\nu'=s'\circ\nu'$. Since $s\in x\cap\xc_{(\Gamma)}a\subseteq\xs_\nu x$, we get that $s'\circ\nu'=s\circ\nu\in x$. (We used that $a\subseteq\xs_\tau a$ and so $q\circ\tau\in a$.) If we suppose for contradiction that $s'\not\in x$ then $s'\in-x\cap\xc_{(\Gamma)}a\subseteq\xs_{\nu'}-x$ and so $s'\circ\nu'\in-x$ but that cannot be the case. \end{proof} Now we can define a homomorphism that maps ${\cal A}$ into $\xp({}^\omega U^{(\langle u,u,\ldots\rangle)})$: $$h(x)=\{f\circ s : s\in x\cap V^*\}.$$ It is straightforward to verify that $h$ preserves $\cap$, while Claim \ref{clll3} proves that it preserves complementation. The following two claims prove that $h$ preserves the extra Boolean operations. \begin{cl}{clll4} $\xc_ih(x)=h(\xc_ix)$. \end{cl} \begin{proof} $r\in \xc_ih(x)\Rightarrow r=(f\circ s)[i/r(i)]$ for some $s\in x$. But $r=(f\circ s)[i/r(i)]=f\circ( s[i/r(i)]) \in h(\xc_ix)$ since $s[i/r(i)]\in\xc_ix$. On the other hand, $r\in h(\xc_ix)\Rightarrow r=f\circ s$ for some $s\in \xc_ix$. So there is $s'\in x$ with $s'[i/s(i)]=s$. But $r=f\circ s= f\circ(s'[i/s(i)])= (f\circ s')[i/f(s(i))])\in\xc_ih(x)$ \end{proof} % \begin{cl}{clll5} $\xs_\tau h(x)=h(\xs_\tau x)$. \end{cl} \begin{proof} $r\in \xs_\tau h(x) \Leftrightarrow r\circ\tau\in h(x) \Leftrightarrow \exists s'\in x\; f\circ s'=r\circ\tau$. $r=f\circ s$ for some $s\in V^*$ so $f\circ s'=r\circ\tau=f\circ s\circ\tau$. Using Claim \ref{clll3} we have that $s'\in x\Leftrightarrow s\circ\tau\in x$. But $s\circ\tau\in x\Leftrightarrow s\in\xs_\tau x\Leftrightarrow r=f\circ s\in h(\xs_\tau x)$ completes the proof. \end{proof} \end{proof} Summarizing the results of this subsection, we prove Theorem \ref{t-csax}. \begin{proofof}{Theorem \ref{t-csax}} Suppose that the algebra ${\cal A}$ is a model of $\xqx\cup\xeq(\xigws_H)$. Lemmas \ref{ll1} and \ref{ll2} state that the ultrafilter extension ${\cal A^*}$ of ${\cal A}$ has an atom with certain properties. Since the ultrafilter extension satisfies all the positive equations valid in the algebra, we have that ${\cal A^*}\models\xeq(\xigws_H)$. Using Theorem \ref{th-nc} we conclude that ${\cal A^*}$ is isomorphic to an algebra ${\cal B}\in \xgwsc_H$. Lemma \ref{ll3} implies that ${\cal B}$ has a homomorphism to a $\xgws_H$ with horizontal unit element. Since ${\cal A}$ is embeddable into its ultrafilter extension and, in that way, into ${\cal B}$, ${\cal A}$ also has a homomorphism to a $\xgws_H$ with horizontal unit element. Finally, Theorem \ref{th-csg} states that the above mentioned result is sufficient to show that ${\cal A}\in \xics_H$. \end{proofof} \subsection{Theorem \protect\ref{t-gen=}: the cylindric reduct of $\xmod(H1,H2)$} \label{subsec-prrca} The proof will have the following structure. Any model of H1 is actually an extension of a model of $\xeq{\xgwsn_{\bar H}}$. But Theorem \ref{th-nc} (i) imply that a model of $\xeq{\xgwsn_{\bar H}}$ is isomorphic to a $\xgwsn_{\bar H}$ We will examine the extra abstract constant $\xd 01$. (In the presence of the substitutions the other $\xd ij$'s are term definable so it is enough to concentrate on $\xd 01$.) Finally, the proper behaviour of $\xd 01$ will lead us to a representation function that proves our theorem. Recall from Notation \ref{nt-approx} that if $q_1$ are $q_2$ sequences then $q_1\approx q_2$ indicates that they agree on all but finitely many coordinates. \begin{nt}{nt-stau} Let $H$ be a set of transformations of $\omega$. Suppose that $\tau=\langle \sigma_1\ldots\sigma_n\rangle\in H^*$. We introduce the notation $\xs_\tau x$ for the term $\xs_{\sigma_1}\ldots\xs_{\sigma_n}x$. \end{nt} \begin{rmk}{rm-H4} Let $H$ be a set of transformations of $\omega$ with the property that $[\bar{\bb H}]$ is rich. (Recall that $[\bar{\bb H}]$ is the subsemigroup of $\langle {}^\omega\omega,\circ\rangle $ generated by $H\cup \{\xre ij\mid i,j \in \omega\}$.) In the definition of a rich semigroup the existence of two special elements $\hat s$ and $\hat p$ were stated. We fix two elements of $[\bar{\bb H}]$ with the required property and denote them by $\hat s$ and $\hat p$. We also fix $\xs_{\hat s}$ and $\xs_{\hat p}$ to stand for the terms $\xs_{\tau_1}$ and $\xs_{\tau_2}$ respectively where $\bb\tau_1=\hat s$, $\bb\tau_2=\hat p$, and $\tau_1, \tau_2\in {\bar H}^*$. It is provable from H1 that for any choice of $\tau_1\in {\bar H}^*$ with $\bb\tau_1=\hat s$, $\xs_{\tau_1}$ is the same operation of the algebra so $\xs_{\hat s}$ (and similarly $\xs_{\hat p}$) is well defined. $\hat s(i)\neq \hat s(j)$ if $i\neq j$ since $\hat p \circ \hat s=\xid$. There is a permutation $f$ of $\omega$ that takes $\hat s(0)$ to 0 and $\hat s(1)$ to 1 and fixes all the elements of $\omega-\{0,1,\hat s(0),\hat s(1)\}$. ($f$ is one of $\xbpe{0}{\hat s(0)}\circ\xbpe{1}{\hat s(1)}$, $\xbpe{1}{\hat s(1)}\circ\xbpe{0}{\hat s(0)}$ or $\xbpe01$ depending on whether any of $\hat s(0)=0$, $\hat s(0)=1$, $\hat s(1)=0$ or $\hat s(1)=1$ hold.) Since $f$ is finite $f\in [\bar{\bb H}]$. So there is a $\tau_H\in \bar H^*$ for that $\bb\tau_H=f$. We formalize a set of equations that are all consequences of H1,H2. \begin{eqsymbol}{H4} \begin{array}{rcl} \xsre 01x &=& \xc_0(\xd 01\wedge x),\\ \xsre 10x &=& \xc_1(\xd 01\wedge x),\\ \xc_i \xd 01 &=& \xd 01 \;\;\;\mbox{whenever $i\geq 2$},\\ \xspe 01\xd 01 &=& \xd 01,\\ \xs_{\tau_H}\xs_{\hat s}\xd01 &=& \xd 01. \end{array} \end{eqsymbol} \noindent Here $\xspe ijx$ stands for the term $\xs_\tau x$ where $\tau\in {\bar H}^*$ and $\bb\tau=\xbpe ij$. Since $[\bar{\bb H}]$ is rich, all the finite transformations (including $\xbpe ij$) belong to $[\bar{\bb H}]$. \end{rmk} \begin{lm}{lm-2} Let $H$ be a set of transformations of $\omega$ with the property that $[\bar{\bb H}]$ is rich. Suppose that ${\cal A}$ is a $\xgws_{\bar H}$ extended with the abstract\footnote{Here the adjective ``abstract'' means that this constant is NOT necessarily the set theoretically definable diagonal element, but any constant that satisfies the required equations. It will be shown that this ``abstract'' constant need to have a nice structure similar to that of the set theoretic diagonal element.} constant $\xd 01$ that satisfies {\rm H4}. If $x$ is an element of ${\cal A}$ and $\langle u_0, u_1, u_2, \ldots \rangle$ is a sequence from the universe of ${\cal A}$ then $\langle u_0, u_1, u_2, \ldots \rangle \in \xd 01\wedge x$ implies $\begin{array}[t]{ccc} \langle u_0, u_0, u_2, \ldots \rangle&\in& x,\\ \langle u_1, u_0, u_2, \ldots \rangle&\in& x,\\ \langle u_1, u_1, u_2, \ldots \rangle&\in& x. \end{array}$ \end{lm} \begin{proof} Suppose that $\langle u_0, u_1, u_2, \ldots \rangle $ satisfies the premise of the lemma. Then $\langle u_0, u_1, u_2, \ldots \rangle\in \xc_0(\xd01\wedge x) \stackrel{H4}= \xsre 01x$. This implies $\langle u_0, u_1, u_2, \ldots \rangle \circ \xbre 01= \langle u_1, u_1, u_2, \ldots \rangle \in x$. Using $\xsre 10x \stackrel{H4}= \xc_1(\xd 01\wedge x)$ we can get $\langle u_0, u_0, u_2, \ldots \rangle\in x $. $\xspe 01\xd 01 \stackrel{H4}= \xd 01$ implies $\langle u_1, u_0,u_2, \ldots \rangle \in \xd 01$. If we suppose for contradiction that $\langle u_1, u_0, u_2, \ldots \rangle \not\in x$ then $\langle u_1, u_0, u_2, \ldots \rangle \in -x$ and according to the previous observation we can conclude that $\langle u_1, u_1, u_2, \ldots \rangle \in -x$ and that is impossible. \end{proof} \begin{lm}{lm-3} Let $H, {\cal A}$ and $\xd 01$ be as in Lemma \ref{lm-2}. If $u$ and $v$ are the first two elements of a sequence $q$ of $\xd01$ then any sequence $r$ of an arbitrary $x\in A$ can be modified in any of its positions from $u$ to $v$ provided that $q$ and $r$ are in the same weak space. In other words, if $q\in \xd 01$, $r\in x$ for some $x\in A$, $q \approx r$, $r(k)=q(0)=u$ for some $k\in \omega$ and $q(1)=v$ then $r[k/v]\in x$. \end{lm} \begin{proof} First suppose that $k\neq 1$. Let $q^*=(r\circ\xbpe 0k)[1/v]$. Clearly, $q^*$ is in the weak space of $q$ (and of $r$). Therefore, $q^*\in\xc_{i_1}\ldots\xc_{i_n}\xd 01$ where $\Gamma=\{i_1,\ldots i_n\}$ is the set where $q$ and $q^*$ do not agree (it is finite). Now $q^*(0)=(r \circ \xbpe 0k)(0)=r(k)=u$ and $q^*(1)=v$ so $0,1 \not\in \Gamma$ and $\xc_i\xd 01 \stackrel{H4}= \xd 01$ whenever $i\geq 2$. We can conclude that $q^* \in \xd 01$. We put $z$ to be an element of $\omega-\xrng(\hat s)$. $[\bar{\bb H}]$ is rich so $\omega-\xrng(\hat s)$ is not empty. $(q^*\circ \hat p)[z/r(1)]\circ \hat s=q^*\in \xd01$ implies that $(q^*\circ \hat p)[z/r(1)]\in \xs_{\hat s}\xd01$. $(q^*\circ \hat p)[z/v][\hat s(1)/r(1)]\circ \hat s= r \circ \xbpe0k\in \xspe0kx$, $(q^*\circ \hat p)[z/v][\hat s(1)/r(1)]\in\xs_{\hat s}\xspe0kx$. Furthermore, $(q^*\circ \hat p)[z/r(1)]= (q^*\circ \hat p)[z/v][\hat s(1)/r(1)]\circ \xbpe{z}{\hat s(1)}$. We put $r^*\xdf=(q^*\circ \hat p)[z/r(1)]\circ \bb\tau_H^{-1}$. Summarizing all the results we get that $r^*\in \xs_{\tau_H}\xs_{\hat s}\xd01\stackrel{H4}=\xd01$ and $r^*\in \xs_{\tau_H}\xspe{z}{\hat s(1)}\xs_{\hat s}\xspe0kx$, $r^*(0)=q^*(0)=u$, $r^*(1)=q^*(1)=v$. Using Lemma \ref{lm-2} we conclude that $r^*[0/v]\in \xs_{\tau_H}\xspe{z}{\hat s(1)}\xs_{\hat s}\xspe0kx$. This means that $r^*[0/v]\circ \bb\tau_H\circ \xbpe{z}{\hat s(1)}\circ \hat s \circ \xbpe0k\in x$. Then $ r^*[0/v]\circ \bb\tau_H\circ \xbpe{z}{\hat s(1)}\circ \hat s \circ\xbpe0k= ((q^*\circ \hat p)[z/r(1)]\circ \bb\tau_H^{-1} \circ \bb\tau_H)[\hat s(0)/v] \circ \xbpe{z}{\hat s(1)}\circ \hat s \circ\xbpe0k= (q^*\circ \hat p \circ \xbpe{z}{\hat s(1)})[\hat s(1)/r(1)][\hat s(0)/v] \circ \hat s \circ\xbpe0k= (q^*\circ \hat p \circ \hat s)[1/r(1)][0/v]\circ\xbpe0k= ((r \circ \xbpe0k)[1/v][1/r(1)]\circ\xbpe0k)[k/v]= (r \circ \xbpe0k\circ\xbpe0k)[k/v]= r[k/v]\in x$. If $k=1$ then $r\in x \;\;\Rightarrow \;\; r \circ \xbpe12\in \xspe12x \;\;\Rightarrow \;\; (r \circ \xbpe12)[2/v]\in \xspe12x \;\;\Rightarrow \;\; (r \circ \xbpe12)[2/v]\circ\xbpe12=r[1/v]\in x$. \end{proof} \begin{proofof}{Theorem \ref{th-rca} (1)} Surely, any representable cylindric set algebra is a subalgebra of a reduct of a model of H1,H2. To see the other direction, suppose that ${\cal A'}$ is a model of H1,H2. ${\cal A'}\models H1$ means that all the valid equations of $\xgwsn_{\bar H}$ hold in ${\cal A'}$. Naturally, some operations of $t_{\bar H}$ are term functions in $\xgwsp_H$. Since $\xigwsn_{\bar H}$ is a variety, the $t_{\bar H}$--reduct of ${\cal A}'$ is isomorphic to a $\xgwsn_{\bar H}$, say to ${\cal A}$. We will use only that ${\cal A}\in \xigws_{\bar H}$. The image of $\xd 01$ under the isomorphism is an element of $A$ not necessary the set theoretic (0,1)--diagonal. The image of any other diagonal constant can be computed from the image of $\xd 01$ since $\xd ij$ is term definable from $\xd 01$ in $\xgws_{\bar H}$. This shows that to represent ${\cal A'}$, it is enough to represent ${\cal A}$ that is to find a isomorphism $\xrep$ mapping the cylindric reduct of ${\cal A}$ into a \xrca. The universe $V$ of ${\cal A}$ is a \gunit\ therefore it is a (disjoint) union of weak spaces. Denote the set of weak spaces building ${\cal A}$ by $\Lambda$. For any weak space $\lambda$ from $\Lambda$, $\xbase(\lambda)$ is the base set of $\lambda$. $\xd 01$ defines an equivalence relation on $\xbase(\lambda)$ in a following way: for any $u, u' \in \xbase(\lambda)$ $$u\sim_\lambda u'\;\mbox{ iff }\; (\exists q\in \xd 01\cap\lambda)\;\;q(0)=u,\;q(1)=u'$$ \begin{cl}{cl-1} $\sim_\lambda$ is reflexive. \end{cl} \begin{proof} Suppose $u\in \xbase(\lambda)$. Let $\langle u_0, u_1, u_2, \ldots\rangle \in \lambda$ arbitrary. It is obvious that $\langle u, u, u_2, \ldots\rangle \in \lambda$. Now $\langle u, u, u_2, \ldots\rangle \in V=\xc_1\xd 01$. So $(\exists v\in \xbase(\lambda))\;\; \langle u, v, u_2, \ldots\rangle \in \xd 01$. Applying Lemma \ref{lm-2} to the case when $x=\xd 01$ it gives that $\langle u, u, u_2, \ldots\rangle \in \xd 01$ \end{proof} \begin{cl}{cl-2} $\sim_\lambda$ is symmetric. \end{cl} \begin{proof} Follows from Lemma \ref{lm-2} when applied to the case $x=\xd 01$. \end{proof} \begin{cl}{cl-3} $\sim_\lambda$ is transitive. \end{cl} \begin{proof} Follows from Lemma \ref{lm-3} when applied to the case $x=\xd 01$, $k=0$. \end{proof} Our aim is to embed the cylindric reduct of the not fully represented algebra ${\cal A}$ into a $\xgwsp_\omega$. For saving energy and not losing what we have already achieved, we are looking for a representation function $\xrep$ that acts not only on the algebra level but deeper, on the sequence level hiding in the elements of ${\cal A}$. In other words, $$\xrep(x)=\{f(q)\mid q \in x\}$$ where $f$ if the sequence level function mapping $V$ into the universe $V^*$ of some algebra ${\cal A^*}$. To ensure that $f(\xd 01)$ is the set theoretic constant we want for any $q,q'\in \lambda\in \Lambda$ that $(\forall i\in \omega)\;\; q(i)\sim_\lambda q'(i)$ should imply $f(q)=f(q')$. This observation gives us a hint for an adequate definition of $f$. For every $\lambda\in \Lambda$, we define $U_\lambda$ to be the set $(\xbase(\lambda)/\xsim_\lambda)\times \{\lambda\}$. $U_\lambda$ corresponds to the $\sim_\lambda$ classes of $\xbase(\lambda)$. Clearly, if $\lambda$ and $\lambda'$ are distinct then $U_\lambda$ and $U_{\lambda'}$ are disjoint. For every $q\in \lambda$, we define $$f(q)=\langle \langle q(0)/\xsim_\lambda,\lambda\rangle, \langle q(1)/\xsim_\lambda,\lambda\rangle, \langle q(2)/\xsim_\lambda,\lambda\rangle, \ldots \rangle $$ The $f$ image of a $\lambda \in \Lambda$ is also a weak space in ${}^\omega U_\lambda$. Let it be denoted by $\lambda^*$. Now we can define the image algebra ${\cal A}^*\in \xgwsp_\omega$: \begin{eqnarray*} V^*&=&\bigcup_{\lambda\in \Lambda} \lambda^*,\\ A^*&=&\{\xrep(x)\mid x\in A\},\\ {\cal A}^*&=&\langle A^*,\cap,-,\xc_i,\xd ij\rangle. \end{eqnarray*} One can easily verify that the above defined $\xrep$ is an isomorphism between the cylindric reduct of ${\cal A}$ and a generalised weak cylindric set algebra. Finally, the result $\xigwsp_\omega\subseteq \xigsp_\omega=\xrca$ published in \cite{hmtii} Theorem 3.1.103. completes the proof. \end{proofof} \subsection{Further observations on $\xmod(H1,H2)$} We have seen that a model ${\cal A'}$ of H1,H2 is isomorphic to an algebra ${\cal A}$ whose $t_{\bar H}$ reduct is a $\xgws_{\bar H}$. In the previous proof another isomorphism $\xrep$ was defined that mapped the cylindric reduct of ${\cal A}$ into ${\cal A}^*\in \xgwsp_\omega$. ${\cal A}^*$ can be expanded with the abstract operations $\xs_\sigma$ ($\sigma\in H$) as follows $$\xs_\sigma y \xdf=\xrep\,\xs_\sigma\xrep^{-1}y.$$ The expanded algebra is denoted by ${\cal A}^*$ as well. We examine the behaviour of the new, abstract operations. In this subsection we collect plenty of the characteristic features that will be useful in the proof of Theorem \ref{t-gen=} (3). All the notations (${\cal A}, {\cal A}^*, \Lambda, \sim_\lambda, f, \xrep$) that were introduced in the previous subsection are kept. The set of weak spaces of ${\cal A}^*$ is denoted by $\Lambda^*$. $\Lambda$ and $\Lambda^*$ is in a one-to-one correspondence in a natural way. We have that $\xbase(\lambda^*)=(base(\lambda)/\xsim_\lambda)\times\{\lambda\}$. >From now we suppose that all the elements of $H$ are bounded transformations of $\omega$. \begin{cl}{cl-bound} If $\sigma\in H$ (and so $\bb\sigma$ is bounded) and $\lambda_1,\lambda_2\in \Lambda$ then the statements below hold. \begin{itemize} \item $\xs_\sigma\lambda_1\supseteq \lambda_2$\hspace{5mm} or \hspace{5mm} $\xs_\sigma\lambda_1\cap \lambda_2=\emptyset$. \item $\xs_\sigma\lambda_1\supseteq \lambda_2$\hspace{5mm} iff \hspace{5mm} $(\exists q\in \lambda_2)(q \circ \bb\sigma\in \lambda_1)$. \item $(\forall \lambda_2\in \Lambda)(\exists!\lambda_1\in \Lambda)( \xs_\sigma\lambda_1\supseteq \lambda_2)$. (Here $\exists !$ stands for `there exists exactly one'.) \end{itemize} \end{cl} \begin{proof} Suppose that $q\in \xs_\sigma\lambda_1\cap\lambda_2$. For all $q'\in \lambda_2$, $q'\circ \bb\sigma\in \lambda_1$ since $q \circ \bb\sigma\in \lambda_1$ and $\{i\in \omega\mid q \circ \bb\sigma(i)\neq q'\circ \bb\sigma(i)\} \subseteq \bb\sigma^{-1}\{i\in \omega\mid q(i)\neq q'(i)\}$ is finite. So $\lambda_2\subseteq \xs_\sigma\lambda_1$. To prove the last statement suppose that $q\in \lambda_2\in \Lambda$. Put $\lambda_1$ to be the weak space of $q \circ \bb\sigma$. Clearly, $q \circ \bb\sigma\in \lambda_1$ and so $\lambda_2\subseteq \xs_\sigma\lambda_1$. If $\lambda'\in \Lambda$ and $\lambda_2\subseteq \xs_\sigma\lambda'$ then $\xs_\sigma\lambda_1\cap\xs_\sigma\lambda'= \xs_\sigma(\lambda_1\cap\lambda')\supseteq \lambda_2$ shows that $\lambda_1\cap\lambda'\neq 0$ and so $\lambda_1=\lambda'$. \end{proof} That claim shows that the following definition is explicit. \begin{df}{d-sonL} For each $\sigma\in H$, we define a transformation $\hat\sigma$ of $\Lambda$: $$\hat\sigma(\lambda_2)=\lambda_1\mbox{ if } \lambda_2\subseteq \xs_\sigma\lambda_1.$$ Since $\Lambda$ and $\Lambda^*$ are in one-to-one correspondence, $\hat\sigma$ can be viewed as a transformation of $\Lambda^*$: $\lambda_1,\lambda_2\in \Lambda$, $\hat\sigma(\lambda^*_2)=\lambda^*_1$ if $\hat\sigma(\lambda_2)=\lambda_1$. \end{df} We present an important property of these transformations. \begin{cl}{cl-hatjo} Suppose that $\sigma_1,\ldots,\sigma_n$ and $\sigma'_1,\ldots,\sigma'_m$ are elements of $H$. If $\bb\sigma_n\circ \ldots \circ \bb\sigma_1\approx \bb\sigma'_m\circ \ldots \circ \bb\sigma'_1$ then $\hat\sigma_1\circ \ldots \circ \hat\sigma_n$ and $\hat\sigma'_1\circ \ldots \circ \hat\sigma'_m$ are the same transformations of $\Lambda$ (and of $\Lambda^*$ as well). \end{cl} \begin{proof} Suppose that $\lambda\in \Lambda$. $\hat\sigma_1\circ\ldots \circ \hat\sigma_n(\lambda)=\lambda'$ if $\lambda\subseteq \xs_{\sigma_n}\ldots\xs_{\sigma_1}\lambda'$. Then for any $q\in \lambda$, $q \circ \bb\sigma_n\circ \ldots \circ \bb\sigma_1\in \lambda'$. Since $\bb\sigma_n\circ \ldots \circ \bb\sigma_1\approx \bb\sigma'_m\circ \ldots \circ \bb\sigma'_1$ and they are bounded, $q \circ \bb\sigma_n\circ \ldots \circ \bb\sigma_1\approx q \circ \bb\sigma'_m\circ \ldots \circ \bb\sigma'_1$. Then $q \circ \bb\sigma'_m\circ \ldots \circ \bb\sigma'_1\in \lambda'$, $\lambda\subseteq \xs_{\sigma'_m}\ldots\xs_{\sigma'_1}\lambda'$, $\hat\sigma'_1\circ \ldots \circ \hat\sigma'_m(\lambda)=\lambda'$ and this was to prove. \end{proof} \begin{rmk}{r-ph} The domain of the function $\hat{\mbox{}}$ defined in Definition \ref{d-sonL} is $H$. The previous claim implies that $\hat{\mbox{}}$ can be defined on $[\bar{\bb H}]$ as well. If $\nu\in [\bar{\bb H}]\subseteq {}^\omega\omega$ then we set $$\hat\nu\xdf=\hat\sigma_1\circ \ldots \circ \hat\sigma_n$$ where $\nu \approx \bb\sigma_n\circ \ldots \circ \bb\sigma_1$. Clearly, $\hat\nu$ does not depend on the choice of $\sigma_1, \ldots ,\sigma_n$. The new $\hat{\mbox{}}:[\bar{\bb H}]\rightarrow {}^{\Lambda^*}\Lambda^*$ has the following properties: \begin{itemize} \item If $\nu,\mu\in [\bar{\bb H}], \nu \approx\mu$ then $\hat\nu=\hat\mu$. \item If $\nu,\mu\in [\bar{\bb H}]$ then $\widehat{\nu \circ \mu}=\hat\mu \circ \hat\nu$. \end{itemize} \end{rmk} \begin{cl}{cl-base} When $\hat\sigma(\lambda_2)=\lambda_1$ for some $\sigma\in H, \lambda_1,\lambda_2\in \Lambda$ then \begin{itemize} \item $\xbase(\lambda_2)\subseteq \xbase(\lambda_1)$, \item $\sim_{\lambda_2}\;= \;\sim_{\lambda_1}\cap\;\;{}^2\xbase(\lambda_2)$. \end{itemize} \end{cl} \begin{proof} Suppose that $\lambda_2\subseteq \xs_{\sigma}\lambda_1$, $q\in \lambda_2$. For all $u\in \xbase(\lambda_2)$, $q[\bb\sigma(0)/u]\in \lambda_2$ and so $q[\bb\sigma(0)/u]\circ \bb\sigma\in \lambda_1$. But $(q[\bb\sigma(0)/u]\circ \bb\sigma)(0)=u\in \xbase(\lambda_1)$. It shows that $\xbase(\lambda_2)\subseteq \xbase(\lambda_1)$. To prove the second statement suppose that $u, u'\in \xbase(\lambda_2)$, $u\sim_{\lambda_2} u'$. There is a $q_2\in \xd01\cap\lambda_2$ for that $q_2(0)=u$, $q_2(1)=u'$. We fix a $k\in \omega$ for that $\bb\sigma(0)\neq\bb\sigma(k)$ and a finite transformation $h$ of $\omega$ that maps $\bb\sigma(0)$ to 0 and $\bb\sigma(k)$ to 1. Since $[\bar{\bb H}]$ is rich $h\in [\bar{\bb H}]$ and so there is $\tau\in \bar H^*$ for that $\bb\tau=h$. We put $q_1\xdf=q_2\circ h \circ \bb\sigma \circ \xbpe1k$. $q_2\in \xd01$ and $\xs_\tau\xs_\sigma\xspe1k\xd01= \xdv{h(\bb\sigma(\xbpe1k(0)))}{h(\bb\sigma(\xbpe1k(1)))}=\xd01$ implies that $q_1\in \xd01$. $q_2\in \lambda_2$ and $\lambda_2\subseteq \xs_\sigma\lambda_1$ gives that $q_1\in \lambda_1$. Finally, $q_1(0)=u$, $q_1(1)=u'$ shows that $u\sim_{\lambda_1}u'$. For the other direction suppose that $u, u'\in \xbase(\lambda_2)$, $u\sim_{\lambda_1} u'$. There is a $q\in \lambda_1\cap\xd01$ for that $q(0)=u$, $q(1)=u'$. Pick any $q_2\in \lambda_2$ with $q_2(0)=u$, $q_2(1)=u'$. We put $q_1\xdf=q_2\circ h \circ \bb\sigma \circ \xbpe1k$. As in the previous case $q_1\in \lambda_1$. $q \approx q_1$ so they disagree on a finite set $\Gamma=\{i_1,\ldots,i_n\}$. $0,1\not\in \Gamma$. We conclude that $q_1\in \xc_{i_1}\ldots\xc_{i_n}\xd01=\xd01$. Using again $\xs_\tau\xs_\sigma\xspe1k\xd01=\xd01$ and $q_1\in \xd01$ we get that $q_2\in \xd01$. This proves that $u\sim_{\lambda_2}u'$. \end{proof} \begin{df}{d-em} We define the function $$b: \displaystyle\bigcup_ {\makebox[10mm]{\scriptsize$\sigma\in H,\lambda^*\in \Lambda^*$}} \{\langle \sigma,\lambda^*\rangle \}\times\xbase(\lambda^*) \rightarrow \displaystyle\bigcup_{\lambda^*\in \Lambda^*}\xbase(\lambda^*)$$ as follows. $b_{\sigma,\lambda^*}(\langle \alpha,\lambda\rangle)= \langle \alpha',\hat\sigma(\lambda)\rangle$ if $\alpha'\in \xbase(\hat\sigma(\lambda))/\xsim_{\hat\sigma(\lambda)}$ and $\alpha\subseteq \alpha'$ holds. The previous claim proved that $b$ is well defined. \end{df} We collect some properties of the function $b$ defined above. \begin{cl}{cl-propb} \begin{arabate} \item $q\in \lambda^*\in \Lambda^*\;\;\Rightarrow \;\; b_{\sigma,\lambda^*}\circ q \circ \bb\sigma\in V^*$. \item $q,q'\in \lambda^*\in \Lambda^*\;\;\Rightarrow \;\; b_{\sigma,\lambda^*}\circ q \circ \bb\sigma \approx b_{\sigma,\lambda^*}\circ q'\circ \bb\sigma$. \item $b_{\sigma,\lambda^*}$ is injective. \item $(\forall \lambda\in \Lambda^*)(\exists ! \lambda'\in \Lambda^*) (\forall q\in \lambda)\; b_{\sigma,\lambda}\circ q \circ \bb\sigma\in \lambda'$. \end{arabate} \end{cl} \begin{proof} (1): Since $q\in V^*$, there is a $s\in V$ for that $f(s)=q$. The weak space of $s$ in ${\cal A}$ is $\lambda$, and that of $q$ in ${\cal A}^*$ is $\lambda^*$. We show that $b_{\sigma,\lambda^*}\circ q \circ \bb\sigma = f(s \circ \bb\sigma)\in V^*$ by checking that they take the same value on an arbitrary $i\in \omega$. $(b_{\sigma,\lambda^*}\circ q \circ \bb\sigma)(i)= b_{\sigma,\lambda^*}(q(\bb\sigma(i)))= b_{\sigma,\lambda^*}(f(s)(\bb\sigma(i)))= b_{\sigma,\lambda^*}(\langle s(\bb\sigma(i))/\xsim_\lambda,\lambda\rangle)= \langle s(\bb\sigma(i))/\xsim_{\hat\sigma(\lambda)},\hat\sigma(\lambda)\rangle= f(s \circ \bb\sigma)(i)$ To prove (2) we need only that $\bb\sigma$ is bounded. (3) follows from the definition, and (4) from (2). \end{proof} \begin{rmk}{rm-sigmab} If a function $g$ satisfies condition (4) of Claim \ref{cl-propb} then for each $\sigma\in H$, a transformation $\hat\sigma_g$ of $\Lambda^*$ can be defined: $$\hat\sigma_g(\lambda)=\lambda'\mbox{ iff } (\forall q\in \lambda)\;g_{\sigma,\lambda}\circ q \circ \bb\sigma\in \lambda'.$$ When $g$ coincides with $b$ then we get back $\hat\sigma$, that is $\hat\sigma_b=\hat\sigma$. \end{rmk} \begin{cl}{cl-prop5} Let $\lambda^*\in \Lambda^*$, $\sigma_1,\ldots,\sigma_n$ and $\sigma'_1,\ldots,\sigma'_m$ be elements of $H$. \begin{symbolate}{(5)} \item If $\hat\sigma_1\circ \ldots \circ \hat\sigma_n(\lambda^*)=\lambda^*$ then $b_{\sigma_1,\hat\sigma_2(\ldots\hat\sigma_n(\lambda^*)\ldots)}\circ b_{\sigma_2,\hat\sigma_3(\ldots\hat\sigma_n(\lambda^*)\ldots)}\circ \ldots \circ b_{\sigma_n,\lambda^*}$ is the identity mapping of $\xbase(\lambda^*)$. \end{symbolate} \begin{symbolate}{(6)} \item If $\hat\sigma_1\circ \ldots \circ \hat\sigma_n(\lambda^*)= \hat\sigma'_1\circ \ldots \circ \hat\sigma'_m(\lambda^*)$ then\\ $b_{\sigma_1,\hat\sigma_2(\ldots\hat\sigma_n(\lambda^*)\ldots)}\circ b_{\sigma_2,\hat\sigma_3(\ldots\hat\sigma_n(\lambda^*)\ldots)}\circ \ldots \circ b_{\sigma_n,\lambda^*}=$\\\mbox{}\hfill $=b_{\sigma'_1,\hat\sigma'_2(\ldots\hat\sigma'_m(\lambda^*)\ldots)}\circ b_{\sigma'_2,\hat\sigma'_3(\ldots\hat\sigma_m(\lambda^*)\ldots)}\circ \ldots \circ b_{\sigma'_m,\lambda^*}$ \end{symbolate} \end{cl} \begin{proof} First we note that the expression formulated above is correct. The range of $b_{\sigma_i,\hat\sigma_{i+1}(\ldots\hat\sigma_n(\lambda)\ldots)}$ is contained in $\xbase(\hat\sigma_{i}(\ldots\hat\sigma_n(\lambda)\ldots))$ and that is the domain of $b_{\sigma_{i+1},\hat\sigma_i(\ldots\hat\sigma_n(\lambda)\ldots)}$. To check the validity of the expression in (6) we evaluate the two sides of the equation on an arbitrary element of $\xbase(\lambda^*)$, say an $\langle u/\xsim_\lambda,\lambda\rangle $. When the left side of the equation is applied to that element we get $\langle u/\xsim_{(\hat\sigma_1\circ\ldots\circ\hat\sigma_n)(\lambda)}, (\hat\sigma_1 \circ \ldots \circ \hat\sigma_n)(\lambda)\rangle$ and that is the same point as the image of $\langle u/\xsim_\lambda,\lambda\rangle $ under the function that appear on the right side of the equation. (5) follows from the definition. \end{proof} \begin{nt}{nt-circ} We define a new composition operation $\bullet$ mapping $V^*\times H$ into $V^*$: $$q \bullet\sigma\xdf=b_{\sigma,[q]}\circ q \circ \bb\sigma$$ where $[q]$ is the weak space of $q$ in ${\cal A}^*$. \end{nt} Now a direct definition can be given to $\xs_\sigma$ ($\sigma\in H$). \begin{cl}{cl-newd2} For all $\sigma\in H, y\in A^*$ $$\xs_\sigma y=\{q\in V^*\mid q \bullet\sigma\in y\}$$ \end{cl} \begin{proof} As a side result, in the proof of Claim \ref{cl-propb} (1) we showed that if $s\in V, q\in V^*, f(s)=q$ then $f(s \circ \bb\sigma)=q\bullet\sigma$. Now we can compute that $q\in \xs_\sigma y\Leftrightarrow s\in \xs_\sigma\xrep^{-1}y\Leftrightarrow s \circ \bb\sigma\in \xrep^{-1}y\Leftrightarrow f(s \circ \bb\sigma)\in y\Leftrightarrow q \bullet\sigma \in y$. \end{proof} We arrived to the point when a new class of set algebras can be introduced. A new algebra has a deeper structure than a $\xgwsp_H$ does and its operations are computable from the structure of the algebra. \begin{df}{df-nonst} An algebra ${\cal A}=\langle A,\cup,- , \xc_k, \xd kl, \xs_\sigma \rangle_{k,l\in \omega, \sigma\in H}$ is called a {\em non-standard generalised weak $H$--cylindric set algebra with equality} (or briefly a $\xnsg_H$) if $\langle A,\cup,- , \xc_k, \xd kl\rangle_{k,l\in \omega}$ is a generalised weak cylindric set algebra and there is a function $b$ with the following properties: \begin{itemize} \item Let $V$ be the unit element of ${\cal A}$. We put $\Lambda$ to be the set of weak spaces building $V$. The domain of $b$ is $\displaystyle\bigcup_{\sigma\in H,\lambda\in \Lambda} \{\sigma,\lambda\}\times\xbase(\lambda)$, the range is a subset of $\displaystyle\bigcup_{\lambda\in \Lambda} \xbase(\lambda)$. \item $b$ satisfies the properties (1)-(6) listed in Claim \ref{cl-propb} and Claim \ref{cl-prop5} where $\hat\sigma=\hat\sigma_b$ is defined as in Remark \ref{rm-sigmab}. \item We put $\bullet:V\times H\rightarrow V$ to be the function $q \bullet\sigma\xdf=b_{\sigma,[q]}\circ q \circ \bb\sigma$. Clearly, the properties of $b$ gives that $b_{\sigma,[q]}\circ q \circ\bb\sigma$ is an element of $V$. Then $\xs_\sigma y=\{q\in V\mid q \bullet\sigma\in y\}$. \end{itemize} If ${\cal A}$ is a $\xnsg_H$ and $b$ is a function with the required properties then $b$ is called a {\em base transformation function of ${\cal A}$}. Note that the base transformation function is not uniquely determined. \end{df} The theorem below is a summary of the results that have achieved so far in this subsection. \begin{theo}{th-nonst} Any model of H1,H2 is isomorphic to a $\xnsg_H$. \end{theo} \begin{theo}{th-st-nst} $\xgwsp_H\subseteq \xnsg_H$. \end{theo} \begin{proof}Any $\xgwsp_H$ is a $\xnsg_H$ with the identity as base transformation function. $(\forall \sigma\in H)(\lambda\in \Lambda)(\forall u\in \xbase(\lambda)) \;\; b_{\sigma,\lambda}(u)\xdf=u$. \end{proof} \begin{cl}{cl-hatjo2} Suppose that ${\cal A}\in \xnsg_H$. Then Claim \ref{cl-hatjo} is true in ${\cal A}$. \end{cl} \begin{proof} As usual, $\Lambda$ is the set of weak spaces of ${\cal A}$. Pick an arbitrary element of $\Lambda$, say $\lambda$, and an arbitrary sequence $q$ in $\lambda$. Using the definition of $\hat\sigma$ in Remark \ref{rm-sigmab} we have that $\hat\sigma_1 \circ \ldots \circ \hat\sigma_n(\lambda)$ and $\hat\sigma'_1 \circ \ldots \circ \hat\sigma'_m(\lambda)$ are the weak spaces of $b_{\sigma_1,\hat\sigma_2(\ldots\hat\sigma_n(\lambda)\ldots)}\circ b_{\sigma_2,\hat\sigma_3(\ldots\hat\sigma_n(\lambda)\ldots)}\circ \ldots \circ b_{\sigma_n,\lambda} \circ q \circ \bb\sigma_n \circ \ldots \circ \bb\sigma_1 = q \bullet\sigma_n \bullet\ldots \bullet\sigma_1$ and $b_{\sigma'_1,\hat\sigma'_2(\ldots\hat\sigma'_m(\lambda)\ldots)}\circ b_{\sigma'_2,\hat\sigma'_3(\ldots\hat\sigma_m(\lambda)\ldots)}\circ \ldots \circ b_{\sigma'_m,\lambda} \circ q \circ \bb\sigma'_m \circ \ldots \circ \bb\sigma'_1 = q \bullet\sigma'_m \bullet\ldots \bullet\sigma'_1$ each respectively. Since $\bb\sigma_n \circ \ldots \circ \bb\sigma_1 \approx \bb\sigma'_m \circ \ldots \circ \bb\sigma'_1$, we have that $q \circ \bb\sigma_n \circ \ldots \circ \bb\sigma_1 \approx q \circ \bb\sigma'_m \circ \ldots \circ \bb\sigma'_1$. This fact and Claim \ref{cl-prop5} implies that $q \bullet\sigma_n \bullet\ldots \bullet\sigma_1 \approx q \bullet\sigma'_m \bullet\ldots \bullet\sigma'_1$ and so they are in the same weak space, that is $\hat\sigma_1 \circ \ldots \circ \hat\sigma_n(\lambda)= \hat\sigma'_1 \circ \ldots \circ \hat\sigma'_m(\lambda)$. \end{proof} \begin{rmk}{r-pb} As we did in Remark \ref{r-ph}, we can introduce the function $\hat{\mbox{}}:[\bar{\bb H}]\rightarrow {}^\Lambda\Lambda$ as $\hat\nu\xdf=\hat\sigma_1\circ \ldots \circ \hat\sigma_n$ when $\nu\in [\bar{\bb H}], \sigma_1,\ldots,\sigma_n\in H$ and $\nu \approx \bb\sigma_n\circ \ldots \circ \bb\sigma_1$. % In the same sense, the domain of $b$ can be expanded $$b:\displaystyle\bigcup_{\nu\in [\bar{\bb H}],\lambda\in \Lambda} \{\nu,\lambda\}\times\xbase(\lambda)\rightarrow \displaystyle\bigcup_{\lambda\in \Lambda} \xbase(\lambda)$$ $$ b_{\nu,\lambda}\xdf= b_{\sigma_1,\hat\sigma_2(\ldots\hat\sigma_n(\lambda)\ldots)}\circ b_{\sigma_2,\hat\sigma_3(\ldots\hat\sigma_n(\lambda)\ldots)}\circ \ldots \circ b_{\sigma_n,\lambda}$$ where $\nu\in [\bar{\bb H}], \sigma_1,\ldots,\sigma_n\in H, \lambda\in \Lambda$ and $\nu \approx \bb\sigma_n\circ \ldots \circ \bb\sigma_1$. If $ \sigma'_1,\ldots,\sigma'_m\in H$ and $\nu \approx \bb\sigma'_m\circ \ldots \circ \bb\sigma'_1$ then $\hat\sigma_1 \circ \ldots \circ \hat \sigma_n= \hat \nu= \hat\sigma'_1 \circ \ldots \circ \hat \sigma'_m$ so $\hat\sigma_1 \circ \ldots \circ \hat \sigma_n (\lambda)= \hat\sigma'_1 \circ \ldots \circ \hat \sigma'_m(\lambda)$. This gives that (6) of Claim \ref{cl-prop5} is applicable showing that the above definition of $b$ does not depend on the choice of $\sigma_1,\ldots, \sigma_n$. We collect some properties of our new $\hat{\mbox{}}$ functions. $\nu,\mu\in [\bar{\bb H}],\lambda\in \Lambda$. \begin{arabate} \item $\nu \approx\mu$ implies $\hat\nu=\hat\mu$. %1 \item $\widehat{\nu \circ \mu}=\hat\mu \circ \hat\nu$. %2 \item $\nu \approx\xid$ implies that $b_{\nu,\lambda}$ is the %3 identity mapping of $\xbase(\lambda)$. \item $b_{\nu \circ \mu,\lambda}=b_{\mu, \hat\nu(\lambda)} \circ %4 b_{\nu,\lambda}$. \item $\hat\nu(\lambda)=\hat\mu(\lambda)$ implies %5 $b_{\nu,\lambda}=b_{\mu,\lambda}$. \end{arabate} (1) and (2) can be found in Remark \ref{r-ph}, (3) and (5) are only reformulations of (5) and (6) of Claim \ref{cl-prop5}, and (4) is a consequence of (6) of Claim \ref{cl-prop5}. \end{rmk} \begin{lm}{th-subd} Let ${\cal A}$ be a subdirect irreducible model of H1,H2,H3. Then either $-\xc_0(-\xd01)=1$ or $-\xc_0(-\xd01)=0$. \end{lm} \begin{proof} Suppose that in a model ${\cal A}$ of H1,H2,H3 neither $-\xc_0(-\xd01)=0$ nor $\xc_0(-\xd01)=0$ holds. We show that the relativizations with $-\xc_0(-\xd01)$ and $\xc_0(-\xd01)$ are homomorphisms, but not isomorphisms, and ${\cal A}$ is a subdirect product of the two image algebras. This proves that ${\cal A}$ cannot be subdirectly irreducible. A relativization with some element $R$ is a homomorphism if and only if $R$ is closed under the operations of the algebra. H3 implies that $-\xc_0(-\xd01)$ and $\xc_0(-\xd01)$ are closed. In the image algebras $-\xc_0(-\xd01)=1$ or $\xc_0(-\xd01)=1$ will hold showing that they cannot be isomorphic to ${\cal A}$. Finally, an element of ${\cal A}$ is solely determined by its two image under the two relativizations. \end{proof} \begin{lm}{l-extr} If $-\xc_0(-\xd01)=1$ holds in ${\cal A}\in \xnsg_H$ then ${\cal A}$ is a $\xgsp_H$. \end{lm} \begin{proof} Let $A$ be the universe, $V$ the unit element, $\Lambda$ the set of weak spaces of ${\cal A}$. $-\xc_0(-\xd01)=1$ shows that for all $\lambda\in \Lambda$, $|\xbase(\lambda)|=1$. Introduce the set theoretical operations on $A$: $$\tilde{\xs}_\sigma x\xdf=\{q\in V\mid q \circ \bb\sigma\in x\}.$$ Then %${\cal A}=\langle A,\cup\,-,\xc_k,\xd kl,\xs_\sigma\rangle_{k,l\in %\omega,\sigma\in H}$ and ${\cal A'}\xdf= \langle A,\cup\,-,\xc_k,\xd kl,\tilde{\xs}_\sigma\rangle_{k,l\in \omega,\sigma\in H}\in \xgsp_H$. We show that $\tilde{\xs}_\sigma=\xs_\sigma$ and so ${\cal A}={\cal A'}\in \xgsp_H$. $\xs_\sigma x=x$ since the axiom $\xs_\sigma(x-\xc_0(-\xd01))=x-\xc_0(-\xd01)$ in H3 can be reduced to that form using $-\xc_0(-\xd01)=1$. On the other hand, $\tilde{\xs}_\sigma x=x$ is a result of that fact that in $V$ all the sequences are of the form $\langle u,u,u,\ldots\rangle$ for some $u$. \end{proof} \subsection{The witness tree method} \label{wtm} In this subsection we build a machinery called the witness tree method to prove Theorem \ref{t-gen=}. The essence of the method is the following. The failure of an equation in a given algebra can be captured by a tree structure that reflects the local nature of the algebra. This tree can be cut out from the algebra and moved to another one with better properties to testify the failure of the same equation therein. In our case we will show that an equation that is not satisfied in a $\xnsg_H$ cannot hold in all the $\xgwsp_H$s. \begin{df}{d-wt} Let $H$ be a set of transformations of $\omega$. We say that $\Omega=\langle V,E,r,U,\tau,\varepsilon,l\rangle $ is a {\em witness tree of type $H$} if the following requirements are fulfilled. \begin{romanate} \item $\langle V,E\rangle$ is a directed tree. $r\in V$. The edges are directed from the root $r$ towards the leaves. \item $U,\tau$ and $\varepsilon$ are functions with domain $V$. If $v\in V$ then $U_v$ is a set, $\tau_v$ is a term of type $t^=_H$, and $\varepsilon_v$ is either $\ni$ or $\not\ni$. (Note that we used the less conventional notation $U_v$ instead of $U(v)$.) \item $l$ is a function with domain $E$. If $e=\vec{vv'}\in E$ is an edge then $l_e$ is one of '$=$', '$[k/u]$' or '$\sigma$' where $k\in \omega$, $u\in U_v$, $\sigma\in H$. We will call $l_e$ the {\em label} of the edge $e$. \item If $e=\vec{vv'}\in E$ is an edge then $U_v\subseteq U_{v'}$. Furthermore, if $l_e$ is not '$\sigma$' for some $\sigma\in H$ then $U_v=U_{v'}$. \item For every vertex $v$, $\tau_v$, $\varepsilon_v$, the number of children of $v$, the labels of the edges pointing to the children of $v$, and the value of $\tau$ and $\varepsilon$ on of the children vertexes of $v$ are in a connection indicated in the following table. \end{romanate} $$\begin{array}{ccccl} \parbox[t]{25mm}{\begin{center}$\tau_v$, $\varepsilon_v$\end{center}}& \parbox[t]{15mm}{\begin{center}The number of children\end{center}}& \parbox[t]{20mm}{\begin{center}The label of an edge pointing to a child\end{center}}& \parbox[t]{15mm}{\begin{center}The value of $\tau$, $\varepsilon$ on a child vertex\end{center}}&\\ (-\varrho),\ni&1&=&\varrho,\not\ni&\\ (-\varrho),\not\ni&1&=&\varrho,\ni&\\ (\varrho_1\cup\varrho_2),\ni&1&=&\varrho_i,\ni&\mbox{where $i$ is 1 or 2}\\ (\varrho_1\cup\varrho_2),\not\ni&2&=&\varrho_i,\not\ni&\mbox{for $i\in\{1,2\}$}\\ \xc_k\varrho,\ni&1&[k/u]&\varrho,\ni&\mbox{where $u\in U_v$}\\ \xc_k\varrho,\not\ni&|U_v|&[k/u]&\varrho,\not\ni&\mbox{for each $u\in U_v$}\\ \xs_\sigma\varrho,\ni&1&\sigma&\varrho,\ni&\\ \xs_\sigma\varrho,\not\ni&1&\sigma&\varrho,\not\ni&\\ X,\ni&0&-&-&\\ X,\not\ni&0&-&-&\\ \xd kl,\ni&0&-&-&\\ \xd kl,\not\ni&0&-&-& \end{array}$$ \end{df} \begin{df}{d-nuv} Let $\Omega$ be a witness tree. We define a function $\nu:V\rightarrow {}^\omega\omega$ by recursion. For the root $r$, $\nu_{r}=\xid$. If $e=\vec{v_1v_2}\in E$ and $\nu_{v_1}$ is already defined then $\nu_{v_2}$ is set to $\nu_{v_1}$ when $l_e$ is '=' or '$[k/u]$' for some $k\in \omega, u\in U_{v_1}$ and to $\nu_{v_1}\circ \bb\sigma$ when $l_e$ is '$\sigma$'. \end{df} \begin{df}{d-Mr} Let $\varrho$ be a term. Then $M_\varrho$ denotes the set of those transformations $f$ of $\omega$ for that exist $\sigma_1, \ldots , \sigma_n\in H$ with the property that $f=\bb\sigma_1 \circ \ldots\bb\sigma_n$ and $\xs_{\sigma_1},\ldots,\xs_{\sigma_n}$ are letters of $\varrho$. We allow $\sigma_i$ to be equal with $\sigma_j$ ($i\neq j$) but in that case $\xs_{\sigma_i}$ and $\xs_{\sigma_j}$ refer to the multiple occurrence of the same letter in $\varrho$. Clearly, $n$ is smaller than or equal to the length of term $\varrho$. \end{df} \begin{cl}{cl-Mfin} The set $M_\varrho$ defined in the previous definition is finite. \end{cl} \begin{proof} The term $\varrho$ has only finite number of letters so there is only finitely many possible choices of $\sigma_1,\ldots,\sigma_n$. \end{proof} \begin{df}{d-M} Let $\Omega$ be a witness tree. Then $M_\Omega$ denotes $M_{\tau_r}$. \end{df} \begin{cl}{cl-nuM} For each vertex $v$ of $\Omega$, $\nu_{v}\in M_\Omega$. \end{cl} \begin{df}{d-M=} $M^=_\Omega, M^{\neq}_\Omega$ denotes the following subsets of $M_\Omega\times M_\Omega$. \begin{eqnarray*} M^=_\Omega&\xdf=&\{\langle \nu,\nu'\rangle\mid \nu \approx\nu\wedge (\exists \mbox{ vertex }v,v')(\nu=\nu_{v}\wedge \nu'=\nu_{v'})\}\\ M^{\neq}_\Omega&\xdf=&\{\langle \nu,\nu'\rangle\mid \nu\not\approx\nu'\wedge (\exists \mbox{ vertex }v,v')(\nu=\nu_{v}\wedge \nu'=\nu_{v'})\} \end{eqnarray*} Both $M^=_\Omega$ and $M^{\neq}_\Omega$ are finite. \end{df} \begin{df}{d-degen} Let $\Omega$ be a witness tree. We say the $\Omega$ is {\em not degenerated} if \begin{eqsymbol}{\ddag} (\forall \mbox{ vertex }v_1,v_2)(\forall \mu\in [\bar{\bb H}])\;\; \nu_{v_1}\circ \mu \approx \nu_{v_2}\Rightarrow U_{v_1}\subseteq U_{v_2} \end{eqsymbol} holds. \end{df} \begin{df}{d-validq} Let $\Omega$ be a witness tree. We say that a function $Q$ is a {\em valuation of the vertex set of $\Omega$} if the conditions below hold. \begin{arabate} \item The domain of $Q$ is the vertex set of $\Omega$. \item For all vertex $v$, $Q_v$ is an $\omega$-sequence over $U_v$. \item If $v_1$ and $v_2$ are two adjacent vertexes of $\Omega$ then the connection between $Q_{v_1}$ and $Q_{v_2}$ is determined by the label of the edge that joins $v_1$ and $v_2$. \begin{itemize} \item If the label is '=' then $Q_{v_2}=Q_{v_1}$. \item If the label is '$[k/u]$' then $Q_{v_2}=Q_{v_1}[k/u]$. \item If the label is '$\sigma$' then $Q_{v_2}=Q_{v_1}\circ \bb\sigma$. \end{itemize} \end{arabate} \end{df} \begin{cl}{cl-vq} A valuation $Q$ of the vertex set of a witness tree $\Omega$ and the value of $Q$ on the root of $\Omega$ uniquely determine each other. \end{cl} \begin{proof} If we know the value of $Q$ on the root then we can compute the values of $Q$ on other vertexes going step-by-step towards the leaves using (3) of Definition \ref{d-validq}. To verify (2), we need only that $U_{v_1}\subseteq U_{v_2}$ whenever $\vec{v_1v_2}$ is an edge. (See the table in Definition \ref{d-wt}.) \end{proof} \begin{cl}{cl-c1} Let $\Omega$ be a witness tree with root $r$, $Q$ be a valuation of the vertex set. Then $$(\exists c_1\in \omega)(\forall \mbox{ vertex } v)(\forall i\in \omega) \;\;Q_v(i)\neq(Q_r \circ \nu_{v})(i)\Rightarrow i\leq c_1.$$ \end{cl} \begin{proof} To get an insight into the relation of $Q_v$ and $Q_r \circ \nu_{v}$, we take an example first. Suppose that we find the sequence $\sigma_1$, $[k_1/u_1]$, $\sigma_2$, $[k_2/u_2]$, $\sigma_3$, $\sigma_4$, $[k_3/u_3]$, $\sigma_5$ of labels on the $r\rightarrow v$ path. Then $$Q_v(i)=\left\{ \begin{array}{cl} u_3 & \mbox{ if } i\in \bb\sigma_5^{-1}(k_3),\\ u_2 & \mbox{ if } i\in (\bb\sigma_3 \circ \bb\sigma_4 \circ \bb\sigma_5)^{-1}(k_2)-\bb\sigma_5^{-1}(k_3),\\ u_1 & \mbox{ if } i\in (\bb\sigma_2 \circ \bb\sigma_3 \circ \bb\sigma_4\circ\bb\sigma_5)^{-1}(k_1) -B,\\ Q_r \circ \nu_{v}(i) &\mbox{ otherwise} \end{array}\right.$$ where $B=(\bb\sigma_3 \circ \bb\sigma_4 \circ\bb\sigma_5)^{-1}(k_2)\cup \bb\sigma_5^{-1}(k_3)$. This example shows that for any $v$, $Q_v$ and $Q_r \circ \nu_{v}$ are equal everywhere but on the union of finitely many sets of the form $(\bb\sigma_1 \circ \ldots \circ \bb\sigma_n)^{-1}(k)$ where $\xs_{\sigma_1},\ldots,\xs_{\sigma_n},\xc_k$ are letters of the root term. In that case $(\bb\sigma_1 \circ \ldots \circ \bb\sigma_n)^{-1}(k)$ is finite since $\bb\sigma_i$ is bounded ($i\leq n$) and $\bb\sigma_1 \circ \ldots \circ \bb\sigma_n\in M_\Omega$. We can conclude that the set $\displaystyle\bigcup_{\makebox[20mm]{\mbox{}\hfill\parbox{0mm}{ \makebox[0cm]{\scriptsize$\nu\in M_\Omega,$}\\ \makebox[0cm]{$\mbox{\scriptsize \bf c}_k$ \scriptsize is a letter of the root term}}\hfill\mbox{}}} \nu^{-1}(k)$ is finite and $c_1$ can be set to be its maximum. \end{proof} \begin{cl}{cl-c2} Let $\Omega$ be a witness tree with root $r$, $Q$ be a valuation of the vertex set. Then $$(\exists c_2\in \omega)(\forall \mbox{ vertex } v,v')(\forall i\in \omega) \; \nu_{v}\approx\nu_{v'}\wedge (Q_r \circ \nu_{v})(i)\neq(Q_r \circ \nu_{v'})(i) \Rightarrow i\leq c_2.$$ \end{cl} \begin{proof} Put $\displaystyle c_2\xdf=\max\bigcup_{\langle \nu,\nu'\rangle \in M^=_\Omega} \{i\in \omega\mid\nu(i)\neq\nu'(i)\}$. This definition is transparent since the set, we have to take the maximum of is finite. ($M_\Omega^=$ is finite, $\{i\in \omega\mid\nu(i)\neq\nu'(i)\}$ is finite if $\nu \approx\nu'$.) \end{proof} \begin{lm}{l-c} Let $\Omega$ be a witness tree with root $r$, $Q$ be a valuation of the vertex set. Then $$(\exists c\in \omega)(\forall \mbox{ vertex } v,v')(\forall i\in \omega) \;\; \nu_{v}\approx\nu_{v'}\wedge Q_{v}(i)\neq Q_{v'}(i) \Rightarrow i< c.$$ \end{lm} \begin{proof} Put $c=\max\{c_1,c_2\}+1$. Claims \ref{cl-c1} and \ref{cl-c2} will prove the statement. \end{proof} \begin{lm}{l-S} Suppose that $U_r$ is a set with cardinality bigger than 2. Then there is a sequence $S\in {}^\omega U_r$ with the property that for all $\mu,\nu\in [\bar{\bb H}]$ $$\mu\not \approx\nu\;\Rightarrow \; S_r \circ \mu\not \approx S_r \circ \nu$$ \end{lm} To prove this lemma we will need the following claim. \begin{cl}{cl-h1} There is a set $D\subseteq {\cal P}(\omega)$ for that \begin{itemize} \item $\alpha\in D\;\Rightarrow \;|\alpha|=2$, \item $\alpha,\beta\in D\wedge \alpha\neq\beta\;\Rightarrow \;\alpha\cap\beta=\emptyset$, \item $\mu,\nu\in [\bar{\bb H}], \mu\not \approx\nu\;\Rightarrow \; |D\cap\{\{\mu(i),\nu(i)\}\mid i\in \omega\}|=\omega$. \end{itemize} \end{cl} \begin{proof} Let $\langle\mu_i,\nu_i \rangle$ $(i\in \omega)$ be a series of pairs of transformations of $\omega$ with the property that for any $\mu,\nu\in [\bb H]$ with $\mu\not \approx\nu$ we have that $\langle \mu_i,\nu_i\rangle=\langle \mu,\nu\rangle$ for infinitely many $i\in \omega$. A series of that kind exists since $|H|\leq \omega, |\bar{H}|\leq \omega, |[\bar{\bb H}]|\leq |\bar{H}^*|\leq \omega, |[\bar{\bb H}]\times [\bar{\bb H}]|\leq \omega$. For all $k\in \omega$ we define the set $\alpha_k$ recursively: \begin{itemize} \item $\alpha_0=\{\mu_0(i),\nu_0(i)\}$ for an $i\in \omega$ with $\mu_0(i)\neq\nu_0(i)$. \item $\alpha_k=\{\mu_k(i),\nu_k(i)\}$ for an $i\in \omega$ with $\mu_k(i)\neq\nu_k(i)$ and $i\not\in \mu^{-1}_k(\displaystyle\bigcup_{j1$. Corollary \ref{cr-help} is applicable, therefore $\Omega$ has a valid valuation into a $\xgwsp_H$. Using again Lemma \ref{l-wing} we get that $\varrho=0$ fails in that algebra of $\xgwsp_H$. \end{proof} \begin{proofof}{Theorem \ref{t-gen=} (3)} Since both $\xhgwsp_H$ and $\xmod(H1,H2,H3)$ are varieties, we need to show that they satisfy the same set of equations. First we show that $\xgwsp_H\models H1, H2, H3$. The only equation that needs explanation is the first one in H3. First suppose that $q\in x-\xc_0(-\xd 01)$. Then the weak space of $q$ has a base of cardinality 1, so $q=\langle u,u,u,\ldots\rangle$. But in that case $q=q\circ\bb\sigma$, $q\in \xs_\sigma(x-\xc_0(-\xd 01))$. Now suppose that $q\in \xs_\sigma(x-\xc_0(-\xd 01))$. Then $q\circ\bb\sigma\in x-\xc_0(-\xd 01)$, so the weak space of $q\circ\bb\sigma$ has a base of cardinality 1. Referring to Claim \ref{cl-base} we have that the base of the weak space of $q$ is contained in that of $q\circ\bb\sigma$ so it is of cardinality 1 as well. Hence, $q=q\circ\bb\sigma$, $q\in x-\xc_0(-\xd 01)$. For the other direction we show that any equation $e$ that fails in an ${\cal A}\in \xmod(H1,H2,H3)$ also fails in some ${\cal B}\in \xgwsp_H$. First we simplify the situation by putting assumptions on ${\cal A}$ and $e$ and then we will apply Corollary \ref{cr-fo} or Lemma \ref{l-extr} to prove the theorem. If $e$ is of the form $\tau=\tau'$ then the equation $\tau\oplus\tau'=0$ is satisfied in exactly those algebras where $e$ ($\oplus$ is the symmetric difference operator). For that reason, without loss of generality we may assume that $e$ of the form $\varrho=0$. Every algebra is a subalgebra of a product of subdirect irreducible algebras. If an equation fails in a subdirect product, then it fails in some of the factors. So we may assume that ${\cal A}$ is a subdirectly irreducible algebra. Furthermore, referring to Theorem \ref{th-nonst} we may put the assumption that ${\cal A}$ is a $\xnsg_H$. According to Theorem \ref{th-subd} either $-\xc_0(-\xd01)=1$ or $-\xc_0(-\xd01)=0$ holds in ${\cal A}$. In the first case Lemma \ref{l-extr}, in the second Corollary \ref{cr-fo} provides the required ${\cal B}$ in which $\varrho=0$ fails. \end{proofof} \begin{proofof}{Theorem \ref{t-gen=} (4)} The proof of Theorem \ref{t-gen=} (3) is applicable with some adjustments. We present the required modifications here. Theorem \ref{th-subd} remains valid. In the proof of Lemma \ref{l-extr} one can note that the algebra ${\cal A'}$ defined therein is a direct product of some two element algebras. (Clearly, any weak space with a base of cardinality 1 is a $H$-cylindric set algebra with equality in itself.) Hence, this lemma can be reformalized as: {\em If $-\xc_0(-\xd01)=1$ holds in ${\cal A}\in \xnsg_H$ then ${\cal A}$ is a $\xpcsp_H$.} Under the conditions listed in Theorem \ref{t-gen=} (4), we have that: {\em If $\Omega$ is a not degenerated witness tree then for every vertex $v$ we have that $U_v=U_r$.} Suppose that $v$ is a vertex. Put $\nu_v^*$ and $\nu_r^*$ to be the right quasi-inverse of $\nu_v$ and $\nu_r$ respectively. Then $\nu_v\circ\nu_v^*\circ\nu_r\approx\nu_r$ and $\nu_r\circ\nu_r^*\circ\nu_v\approx\nu_v$ shows that $U_v\supseteq U_r$ and $U_r\supseteq U_v$ giving $U_v=U_r$. (We used that $\nu_r$ and $\nu_v$ are bounded transformations.) Claim \ref{cl-compl} can be modified to: {\em Let $\Omega$ be witness tree with root $r$, $P$ be a consistent valuation of the vertex set of $\Omega$. Then there is a function $w$ for that $\langle P,w\rangle$ is a valid valuation of $\Omega$ into the full $H$--cylindric set algebra with equality over the base set $U_r$.} To prove that statement we need to skip the argumentation about the algebra itself in the original proof and start reading from the point where $w$ is defined. Using that modified Claim we get: {\em Suppose that the equation $\varrho=0$ fails in an algebra ${\cal A}\in \xnsg_H$, and ${\cal A}\models -\xc_0(-\xd01)=0$. Then $\xcsp_H\not\models\varrho=0$.} Following the argument described in the proof of Theorem \ref{t-gen=} (3) and inserting the modifications listed above we get that the statement in Theorem \ref{t-gen=} (4) holds. \end{proofof} %%% %model-\models %semigroup-semigroup %circ-\circ %id-\xid %barh-[\bar{\bb H}] %permutation-permutation %nyil-\;\;\Rightarrow \;\; %noproof-\begin{proof} WILL COME SOON. \end{proof} %item-\item %witness-witness tree %transformation-transformation of %nv-\nu_{v} %valuation-valuation of the vertex set of %displaystyle-\displaystyle %approx-\approx %bullet-\bullet % Local Variables: % mode: latex % TeX-master: "suc" % End: \section*{Historical remark} The early versions of the ideas presented in this work can be found in \cite{SaFIN} but the investigations here go much further than the ones therein. Many of our results {\em for the special choice} $H=G$ are already stated in \cite{SaFIN} in less developed form. The case without equality is fully proved there, but our axiom system \xax\ is considerably simpler than the one in \cite{SaFIN}. (Cf.\ around the end of Part I and beginning of Part II of \cite{SaFIN}.) The {\em Tarski--Givant style} part of the case with equality is implicit in \cite{S87}. These research directions are not investigated in \cite{S9}. The works of S\'andor Csizmazia (e.g.\ \cite{Cs93}, \cite{Cs95}) were based on the early version \cite{SaFIN} of the present ideas. \section*{Acknowledgement} The authors are grateful to W.Craig, L.Henkin, J.D.Monk and I.N\'emeti for encouragement, valuable discussions and suggestions concerning the topic of this paper. Thanks are due to S.Csizmazia for pointing out the data written in the Historical remark section above. {\small \begin{thebibliography}{MMMM} \newcommand{\maki}{Math. Inst. \mta} \newcommand{\mta}{Hungarian Academy of Sciences, Budapest} \newcommand{\ams}{American Math. Society} \bibl{A91}{diszi} Andr{\'e}ka,H. {\em Complexity of the Equations Valid in Algebras of Relations} PhD thesis, \mta, Budapest, 1991. (Thesis for D.Sc --- a post--habi\-li\-ta\-tion degree). \bibl{ANS93}{amast} Andr\'eka,H. N\'emeti,I. and Sain,I. {\em Applying Algebraic Logic to Logic} In: Algebraic Methodology and Software Technology (AMAST '93) (Proceedings of the Third International Conference on Algebraic Methodology and Software Technology, University of Twente, The Netherlands, 21--25 June 1993.) eds.: Nivat,M. Rattray,C. Rus,T. and Scollo,G., Springer-Verlag, London, Workshops in Computing series. \bibl{ANSK}{ansk} Andr\'eka,H. Kurucz,\'A. N\'emeti,I. and Sain,I. {\em Methodology of applying algebraic logic to logic} Course material of the Summer School ``Algebraic Logic and the Methodology of Applying it'', Budapest, 1994. 67pp. Preprint of \maki, 1994. A short version of this appeared as \cite{amast}. \bibl{vB91}{benthem} van Benthem,J. {\em Language in Action} North--Holland, Amsterdam, 1991. \bibl{vB96}{vb96} van Benthem,J. {\em Exploring Logical Dynamics} CSLI Publications \& Cambridge Univ. Press, 1996. \bibl{Bi89}{biro} Bir\'o,B. {\em Non-finite Axiomatizability Results in Algebraic Logic} Journal of Symbolic Logic, vol.57, 1992, p832--843. \bibl{BP89}{memoirs} Blok,W.J. and Pigozzi,D. {\em Algebraizable Logics} Memoirs of \ams, vol.77, 396pp, 1989. \bibl{Cr74}{craig} Craig,W. {\em Logic in Algebraic Form} North--Holland, Amsterdam, 1974. \bibl{Cs93}{Cs93} Csizmazia,S. {\em Databases and Cylindric Algebras} PhD dissertation \mta, 1993. \bibl{Cs95}{Cs95} Csizmazia,S. {\em Additions to ``Databases and Cylindric Algebras''} PhD dissertation \mta, 1995. \bibl{GG85}{philos} {\em Handbook of Philosophical Logic} Eds: Gabbay,D. and Guenthner,F.\\ D. Reidel Publ. Co., Dordrecht, 1985. \bibl{HM74}{hm74} Henkin,L. and Monk,J.D. {\em Cylindric Algebras and Related Structures} Proc. Tarski Symp., \ams, vol.25, 1974, p105--121. \bibl{HMTI}{hmti}Henkin,L. Monk,J.D. and Tarski,A. {\em Cylindric Algebras Part I.} North--Holland, Amsterdam, 1971. \bibl{HMTII}{hmtii}Henkin,L. Monk,J.D. and Tarski,A. {\em Cylindric Algebras Part II.} North--Holland, Amsterdam, 1985. \bibl{HT61}{ht}Henkin,L. and Tarski,A. {\em Cylindric Algebras} In Proceedings of Symp. Pure Math. Vol II. Lattice Theory, \ams, 1961, p83--113. North--Holland, Amsterdam, 1971. \bibl{Jo69}{jj} Johnson,J.S. {\em Nonfinitizability of Classes of Representable Polyadic Algebras} Journal of Symbolic Logic, vol.34, 1969, p344--352. \bibl{J\'o86}{jo86} J{\'o}nsson,B. {\em On Binary Relations} In: Proceedings of the NIH Conference on Universal Algebra and Lattice Theory (ed.:Hutchinson,G.) Laboratory of Computer Research and Technology, National Institute of Health, Bethesda, Maryland, 1986, p2--5. \bibl{LT36}{lt} Lindenbaum,A. and Tarski,A. {\em \"Uber die Beschr\"anktheit der Ausdrucksmittel deduktiven Theorien} Ergeb. Math. Kolloq. vol.7, 1936, p15--22. \bibl{M70}{mo70} Monk,J.D. {\em On an Algebra of Sets of Finite Sequences} Journal of Symbolic Logic, vol.35, 1970, p19--28. \bibl{NA93}{nean} N\'emeti,I. and Andr\'eka,H. {\em General Algebraic Logic: A Perspective on What is Logic.} In: What is a logical system (ed.:Gabbay,D.) Oxford University Press. To appear. \bibl{N91}{Ne91} N{\'e}meti,I. {\em Algebraizations of Quantifier Logics: An Introductory Overview} Shortened version in Studia Logica, vol.5(3--4) (a special issue devoted to Algebraic Logic, eds.: Blok,W.J. and Pigozzi,D.L.) 1991, p485--569. \\ Expanded version (with proofs etc.) is Preprint of \maki, 1996. \bibl{N93}{ne93} N{\'e}meti,I. {\em Algebras of Relations of Various Ranks with Applications to Logics} Technical Report No.50/1993, \maki, November 1993. (A much shorter version of this is \cite{Ne91}.) \bibl{NS95}{SagNe95} N{\'e}meti,I. and S\'agi,G. {\em Polyadic Equality Algebras, Their Axiomatizability Issues} Preprint of \maki, November 1995. \bibl{P73}{P} Pinter,C.C. {\em A Simple Algebra of First Order Logic} Notre Dame Journal of Formal Logic, vol.14(3), 1973. \bibl{S\'a95}{sagi} S\'agi,G. {\em A Warning on Schemas in Completeness Theorems} Manuscript of \maki, 1995. \bibl{Sa87}{SaFIN} Sain,I. {\em On the Search for a Finitizable (w.r.t.\ the Representables) Algebraization of First Order Logic, Parts i--ii} Technical Report No.53/1987, \maki, 1987. 58pp. \bibl{Sa87a}{S87} Sain,I. {\em Positive Results Related to the J\'onsson, Tarski--Givant Representation Problem} Expanded version of \cite{SaFIN}, 1987. \bibl{Sa92}{gabbay} Sain,I. {\em On the Problem of Finitizing First Order Logic and its Algebraic Counterpart (A survey of results and methods)} In: Proceedings of Logic Colloquium'92, (eds.: Csirmaz,L. and Gabbay,D.) To appear. \bibl{Sa93}{S9} Sain,I.\ {\em On the Search for a Finitizable Algebraization of First Order Logic (Shortened Version A)} \\ Preprint of \maki, 1988, revised in April 1993. \bibl{Sa94}{bull} Sain,I. {\em On Finitizing First Order Logic} Bull. Section of Logic (Wroclaw) 1994. vol.23(2). \bibl{SaT91}{st} Sain,I. and Thompson,R.J. {\em Strictly Finite Schema Axiomatization of Quasi-polyadic Algebras} Algebraic Logic, Proc. Conf. Budapest 1988, (eds.: And\-r\'e\-ka,H. Monk,J.D. and N\'emeti,I.) Colloq. Math. Soc. J. Bolyai vol.54, North-Holland, Amsterdam, 1991, p539--571. \bibl{Sh91}{sher} Sher,G. {\em The Bounds of Logic} MIT Press, Cambridge, Mass., 1991. \bibl{Si93}{whatnot} Simon,A. {\em What the Finitization Problem is Not} In: Algebraic Methods in Logic and in Computer Science, Proc.\ Banach Semester Fall 1991, (ed.: Rauscher,C.) Institute of Mathematics, Polish Academy of Sciences, Banach Center Publications vol.28, 1993, p95--116. (Improved version available from author.) \bibl{Ta87}{tarski} Tarski,A. {\em What are logical notions?} In: History and philosophy of logic (ed.:Corcoran,J.) vol.7 1986, p143-154. \bibl{TaG87}{tg87} Tarski,A. and Givant,S. {\em A Formalization of Set Theory without Variables} AMS Colloquium publications, vol.41, 1987, Providence, Rhode Island. \bibl{To93}{T} Thompson,R.J. {\em Complete Description of Substitutions in Cylindric Algebras and other Algebraic Logics} Institute of Mathematics, Polish Academy of Sciences, Banach Center Publications, vol.28, 1993, p327--341. \bibl{W88}{wojcicki} W\'ojcicki,R. {\em Theory of Logical Calculi (Basic Theory of Consequence Operations)} Kluwer Academic Publishers, Dordrecht, 1988. \end{thebibliography}} \end{document}