FORMATIVE PROCESSES WITH APPLICATIONS TO THE DECISION PROBLEM IN SET THEORY: ~II. POWERSET AND SINGLETON OPERATORS, FINITENESS PREDICATE\thanks{This research has been partially funded by PRIN project 2006/2007 `Large-scale development of certified mathematical proofs'.}
Domenico Cantone (corresponding author)
Dipartimento di Matematica e Informatica, Universit\`a di Catania
Viale Andrea Doria 6, I-95125 Catania, Italy.
[1cm] % %Eugenio G. Omodeo
%Dipartimento di Matematica e Informatica, Universit\`a di Trieste, Italy.
[1cm] % Pietro Ursino
In this paper we solve the satisfiability problem for a quantifier-free fragment of set theory involving the powerset and the singleton operators and a finiteness predicate, besides the basic Boolean set operators of union, intersection, and difference. % The more restricted fragment obtained by dropping the finiteness predicate has been shown to have a solvable satisfiability problem in a previous paper, by establishing for it a small model property. % To deal with the finiteness predicate we have formulated and proved a small model witness property for our fragment of set theory, namely a property which asserts that any satisfiable formula of our fragment has a model admitting a ``small'' representation. \vspace{0.2cm} \noindent {Key words}~~Satisfiability decision problem, satisfaction algorithm, Zermelo-Fraenkel set theory.
math0411227.tex
% (1) Corretto l'indirizzo di posta elettronica di Eugenio.
% (2) Ringraziato il nuovo PRIN invece di quello vecchio e di SETA.
% (3) Cambiata la locuzione "witness small model property" in
%     "small model witness property".
%
% ridefinirei la macro \st cosi`:
% \newcommand{\st}{\mid}

\documentclass[11pt]{article}

% \usepackage{setspace}

%\usepackage{amssymb,latexsym,mathrsfs,amsmath}
\usepackage{amssymb,latexsym,color,amsmath}
\usepackage[mathscr]{eucal}
\usepackage{xspace}


\newcommand{\seq}[1]{{\cal {A}} _{#1}}
\newcommand{\proof}{\noindent{\bf Proof.}~~}

% \newcommand{\mimmo}[1]{\begin{quotation}\marginpar{\vspace{0.15cm}$\bullet$}
% \hrule\vspace{1pt}\hrule\vspace{2pt}
% \noindent \textbf{MIMMO:} #1\vspace{2pt}
% \hrule\vspace{1pt}\hrule
% \end{quotation}
% }

\definecolor{grey}{rgb}{0.9, 0.9, 0.9}
\newlength{\savefboxrule}
\setlength{\savefboxrule}{\fboxrule}
\newcommand{\mimmo}[1]{
\setlength{\fboxrule}{.1cm}
\begin{quotation}
\vspace{2pt}
\noindent \fcolorbox{red}{grey}{\begin{minipage}{13cm}\textbf{MIMMO:} #1
\end{minipage}
}\vspace{2pt}
\end{quotation}
\setlength{\fboxrule}{\savefboxrule}
}

\pagestyle{myheadings}

\topmargin         -1cm
\oddsidemargin      1cm
\evensidemargin     0cm
\textheight      23.5cm
\textwidth         15cm
\parindent        0.5cm
\headsep           1cm
\headheight        12pt
\lineskip           1pt
\normallineskip     1pt
\def\baselinestretch{1}

\markboth{\scriptsize Formative processes with applications to
the decision problem in set theory}{}

\title{FORMATIVE PROCESSES WITH APPLICATIONS TO THE DECISION PROBLEM
IN SET THEORY: ~II. POWERSET AND SINGLETON OPERATORS, FINITENESS
PREDICATE\thanks{This research has been partially funded by PRIN
project 2006/2007 \emph{`Large-scale development of certified
mathematical proofs'.}}}

\author{Domenico Cantone (corresponding author)\\
\emph{Dipartimento di Matematica e Informatica, Universit\`a di Catania}\\
\emph{Viale Andrea Doria 6, I-95125 Catania, Italy.}  \\
\mbox{E-mail:} \texttt{cantone@dmi.unict.it}~~~~Phone: +39 095
7383052~~~~Fax: +39 095 330094\\[1cm]
%
%Eugenio G. Omodeo\\
%\emph{Dipartimento di Matematica e Informatica, Universit\`a di Trieste, Italy.}  \\
%\mbox{E-mail:} \texttt{eomodeo@units.it}\\[1cm]
%
Pietro Ursino\\
\emph{Dipartimento di Matematica e Informatica, Universit\`a di Catania}\\
\mbox{E-mail:} \texttt{ursino@dmi.unict.it}
}
%
% \and Eugenio G. Omodeo\thanks{Dipartimento di Matematica e Informatica,
% Universit\`a di Trieste, Italy.  \mbox{E-mail:} \texttt{eomodeo@units.it}}
% %
% \and Pietro Ursino\thanks{Dipartimento di Matematica e
% Informatica, Universit\`a di Catania, Viale Andrea Doria 6,
% I-95125 Catania, Italy. \mbox{E-mail:}
% \texttt{ursino@dmi.unict.it}}}
\date{}
\newtheorem{mydef}{Definition} % in corsivo
\newtheorem{mylemma}{Lemma} % in corsivo
\newtheorem{myproposition}{Proposition} % in corsivo
\newtheorem{mytheorem}{Theorem} % in corsivo
\newtheorem{myclaim}{Claim} % in corsivo
\newtheorem{mycorollary}{Corollary} % in corsivo
\newtheorem{myalgorithm}{Algorithm} % in corsivo
\newtheorem{myprocedure}[myalgorithm]{Procedure} % in corsivo
\newtheorem{myremarks}{Remarks} % NON in corsivo
\newtheorem{myremark}[myremarks]{Remark} % NON in corsivo
\newtheorem{myprinciple}{Principle} % in corsivo
\newtheorem{myexerc}{Exercise} % NON in corsivo
\newtheorem{myexample}{Example} % NON in corsivo
\newtheorem{myexamples}[myexample]{Examples} % NON in corsivo
\newtheorem{myproblem}{Problem} % NON in corsivo
\newtheorem{myproperty}{Property} % in corsivo

\newcommand{\cor}[1]{Corollary~{\ref{#1}}}
\newcommand{\cha}[1]{Chapter~{\ref{#1}}}
\newcommand{\sect}[1]{Sec.{\ref{#1}}}
\newcommand{\sects}[1]{Sections~{\ref{#1}}}
\newcommand{\defn}[1]{Def.$\;${\ref{#1}}}
\newcommand{\defs}[1]{Definitions~{\ref{#1}}}
\newcommand{\thm}[1]{Thm.{\ref{#1}}}
\newcommand{\lem}[1]{Lemma~{\ref{#1}}}
\newcommand{\prop}[1]{Prop.{\ref{#1}}}
\newcommand{\fig}[1]{Figure~{\ref{#1}}}
\newcommand{\figs}[1]{Figures~{\ref{#1}}}
\newcommand{\alg}[1]{Algorithm~{\ref{#1}}}
\newcommand{\rem}[1]{Remark~{\ref{#1}}}
\newcommand{\rems}[1]{Remarks~{\ref{#1}}}
\newcommand{\exa}[1]{Example~{\ref{#1}}}
\newcommand{\exas}[1]{Examples~{\ref{#1}}}
\newcommand{\exe}[1]{Exercise~{\ref{#1}}}
\newcommand{\exes}[1]{Exercises~{\ref{#1}}}
\newcommand{\GE}{\mathrm{GE}}

\newcommand{\COMMENT}[1]{}
% \newcommand{\proof}{\noindent{\bf Proof.}~~}
\newcommand{\sz}{\scriptsize}
\newcommand{\uz}{\mbox{\boldmath$0$}}
\newcommand{\esot}{{\bf (*)}~}
\newcommand{\tinyvspace}{\mbox{$\stackrel{\phantom{\_}}{\phantom{\overline{i}}}$}}

\newcommand{\disj}[2]{#1\cap #2=\emptyset}
\newcommand{\inters}[2]{#1\cap #2\neq\emptyset}
\newcommand{\card}[1]{{\left|{#1}\right|}}
\newcommand{\equivAs}
   {\:\equiv \! \! \raisebox{-0.5 ex}[0 ex][0 ex]{\tiny Def}\:}
\newcommand{\defAs}
   {\mbox{$\:= \! \! \raisebox{-0.5 ex}[0 ex][0 ex]{\tiny Def}\:$}}
\newcommand{\defFoAs}
   {\:\biimplies \! \! \raisebox{-0.5 ex}[0 ex][0 ex]{\tiny Def}\:}
\newcommand{\iffAs}
   {\;\mbox{iff}\raisebox{-0.5 ex}[0 ex][0 ex]{\tiny
Def}\:}
\newcommand{\undef}{\Omega}
\newcommand{\ling}{I\!\!L}
% \newcommand{\nats}{\mbox{\rm I}\!\mbox{\rm N}}
\newcommand{\nats}{\omega}
\newcommand{\ints}{\mbox{\rm Z}\!\!\!\mbox{\rm I}}
\newcommand{\herb}{\mbox{$\mbox{\rm I}\!\mbox{\rm H}\!\mbox{\rm I}$}}
\newcommand{\produ}{{\sf ::=}}
\newcommand{\alt}{\mbox{\tt|}}
\newcommand{\nullstr}{\epsilon}
\newcommand{\opar}{\mbox{\sf(}\,}
\newcommand{\cpar}{\,\mbox{\sf)}}
\newcommand{\bigopar}{\mbox{\large\sf(}\,}
\newcommand{\bigcpar}{\,\mbox{\large\sf)}}
\newcommand{\Bigopar}{\mbox{\Large\sf(}\,}
\newcommand{\Bigcpar}{\,\mbox{\Large\sf)}}
\newcommand{\hugeopar}{\mbox{\Huge\sf(}\,}
\newcommand{\hugecpar}{\,\mbox{\Huge\sf)}}
\newcommand{\tinyopar}{\mbox{\scriptsize\sf(}\,}
\newcommand{\tinycpar}{\,\mbox{\scriptsize\sf)}}
\newcommand{\obra}{\mbox{\sf\{}\,}
\newcommand{\cbra}{\,\mbox{\sf\}}}
\newcommand{\bigobra}{\mbox{\large\sf\{}\,}
\newcommand{\bigcbra}{\,\mbox{\large\sf\}}}
\newcommand{\Bigobra}{\mbox{\Large\sf\{}\,}
\newcommand{\Bigcbra}{\,\mbox{\Large\sf\}}}
\newcommand{\false}{{\bf f}}
\newcommand{\true}{{\bf t}}
\newcommand{\Not}{{\bf\neg}}
% \newcommand{\And}{\:\&\:}
%\renewcommand{\And}{\wedge}
\renewcommand{\And}{\wedge}
\newcommand{\Or}{{\bf\vee}}
%\renewcommand{\implies}{{\bf\rightarrow}}
\renewcommand{\implies}{{\bf\rightarrow}}
\newcommand{\revimplies}{{\bf\leftarrow}}
\newcommand{\biimplies}{{\bf\leftrightarrow}}
%\newcommand{\nor}{\stackrel{\Not}{\vee}}
\newcommand{\nor}{{\bf\downarrow}}
%\newcommand{\nand}{\stackrel{\Not}{\wedge}}
\newcommand{\nand}{{\bf\mid}}
%\newcommand{\nimplies}{\stackrel{\Not}{\implies}}
\newcommand{\nimplies}{\mbox{\boldmath$>$}}
\newcommand{\revnimplies}{\mbox{\boldmath$<$}}
%\newcommand{\nbiimplies}{\stackrel{\Not}{\leftrightarrow}}
\newcommand{\nbiimplies}{\mbox{\boldmath$+$}}
% \newcommand{\bigAnd}{\mbox{\Large\&}}
\newcommand{\bigAnd}{\bigwedge}
% \newcommand{\BigAnd}{\mbox{\huge\&}}
\newcommand{\BigAnd}{{\Large\bigwedge}}
\newcommand{\bigOr}{\bigvee}
\newcommand{\anonymous}{\_} % anonymous variable
\newcommand{\llhd}{< \hspace{-.08cm} |}
\newcommand{\e}{\mbox{$\emptyset$}}
\newcommand{\with}{\mbox{$\:{\sf with}\:$}}
\newcommand{\less}{\mbox{$\:{\sf less}\:$}}

\newcommand{\Pow}{{\mathscr{P}}}
\newcommand{\pow}[1]{\Pow({#1})}
\newcommand{\smallpow}[1]{\Pow({#1})}
\newcommand{\powAst}{\Pow^{\ast}}
\newcommand{\powast}[1]{\powAst({#1})}
\newcommand{\wt}{\,\texttt{:}\:}
\newcommand{\st}{\,\texttt{|}\:}
\newcommand{\finite}[1]{\card{#1}<\aleph_0}
\newcommand{\infinite}[1]{\card{#1}\geqslant\aleph_0}

\newcommand{\rk}{\hbox{\sf rk}\;}
\newcommand{\dom}{\hbox{\sf dom}\:}
\newcommand{\Places}{\mathcal{P}}
\newcommand{\TARGETS}{\mathcal{T}}
\newcommand{\Targets}[1]{\TARGETS({#1})}
\newcommand{\REDS}{\mathcal{F}}
\newcommand{\POWNODES}{\mathcal{Q}}
\newcommand{\symm}{\bigtriangleup}
\newcommand{\ue}{\mbox{\tt\O}}
\newcommand{\univSyn}{{\tt 1}\!\!{\tt l}}
\newcommand{\bfsubseteq}{\mbox{\boldmath$\subseteq$}}
\newcommand{\bfsupseteq}{\mbox{\boldmath$\supseteq$}}
\newcommand{\smbox}{{\scriptstyle\Box}}
%%
\newcommand{\Two}{\mbox{\large\bf 2}}
%%%
\newcommand{\cen}{&& \!\!\!\!\!\!}
\newcommand{\Wbox}{$\Box$}
\newcommand{\Bbox}{\rule{2mm}{2mm}}
\def\eod {{\unskip\nobreak\hfil\penalty50
\hskip2em\hbox{}\nobreak\hfil $\Box$
\parfillskip=0pt \finalhyphendemerits=0 \par \medskip}}
%%%
\newcommand{\newarcs}{\mathrm{\Places}}
\newcommand{\Ordinals}{\mathit{On}}
%%%
\def \R {{\mathbb R}}
\def \N {{\mathbb N}}
\def \Z {{\mathbb Z}}
\def \Q {{\mathbb Q}}
\def\qed {{\unskip\nobreak\hfil\penalty50
\hskip2em\hbox{}\nobreak\hfil \rule{2mm}{2mm}
\parfillskip=0pt \finalhyphendemerits=0 \par \medskip}}

\newcommand{\leastInf}{\mathsf{leastInf}}
\newcommand{\PLACES}[1]{(#1)_{{\textit{\scriptsize places}}}}
\newcommand{\NODES}[1]{(#1)_{{\textit{\scriptsize nodes}}}}
\newcommand{\PN}[1]{\mathcal{N}(#1)}

\newcommand{\mypsi}{\Phi}

% da sopprimere prima o poi
\newcommand{\tbc}{\centerline{[$\cdots\cdots$ TO BE ELABORATED
$\cdots\cdots$]}}
\newcommand{\unknownpage}{p.\ldots[?]}
\newcommand{\str}{\sc}
%

\newcommand{\epigraph}[2]{{\small\begin{quote} {\em #2 }
   {\unskip\nobreak\hfil\penalty50 \hskip2em\hbox{}\nobreak\hfil (#1)
\parfillskip=0pt \finalhyphendemerits=0 \par \medskip}
\end{quote}}\noindent}

% macro per la gestione di tableaux
\newcommand{\stack}[2]{
\mbox{
\begin{tabular}{c}
   $#1$ \\
   $#2$
\end{tabular}
}}
%
\newcommand{\Ker}{{\bf K}}

\newcommand{\trcl}{\mathsf{TrCl}}
\newcommand{\Finite}{\mathit{Finite}}


\newenvironment{des}{
\begin{list}
   {$\bullet$}
   {\topsep = 0 mm
\labelwidth = 3 mm \labelsep = 2 mm
\parsep = 0.4 mm
\itemsep = \parskip
\leftmargin = 5 mm} }{\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newenvironment{example}{\noindent{\bf Example.~}}{}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\bfeq}{\mbox{\bf =}}
\newcommand{\bfneq}{\mbox{\bf $\not$=}}


\newcommand{\tyus}{\mbox{\boldmath$\univSyn\!\circ\! s$}}
\newcommand{\tys}{\mbox{\boldmath$s$}}
\newcommand{\tysu}{\mbox{\boldmath$s\!\circ\!\univSyn$}}
\newcommand{\tyu}{\mbox{\boldmath$\univSyn$}}
\newcommand{\tyi}{\mbox{\boldmath$\Iota$}}
\newcommand{\tyz}{\mbox{\boldmath$\ue$}}
\newcommand{\tyx}{\phantom{\tyus}}
\newcommand{\tyt}{\mbox{\boldmath$t$}}

% \doublespacing

\begin{document}
\maketitle

\newpage
%\thispagestyle{plain}
% \baselineskip=.9cm

\newcommand{\tbd}{\centerline{------TO BE DONE------}}
\newcommand{\MLSSP}{\textnormal{\textsf{MLSSP}}\xspace}
\newcommand{\MLSSPF}{\textnormal{\textsf{MLSSPF}}\xspace}

\begin{abstract}
In this paper we solve the satisfiability problem for a
quantifier-free fragment of set theory involving the powerset and the
singleton operators and a finiteness predicate, besides the basic
Boolean set operators of union, intersection, and difference.
%
The more restricted fragment obtained by dropping the finiteness
predicate has been shown to have a solvable satisfiability problem in
a previous paper, by establishing for it a small model property.
%
To deal with the finiteness predicate we have formulated and proved a
\emph{small model witness property} for our fragment of set theory,
namely a property which asserts that any satisfiable formula of our
fragment has a model admitting a ``small'' representation.

\vspace{0.2cm}

\noindent {\bf Key words}~~Satisfiability decision problem,
satisfaction algorithm, Zermelo-Fraenkel set theory.
\end{abstract}



\newpage

% \vspace{0.2cm}



\section{Introduction}
\label{introd}

Since the late seventies, the decision problem in set theory has been
investigated very actively, as part of a project aiming at the
mechanical formalization of mathematics using a proof verifier based
on the set-theoretic formalism \cite{OS02,COSU03,OCPS06}.

The large body of decidability results gave rise to the field of
\emph{Computable Set Theory}; the reader is referred to
\cite{CFO89,COP01} for a very comprehensive account.

Using specialized techniques, several fragments of set theory were
shown to have a solvable satisfiability decision problem.  But it soon became clear
that in order to combine such decidable fragments into more comprehensive ones,
more sofisticated methods were needed, which would make the growing
mass of technicalities involved more manageable.

Such methods began to emerge in \cite{Can91} and gained perspicuity and uniformity of approach in \cite{CU97,COU02}; they rely on a careful analysis of the formation process of families of pairwise
disjoint sets. This analysis brought into light decidable conditions which are necessary and
sufficient to ensure satisfiability within a collection of set-theoretic formulae denoted
\MLSSP (viz., \emph{``Multi-Level Syllogistic with Singleton and
Powerset operators''}).
%
Specifically, \MLSSP is the quantifier-free language of set theory,
consisting of all propositional combinations of literals involving the set
operators of union, intersection, difference, powerset, finite
enumerations, and the set relators of equality, membership, and
inclusion.



% type $\mathit{Finite}(x)$, asserting that the cardinality of the
% set $x$ is finite, as well as literals of type
% $\Not\,\mathit{Finite}(x)$, asserting that $x$ is infinite.
% smaller than $\aleph_0$\/.  Since we admit negation among
% propositional connectives, we can also assert that a set $x$ is
% infinite, by means of the literal $\Not\,\mathit{Finite}(x)$.

% The main result of the paper is that also the set-theoretic language
% \MLSSPF has a decidable satisfiability problem.

Let us recall that the satisfiability problem for \MLSSP was shown to be
decidable by singling out a computable function $c$ which associates
a positive integer with every formula of \MLSSP so that the following
``small model property'' holds: any satisfiable
\MLSSP-formula $\mypsi$ can be satisfied by a set assignment mapping the variables of
$\mypsi$ into sets of finite rank bounded by $c(\mypsi)$.
Decidability then follows readily, in view of the facts
that finitely many such assignments exist, that their collection can be
effectively generated, and, additionally, for every such assignment one can
effectively test whether or not it satisfies $\mypsi$. As an immediate
by-product, one has that any satisfiable \MLSSP-formula is satisfied
by an assignment of finite sets (of bounded rank) to the variables.

A natural question then arises: how can one tackle the
satisfiability problem regarding a collection of formulae which extends \MLSSP and
comprises formulae satisfiable only by means of assignments some of whose images are
\emph{infinite} sets?

The present paper contributes to answering this question by providing a
positive solution to the satisfiability problem for the language
\MLSSPF which extends \MLSSP by a predicate $\Finite(x)$ asserting
that its argument $x$ has finite cardinality. Obviously, since
the negated predicate $\neg \Finite(x)$ expresses
that $x$ is an infinite set, \MLSSPF cannot enjoy the above-described
small model property; but,
%
% Plainly, \MLSSPF can not enjoy the small model property, since there
% are satisfiable \MLSSPF-formulae, such as the one which simply asserts
% that a given set is not finite, which are not satisfied by any
% finite assignment.
%
on the other hand, we will show that \MLSSPF enjoys a less demanding property,
called ``small model witness property''
(cf.\ \cite{Urs06}), asserting the existence of a computable function
$c$ defined over the formulae of \MLSSPF and such that any satisfiable
\MLSSPF-formula $\mypsi$ has a ``witness satisfying assignment'' of
finite rank bounded by $c(\mypsi)$.  Though a witness satisfying
assignment for a formula $\mypsi$ is not required to directly satisfy
$\mypsi$, it represents a satisfying assignment for $\mypsi$ through a
``pumping mechanism'' which will be illustrated at length in the
paper.  Additionally, since one can test algorithmically whether a
given assignment of finite rank is a witness satisfying assignment for
a formula $\mypsi$, decidability of the satisfiability problem for
\MLSSPF follows.

% Nevertheless, we will show that \MLSSPF enjoys a ``small model witness
% property'' of the kind described in \cite{Urs06}, which is a weaker form
% of the small model property.  The small model witness property for
% \MLSSPF asserts the existence of a computable function $c$ defined
% over the formulae of \MLSSPF such that any satisfiable \MLSSPF-formula
% $\mypsi$ can be satisfied by a set assignment (possibly infinite over
% some variables) which has a ``witness'' assignment for $\mypsi$ of
% finite rank bounded by $c(\mypsi)$.  Though a witness assignment for
% $\mypsi$ is not required to directly satisfy $\mypsi$, we will show that
% it can be used as a starting point for the generation of a set
% assignment satisfying $\mypsi$.  Additionally, we will also show that
% for any assignment whose rank is bounded by $c(\mypsi)$, we can
% algorithmically test whether it is a witness assignment for $\mypsi$.
% Since the collection of witness assignments of bounded rank is finite,
% decidability of the satisfiability problem for \MLSSPF will follow.

To achieve these results we will rely on the notion of formative
process introduced in \cite{COU02} and \cite{COP01}, which enables one
to characterize any given collection of sets by means of a (transfinite)
sequence of construction steps.  By suitable manipulations, namely through
the pumping technique mentioned above, a formative process for a witness
satisfying assignment can be turned into a formative process for a(n
infinite) satisfying assignment.

We expect that similar techniques will demonstrate very useful in the
investigation of the satisfiability problem for various fragments of
set theory involving operators such as the unary union $\bigcup$ and
the Cartesian product $\times$, since these can be used to express
satisfiable formulae such as
\[
x \subseteq \bigcup x \wedge x \neq \emptyset  \text{ ~~~and~~~ }
x \times x \subseteq x \wedge x \neq \emptyset \,,
\]
which admit only infinite satisfying assignments.

\smallskip

The paper is organized as follows.  In Section~\ref{se_MLSSPF}, after
reviewing some basic set-theoretic notions and terminology, we give a
precise definition of the language \MLSSPF of our
interest and briefly discuss its satisfiability problem.
%
Then in Section~\ref{se_boards_proc} we present and extend the notion
of $\Places$-boards and the technique of formative processes.  We also
introduce the notion of \emph{pumping path} and prove a related
\emph{pumping theorem} which is then used in the subsequent
Section~\ref{se_fin_infin} as a basic tool for showing how to produce
a satisfying assignment from a witness satisfying assignment.
%
Section~\ref{conclusions} contains some closing remarks and hints at
possible directions of future research.
%
Finally, an appendix containing the proof of a technical result used
in Section~\ref{se_fin_infin} concludes the paper.

% of basic importance
% %
% The techniques which allow to produce a satisfying assignment from a
% ``witness'' satisfying assignment are developed at length in
%  and in an appendix.
% %
% Finally, in Section~\ref{conclusions} we draw our conclusion and give
% some hints to some directions for future research.

% \tbd

%
% DA FARE:
%
% -INQUADRAMENTO STORICO DEL PROBLEMA
% -CONCLUSIONI, CON FUTURI PROBLEMI
% -ORGANIZZAZIONE DEL LAVORO
%
% \section{Introduction}                                                                                                                                                    �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
% \section{The satisfiability problem for \MLSSPF}                                                                                                                                                  �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
%     \subsection{Basic notions}                                                                                                                                                    �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
%     \subsection{\MLSSPF: assignments, models, and its satisfiability                                                                                                                                                  �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
%     \subsection{Decision tests and Venn partitions}                                                                                                                                                   �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
% \section{Syllogistic boards and formative processes}                                                                                                                                                  �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
%     \subsection{Basics on syllogistic boards}                                                                                                                                                 �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
%     \subsection{Formative processes and basic events}                                                                                                                                                 �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
%     \subsection{Historical profile of an infinite block}                                                                                                                                                  �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
%   \subsubsection{Pumping paths}                                                                                                                                                   �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
%   \subsubsection{Grand events and local trash}                                                                                                                                                    �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
% \section{A finite representation of an infinite model}                                                                                                                                                    �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
% \section{Conclusions}                                                                                                                                                 �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex
%
% \appendix{Proof of Theorem \ref{upwards}}                                                                                                                                                 �/Users/cantone/Documents/RICERCA/PUBBLICAZIONI/PAPERI/workingPapers/COLLABORAZIONI/PIERO/Formative Processes II/FormativeProcesses061029.tex


% This result is achieved through an application of the theory of
% formative prcesses (see \cite{COU02},
% \cite{COP01}, and \cite{Urs06} for a more
% sophisticated approach).  Indeed, although a language can force a
% model to be of infinite size in some cases the structure of the
% formative process which generates it satisfy some regularity
% properties.
%
% Roughly speaking, whenever a formative process create an infinite
% assignment it must follow an infinite number of times a finite
% procedure.  As soon as such a procedure is singled out, ones can
% assert that even if at that stage a model is not available yet, it
% could be construct.  This is enough to assert that the above
% assignment witnesses the existence of a model, or, in other terms,
% that the above assignment is a finite representation of an infinite
% model.

% In case of \MLSSPF the assignment which witnesses the existence of a
% model is the same of that one found in \cite{COU02},
% therefore we can exhibit a concrete extimation of the rank behind
% which such an assignment can be found.
%
% The first part of the article is devoted to show that a model of an
% \MLSSPF-formula must have some regularity properties.
%
% In the second part these properties are exploited in order to prove
% that the small model witness property holds for \MLSSPF.
% \newpage


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{The satisfiability problem for \MLSSPF}
\label{se_MLSSPF}

Before giving the precise definition of the language \MLSSPF and
discussing its satisfiability problem, we review some basic set-theoretic
concepts and terminology.

\subsection{Basic notions}\label{basics}
Our considerations will refer to the von Neumann's
cumulative hierarchy \mbox{\boldmath$\mathcal{V}$}, often regarded as the intended model of
Zermelo-Fraenkel set theory, also referred to as ``$\{\:\mbox{\rm sets}\:\}$'' throughout the paper,
which is defined in the following recursive manner:
\[
\begin{array}{rcll}
    {\cal V}_0 & = & \emptyset\,,  \\[0.2cm]
    {\cal V}_{\alpha+1} & = & \pow{{\cal V}_\alpha}\,,  &
      \hbox{{for each ordinal} $\alpha$,} \\[0.2cm]
    {\cal V}_\lambda & = & \bigcup_{\mu < \lambda} {\cal V}_\mu \,, &
      \hbox{{for each limit ordinal} $\lambda$,} \\[0.2cm]
    \mbox{\boldmath$\mathcal{V}$} & = & \bigcup_{\mu \in \Ordinals} {\cal V}_{\mu}
\end{array}
\]
(where $\pow{S}$ denotes the powerset of $S$ and $\Ordinals$ is the
class of all ordinal numbers --- recall
that a \textsc{limit} ordinal is an ordinal which differs from $0$ and from any \textsc{successor} ordinal, of the form $\alpha + 1$).  Then we can readily define a rank
function $\;\rk$ on \mbox{\boldmath$\mathcal{V}$} by putting
\[
\begin{array}{rcl}
\rk (S) & \defAs & \min \{\, \alpha \in \Ordinals \st S \in
\mathcal{V}_{\alpha +1}\,\}\,,
\end{array}
\]
for each $S \in \mathcal{V}$ (see \cite{Jec78} for further details).
% In other words, we will operate only with sets which are members of
% the class $\mathcal{V}$.
%
% This has been done in order to prevent particular pathologies which
% can conflict with our methods (for example assignments which involve
% inaccessible cardinals; see \cite{Jec78}).

\smallskip

A set $S$ is \textsc{transitive} if $\bigcup S\subseteq S$, i.e., every member of a member of $S$
belongs to $S$.  The \textsc{transitive closure} $\trcl(S)$ of
a set $S$ is the minimal transitive set containing $S$, i.e.,
\[
\trcl(S) \defAs \bigcap \{ T \in \mbox{\boldmath$\mathcal{V}$} \st S \subseteq T
\,\And\, T \hbox{ is transitive} \}\,.
\]

A set $S$ such that $\trcl(S)$ is finite is said to be
\textsc{hereditarily finite}. By $\omega$ we denote the rank of the
collection of all hereditarily finite sets. It can be shown that
$\omega$ is the smallest infinite (limit) ordinal.

We also recall that a partition $\Sigma$ is a collection of pairwise
disjoint nonnull sets, called \textsc{blocks} of $\Sigma$.  The union $\bigcup \Sigma$ of a
partition $\Sigma$ is the \textsc{domain} of $\Sigma$.  If the domain
of a partition $\Sigma$ is transitive, then we will say that $\Sigma$
is a \textsc{transitive partition}.

For the sake of completeness, we briefly review the notations which
will be used in the rest of the paper.  We denote: by $X^Y$\/, the set
of all functions $f$ from $Y$ into $X$\/; by $f[S]$\/, the multi-image
$\{Y\st (\exists\,z\in S) Y=f(z)\}$\/; by $R\circ S$\/, the map
composition of $R$ and $S$\/.  To describe a function $f=\{\langle
X,Y_{X}\rangle\st X\in Z\}$\/, we will interchangeably use the
notation $f=\left\{Y_{X}\right\}_{X\in Z}$ and the notation
$X\stackrel{f}{\mapsto} Y_{X}$ (\/$X\in Z$\/); moreover, when $Z$ is
an ordinal and accordingly $f$ is a $Z$-sequence, we will make use of
the notation $f=\left( Y_{X} \right)_{X<Z}\:$\/.  \COMMENT{To briefly
indicate that two sets $x,y$ are {\em not} disjoint, i.e., $x\cap
y\neq\emptyset$\/, we write $x\ni\in y$\/.}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{\MLSSPF: assignments, models, and its satisfiability problem}
\label{sse_MLSSPF}

The syntax of the quantifier-free language \MLSSPF is defined as
follows.  The symbols of \MLSSPF are:
\begin{itemize}
\item infinitely many variables $x, y, z$, \ldots;

\item the constant symbol $\emptyset$;

\item the set operators $\cdot\cup\cdot$, $\cdot\cap\cdot$, $\cdot\setminus\cdot$,
$\{\cdot,\ldots,\cdot\}$, and $\Pow(\cdot)$;

\item the set predicates $\cdot\subseteq\cdot$, $\cdot=\cdot$,
$\cdot\in\cdot$, and $\Finite(\cdot)$.
\end{itemize}
%
The set of \MLSSPF-\textsc{terms} is the smallest collection
satisfying the following conditions:
\begin{itemize}
\item all variables and the constant $\emptyset$ are \MLSSPF-terms;

\item if $s$ and $t$ are \MLSSPF-terms, so are $s \cup t$, $s \cap
t$, $s \setminus t$, and $\Pow(s)$;

\item if $s_{1},\ldots,s_{n}$ are \MLSSPF-terms, so is $\{s_{1},\ldots,s_{n}\}$.
\end{itemize}


\MLSSPF-\textsc{atoms} have the form $s\subseteq t$, $s=t$, $s\in t$,
and $\Finite(s)$, where $s, t$ are \MLSSPF-terms.

\MLSSPF-\textsc{formulae} are propositional combinations of \MLSSPF-atoms.
%
\MLSSPF-\textsc{lit\-er\-als} are \MLSSPF-atoms and their
negations.

\smallskip

The semantics of \MLSSPF is defined in the obvious way.  A \textsc{set
assignment} $M$ over a collection $V$ of variables is any map from $V$
into the universe $\mathcal{V}$ of all sets (in symbols, $M \in
\mathcal{V}^{V}$ or $M \in \{\:\mbox{\rm sets}\:\}^{V}$).  The rank of a set
assignment $M$ over a collection $V$ of variables is given by
\[
\begin{array}{rcl}
\rk (M) & \defAs & \max_{v \in V} ~\rk (Mv)\,.
\end{array}
\]
%
If $V$ is the collection of variables occurring in an \MLSSPF-formula
$\mypsi$, then a set assignment $M$ over $V$ is said to \textsc{satisfy}
$\mypsi$ if the sentence $\mypsi^{M}$ obtained by substituting in $\mypsi$
each variable $x$ by its interpretation $Mx$ is true, where the operators
and predicates in $\mypsi$ are interpreted in the standard way.  We will call
any set assignment which satisfies a given \MLSSPF-formula
$\mypsi$ a \textsc{model} for $\mypsi$.  When $\mypsi$ has a model, we
will say that $\mypsi$ is \textsc{satisfiable}.

The \textsc{satisfiability problem} for \MLSSPF is the problem of
establishing whether any given \MLSSPF-formula is satisfiable.

By using a normalization procedure of the kind described in \cite[pp.\
96--99]{CFO89}, the satisfiability problem
for \MLSSPF can easily be reduced  to the satisfiability problem for
\textsc{normalized conjunctions} of \MLSSPF, namely conjunctions of
literals of the following types:
%?\begin{gather}
\[
\begin{array}{@{~~~~~~}l@{~~~~~~}l@{~~~~~~}l@{~~~~~~}l@{~~~~~~}l}
      x=y\/, & x\neq y\/, & x=\emptyset \/, & x=y \cup z \/, & x=y \cap z\/,\\
      x=y \setminus z\/, & x \subseteq y \/, & x \not\subseteq y \/, & x\in y\/, & x\notin y\/,\\
      x=\pow{y} \/, & x=\{y_{1},\dots,y_{H}\}\/, & \Finite(y)\/, &
      \neg \Finite(y)\/.
\end{array}
\]
%?\label{literals}\tag{$\mathbf{\dagger}$}
%?\end{gather}

By dropping from \MLSSPF the literals involving the finiteness
predicate, one obtains the theory \MLSSP, whose decision problem has
been solved in \cite{Can91} and later revisited in \cite{COU02} with
the approach relying on formative processes.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Decision tests and Venn partitions}
\label{sse_Venn}

The decidability of \MLSSP has been shown in \cite{Can91,COU02} by
proving that \MLSSP enjoys a \textsc{small model property}.  This
amounts to proving that there exists a computable function $c$ defined
over the collection of \MLSSP-formulae such that any satisfiable
\MLSSP-formula $\mypsi$ has a model of rank bounded by $c(\mypsi)$.
Therefore, to test the satisfiability of an \MLSSP-formula $\mypsi$
involving the variables $V_{\mypsi}$, one could execute the following
procedure:

\bigskip

\begin{tabular}{@{\,\,\,}r@{\!\!\!\!\!}l@{\,\,\,}}

    1. &\qquad \textbf{for each} set assignment $M$ over $V_{\mypsi}$,
    whose rank is limited by $c(\mypsi)$ \textbf{do}\\

    2.  &\qquad \qquad \textbf{if} $M$ satisfies $\mypsi$
    \textbf{then}\\

    3. &\qquad \qquad \qquad \textbf{return} ``$\mypsi$ is
    satisfiable''\\

    4. &\qquad \textbf{return} ``$\mypsi$ is unsatisfiable''

\end{tabular}

\bigskip

The effectiveness of the above procedure follows immediately from the
fact that there are only finitely many set assignments over $V_{\mypsi}$
of finite bounded rank (and these can be effectively generated) and,
additionally, it can be effectively verified whether any such set
assignment satisfies the formula $\mypsi$.

In the case of \MLSSPF, we will not be able to prove a small model
property of the kind seen for \MLSSP, since there are satisfiable
\MLSSPF-formulae which admit only models of infinite rank (e.g.,
$\neg\Finite(x)$).  Thus, we will only prove a weaker property for
\MLSSPF, the \textsc{small model witness property}, which still yields
the decidability of the satisfiability problem for \MLSSPF. To be more
specific, we will show that there exists a computable function $c'$,
defined over the the collection of \MLSSPF-formulae, such that for any
satisfiable \MLSSPF-formula $\mypsi$ there exists a (witness) set
assignment $M$ over the variables $V_{\mypsi}$ of $\mypsi$, having finite
rank bounded by $c'(\mypsi)$, such that, by means of a ``pumping
process'' to be defined later, $M$ can be transformed into a set
assignment $M'$ which satisfies $\mypsi$.  Since, as will be shown
later, one can effectively test whether a set assignment over
$V_{\mypsi}$ of finite rank can be pumped into a model for $\mypsi$, the
decidability of the satisfiability problem for \MLSSPF will follow.

\smallskip

For the purpose of studying the satisfiability problem for
\MLSSPF, it is helpful to associate with any set
assignment $M$ over $V$ its \textsc{Venn partition} $\Sigma_{M}$,
defined by
\[
\Sigma_{M} \defAs
\Big\{\:\bigcap_{v\in U}M\,v \setminus \bigcup_{v\in V
\setminus U} M\,v  \;\wt\;\;
U \subseteq V\;
\hbox{~~\put(0,-8.5){\line(0,0){24}}~}
\;\;U\neq\emptyset\:\Big\} \setminus \Big\{\:\emptyset\:\Big\}\,,
\]
i.e., the coarsest partition of $\bigcup_{v \in V} M\,v$ induced by
the sets $M\,v$, for $v$ in $V$.

It is also convenient to define the map $\Im_{M}: V \rightarrow
\pow{\Sigma_{M}}$, where
\[
\Im_{M}(v) = \{\sigma \in \Sigma_{M} \st
\sigma \subseteq M\,v\}\,, \text{ for $v$ in $V$,}
\]
so that $M\,v = \bigcup \Im_{M}(v)$ holds, for each $v$ in $V$.

A basic technique to prove the decidability result of our interest
consists in transforming a given model of an \MLSSPF-formula $\mypsi$
into a witness set assignment for $\mypsi$ of bounded rank.
Therefore, we need to find appropriate ways to manipulate set
assignments.

A set assignment $M$ over $V$ can be manipulated through its
associated Venn partition $\Sigma_{M}$ as follows.  Let $\Sigma'$ be
any partition of the same cardinality as $\Sigma_{M}$ and let $\beta:
\Sigma_{M} \rightarrow \Sigma'$ be a \emph{bijection}.  Then we define
a set assignment $M'$ over $V$ by putting
\[
M'\,v \defAs \bigcup \beta[\Im_{M}(v)]\,, \text{ for $v$ in $V$.}
\]
Plainly, the Venn partition of $M'$ is just $\Sigma'$.

Next, let us assume that $M$ satisfies an \MLSSPF-normalized
conjunction $\mypsi$.

Under which conditions on $\Sigma'$ and $\beta$ can we infer that
the formula $\mypsi$ is also satisfied by $M'$\,?

If $\mypsi$ involves only literals of the form
\begin{equation}
    \label{eq:S}
\begin{array}{@{~~~~~~}l@{~~~~~~}l@{~~~~~~}l@{~~~~~~}l}
      x=y\/, & x\neq y\/, & x=\emptyset \/, & x=y \cup z \/,\\
      x=y \cap z\/, & x=y \setminus z\/, & x \subseteq y \/, & x \not\subseteq y \/,
\end{array}
\end{equation}
then it easily follows that $M'$ satisfies $\mypsi$, without
requiring any particular condition on $\Sigma'$ and $\beta$.

If, in addition to literals of type (\ref{eq:S}), the conjunction
$\mypsi$ involves also literals of type
\begin{equation}
    \label{eq:MLSSP}
\begin{array}{@{~~~~~~}l@{~~~~~~}l@{~~~~~~}l@{~~~~~~}l}
      x\in y\/, & x\notin y\/, & x=\pow{y} \/, & x=\{y_{1},\dots,y_{H}\}\/,
\end{array}
\end{equation}
then in order for $M'$ to satisfy $\mypsi$ we require that the
following three conditions hold (a proof of this fact can be found
in \cite[Lemma 10.1]{COU02}):
\begin{description}
%
    \item[Condition 1:] \emph{$\Sigma'$ $\in$-simulates $\Sigma_{M}$ via
    $\beta$}, i.e., $\bigcup \beta[X] \in \bigcup \beta[Y]$ if and
    only if $\bigcup X \in \bigcup Y$, for $X,Y \subseteq \Sigma_{M}$;

    \item[Condition 2:] \emph{$\Sigma'$ $\Pow$-simulates $\Sigma_{M}$
    via $\beta$}, i.e., $\bigcup \beta[X] = \pow{\bigcup \beta[Y]}$, if
    $\bigcup X = \pow{\bigcup Y}$, for $X,Y \subseteq \Sigma_{M}$;

    \item[Condition 3:] \emph{$\Sigma'$ $L$-simulates $\Sigma_{M}$ via
    $\beta$}, i.e., $\bigcup \beta[X] =
    \left\{\bigcup\beta[Y_{1}]\,,\ldots\,,\bigcup\beta[Y_{L}]\right\}$,
    if $\bigcup X = \left\{\bigcup Y_{1}\,,\ldots\,,\bigcup
    Y_{L}\right\}$, for $X,Y_{1},\ldots,Y_{L} \subseteq \Sigma_{M}$,
    where $L$ is an upper bound for the value $H$ in each literal of
    type $x=\{y_{1},\dots,y_{H}\}$ in $\mypsi$.
%
\end{description}

If we further assume that besides literals of type (\ref{eq:S})
and (\ref{eq:MLSSP}) the formula $\mypsi$ contains also literals of
the form $\Finite(y)$ and $\neg \Finite(y)$, then $M'$ satisfies
$\mypsi$ if, in addition to Conditions 1--3, also the following
condition holds:
\begin{description}
%
    \item[Condition 4:] $\beta(\sigma)$ is finite if and only if
    $\sigma$ if finite, for $\sigma \in \Sigma_{M}$.
%
\end{description}

\bigskip

% \centerline{\textbf{TO ADD: HOW TO MANIPULATE PARTITIONS}}

\bigskip

In fact, it is convenient to include among the Venn regions associated
with $M$ also an ``outer'' disjoint region $\mathcal{E}_{M}$, defined
in such a way that $\Sigma_{M} \cup \{\mathcal{E}_{M}\}$ is a
transitive partition whose domain is the transitive closure of the set
$\{M\,v \,:\, v \in V\}$, namely
\[
\mathcal{E}_{M} = \trcl(\{M\,v \st v \in V\}) \setminus
\bigcup \Sigma_{M}\,.
\]

% For the sake of completeness, we recall that a partition $\Sigma$ is a
% collection of pairwise disjoint sets called \textsc{blocks}
%
% In general, given a partition $\Sigma$
%
%
% A partition $\Sigma$ such that its \textsc{domain} $\bigcup \Sigma$ is
% transitive is called \textsc{transitive partition}.

% Given a partition $\Sigma$, i.e., a collection of pairwise disjoint
% sets called \textsc{blocks}, the union $\bigcup \Sigma$ of its blocks
% will be called the \textsc{domain} of $\Sigma$.  If the domain of a
% partition $\Sigma$ is transitive, i.e., if every member of a member of
% $\bigcup \Sigma$ belongs to $\bigcup \Sigma$ (in symbols
% $\bigcup\bigcup\Sigma\subseteq\bigcup\Sigma$), then the partition
% $\Sigma$ will be called a \textsc{transitive partition}.

% Transitive partions will interest us in connection with the
% satisfiability problem for \MLSSPF described above.

In the study of transitive partitions, we will make use of
\emph{$\Places$-boards} and \emph{formative processes}, conceptual
tools already introduced in \cite[Chapter 9]{COP01} and treated in
greater depth, but in slightly different terms, in \cite{COU02}.
In the next section we review the definitions and basic facts related
to $\Places$-boards and formative processes, suitably extended for
the purpose of properly dealing with infinite blocks.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Syllogistic boards and formative processes}
\label{se_boards_proc}

\subsection{Basics on syllogistic boards}
% We denote: by $X^Y$\/, the set of all functions $f$ from $Y$ into
% $X$\/; by $f[S]$\/, the multi-image $\{Y\st (\exists\,z\in S)
% Y=f(z)\}$\/; by $R\circ S$\/, the map composition of $R$ and $S$\/.
% To describe a function $f=\{\langle X,Y_{X}\rangle\st X\in Z\}$\/, we
% will interchangeably use the notation $f=\left\{Y_{X}\right\}_{X\in
% Z}$ and the notation $X\stackrel{f}{\mapsto} Y_{X}$ (\/$X\in Z$\/);
% moreover, when $Z$ is an ordinal and accordingly $f$ is a
% $Z$-sequence, we will make use of the notation $f=\left( Y_{X}
% \right)_{X<Z}$\/.  \COMMENT{To briefly indicate that two sets $x,y$
% are {\em not} disjoint, i.e., $x\cap y\neq\emptyset$\/, we write
% $x\ni\in y$\/.}


\label{basicsOnboards} We consider a \emph{finite} set $\Places$,
whose elements we will call \textsc{places} and whose subsets we will
call \textsc{nodes}.  We assume that $\disj{\Places}{\pow{\Places}}$,
so that no node is a place, and vice versa.  We will use these places
and nodes as the vertices of a directed bipartite graph $\mathcal{G}$
of a special kind, which we will call a \textsc{$\Places$-board}.  The edges
issuing from each place $q$ are, mandatorily, all pairs $q,B$ such
that $q\in B\subseteq \Places$\/.  The remaining edges of
$\mathcal{G}$ must lead from nodes to places; hence, $\mathcal{G}$ is
fully characterized by the function
\[
\TARGETS\:\in\:\pow{\Places}^{\pow{\Places}}
\]
associating with each node $A$ the set of all places $t$ such that
$\langle A,t\rangle$ is an edge of $\mathcal{G}$\/.  The elements of
$\Targets{A}$ are called the \textsc{targets} of $A$\/.  We will
usually represent $\mathcal{G}$ simply by $\TARGETS$.

Places and nodes of a $\Places$-board are meant to represent the
blocks $\sigma$, and the subsets $\Gamma$ (or, quite often, their
unionsets $\bigcup\Gamma$), of a transitive partition $\Sigma$,
respectively. Thus, if we indicate by $q^{(\bullet)}$ the block
which corresponds to the place $q$, and by $B^{(\bullet)}$ the set
which corresponds to the node $B$, our understanding is that
\begin{itemize}
\item $q^{(\bullet)}\neq\emptyset$, for all $q\in\Places$\/;
\item $q^{(\bullet)}\cap p^{(\bullet)}=\emptyset$ when $q\neq p$,
for all $q,p\in\Places$\/;
\item $B^{(\bullet)}$ is the sub-partition $\{q^{(\bullet)}\wt q\in
B\}$ of the partition
$\Places^{(\bullet)}=\Sigma$\/, for all $B\subseteq \Places$\/;
\item every element of any element of a block in
$\Places^{(\bullet)}$, belongs to a block in
$\Places^{(\bullet)}$.
\end{itemize}
Moreover, the intended meaning of $t\in\Targets{A}$ is that
$\inters{t^{(\bullet)}}{\powast{A^{(\bullet)}}}$\/, where the
following shorthand notation is used:
\[
\begin{array}{rcl}
\COMMENT{U\ni\in V & \defFoAs & \inters{U}{V}, \\} \powast{X} &
\defAs & \{\,v\subseteq\bigcup X\st(\forall\,u\in X)\inters{u}{v}\,\}.
\end{array}
\]
More precisely, \emph{not only
$\inters{t^{(\bullet)}}{\powast{A^{(\bullet)}}}$ must hold when
$t\in\Targets{A}$\/, but also
$s^{(\bullet)}\cap\powast{A^{(\bullet)}}=\emptyset$ when
$s\in\Places\setminus\Targets{A}$.}


\begin{mydef}\rm
A transitive partition $\Sigma$ is said to
\textsc{comply with} $\mathcal{G}$ via $q\mapsto
q^{(\bullet)}$, where $\mathcal{G}$ is a
$\Places$-board,
$q\mapsto q^{(\bullet)}$ belongs to
$\Sigma^{\Places}$
and $\TARGETS (A)=\{q\in\Places\st\powast{A^{(\bullet)}}
\cap q^{(\bullet)} \neq \emptyset\}$, if the latter function satisfies all the
constraints associated with $\mathcal{G}$, as indicated above (in
particular, this requires $q\mapsto q^{(\bullet)}$ to be
injective).
\eod\end{mydef}

Any such board is said to be \emph{induced} by $\Sigma$
(for short, a \emph{$\Sigma$-board}).
We denote a transitive $\Sigma$-board by a couple $(\Sigma,\mathcal{G})$,
where $\Sigma$ is a transitive partition and
$\mathcal{G}$ is the induced $\Places$-board.

For the purposes of this paper, some additional structure must be
superimposed on $\Places$-boards:

\begin{mydef}\rm
A $\Places$-board $\mathcal{G}=(\TARGETS,\REDS,\POWNODES)$
is said to be \textsc{colored} when it has
\begin{itemize}
\item a designated set $\REDS$ of places,
\item a designated set $\POWNODES$ of nodes, such that
$D\in\POWNODES$ holds whenever $D\subseteq B\in\POWNODES$ \\ (in
short, $\bigcup\Pow[\POWNODES]\subseteq\POWNODES$ ), and
\item a target function $\TARGETS$.
\end{itemize}
The places in $\REDS$ are said to be \emph{red}, the ones in
$\Places\setminus\REDS$ are said to be \emph{green}; the nodes
in $\POWNODES$ are called \emph{$\Pow$-nodes}.
A node is red if all places in it are red, and
green otherwise; a list of vertices is
green if all vertices lying on it are green.
\eod\end{mydef}

Assume that $\Phi$ belongs to \MLSSP,
and let
${\mathcal M}\in\{\:\mbox{\rm sets}\:\}^{{\mathcal X}_{\Phi}}$
be a set-valued assignment defined on the collection
${\mathcal X}_{\Phi}$
of variables in $\Phi$.
We denote by $\Sigma_{{\mathcal X}_{\Phi}}$
the Venn partition of the set ${\mathcal M}[{\mathcal X}_{\Phi}]$, and by $\Im_{{\mathcal M}}$
the function $\Im_{{\mathcal M}}\in\pow{\Sigma_{{\mathcal X}_{\Phi}}}^{{\mathcal X}_{\Phi}}$ such that
${\mathcal M}(v)= \bigcup\Im_{{\mathcal M}}(v)$ holds for every $v$ in ${\mathcal X}_{\Phi}$.

\begin{myremark}\rm
Observe that any formula $\Phi$ with variables ${\mathcal X}_{\Phi}$
of a language resulting from an extension of Multi Level Syllogistic can be modified,
without affecting its satisfiability, in such a way any model ${\mathcal M}$ generates a transitive
$\Sigma_{{\mathcal X}_{\Phi}}$ \cite[pp.195-196]{Can91}.
Because of that, from now on we shall assume that
$\Sigma_{{\mathcal X}_{\Phi}}$ is transitive, for any model ${\mathcal M}$
of a formula $\Phi$
with variables ${\mathcal X}_{\Phi}$.
\end {myremark}

The intended meaning of $r\in\REDS$ is that
$\finite{r^{(\bullet)}}$; $B\in\POWNODES$ means that
$\powast{B^{(\bullet)}}\subseteq \bigcup\Places^{(\bullet)}$. To
see that the latter constraint belongs to \MLSSP, note that an
alternative way of stating it is as $\Pow(\bigcup
B^{(\bullet)})\subseteq\bigcup\Places^{(\bullet)}$ (this,
globally, needs to be made explicit only for the
inclusion-maximal nodes $B$ in $\POWNODES$). It is, in fact,
obvious that $\powast{B^{(\bullet)}}\subseteq
\bigcup\Places^{(\bullet)}$ follows from $\Pow(\bigcup
B^{(\bullet)})\subseteq\bigcup\Places^{(\bullet)}$, because
$\powast{B^{(\bullet)}}\subseteq\Pow(\bigcup B^{(\bullet)})$;
conversely, if $B$ is a $\Pow$-node, and the condition
$\powast{D^{(\bullet)}}\subseteq \bigcup\Places^{(\bullet)}$ is
satisfied by every $\Pow$-node $D$ (and hence it holds when
$D\subseteq B$), then
\\\centerline{$\Pow(\bigcup
B^{(\bullet)})=\bigcup\powAst[\{D^{(\bullet)}\wt D\subseteq
B\}]\subseteq\bigcup\powAst[\{D^{(\bullet)}\wt D\in \POWNODES\}]
\subseteq \bigcup\Places^{(\bullet)}$.} Likewise, the constraints
$\inters{t^{(\bullet)}}{\powast{A^{(\bullet)}}}$ associated with
edges $\langle A,t\rangle$ (and also constraints of the form
$s^{(\bullet)}\cap\powast{A^{(\bullet)}}=\emptyset$) can be
written in terms of the customary operator $\Pow$, because
\\\centerline{$\powast{A^{(\bullet)}}=\pow{\bigcup A^{(\bullet)}}\setminus
\bigcup\big\{\Pow\big(\bigcup
(A\setminus\{q\})^{(\bullet)}\big)\wt q\in A\big\} $\/.} Observe,
thirdly, that the transitivity condition $\bigcup\bigcup
P^{(\bullet)}\subseteq \bigcup P^{(\bullet)}$ is reducible to the
\MLSSP fragment of the set-theoretic language, too, because it can
be restated as $\bigcup P^{(\bullet)}\subseteq\pow{\bigcup
P^{(\bullet)}}$.

In conclusion, we may view a colored board $\mathcal{G}$ as being
the representation of a conjunction
$\varphi\equiv\varphi_\mathcal{G}$ of constraints each of which
either belongs to \MLSSP or has the form $\mathit{Finite}(r)$. Here
we are momentarily regarding each place $q$ as the name of an
unknown set; when the unknowns are replaced by concrete sets
$q^{(\bullet)}$ within $\varphi$, the overall substitution must
satisfy $\varphi$, and the sets $q^{(\bullet)}$ will then
collectively form a partition $\Sigma$ actually complying with
$\varphi$. Let us now obtain
$\widehat{\varphi}\equiv\widehat{\varphi}_\mathcal{G}$ by adding
to $\varphi$ all constraints $\Not \mathit{Finite}(g)$ with
$g\in\Places\setminus\REDS$. By investigating how we can get a
solution to $\widehat{\varphi}$ out of a solution to $\varphi$ (if
possible), we will shed light on the conditions for the
satisfiability of any formula of the quantifier-free language \MLSSP
extended with the $\mathit{Finite}$ relator; and, ultimately, we
will come to an algorithm which is able to test any formula of
this extended language for satisfiability.

When affirmative literals of the form $Finite(v)$, with $v$ in $\mathcal{X}_{\Phi}$, are also included in $\Phi$, the $\Sigma_{{\mathcal X}_{\Phi}}$-board can be colored naturally, by putting

\begin{itemize}
\item[(a)]
$\begin{array}[t]{ll}\REDS=\bigcup\{\Im_{\mathcal{M}}(v)\st & \!\!\!\!\!
\mbox{a literal of either the form $v=\{w_{1},\dots,w_{H}\}$} \\& \!\!\!\!\!
\mbox{or the form $Finite(v)$ occurs in $\Phi$}\};\end{array}$
\item[(b)] $\POWNODES$ is the minimal collection
of nodes such that
\begin{itemize}
\item $\Im_{\mathcal{M}}(u)\in\POWNODES$ for all literals of the form $u=\pow{w}$ in $\Phi$, and
\item $\bigcup\Pow[\POWNODES]\subseteq\POWNODES\:$.
\end{itemize}
\end{itemize}
This will be called \textsc{ the canonical board of the assignment
${\mathcal M}$ for the \MLSSPF-formula $\Phi$}.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Formative processes and basic events}
\label{basicsOnProcesses}

We will now discuss a technique by
which one can find a transitive partition
\\\centerline{$\Sigma_\xi=\{q^{(\bullet)}\wt q\in\Places\}$} complying with a
given $\Places$-board by
\begin{itemize}
    \item[*] constructing a $\xi$-sequence of partitions which is a
    \emph{formative process} in the sense specified by
    \defn{defFormativeProc} below, by then

    \item[*] ascertaining that every edge $\langle A,t\rangle$ of the
    $\Places$-board has been \emph{activated} along the process (in a
    sense to be clarified below), and by then

    \item[*] taking as $\Sigma_\xi$ the last partition of the
    sequence.
\end{itemize}

\begin{mydef}\label{defFormativeProc}\rm
Let $\Sigma,\Sigma'$ be partitions such that
\begin{itemize}
\item every block $\sigma\in\Sigma$ has a block $\sigma'\in\Sigma'$
for which $\sigma\subseteq\sigma'$\/;
\item $\sigma_0,\sigma_1\subseteq\tau$ implies $\sigma_0=\sigma_1$
when $\sigma_0,\sigma_1\in\Sigma$ and $\tau\in\Sigma'$.
\end{itemize}
Then we say that $\Sigma'$ \textsc{frames} $\Sigma$.

When $\Sigma'$ frames $\Sigma$, and moreover $$\Sigma\neq
\Sigma',\;\;\;\mbox{and}\;\;\;
\bigcup\Sigma'\setminus\bigcup\Sigma\subseteq\powast{\Gamma}\;\;\;
\mbox{for some}\;\;\;\Gamma\subseteq\Sigma,$$ then the ordered
pair $\Sigma,\Sigma'$ is called an \textsc{action}.

A \textsc{(formative) process} is a  sequence
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi}$ of partitions, where
$\xi$ can be any ordinal and, for every ordinal $\nu<\xi$:
\begin{itemize}
\item $\Sigma_\nu=\emptyset$ if $\nu=0$;
\item $\Sigma_{\nu}$\/, $\Sigma_{\nu+1}$ is an action;

\item $\Sigma_{\lambda}$ frames $\Sigma_\nu$\/, and
\emph{$\bigcup\Sigma_\lambda
\subseteq\bigcup\bigcup\{\Sigma_\gamma\wt\gamma\in\lambda\}$}, for
every limit ordinal $\lambda$ such that $\nu<\lambda\leqslant\xi$.
\end{itemize}

\noindent For all $\mu\leqslant\xi$ and $\tau\in\Sigma_\xi$, we
will designate by $\tau^{(\mu)}$ the unique set such that
$$\begin{array}{lcl}
\tau^{(\mu)} &=& \mbox{the $\sigma\in\Sigma_\mu$ such that
$\sigma\subseteq \tau$, if any exists, else $\emptyset$}.
\end{array}$$

A process $\big(\Sigma_\mu\big)_{\mu\leqslant\xi}$ is said to be
\textsc{greedy} if, for all $\nu<\xi$ and
$\Gamma\subseteq\Sigma_\nu$, the following holds:
$$\inters{\powast{\Gamma}}{\left(\bigcup\Sigma_{\nu+1}\setminus
\bigcup\Sigma_{\nu}\right)}\;\;\;\mbox{implies}\;\;\;
\left(\powast{\Gamma}\setminus\bigcup\Sigma_{\nu+1}\right)\cap\bigcup\Sigma_\xi\:=\:\emptyset.$$

If we take, along with a colored $\Places$-board
$\TARGETS,\REDS,\POWNODES$, a bijection $q\mapsto q^{(\bullet)}$
from the places $\Places$ to the final partition $\Sigma_\xi$ of
a formative process, and if moreover $\Sigma_\xi$ complies with
$\TARGETS,\REDS,\POWNODES$, we get what we will call a
\textsc{colored $\Places$-process}: namely the quintuple
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi},(\bullet),\TARGETS,\REDS,\POWNODES$.
Then, for all $\mu\leqslant\xi$, $\nu<\xi$, $p\in\Places$,
$B\subseteq\Places$, we will designate by
$p^{(\mu)},B^{(\mu)},B^{(\bullet)},A_\nu$ the unique sets such
that \\\centerline{$\begin{array}{lcl}
p^{(\mu)} &=& \left({p^{(\bullet)}}\right)^{(\mu)}; \\
\Delta^{(\nu)}(q) &=& q^{(\nu+1)}\setminus\bigcup\Places^{(\nu)}.\\
B^{(\mu)} &=& \begin{array}{lclclcl} \{q^{(\mu)}\wt q\in B\}, &
\mbox{and} &
B^{(\bullet)} &=& \{q^{(\bullet)}\wt q\in B\};\end{array} \\
A_\nu &=& \mbox{the set $A\subseteq\Places$ for which
$\bigcup\Sigma_{\nu+1}\setminus
\bigcup\Sigma_\nu\subseteq\powast{A^{(\nu)}}$}.
\end{array}$}

\noindent We will call $A_\nu$ the \textsc{$\nu$-th move} of the
process. \eod\end{mydef}

As an easy illustration of how one can reason about processes, let
us prove the following:
\begin{mylemma}
In a process $\big(\Sigma_\mu\big)_{\mu\leqslant\xi}$, each
$\Sigma_\mu$ frames $\Sigma_\nu$, and $\bigcup\Sigma_\nu\subsetneq
\bigcup\Sigma_\mu$, for all $\nu<\mu$\/.
\end{mylemma} \proof Arguing by contradiction, suppose that the statement
is false, and let $\mu$ be the least ordinal such that, for some
$\nu<\mu$, either $\bigcup\Sigma_\nu\subsetneq \bigcup\Sigma_\mu$
does not hold or $\Sigma_\nu$ is not framed by $\Sigma_\mu$.

Trivially, since $\nu<\mu$\/, we have $\mu\neq 0$; moreover $\mu$
cannot be a successor ordinal $\mu=\gamma+1$, else $\Sigma_\mu$
would frame $\Sigma_\gamma$, and $\Sigma_\gamma$ would frame
$\Sigma_\nu$ by the assumed minimality of $\mu$, and hence,
transitively, $\Sigma_\mu$ would frame $\Sigma_\nu$, a
contradiction.

But $\mu$ cannot be a limit ordinal either. In fact, if $\mu$ is
a limit ordinal and we consider any ordinal $\nu<\mu$, then
$\Sigma_{\mu}$ frames $\Sigma_{\nu}$; moreover, since
$\nu+1\leqslant\mu$, we have
$\bigcup\Sigma_{\nu}\subsetneq\bigcup\Sigma_{\nu+1}\subseteq
\bigcup\Sigma_{\mu}$. \qed

Relative to a formative process $(\Sigma_\mu)_{\mu\leqslant\xi}$,
we can identify certain \emph{events}: these, roughly speaking,
are ordinals $\nu$ where something important is about to happen.
Examples of events are, for any $\Gamma\subseteq\Sigma_\xi$ and
$\sigma\in\Sigma_\xi$\/:
\begin{description}
\item[Edge-activation move:] a $\nu<\xi$ such that
$\inters{\sigma^{(\nu+1)}}{\powast{\Gamma}}$ and
$\sigma^{(\nu)}\cap\powast{\Gamma}=\emptyset$;
\item[Grand move:] a $\nu<\xi$ such that $\bigcup\Gamma\in\bigcup\Sigma_{\nu+1}
\setminus\bigcup\Sigma_\nu$.
\end{description}
Subtler events, which will be discussed later, create conditions
that enable expansion of the block associated with a green place
into an infinite block.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Historical profile of an infinite block}
\label{historicalProfile}

Let the triple $\TARGETS,\REDS,\POWNODES$ represent a colored
$\Places$-board: what guarantee do we have that a colored process
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi},(\bullet),\TARGETS,\REDS,\POWNODES$
exists? \emph{A priori}, according to our definitions, none; as a
matter of fact, should some place have no afferent edges, that is,
should there be some $s\in\Places$ such that $s\notin\Targets{A}$
for any $A\subseteq\Places$, then no move $A_\nu$ would ever be
allowed to bring elements into $s^{(\nu+1)}$, and consequently
$s^{(\bullet)}$ could not be a block in a partition.

The situation is quite different if the colored $\Places$-board
with which we start is induced by a transitive partition
$\Sigma$, because then one can prove (cf.\
\cite[p.176]{COU02}) the following

\begin{mytheorem}[Trace theorem]
If $\TARGETS,\REDS,\POWNODES$ is a colored $\Sigma$-board induced
by a finite transitive partition $\Sigma$, then a greedy colored
process
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi},\iota_\Sigma,\TARGETS,\REDS,\POWNODES$
exists which ends with $\Sigma_\xi=\Sigma$ and has
$\card{\xi}\leqslant\card{\bigcup\Sigma}$\/.\qed
\end{mytheorem}

As we showed in \cite[p.180 ff.]{COU02}, if we
have `in our pocket', so to speak, this kind of oracular
guarantee, namely a transitive partition $\Sigma$ which induces a
particular colored board, then we can imitate $\Sigma$ by means
of a `small' partition $\Sigma'$, with rank
$$\rk(\Sigma')\leqslant
c(\card{\Sigma}),$$ where $c$ is a specific computable function,
namely $c(n)=\lceil{\frac{25}{24}\rceil\cdot m+5}\cdot
2^{{2^m}+m}+3$ with $m=\lceil \log_2(n+1)\rceil$. Instead of being
obtained directly from $\Sigma$, this $\Sigma'$ is obtained
through a process $\big(\Sigma_j'\big)_{j\leqslant\ell}$ which
`mimics' a greedy colored process
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi}$ corresponding to $\Sigma$
as stated in the trace theorem, and by then putting
$\Sigma'=\Sigma_\ell'$. Here $\ell<\aleph_0$; moreover one can
manage that the sequence of edge-activation moves and grand moves
are `synchronized'---in a sense to be clarified below---between
the two processes. In what follows, we will refer to
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi}$ and to
$\big(\Sigma_j'\big)_{j\leqslant\ell}$~, respectively, when
speaking of the \emph{original process} and of the \emph{shadow
process}.

Under one major respect, however, the way in which the small
partition $\Sigma'$ portrays $\Sigma$ is unfaithful to the
original: all of its blocks have in fact finite cardinality,
regardless of the cardinality of corresponding blocks in the
original partition. To find a remedy to this, we will first
detect the causes which can make a block in $\Sigma$ infinite:
such causes are to some extent static, viz. features of the
$\Sigma$-board, and to some other extent dynamic, viz.
\emph{`pumping' events} which activate certain special paths of
the $\Sigma$-board during the original process. On the basis of a
careful analysis of how infinity can enter into play in the
original process, we will discover how to infinitely expand,
again, the green blocks of our small partition, taking advantage
of two facts:
\begin{itemize} \item the board of the original and of the
shadow process is the same; and \item we can synchronize with each
pumping event $\nu$ of the original process a regular chain of
actions that can safely be interpolated next to the move of the
shadow process corresponding to the original $\nu$-th move.
(`Safely' means that the imitation, in the sense of
Def.~\ref{formimit} below, is not disrupted by the extra moves.)
\end{itemize}

\subsubsection{Pumping paths}\label{sse_pumpingPaths}
The block at a place $s$ cannot become infinite, during a
formative process, without some afferent edge carrying to $s$
infinitely many elements drawn from a cycle. Otherwise stated, to
make it possible that $\card{s^{(\bullet)}}\geqslant\aleph_0$, the
board of the process must have a path
$C_0,q_0,C_1,q_1,\ldots,C_n,q_n,C_0,t_0,D_1,t_1,\ldots,D_{m+1},t_{m+1}$
ending with $t_{m+1}= s$. This fact should be easy to grasp, but
we will nevertheless provide a proof of it soon. Notice that we
can insist w.l.o.g. that, besides the double occurrence of $C_0$,
the only possible repetitions of vertices are $q_0=t_0$ and
$q_0=t_0$\/, $C_1=D_1$\/. These considerations lead to the
following two definitions, of which the former is preparatory to
the subsequent, very important \defn{pumpingPaths}.


\begin{mydef}\label{prepareForPumpingPaths}\rm In a $\Places$-board
$\mathcal{G}$, a \textsc{path} is an ordered vertex list
$W_1,\dots,W_k$ within which places and nodes so alternate that
$W_i,W_{i+1}$ is an edge of $\mathcal{G}$ for $i=1,\dots,k-1$. A
path is said to be \textsc{simple} if no place or node occurs
twice in it (i.e., $W_i\neq W_j$ when $0<i<j\leqslant k$ and
$i\equiv j\;(\mbox{\emph{mod }}2)$\/).

If $$\begin{array}{lcll} \mathcal{D}' & \equiv &
q_0,C_1,\dots,q_n,C_{n+1} &  \mbox{and} \\
\mathcal{D}'' & \equiv & t_{0},D_{1},\dots,t_{m-1},D_{m},t_{m} \,,
\end{array}$$
with $n,m \geqslant 0$, are \emph{simple} paths in $\mathcal{G}$ which meet
the following conditions,
\begin{itemize}
\item $\langle C_{n+1},t_0\rangle$ is an edge of $\mathcal{G}$,
\item
$\{q_0,\dots,q_n\}\cap\{t_0,\dots,t_{m}\}\subseteq\{q_{0}\}\cap\{t_0\}$,
\item $\{C_1,\dots,C_{n+1}\} \cap \{D_1,\dots,D_{m+1}\} \subseteq
\{C_{1}\}\cap\{D_1\}$,
 \item if $C_1=D_1$\/, then $q_0=t_0$\/,
\end{itemize}
then $\mathcal{D}''$ is said to be \textsc{contiguous} to
$\mathcal{D}'$\/.

A path $W'_{1},\dots,W'_{\ell}$ in $\mathcal{G}$ is said to be
\textsc{adjacent} to another path $W_1,\dots,W_k$ in $\mathcal{G}$ if
$W_{k},W'_{\ell}$ is an edge of $\mathcal{G}$.  \eod
\end{mydef}

\begin{mydef}\label{pumpingPaths}\rm In a colored $\Places$-board
$\mathcal{G}=(\TARGETS,\REDS,\POWNODES)$, consider paths
$$\begin{array}{lcll} \mathcal{C} & \equiv &
C_0,q_0,C_1,\dots,q_n,C_{n+1} & \mbox{and} \\
\mathcal{D} & \equiv & q_{n+1},C_{n+2},q_{n+2},\dots,C_{n+m+1},q_{n+m+1} &
\end{array}$$
(where $n,m\geqslant 0$), \emph{devoid} of red places and such
that $C_{n+1} = C_{0}$ and $\mathcal{D}$ is contiguous to the path
$q_0,C_1,\dots,q_n,C_{n+1}$. (Hence, in particular,
$q_{n+m+1}\in\Targets{C_{n+m+1}}\setminus\REDS$, and
$q_i\in\Targets{C_i}\cap C_{i+1}\setminus\REDS$ for
$i=0,1,\dots,n+m$.)

 Then $\mathcal{C}$ is said to be a
\textsc{pumping cycle}, and the path resulting from the
concatenation of $\mathcal{D}$ at the end of $\mathcal{C}$ is said
to be a \textsc{pumping path}. \emph{(cf.\ \fig{figPumpingPath}.)}
\eod\end{mydef}
\begin{figure}
\centerline{\begin{tabular}{|l|}\hline
\begin{picture}(305,300)
\put(2.5,264){ $q_{n}$} %
\put(3,257){ $\bullet$} \put(5,258.5){ \vector(2,1){45.5}} %
\put(40,286){ $C_{0}\equiv C_{n+1}$ } %
\put(47,279){ $\bullet$ } \put(48.5,281.5){ \vector(2,-1){45.5}} %
\put(89,264){ $q_{0}\equiv q_{n+1}$} %
\put(91,257){ $\bullet$} \put(93,258.5){ \vector(0,-1){28}} %
\put(91,229){ $\bullet$ } \put(92.5,230.5){ \vector(-2,-1){44.5}} %
\put(90.5,219){ $C_1$} %
\put(46.5,214){ $q_{1}$} %
\put(47,207){ $\bullet$} %
\put(48.5,209.5){ \vector(-1,0){43}} %
\qbezier[25](9.4,257)(9.4,237)(9.4,211) %%%
\put(91.5,259){ \vector(1,0){50}} \put(141,257){ $\bullet$} %
\put(138,247){ $C_{n+2}$} %
\qbezier[10](142.5,259)(160.5,259)(178.5,259) %
\put(179,257){$\bullet$} \put(169,247){ $C_{n+m+1}$}%
\put(180.5,259){ \vector(1,0){50}} \put(230,257){$\bullet$}
\put(225,264){ $q_{n+m+1}$} %%%
\put(180,215){ \fbox{$\overline{\cal D}_0\equiv [q_{n+1}]$}}
%%%
%%%
\put(2.5,164){ $q_{n}$} %
\put(3,157){ $\bullet$} \put(5,158.5){ \line(2,1){45.5}} %
\put(40,186){ $C_{0}\equiv C_{n+1}$ } %
\put(47,179){ $\bullet$ } \put(48.5,181.5){ \line(2,-1){45.5}} %
\put(90.5,164){ $q_{0}$} %
\put(91,157){ $\bullet$} \put(93,158.5){ \line(0,-1){28}} %
\put(91,129){ $\bullet$ } \put(92.5,130.5){ \line(-2,-1){44.5}} %
\put(88,119){ $C_1$} %
\put(46.5,114){ $q_{1}$} %
\put(47,107){ $\bullet$} %
\put(48.5,109.5){ \line(-1,0){43}} %
\qbezier[25](9.4,157)(9.4,137)(9.4,111) %%%
\put(49.5,181){ \line(1,0){50}} \put(99,179){ $\bullet$} %
\put(98,186){ $q_{n+1}$} \put(100.5,181){ \line(1,0){36}} %
\put(136,179){$\bullet$} \put(128,169){ $C_{n+2}$}%
\qbezier[10](136.5,181)(154.5,181)(172.5,181) %
\put(173,179){$\bullet$} \put(163,169){ $C_{n+m+1}$}%
\put(174.5,181){ \line(1,0){50}} \put(224,179){$\bullet$}
\put(219,186){ $q_{n+m+1}$} %%%
\put(180,135){ \fbox{$\overline{\cal D}_0\equiv [q_{n+1}]$}}
%%%
%%%
\put(2.5,64){ $q_{n}$} %
\put(3,57){ $\bullet$} \put(5,58.5){ \line(2,1){45.5}} %
\put(40,86){ $C_{0}\equiv C_{n+1}$ } %
\put(47,79){ $\bullet$ } \put(48.5,81.5){ \line(2,-1){45.5}} %
\put(90.5,64){ $q_{0}\equiv q_{n+1}$} %
\put(91,57){ $\bullet$} \put(93,58.5){ \line(0,-1){28}} %
\put(91,29){ $\bullet$ } \put(92.5,30.5){ \line(-2,-1){44.5}} %
\put(86,19){ $C_1\equiv C_{n+2}$} %
\put(46.5,14){ $q_{1}$} %
\put(47,7){ $\bullet$} %
\put(48.5,9.5){ \line(-1,0){43}} %
\qbezier[25](9.4,57)(9.4,37)(9.4,11) %%%
\put(91.5,31){ \line(1,0){50}} \put(141,29){ $\bullet$} %
\put(140,36){ $q_{n+2}$} \put(142.5,31){ \line(1,0){36}} %
\qbezier[10](178.5,31)(196.5,31)(214.5,31) %
\put(215,29){$\bullet$} \put(205,19){ $C_{n+m+1}$}%
\put(216.5,31){ \line(1,0){50}} \put(266,29){$\bullet$}
\put(261,36){ $q_{n+m+1}$} %%%
 \put(180,65){ \fbox{$\overline{\cal D}_0\equiv [q_{n+1},C_{n+2},q_{n+2}]$}}
\end{picture}
\\\hline\end{tabular}
} \caption{\label{figPumpingPath} The three kinds of pumping path}
\end{figure}

In what follows, we will set up the ground for a theorem
generalizing the following easy proposition (whose proof we delay
until we can generalize the statement):

\begin{mylemma}\label{liesOnPumpLem}
Relative to a colored $\Places$-process
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi},(\bullet),\TARGETS,\REDS,\POWNODES$,
consider a place $s$ such that $\infinite{s^{(\bullet)}}$. Then
$s$ lies on a pumping path.\qed\end{mylemma}

\noindent In sight of a proposition generalizing this one, which
will follow from two other lemmas, we give the following
definition:
\begin{mydef}\rm
For any node $B$ and place $t$ of a colored process,
\emph{$$\begin{array}{lcl} \leastInf(B) &
\defAs & \left\{\begin{array}{ll} \mbox{the least ordinal $\mu$ for
which $\infinite{\powast{B^{(\mu)}}}$,} & \mbox{if}\ \
\infinite{\bigcup B^{(\bullet)}}\:, \\
0 & \mbox{otherwise;}\end{array}\right. \\
\leastInf(t) &
\defAs & \leastInf(\{t\}).
\end{array}$$}

\noindent\emph{Note that $\leastInf(B)\neq 0$ and $\leastInf(t)\neq 0$
imply respectively $B$ and $t$ to be green, else the ending partition
would not comply with the color of the board.  Note also that
$$\begin{array}{lcl} \leastInf(t) & = &
\left\{\begin{array}{ll} \mbox{the least ordinal $\mu$ for
which $\infinite{{t^{(\mu)}}}$,} & \mbox{if}\ \ %
\infinite{t^{(\bullet)}}\:, \\
0 & \mbox{otherwise.}\end{array}\right.
\end{array}$$
}\eod\end{mydef}

Here are the two lemmas preliminary to \thm{liesOnPump}, which
will generalize \lem{liesOnPumpLem}:
\begin{mylemma}\label{lemLeastInf}
Relative to a greedy colored $\Places$-process
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi},(\bullet),\TARGETS,\REDS,\POWNODES$
whose sequence of moves is $\big(A_\nu\big)_{\nu<\xi}$, consider a
place $s_{0}$ such that $\leastInf(s_{0})=\nu+1$ for some ordinal
$\nu$\/.  Then there exist a place $s_{k+1}$ and a green path
$\mathcal{D} \equiv
s_{k+1},B_{k},s_{k},\ldots,B_{1},s_{1},B_{0},s_{0}$ from $s_{k+1}$
to $s_{0}$, with $k \geqslant 0$, such that %
\begin{itemize}
\item[(a)] $\leastInf(s_{k+1})$ is a limit ordinal $\lambda$;

\item [(b)] $\leastInf(s_{i+1}) \leqslant \leastInf(B_{i}) <
\leastInf(s_{i})$, for $i=0,1,\ldots,k$;

\item [(c)] for every edge $\langle B_{i},s_{i}\rangle$ lying on
$\mathcal{D}$ and for every node $H$ other than $B_{i}$, it holds that
$$\begin{array}{lclcl}
\card{s_{i}^{(\leastInf(s_{i}))}\cap\powast{B_{i}^{(\leastInf(s_{i})-1)}}}
& \geqslant & \aleph_0 & & \mbox{and} \\[0.2cm]
\card{s_{i}^{(\leastInf(s_{i}))}\cap\powast{H^{(\leastInf(s_{i})-1)}}}
& < & \aleph_0\;.  & &
\end{array}$$
\end{itemize}
\end{mylemma}
\proof Arguing by contradiction, let us assume that $\nu_0$ is the
least ordinal such that an $s_0$ with $\leastInf(s_0)=\nu_0+1$
exists violating the thesis. (Clearly $s_0$ must be green.) Then
$\infinite{\powAst(A_{\nu_0}^{(\nu_0)})}$, where $A_{\nu_0}$ is
the $\nu_0$-th move, and hence there is a green place $s_1\in
A_{\nu_0}$ such that
$0<\leastInf(s_1)\leqslant\leastInf(A_{\nu_0})\leqslant \nu_0$\/.
It can easily be checked that the edge $\langle
A_{\nu_0},s_0\rangle$ satisfies condition (c). Thus, if
$\leastInf(s_1)$ were a limit ordinal, our initial assumption
would be violated, because we could take $k=0$ and
$\mathcal{D}\equiv s_1,A_{\nu_0},s_0$. Hence
$\leastInf(s_1)=\gamma+1$, and therefore, by the assumed
minimality of $\nu_0$, a green path $\mathcal{D}'$ leading to
$s_1$ and satisfying the conditions of the lemma can be found.
But then, prolonging $\mathcal{D}'$ first with $A_{\nu_0}$ and
next with $s_0$ would give us a $\mathcal{D}$ whose existence
conflicts with our initial assumption.  \qed


\begin{mylemma}\label{lemCofin}
Consider a \emph{greedy} process over a $\Places$-board
$\mathcal{G}$, and let $\lambda$ be a limit ordinal. Let,
moreover, the subgraph $\mathcal{G}_{\lambda}$ of $\mathcal{G}$
consist of all
\begin{itemize}
\item places $q$ such that the set
\\\centerline{\emph{$I_{\lambda,q}\;=\;\{\nu<\lambda\st q^{(\nu+1)}\neq
q^{(\nu)}\}$}}
is cofinal in $\lambda$ (i.e., $\bigcup
I_{\lambda,q}=\lambda$\/);

\item nodes $B$ such that the set
\\\centerline{\emph{$I_{\lambda}^{B}\;=\;
\{\nu<\lambda\st A_\nu=B\}$}}
is cofinal in $\lambda$\/;

\item edges $\langle B,q\rangle$ such that
\\\centerline{\emph{$I_{\lambda,q}^B\;=\;\{\nu<\lambda\st A_\nu=B\And
q^{(\nu+1)}\neq q^{(\nu)}\}$}}
is cofinal in $\lambda$\/;

\item edges $\langle q,B\rangle$ such that $q \in B$\/.
\end{itemize}
Then every \emph{vertex} $W$ of $\mathcal{G}_{\lambda}$ (if any
exists) has at least one predecessor in $\mathcal{G}_{\lambda}$.
\end{mylemma}
\proof If $W$ is a \emph{place} $p$ of $\mathcal{G}_{\lambda}$
then, since
$$
I_{\lambda,p}\;=\;\bigcup\{I_{\lambda,p}^B\wt B\subseteq
\Places\}\/,
$$
from the assumption $\bigcup I_{\lambda ,p}=\lambda$ and the
finiteness of $\Places$ it follows that $\bigcup
I_{\lambda,p}^B=\lambda=\bigcup I_{\lambda}^B$ for some $B$\/:
hence $B$ is an immediate predecessor of $p$ in
$\mathcal{G}_{\lambda}$\/.

On the other hand, if $W$ is a \emph{node} $B$ of
$\mathcal{G}_{\lambda}$ then, from the assumption $\bigcup
I_{\lambda}^B=\lambda$ and from the greediness of the process it
follows that $\bigcup\bigcup\{I_{\lambda,q}\wt q\in B\}=\lambda$.
Therefore $\bigcup I_{\lambda,q}=\lambda$ for some $q\in B$, in
view of the finiteness of $B$\/, and hence $q$ is an immediate
predecessor of $B$ in $\mathcal{G}_{\lambda}$\/.
\qed

We can now combine the preceding two lemmas into the following
important result:
% \mimmo{Nel seguente teorema si fa uso del termine
% \emph{contiguous} che ha una definizione formale.  Per\`o, la
% definizione impedisce l'esistenza di una terna di cammini contigui, in
% quanto per la prima relazione di contiguit\`a, (il primo cammino deve
% iniziare con un posto e terminare con un nodo e) il secondo deve
% iniziare e finire con un posto.  D'altra parte, per la seconda
% relazione di contiguit\`a il secondo cammino deve iniziare con un
% posto e finire con un nodo (e il terzo iniziare e finire con un
% posto).  Ma ci\`o \`e impossibile.  Occorrerebbe quindi utilizzare nel
% seguente teorema un termine pi\`u generico al posto di
% \emph{contiguous}.}
\begin{mytheorem}[Pumping theorem]\label{liesOnPump}
\begin{sloppypar}
    Relative to a greedy colored $\Places$-process
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi},(\bullet),\TARGETS,\REDS,\POWNODES$
whose sequence of moves is $\big(A_\nu\big)_{\nu<\xi}$, consider a
place $s$ such that $\infinite{s^{(\bullet)}}$. Then $s$ is the
last node of a pumping path which can be split into adjacent
paths $\mathcal{C},\mathcal{D}',\mathcal{D}''$ such that
\end{sloppypar}
\begin{enumerate}
\item $\mathcal{C}$ is a cycle;
\item the path $\mathcal{C},\mathcal{D}'$ ends with a place $g$ whose
$\leastInf(g)$ is a limit ordinal $\lambda$;
\item $0<\leastInf(q)\;\leqslant\;\lambda\;=\;\bigcup I_{\lambda,q}^B$
holds, where
\emph{$I_{\lambda,q}^B\;\defAs\; \{\nu<\lambda\st A_\nu=B\And
q^{(\nu+1)}\neq q^{(\nu)}\}$}, for every edge $\langle B,q \rangle$ lying on
$\mathcal{C},\mathcal{D}'$;
\item $\lambda \leqslant \leastInf(B) < \leastInf(q)$, for every edge
$\langle B,q\rangle$ lying on $\mathcal{D}''$;
\item $\leastInf(q) \leqslant \leastInf(B)$, for every edge $\langle
q,B \rangle$ lying on $\mathcal{D}''$;
\item for every edge $\langle D,p \rangle$ lying on
$\mathcal{D}''$ and for every node $H$ other than $D$, it holds
that $$\begin{array}{lclcl}
\card{p^{(\leastInf(p))}\cap\powast{D^{(\leastInf(p)-1)}}}
&
\geqslant & \aleph_0 & & \mbox{and} \\[0.1cm]
\card{p^{(\leastInf(p))}\cap\powast{H^{(\leastInf(p)-1)}}}
& < & \aleph_0\;. & & \end{array}$$
\end{enumerate}
\end{mytheorem}
\proof If $\leastInf(s)$ is a limit ordinal, then we can
take $\lambda=\leastInf(s)$, $g=s$, and $\mathcal{D}''$
void. To construct $\mathcal{C},\mathcal{D}'$\/, we can exploit
\lem{lemCofin}, where $\mathcal{G}_{\lambda}$ turns out to be
non-void since it contains $s$\/. Thanks to the fact that every
vertex of $\mathcal{G}_{\lambda}$ has a predecessor in
$\mathcal{G}_{\lambda}$\/, starting with $s$ and proceeding in a
backward fashion we will sooner or later hit the same vertex
twice, since $\mathcal{G}_{\lambda}$ is finite.

If $\leastInf(s)$ is a successor ordinal, then by
\lem{lemLeastInf} there exists a green path
$$
\overline{\mathcal{D}''} \equiv s_{k+1},B_{k},s_{k},\ldots,
B_{1},s_{1},B_{0},s_{0},~~\textrm{with } s_{0} = s\/,
$$
such that
\begin{itemize}
\item $\leastInf(s_{k+1})$ is a limit ordinal $\lambda$;

\item $\leastInf(s_{i+1}) \leqslant \leastInf(B_{i}) <
\leastInf(s_{i})$, for $i=0,1,\ldots,k$;

\item for every edge $\langle B_{i},s_{i}\rangle$ lying on
$\overline{\mathcal{D}''}$ and for every node $H$ other than $B_{i}$, it holds that
$$\begin{array}{lclcl}
\card{s_{i}^{(\leastInf(s_{i}))}\cap\powast{B_{i}^{(\leastInf(s_{i})-1)}}}
& \geqslant & \aleph_0 & & \mbox{and} \\[0.2cm]
\card{s_{i}^{(\leastInf(s_{i}))}\cap\powast{H^{(\leastInf(s_{i})-1)}}}
& < & \aleph_0\;.  & &
\end{array}$$
\end{itemize}
Let us put $g \defAs s_{k+1}$.  To construct the paths
$\mathcal{C},\mathcal{D}',\mathcal{D}''$ of the theorem, we argue as
follows.  Much as in the previous case, we use again \lem{lemCofin} to
construct a pumping path $\mathcal{C},\mathcal{D}'$ leading to
$s_{k+1}$.  Starting in $\mathcal{G}_{\lambda}$ with $s_{k+1}$, we
proceed backwards until either we hit the same vertex twice, or we hit
the vertex $B_{k}$, provided that $B_{k}$ is in
$\mathcal{G}_{\lambda}$. In the latter case, we form a cycle by making
a further backward step through the edge $\langle s_{k+1},B_{k}\rangle$.
Finally, we put $\mathcal{D}'' \equivAs B_{k},s_{k},\ldots,
B_{1},s_{1},B_{0},s_{0}$.

It is an easy matter to verify that the paths
$\mathcal{C},\mathcal{D}',\mathcal{D}''$ satisfy the conditions of the
theorem. \qed


\subsubsection{Grand events and local trash}

In what follows, we will refine into a useful proposition the
following easy remark: the block at a place $s$ belonging to a
$\Pow$-node $A$ cannot become infinite during a colored process unless
$A$ has a green place among its targets.  To see this, assume that
$s\in A\in\POWNODES$ and $\infinite{s^{(\bullet)}}$.  Consequently,
$\card{\powast{A^{(\bullet)}}}>\aleph_0$ and
$\powast{A^{(\bullet)}}\subseteq\bigcup\Places^{(\bullet)}$, and hence
there must be a place $g$ such that $\card{\powast{ A^{(\bullet)}}\cap
g^{(\bullet)}}>\aleph_0$, because
$\card{\Places^{(\bullet)}}=\card{\Places}<\aleph_0$; which obviously
implies that $g\in\Targets{A}\setminus\REDS$.

In sight of generalizing the above remark, recalling the notion
of grand move and noticing that such an event occurs, in a colored
process, at most once for each node $A$\/, we give the following
definition of \emph{grand event} $\GE(A)$ associated with $A$:
\begin{mydef}\rm
For every node $A$ and every $\nu$ such that
$0\leqslant{\nu}<\xi$,
$$
\GE(A)\;\defAs\;\left\{\begin{array}{ll}
\mbox{\rm the ordinal $\nu$ for which $\bigcup
A^{(\bullet)}\in\bigcup\Places^{(\nu+1)}\setminus\bigcup\Places^{(\nu)}$,}
& \mbox{\rm if any exists}, \\
\mbox{\rm the length $\xi$ of the process} & \mbox{\rm otherwise}.
\end{array}\right.
$$
Moreover, for any given collection ${\cal A}$ of nodes, we put
$$
\GE({\cal A})\;\defAs\; \min \{\GE(A)\wt A \in {\cal A}\}\,.
$$
\eod\end{mydef}

Notice that this definition implies that for any node $A$ and any
$\nu$ such that $0\leqslant\nu<\xi$,
\\\centerline{
$\begin{array}{lcl} \nu\leqslant \GE(A) & \biimplies &
\bigcup A^{(\bullet)}\notin\bigcup\Places^{(\nu)},\\
\nu= \GE(A) & \biimplies & \bigcup
A^{(\bullet)}\in\bigcup\Places^{(\nu+1)}\setminus\bigcup\Places^{(\nu)},
\\
\nu> \GE(A) & \biimplies & \bigcup
A^{(\bullet)}\in\bigcup\Places^{(\nu)}.
\end{array}$}

Other elementary properties, whose proofs are left to the reader, are
stated in the following lemma.

\begin{mylemma}
Let
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi},(\bullet),\TARGETS,\REDS,\POWNODES$
be a greedy colored $\Places$-process and let $A \subseteq \Places$ be
a node. Then
\begin{itemize}
\item[(a)] $A^{(\alpha)} = A^{(\bullet)}$, where $\alpha = \GE(A)$;

\item[(b)] if $q^{(\nu+1)} \supsetneq q^{(\nu)}$, for some $q \in A$
and some $\nu < \xi$, then $\GE(A) > \nu$.
\end{itemize}
\end{mylemma}
\proof
Straightforward.
\qed

The following definitions show properties which allow one to ``drain off'' the ``residual'' elements of
a pumping process:
\begin{mydef}\rm
A place $g$ is said to be a \textsc{local trash} for a node $A$ and a {colored $\Places$-process}
$\left(\{q^{(\mu)}\}_{q\in\Places}\right)_{\mu\leqslant\xi},
(\bullet),\TARGETS,\REDS,\POWNODES$ if
\begin{des}
\item $g\in\Targets{A}\setminus\REDS$\/, i.e., $g$ is a green
target of $A$\/;
\item every node $B$ such that $g\in B$ has $\GE(B) > \GE(A)$\/. \eod
\end{des}
\end{mydef}



\begin{mylemma}\label{cofinal2}
Relative to a \emph{greedy} colored $\Places$-process
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi},(\bullet),\TARGETS,\REDS,\POWNODES$,
consider a node $A \subseteq \Places$ such that $\bigcup
A^{(\bullet)}$ is infinite and $\alpha = \GE(A) < \xi$. Then the
set $\powAst (A^{(\alpha)}) \setminus \bigcup \Places^{(\alpha)}$
is infinite.
% , i.e., the set $\powAst (A^{(\alpha)}) = \powAst (A^{(\bullet)})$ has
% infinitely many new elements at step $\alpha$.
\end{mylemma}
\proof Let $\big(A_\nu\big)_{\nu<\xi}$ be the sequence of moves of the
given $\Places$-process and let
$$
u_{A} \defAs \bigcup A^{(\alpha)} \setminus \bigcup
    A^{(\nu_{0})}\,,
$$
where $\nu_{0} \defAs \min \{\nu \leqslant \alpha : A_{\nu} = A\}$.
% For each $\nu \in C(A)$, we put $\nu^{+} \defAs \min \{\mu \in
% C(A) \cup \{\alpha\} \mid \mu > \nu\}$.  By the greediness of the
% process, we have $\bigcup A^{(\nu)} \subsetneq \bigcup A^{(\nu^{+})}$ for
% every $\nu \in C(A)$.  Also, let
% $$
% u_{A} \defAs \bigcup \left\{\bigcup A^{(\nu^{+})} \setminus \bigcup
% A^{(\nu)} \mid \nu \in C(A)\right\}\,.
% $$
If $u_{A}$ is finite then, since $A^{(\alpha)}$ is finite and $\bigcup
A^{(\alpha)} = \bigcup A^{(\bullet)}$ is infinite, the set $\{v \in
\powAst (A^{(\alpha)}) :
u_{A} \subseteq v\}$ is an infinite subset of $\powAst
(A^{(\alpha)})$ disjoint from $\bigcup \Places^{(\alpha)}$, and therefore
$\powAst (A^{(\alpha)}) \setminus \bigcup \Places^{(\alpha)}$ is
infinite.

On the other hand, if $u_{A}$ is infinite, then the set $\{\bigcup
A^{(\alpha)} \setminus \{w\} : w \in u_{A}\}$ is an infinite subset of
$\powAst (A^{(\alpha)})$. Since $\left| \{\bigcup A^{(\alpha)}
\setminus \{w\} : w \in u_{A}\} \cap \bigcup \Places^{(\alpha)}\right|
\leqslant 1$, we again conclude that $\powAst (A^{(\alpha)}) \setminus
\bigcup \Places^{(\alpha)}$ is infinite.  \qed


\begin{mylemma}\label{ClosedPump}
Relative to a \emph{greedy} colored $\Places$-process
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi},(\bullet),\TARGETS,\REDS,\POWNODES$,
consider a node $A \subseteq \Places$ such that $\bigcup
A^{(\bullet)}$ is infinite. Then $A$ has a local trash $p$ such
that $p^{(\bullet)}$ is infinite.
\end{mylemma}
\proof Let $\alpha = \GE(A)$.  Since $A$ is a node, we have
$\powAst (A^{(\alpha)}) = \powAst (A^{(\bullet)}) \subseteq
\bigcup \Places^{(\bullet)}$; hence $\powAst (A^{(\alpha)}) \setminus \bigcup
\Places^{(\alpha)} \subseteq \bigcup \Places^{(\alpha+1)}$, by the greediness of the
process.
Moreover, since $\powAst(A^{(\alpha)}) \setminus \bigcup \Places^{(\alpha)}$
is an infinite set by Lemma~\ref{cofinal2}, there must be a place $p \in \TARGETS(A)$
for which the set $p^{(\alpha+1)} \cap (\powAst (A^{(\alpha)}) \setminus \bigcup
\Places^{(\alpha)})$ is infinite too. Hence $p^{(\bullet)}$ is
infinite, and therefore $p \notin \REDS$.

Moreover, since $p^{(\alpha+1)} \setminus p^{(\alpha)} \neq
\emptyset$, it readily follows that  $\GE(B) > \alpha = \GE(A)$
must hold for every node $B \subseteq \Places$ such that $p \in B$,
whch proves that $p$ is a local trash for $A$. \qed


% \begin{mytheorem}\label{ClosedPump}
% Relative to a greedy colored $\Places$-process
% $\big(\Sigma_\mu\big)_{\mu\leqslant\xi},(\bullet),\TARGETS,\REDS,\POWNODES$
% whose sequence of moves is $\big(A_\nu\big)_{\nu<\xi}$, consider a
% place $s$ such that $\infinite{s^{(\bullet)}}$ then there is a pumping cycle
% $\mathcal{C},\mathcal{D}$ on which it lies on and
% $(\mathcal{C},\mathcal{D})_{places}$ is contained in a closed
% set $\mathcal{W}$ of places.
% \end{mytheorem}
% \proof
% We are aware of such a pumping cycle $\mathcal{C},\mathcal{D}$ on which $s$
% lies on by lemma \ref {liesOnPump}. We are going to show actually
% more than we
% expect, indeed we shall prove that there exists a collection of infinite
% places $W$ closed.\\ By contradiction suppose that such closed
% collection does
% not exist, which means that all collection of infinite places containing
% $(\mathcal{C},\mathcal{D})_{places}$  fail to be closed.
% Pick $W$ a maximal one, then there must exist a P-node $B$ which witnesses
% that $W$ fails to be closed. $B$ cannot have a local trash outside $W$ by the
% maximality assumption, therefore $B$ has not any local trash in order to
% witness that $W$ is not closed.\\
% Let $\alpha$ be the grand event of $B$, since $B$ intersect $W$ it has at
% least one infinite element, by lemma \ref{cofinal2} $\powAst (B^{(\alpha )})$
% has infinitely many new elements.\\
% $B$ is a P-node therefore it must distribute all its elements
% besides $\powAst (B^{(\alpha )})\setminus\Sigma_{\alpha}$ is
% infinite and by greediness of the process $\Sigma_{\alpha
% +1}\setminus\Sigma_{\alpha}\supseteq\powAst (B^{(\alpha )})$. The
% above  facts cause the existence of, at least, one local trash
% for $B$.   \qed


Given a path $\mathcal{D}$ in a $\Places$-board $\mathcal{G}$, we
denote by $\PLACES{\mathcal{D}}$ and $\NODES{\mathcal{D}}$ the
collections of places and of nodes occurring in $\mathcal{D}$,
respectively. Moreover, given a node $B$ in $\mathcal{G}$, we denote
by $\PN{B}$ the collection of all nodes which have nonnull
intersection with $B$.
\begin{mydef}\label{pumpchain}\rm Let $\mathcal{C,D}$ be a pumping path
relative to a given colored $\Places$-process
\\
$\big(\Sigma_\mu\big)_{\mu\leqslant\ell},[\bullet],\TARGETS,\REDS,\POWNODES$,
with $\ell$ finite. Then $\langle(\mathcal{C},\overline{\mathcal{D}}_{0},
     \mathcal{D}_{1},\ldots,\mathcal{D}_{N}),\vec m,q_0,\sigma\rangle$ is called a
\emph{pumping chain} if
\begin{itemize}
     \item $\overline{\mathcal{D}}_{0},
     \mathcal{D}_{1},\ldots,\mathcal{D}_{N}$ is a partition of $\mathcal{D}$ into
     contiguous paths each ending with a place, where in particular
     \item $\mathcal{D}_{N}$ ends with the place $\sigma$;
     \item $\vec m=m_{0}, m_{1},\dots, m_{N}$ is a non-decreasing sequence
      $m_{0}\leqslant m_{1} <m_{2} < \ldots < m_{N}< \xi$
            of ordinals; and
        \item putting $\mathcal{D}_{0} \equivAs \mathcal{C},\overline{\mathcal{D}}_{0}$, we have:
\begin{itemize}
     \item[(i)] $q_0 \in
     \PLACES{\mathcal{C}}$ and $q^{[m_{0}]} \setminus \bigcup\bigcup
     \Places^{[m_{0}]} \neq \emptyset$;

     \item[(ii)]  $\GE(\PN{\PLACES{\mathcal{D}_{i}}}) \geqslant m_{i}$, for
     $i=0,1,\ldots,N$;

     \item[(iii)] $\powAst(B^{[m_{i}]}) \neq \emptyset$
     (i.e., $\emptyset\notin B^{[m_{i}]}$), for $B
     \in \NODES{\mathcal{D}_{i}}$ and $i=0,1,\ldots,N$.  \eod
\end{itemize}
\end{itemize}
\end{mydef}



\begin{myremark}\rm For a wholesale re-use of all notation
concerning formative processes, we designate the entities associated with the shadow process as
$\widehat{\_}^{[\_]}$ ($\widehat{q}^{[i]}$, $\widehat{B}^{[i]}$, $\Delta^{[i]}(q)$,
etc.).

Related to a weak ``shadow'' formative process
$\widehat{\varpi}=(\{\widehat{q}^{[i]}\}_{q\in\Places})_{i
\leqslant \ell}$, we use the collection of ``salient'' steps $\{\mu_{i}\}_{i
\leqslant \ell}$ of the original process, as defined in
\cite[Def.~7.1]{COU02}.
\end{myremark}

\begin{mydef}\rm
A set $\mathcal{W}$ of places is said to be \textsc{closed} for a {colored $\Places$-process}\\
$\left(\{q^{(\mu)}\}_{q\in\Places}\right)_{\mu\leqslant\xi},
(\bullet),\TARGETS,\REDS,\POWNODES$
if
\begin{des}
\item all of its elements are green;
\item every $\Pow$-node which intersects $\mathcal{W}$ has a local
trash belonging to $\mathcal{W}$\/.
\end{des}

If $\cal C$ is a path in a $\Places$-board, we define a collection of places $B$ to be a \textsc{closure} of $\cal C$
when $B$ is closed and it contains $\PLACES{{\cal C}}$.
A path $\cal C$ is said to be \textsc{closure equipped} whenever it owns a closure.
\eod \end{mydef}

\begin{myremark}\label{orderiso}\rm
Observe that the following function $i\mapsto\mu_{i}$ is an order
isomorphism between the following structures $(\ell,<)$ and
$(\{\mu_{i}\}_{i\leqslant \ell},<)$. This fact has valuable consequences:
\begin{itemize}

         \item[(i)] For every node $B$, $\mu_{\GE(\widehat{B})}=\GE(B)$;
         \item[(ii)] $g$ is a local trash for $A$ if and only if
$\widehat{g}$ is a local trash for $\widehat{A}$;
         \item[(iii)] $\widehat{{\cal C}}$ is closure equipped if and only
if ${\cal C}$ is closure equipped.

\end{itemize}
\end {myremark}

\begin{myremark}\label{elemprop1}\rm
The following properties are easily verified.
\begin{itemize}

         \item $q^{[m_{0}]}
         \setminus q^{[m_{0}-1]} \neq \emptyset$ implies $q^{[m_{0}]} \setminus
         \bigcup\bigcup \Places^{[m_{0}]} \neq \emptyset$.

         \item  If $\powAst(B^{(\mu_{j})}) \neq \emptyset$ then
         $\powAst(\widehat{B}^{[j]}) \neq \emptyset$.
\end{itemize}

\end {myremark}

% We choose the following shorthand notation
% $(\mathcal{D})_{places}[(\mathcal{D})_{nodes}]$ to briefly
% indicate the collection of all places [respectively nodes]
% contained in an assigned subgraph and $PN(A)$ to indicate the
% following collection of nodes $\{ B\mid\ B\cap A\neq\emptyset\}$.

% \begin{mylemma}\label{cofinal1}
% Let $A$ be a cofinal subset of a limit ordinal $\lambda$ then there are
% infinitely many different subsets cofinal in $\lambda$.
% \end{mylemma}
% \proof Let $\alpha$ be the order type of $<A,\leqslant>$, where
% $\leqslant$ is meant to be the
% usual order on the ordinals.\\
% $\alpha$ is obviously infinite otherwise $\lambda$ should be not limit.\\
% So far we simply provided $A$ of a set of indices $\alpha$,
% from now later on we indicate $A$ as the sequence
% $\{a_{\beta}\}_{\beta<\alpha}$.\\
% Let now consider
% the following initial segment $\{a_{i}\}_{i<\omega}$ [obviously if
% $\alpha=\omega$ this is the whole sequence].\\
% Let $\varphi$ be a bijection between $\omega\times\omega$ and
% $\omega$. The following countable collection of subsets of $A$
% provides the desired collection of infinitely many different
% subsets cofinal in $\lambda$:
% $$K_i=\{a_{\varphi(i\times j)}\}_{j\in\omega} \cup
% \{a_{\beta}\}_{\beta\in\alpha\setminus\omega}$$
% \qed

% \newpage
The following is the key result of the present section.
%
Roughly speaking, it shows that the ``shadow'' formative process
$\widehat{\varpi}=(\{\widehat{q}^{[i]}\}_{q\in\Places})_{i
\leqslant \ell}$ discovered in \cite{COU02} preserves the pumping chains.
\vspace{0.2cm}

\begin{mylemma}\label{pumping1}
If $\Places$ with greedy formative process $\varpi =
(\{q^{(\alpha)}\} _{q\in\Places})_{\alpha\leqslant\xi}$ has an
infinite place $p^{(\bullet)}$, then $\widehat{\Places}$, with
weak ``shadow'' formative process
$\widehat{\varpi}=(\{\widehat{q}^{[i]}\}_{q\in\Places})_{i
\leqslant \ell}$ and with salient steps $\{\mu_{i}\}_{i
\leqslant \ell}$, owns a pumping chain at $\widehat{p}$ which is closure equipped.
\end{mylemma}

\proof By \thm{liesOnPump}, $p$ lies on a pumping path which can
be split into paths $\mathcal{C},\mathcal{D}',\mathcal{D}''$ such
that
\begin{enumerate}
\item $\mathcal{C}$ is a cycle;
\vspace{-.3cm}
\item the path $\mathcal{C},\mathcal{D}'$ ends with a place $g$ whose
$\leastInf(g)$ is a limit ordinal $\lambda$;
\vspace{-.3cm}
\item $0<\leastInf(q)\;\leqslant\;\lambda\;=\;\bigcup I_{q,\lambda}^B$
holds, where
$$I_{q,\lambda}^B\;\defAs\; \{\nu<\lambda\st A_\nu=B\And
q^{(\nu+1)}\neq q^{(\nu)}\}\:,$$ for every edge $\langle B,q \rangle$ lying on
$\mathcal{C},\mathcal{D}'$;
\vspace{-.3cm}
\item $\lambda \leqslant \leastInf(B) < \leastInf(q)$, for every edge
$\langle B,q\rangle$ lying on $\mathcal{D}''$;
\vspace{-.3cm}
\item $\leastInf(q) \leqslant \leastInf(B)$, for every edge $\langle
q,B \rangle$ lying on $\mathcal{D}''$.
\end{enumerate}

% $\mathcal{C}$ is a cycle, $\mathcal{C},\mathcal{D}'$ ends
% with a place $g$ whose $\leastInf(g)$ is a limit ordinal
% $\lambda$, $\leastInf$ strictly increases along $\mathcal{D}''$,
% and $\leastInf(q)\leqslant\lambda$ for every place $q$ lying on
% $\mathcal{C},\mathcal{D}'$.

We will show that
$\mathcal{C},\mathcal{D}',\mathcal{D}''$ is actually a pumping
chain relative to the shadow formative process $\widehat{\varpi}$.

Let
% $$\widehat{\lambda} \defAs \left\{
% \begin{array}{ll}
% \min \{i \mid \mu_{i} \geqslant \lambda\} & \text{if }
%    \{i \st \mu_{i} \geqslant \lambda\} \neq \emptyset\,, \\
% \ell + 1 & \text{otherwise}\,.
% \end{array}
% \right.
% $$
$$\widehat{\lambda} \defAs
\min \{i \st \mu_{i} \geqslant \lambda\} \,.
$$
Then we define
$$m_0 \defAs \max \big\{ 1 \leqslant i \leqslant \widehat{\lambda} \st
\langle A_{\mu_{i-1}},q\rangle \textrm{ lies on } \mathcal{C}
\textrm{ and } \widehat{q}^{[i]} \setminus \widehat{q}^{[i-1]}
\neq \emptyset\;\mbox{for some place $q$}\,\big\}\/.$$

Notice that the definition of $m_0$ is well-given, i.e.,
$$\big\{i\st 1\leqslant i\leqslant\widehat{\lambda},\;\langle
A_{\mu_{i-1}},q\rangle \textrm{ lies on } \mathcal{C} \textrm{ and
} \widehat{q}^{[i]} \setminus \widehat{q}^{[i-1]} \neq
\emptyset\;\mbox{for some place $q$}\,\big\}\:\neq\:\emptyset.$$
Indeed, let $q\in\PLACES{\mathcal{C}}$ and let $B$ be the
predecessor of $q$ in $\mathcal{C}$\/. Let $\mu_{j_0}\in
\mathit{Sal}$ be such that $B=A_{\mu_{j_0}}$,
$\disj{q^{(\mu_{j_0})}}{\powast{B^{(\mu_{j_0})}}}$\/, and
$\inters{q^{(\mu_{j_0}+1)}}{\powast{B^{(\mu_{j_0})}}}$\/. Since
$I_{\lambda,q}^B\neq\emptyset$\/, we have
$\mu_{j_0}<\lambda\leqslant\mu_{\widehat{\lambda}}$\/, so that
$1\leqslant j_0+1\leqslant\widehat{\lambda}$\/. Therefore,
$$j_0+1\in\,\big\{i\st 1\leqslant i\leqslant\widehat{\lambda},\;\langle
A_{\mu_{i-1}},q\rangle \textrm{ lies on } \mathcal{C} \textrm{ and
} \widehat{q}^{[i]} \setminus \widehat{q}^{[i-1]} \neq
\emptyset\;\mbox{for some place $q$}\,\big\}\,.$$

Next we define $\overline{\mathcal{D}}_{0}$ to be the longest
initial subpath of $\mathcal{D}',\mathcal{D}''$ which contains only
nodes occurring in $\NODES{\mathcal{C}}$.

Assuming that we have already defined the paths
$\overline{\mathcal{D}}_{0}, \mathcal{D}_{1}, \ldots,
\mathcal{D}_{k}$, each ending with a place, and the integers
$m_{0} \leqslant m_{1} < \ldots < m_{k}$, for some $k \geqslant
0$, we define $\mathcal{D}_{k+1}$ and $m_{k+1}$ as follows,
provided that $\mathcal{D}',\mathcal{D}'' \not\equiv
\overline{\mathcal{D}}_{0},\mathcal{D}_{1}, \ldots,
\mathcal{D}_{k}$. Let $D_{k+1}$ be the first node in
$\mathcal{D}',\mathcal{D}''$ not occurring in
$\overline{\mathcal{D}}_{0}, \mathcal{D}_{1}, \ldots,
\mathcal{D}_{k}$. We define $m_{k+1}$ as the least integer $j
\geqslant m_{k}$ such that $\powAst(\widehat{D}_{k+1}^{[j]}) \neq
\emptyset$. Moreover, we define $\mathcal{D}_{k+1}$ as the
longest subpath $\mathcal{E}$ of $\mathcal{D}',\mathcal{D}''$
starting at $D_{k+1}$, ending at a place, and such that
$\powAst(\widehat{D}^{[m_{k+1}]}) \neq \emptyset$, for each $D \in
\NODES{\mathcal{E}}$.

Since $\mathcal{D}',\mathcal{D}''$ is finite, the above
definitional process must terminate and produce a finite sequence
$m_{0} \leqslant m_{1} < \ldots < m_{N}$ of natural numbers and a
partition $\overline{\mathcal{D}}_{0}, \mathcal{D}_{1}, \ldots,
\mathcal{D}_{N}$ of $\mathcal{D}',\mathcal{D}''$ into contiguous
paths each ending with a place and such that $\mathcal{D}_{1}$
starts with the first node in $\mathcal{D}',\mathcal{D}''$ not
occurring in $\mathcal{C}$. Finally, we put $\mathcal{D}_{0}
\equivAs \mathcal{C},\overline{\mathcal{D}}_{0}$.

To show that $\mathcal{C},\mathcal{D}',\mathcal{D}''$ is a
pumping chain for the shadow process, it is now enough to verify
that conditions (i), (ii), and (iii) of \defn{pumpchain} are
satisfied, relative to the above partition of
$\mathcal{C},\mathcal{D}',\mathcal{D}''$ and to the sequence of
natural numbers $m_{0} \leqslant m_{1} < \ldots < m_{N}$.

\smallskip

Concerning condition (i), it is enough to observe that by the very
definition of $m_{0}$ we must have $q^{[m_{0}]} \setminus
q^{[m_{0}-1]} \neq \emptyset$, for some $q \in \PLACES{\mathcal{C}}$,
so that $q^{[m_{0}]} \setminus \bigcup\bigcup
     \Places^{[m_{0}]} \neq \emptyset$ follows immediately.

\smallskip

The proof that condition (ii) of \defn{pumpchain} is satisfied can be
simplified by the following properties(1-6), whose proofs are straightforward and are therefore omitted.

\begin{myproperty}\label{p1}
Let $q \in \Places$ and let $B \subseteq \Places$ such
that $q \in B$. Then $\GE(B) \geqslant \leastInf(q)$.
\end{myproperty}

\begin{myproperty}\label{p2}
Let $q \in \PLACES{\mathcal{D}''}$.
Then
\begin{itemize}
     \item[(a)] $\leastInf(q) > \lambda$;

     \item[(b)] for each node $D \in \NODES{\mathcal{D}''}$ which
     precedes $q$ in $\mathcal{D}''$, we have
     $\leastInf(q) > \leastInf(D)$.
\end{itemize}
\end{myproperty}
{\small \proof The property follows immediately from conditions 4 and 5 of
\thm{liesOnPump}.\qed}

\begin{myproperty}\label{p3}
Let $i \in \{1,\ldots,N\}$ and assume also that $m_{i-1} < m_{i}$.
If $D_{i}$ is the initial node of $\mathcal{D}_{i}$, then
\emph{$$
\min \{\mu < \xi \st \powAst(D_{i}^{(\mu)}) \neq \emptyset\} =
\mu_{m_{i}-1}+1\/.
$$}
\end{myproperty}



\begin{myproperty}\label{p4}
Let $D \in \NODES{\mathcal{C},\mathcal{D}'}$. Then
\emph{$$
\min \{\mu < \xi \st \powAst(D^{(\mu)})\neq \emptyset\} < \lambda\/.
$$}
\end{myproperty}


\begin{myproperty}\label{p5}
Let $q \in \PLACES{\mathcal{C},\mathcal{D}'}$ and let $B \subseteq
\Places$ be a node such that $q \in B$. Then $\GE(A) \geqslant
\lambda$.
\end{myproperty}


\begin{myproperty}\label{p6}
Let $i \in \{0,1,\ldots,\widehat{\lambda}\}$. Then
  $\mu_{i} < \lambda$.
\end{myproperty}

To show that condition (ii) of \defn{pumpchain} holds, it is enough to
prove that for every index $i \in \{0,1,\ldots,N\}$, place $q \in
\PLACES{\mathcal{D}_{i}}$, and node $B \subseteq \Places$ such that $q
\in B$, we have $\GE(B) \geqslant m_{i}$.

In view of Properties \ref{p1}--\ref{p6}, this can be done by
distinguishing the following cases:

\begin{itemize}
     \item[\textbf{I:}]
     $1 \leqslant i \leqslant N$,~~~
     $m_{i} > m_{i-1}$,~~~
     $q \in \PLACES{\mathcal{D}''}$,~~~ and ~~~
     $D_{i} \in \NODES{\mathcal{D}''}$;

     \item[\textbf{II:}]
     $1 \leqslant i \leqslant N$,~~~
     $m_{i} > m_{i-1}$,~~~
     $q \in \PLACES{\mathcal{D}''}$,~~~ and ~~~
     $D_{i} \in \NODES{\mathcal{D}'}$;

     \item[\textbf{III:}]
     $1 \leqslant i \leqslant N$,~~~
     $m_{i} > m_{i-1}$,~~~ and ~~~
     $q \in \PLACES{\mathcal{D}'}$;

     \item[\textbf{IV:}]
     $i = 1$~~~ and ~~~
     $m_{1} = m_{0}$;

     \item[\textbf{V:}]
     $i = 0$.
\end{itemize}

For instance, assume that conditions of case I hold. Then we have
$$
\begin{array}{lcll}
     \mu_{\GE(\widehat{B})} & = & \GE(B) & \mbox{(by Remark \ref{orderiso}(i))}   \\
      & \geqslant & \leastInf(q) & \mbox{(by Property~\ref{p1})}   \\
      & > & \leastInf(D_{i}) & \mbox{(by Property~\ref{p2}(b))}   \\
      & \geqslant & \min \{\mu < \xi \st \powAst(D_{i}^{(\mu)})
      \neq \emptyset\}  &  \mbox{(by the very definition of the $\leastInf$ of a node)}  \\
      & = & \mu_{m_{i}-1}+1 & \mbox{(by Property~\ref{p3})}  \\
      & > & \mu_{m_{i}-1} &
\end{array}
$$
Therefore $\widehat{\GE}(B) > m_{i}-1$, i.e., $\widehat{\GE}(B) \geqslant m_{i}$.

The remaining cases can be proved similarly, by suitably exploiting
Properties \ref{p1}--\ref{p6}.



\smallskip

Concerning condition (iii) of \defn{pumpchain}, let $B \in
\NODES{\mathcal{C}}$ and let $q \in \Places$ be the place such
that the edge $\langle B,q\rangle$ occurs in $\mathcal{C}$.  Let
$\overline{\mu} < \xi$ be the ordinal such that $B =
A_{\overline{\mu}}$, $q^{(\overline{\mu})} \cap
\powAst(B^{(\overline{\mu})}) = \emptyset$ and
$q^{(\overline{\mu}+1)} \cap \powAst(B^{(\overline{\mu})}) \neq
\emptyset$. Then, since $I_{q,\lambda}^{B} \neq \emptyset$, we
have $\overline{\mu} < \lambda$. Moreover, since $\overline{\mu}
\in \mathit{Sal}$, we must have $\overline{\mu} = \mu_{j_{0}}$,
for some $j_{0} \in \{0,1,\ldots, \ell-1\}$ such that
$\disj{\widehat{q}^{[j_0]}}{\powast{\widehat{B}^{[j_0]}}}$ and
$\inters{\widehat{q}^{[j_0+1]}}{\powast{\widehat{B}^{[j_0]}}}$.
Since $\mu_{j_{0}} = \overline{\mu} < \lambda\leqslant
\mu_{\widehat{\lambda}}$, we have $j_{0}+1 \leqslant \widehat{\lambda}$
and therefore $j_{0} < m_{0}$. In particular, since
$\powAst(B^{({\mu}_{j_{0}})})\neq \emptyset$, it follows that
$\powAst(\widehat{B}^{[m_{0}]}) \supseteq
\powAst(\widehat{B}^{[j_{0}]}) \neq \emptyset$, and therefore
$\powAst(\widehat{B}^{[m_{0}]}) \neq \emptyset$.

Since $\powAst(\widehat{B}^{[m_{j}]}) \neq \emptyset$ holds by
construction, for $B \in \NODES{\mathcal{D}_{j}}$ and
$j=1,\ldots,N$, it follows that condition (iii) of
\defn{pumpchain} is met.

Finally, by Remark \ref{orderiso}(iii), we can assert that
$\widehat{\varpi}=(\{\widehat{q}^{[i]}\}_{q\in\Places})_{i
\leqslant \ell}$, with salient steps $\{\mu_{i}\}_{i
\leqslant \ell}$, has a closure equipped pumping chain at
$\widehat{p}$.  \qed
% For a given transitive partition $\Sigma$ an element
% $x\in\bigcup\Sigma$ is said to be "new" iff
% $x\in\bigcup\Sigma\setminus\bigcup\bigcup\Sigma$.\\


% \begin{mydef}\label{lastcallgen}\rm
% For a given collection of nodes ${\cal A}$ we
% denote by $\GE({\cal A})$ the following ordinal $min \{\GE(A)\st A \in {\cal
% A}\}$  \end{mydef}
% \newpage


\section{A finite representation of an infinite model}
\label{se_fin_infin}

In this section we show how a finite transitive partition with a related formative process can be seen as a finite
representation of an infinite model.

Consider a transitive partition related to a model for a formula $\Phi^-$ of \MLSSP.
Assume that a formative process of such a transitive partition is equipped with a pumping chain.

Our goal consists in iterating the sequence of the pumping chain trying to preserve, roughly speaking, the satisfiability of the formula.
In this way we make the resulting model invariant under expansion of the formative process, which, from a semantic point of view, means that
some places can be increased without affecting the capability of the resulting transitive partition to model the formula.

Now let $\Phi$ be the previous formula enriched with new literals of the following type: $\neg Finite(x)$.
Provided that at least one place for each variable $x$ lies in the pumping chain, $\Phi$ is automatically satisfied
by the transitive process which results from an infinite prolongation of the formative process obtained by repeating infinitely many times
the pumping chain.

This in turn implies that the formative process with the pumping chain together with the model of $\Phi^-$ can be seen as
a finite representation of an infinite model of $\Phi$.

The following definitions serve the above strategy.

\begin{mydef}\rm
When $\Phi$ is a formula of \MLSSPF, we denote by $\Phi^-$ the formula which results
from $\Phi$ by withdrawal of all literals of the form $\neg Finite(x)$.
\eod\end{mydef}
\begin{mydef}\rm
When $\Phi$ is a formula of \MLSSPF, we name \textsc{a collection
of infinite for $\Phi$} any subcollection $\Gamma$ of $\Sigma_{{\mathcal X}_{\Phi}}$ which satisfies
the following requirement: for any infinite clause  $\neg Finite(x)$
in $\Phi$ there exists a $\sigma\in\Gamma\cap\Im(x)$.
\eod\end{mydef}

These definitions enable us to summarize the content of the
preceding sections into the following
necessary condition for satisfiability of an \MLSSPF-formula.
\begin{mytheorem}\label{necessita}
Let $\Phi$ be a satisfiable formula of \MLSSPF. Then there exist a model
${\cal M}\in\{\:\mbox{\rm sets}\:\}^{{\mathcal X}_{\Phi}}$
of $\Phi^-$ and a formative process
$(\Sigma_{i})_{i\leqslant\ell}$ for $\Sigma_{{\mathcal X}_{\Phi}}$
such that:
\begin{itemize}
\item $\ell\leqslant f(\vert{\mathcal X}_{\Phi}\vert)$, where $f\in\N^{\N}$ is a specific
computable function;
\item the canonical board of ${\cal M}$ satisfies the following condition:

There exists a ``collection of infinite'' $\Gamma$ for $\Phi$ such
that to every $\sigma\in\Gamma$ there corresponds a pumping chain, closure
equipped, at $\sigma$.

\end{itemize}
\end{mytheorem}

The main result of this section is to show that these conditions are
sufficient, too. Remember that, in order to preserve the
satisfiability of the \MLSSP literals, we must guarantee satisfaction of the
conditions 1-3 listed in Section~\ref{sse_Venn}. Hence our claim
consists in detecting which structural properties two formative
processes have to share in order to produce transitive partitions which
model the same \MLSSP literals. Then we can verify those
properties with the original process and the process obtained from the
previous one by repeating infinitely many times the sequence of the
pumping chain. If these properties are not disrupted by prolongation of the formative
process, we obtain automatically a transitive partition that simultaneously satisfies the
\MLSSP literals and makes the variables involved in the
pumping chain infinite through one or more of their places.
Thus the infinite clauses $\neg Finite(x)$ of $\Phi$ will be satisfied,
because the prolongation can be performed for any pumping chain of the original
formative process and the following holds
\begin{quote}
``There exists a `collection of infinite' $\Gamma$ for $\Phi$ such
that to every $\sigma\in\Gamma$ there corresponds a pumping chain, closure
equipped, at $\sigma$.''
\end{quote}

In order to proceed with such approach, we need some technical tools
which have been introduced in \cite{Urs06}.  For the reader's
convenience, we report below the essential proofs and definitions.

\begin{mydef}\rm
$e\in\bigcup\Places^{(\bullet)}$ is said to be \textsc{unused}
at $\mu\leqslant\xi$ if $e\notin
\bigcup\bigcup\Places^{(\mu)}$, i.e., if $e\notin z$ for any
$q\in\Places$ and any $z\in q^{(\mu)}$.

We denote by {\em unused}$(q)$ the collection of all unused elements of $q$.
\eod\end{mydef}

\begin{mydef}\rm
An $e\in\bigcup\Places^{(\bullet)}$ is said to be \textsc{new}
at $\mu\leqslant\xi$ if $e\in\Delta^{(\mu)}(q)$ for some $q\in\Places$.
\eod\end{mydef}

Obviously a new element is, in particular, unused.

\begin{mylemma}\label{unused}
If $b$ is a set made of unused elements only, the same is true of
$\powast{\{b\}\cup A}$.
\end{mylemma}

We shall adopt the following notation. For a couple of
ordinals $\beta ',\beta ''$ we denote by
$[\beta ',\beta '']$ the collection of ordinals
$\{\beta\st \beta '\leqslant\beta\leqslant\beta ''\}$.

The following definitions are introduced to distinguish between the
new sets used to imitate the old process and elements used to
increase the cardinality of the places in the collection of infinity.

We say that a transitive partition $\Sigma$ is equipped with a Minus-Surplus
partitioning if each block $q$ is partitioned into two sets,
namely, $\text{Surplus}(q)$ and
$\text{Minus}(q)$. Consistently, we can extend this notation to a
formative process $\big(\Sigma_\mu\big)_{\mu\leqslant\xi}$.
Given a node $\Gamma$, we indicate by $\text{Minus}(\Gamma ^{(\mu)})$
the collection of sets
$$\{\text{Minus}(q^{(\mu)})\st q\in\Gamma\}.$$
Define now a Minus-Surplus partitioning for $\Sigma _0$, and assume that
for each step $\mu$ of the process a refinement of the partition
$\{\Delta ^{(\mu)}(q)\}_{q\in\Sigma}$ is carried out
in the following way:
for each $q\in\Sigma$, the set $\Delta ^{(\mu)}(q)$
is split into two sets
$\Delta ^{(\mu)}\text{Minus}(q)\subseteq\powAst (\text{Minus}(A_{\mu}^{(\mu)}))$
and $\Delta ^{(\mu)}\text{Surplus}(q)\subseteq(\powAst(A_{\mu}^{(\mu)})\setminus
\powAst (\text{Minus}(A_{\mu}^{(\mu)}))$.\\
Then define inductively $$\text{Surplus}(q^{(\mu+1)})=\text{Surplus}(q^{(\mu)})\cup
\Delta ^{(\mu)}\text{Surplus}(q)$$ and
$$\text{Minus}(q^{(\mu+1)})=\text{Minus}(q^{(\mu)})\cup\Delta ^{(\mu)}\text{Minus}(q).$$
As for $\xi$,  put
$$\text{Minus}(q^{(\xi)})=\bigcup_{\mu <\xi}\text{Minus}(q^{(\mu)})$$
and, analogously,
$$\text{Surplus}(q^{(\xi)})=\bigcup_{\mu <\xi}\text{Surplus}(q^{(\mu)})$$
If $\Gamma$ is a subset of $\Sigma$, we denote by $\text{Surplus}(\Gamma)$ the
set
$$\{q\in\Gamma\st \text{Surplus}(q)\neq\emptyset\}.$$
\begin{mydef}\rm
Whenever a Surplus-Minus partition is defined for all blocks of a
transitive partition $\Sigma$, we say that $\Sigma$ is equipped with
a \textsc{Minus-Surplus partitioning},
and we denote by $\text{Surplus}$-$\text{Minus}(\Sigma )$ the following
refinement of the original partition:
$$\{\text{Minus}(q),\text{Surplus}(q)\wt q\in\Sigma\}.$$
It is rather obvious that $\text{Surplus}$-$\text{Minus}(\Sigma )\sqsubseteq\Sigma$.
\eod\end{mydef}

\begin{myremark}\label{powdisj}\rm
Easy combinatorial arguments (see \cite[Lemma 3.1 5(b)]
{COU02})
show that $\powast\_$ of Surplus
and Minus nodes are mutually disjoint.
\end {myremark}
Whenever you have to compare two formative processes, as in dynamical systems, you have to check initial conditions of the phenomenon and the way
it evolves. In our cases the initial conditions are the two starting transitive partitions and the evolutions are the couple of formative processes
that begin with the above transitive partitions. Therefore the conditions of similiarity are to be divided into two groups, the former on the
initial conditions the latter on the evolutions.

The following requirements are to be satisfied as
initial conditions of a transitive partition
in order to play the role of starting point of an imitation process
(as is easily seen, they are merely combinatorial).

\begin{mydef}\label{weakimit}\rm
Let
$\left(\{q^{(\mu)}\}_{q\in\Places}\right)_{\mu\leqslant\xi},
(\bullet),\TARGETS,\REDS,\POWNODES$
be a {colored $\Places$-process},
$(\widehat{\Sigma},\widehat{\mathcal{G}})$ be a {$\widehat{\Sigma}$-board}
equipped with a Minus-Surplus
partitioning,
$q\mapsto \widehat{q}$ be a bijection from $\Places$
to $\widehat{\Places}$, and
${\mathcal C}$ be a closed collection of green blocks.
Assume $k'<\xi$,
such that (i), (vii), (viii) and (x) of Def.~\ref{formimit} hold in the version
$\widehat{\Sigma}_{\gamma (k')}=
\widehat{\Sigma}$.
We say that $\widehat{\Sigma}$ \textsc{weakly imitates}
$\Sigma$ \textsc{upwards}, provided that
the following conditions are satisfied:
\begin{itemize}
\item [(a)] for all $\Gamma\subseteq\Sigma$ and $q\in\Sigma$,
$$\bigcup \text{Minus}(\widehat{\Gamma})\in\powAst (\text{Minus}(\widehat{\Gamma}))
\setminus \bigcup _{q\in\Sigma}\widehat{q}\quad {\rm iff}
\quad\bigcup\Gamma^{(k')}\in
\powAst (\Gamma^{(k')})\setminus \bigcup _{q\in\Sigma}q^{(k')};$$
\item [(b)] $q\in\Gamma\wedge \text{Surplus}(q)\neq\emptyset\wedge \GE(\Gamma)\geqslant k'$
implies $\bigcup\widehat{\Gamma}\in\powAst
(\widehat{\Gamma})
\setminus \bigcup _{q\in\Sigma}\widehat{q}$;
\item [(c)] if $\GE(\Gamma)<k'$, then $\bigcup\Gamma^{(k')}\in q^{(k')}$ iff
$\bigcup \widehat{\Gamma}\in \widehat{q}$ and $\Gamma\in\POWNODES$
implies $\powAst (\widehat{\Gamma})\subseteq\bigcup\widehat{\Sigma}$.\eod
\end{itemize}
\end{mydef}

The following are instead the properties that guarantee that the processes are similar enough in order to produce transitive partitions
that model the same \MLSSP literals.

\begin{mydef}\label{formimit}\rm
Let
$\left(\{q^{(\mu)}\}_{q\in\Places}\right)_{\mu\leqslant\xi},(\bullet),
\TARGETS,\REDS,\POWNODES$
be a {colored $\Places$-process}. Besides, let\\
$\big(\{\widehat{q}^{[\alpha]}\}_{\widehat{q}\in\widehat{\Places}}\big)_
{\alpha\in [\alpha',\alpha '']}$ be
a simple formative processes equipped with a Minus-Surplus
partitioning. Assume that
$q\mapsto \widehat{q}$ is a bijection from $\Places$ to
$\widehat{\Places}$,
$\beta''\leqslant\xi$, and $\gamma$ is an order preserving
injection from
$[\beta ',\beta '']$ to $[\alpha',\alpha '']$.
Let ${\mathcal C}$ be a closed collection of green blocks,
and $q\mapsto \widehat{q}$ be a bijection from $\Places$ to
$\widehat{\Places}$.
We
say that $\big(\{\widehat{q}^{[\alpha]}\}_{\widehat{q}
\in\widehat{\Places}}\big) _{\alpha\in\gamma
[[\beta ',\beta '']]}$ \textsc{imitates}
the segment $[\beta ',\beta '']$ of the process
$(\left(\{q^{(\mu)}\}_{q\in\Places}\right)_{\mu\leqslant\xi}$
if the following hold
for all $\beta$ in $[\beta ',\beta '']$:
\begin{itemize}
\item[(i)]$\vert q^{(\beta)}\vert=\vert \text{Minus}^{[\gamma(\beta)]}(\widehat{q})\vert$;
\item[(ii)] $\vert \Delta ^{(\beta)}(q)\vert=
\vert\Delta ^{[\gamma (\beta)]} \text{Minus}(\widehat{q})\vert$;
\item[(iii)]$\Delta ^{[\gamma (\beta)]}\text{Surplus}(\widehat{q})\neq\emptyset$
implies
$\beta=\GE(A_{\beta})$, $q$ local trash for $A_{\beta}$ and
$q\in {\mathcal C}$;
\item[(iv)] If $\Gamma\in\POWNODES$ holds, then
$\powast{\widehat{\Gamma}^{[\gamma (\GE(\Gamma))]} }
\subseteq\bigcup\widehat{\Sigma}^{[\gamma (\GE(\Gamma)+1)]}$;
\item[(v)]For all $\beta\ne \GE(\Gamma)$
$\bigcup\Gamma^{(\beta)}\in\Delta ^{(\beta)}(q)$ iff
$\bigcup \text{Minus}\widehat{\Gamma}^{[\gamma (\beta)]}\in\Delta ^{[\gamma (\beta)]}(
\widehat{q})$;
\item[(vi)] If $\beta =\GE(\Gamma)$ then $\bigcup\Gamma^{(\beta)}\in
\Delta ^{(\beta)}(q)$ iff
$\bigcup\Gamma^{[\gamma (\beta)]}\in\Delta ^{[\gamma (\beta)]}(\widehat{q})$;
\item[(vii)] For all $q\in\REDS$ $\widehat{q}^{[\gamma (\beta)]}=
\text{Minus}^{[\gamma(\beta)]}(\widehat{q})$;
\item[(viii)] For all ordinals $\beta$ $\{q\wt
\widehat{q}\in \text{Surplus}(\widehat{\Sigma})^{[\gamma (\beta)]}\}
\subseteq{\mathcal C}$;
\item[(ix)] $\vert\powAst (\text{Minus} (\widehat{\Gamma}^{[\gamma(k)]}))
      \setminus \bigcup _{q\in\Sigma}q^{[\gamma(k)]}\vert=
\vert\powAst (\Gamma) ^{(k)}\setminus \bigcup _{q\in\Sigma}q^{(k)}\vert$;
\item[(x)] $\vert\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k-1)]})) \cap  q^{
[\gamma(k)]}\vert
=\vert \powAst (\Gamma^{(k-1)})\cap q^{(k)}\vert$.
\end{itemize}
\eod\end{mydef}

\smallskip
\begin{myremark}\rm
\label{rem1}
We make some simple remarks.
\begin{itemize}
\item $\powAst (\Gamma^{(k-1)})\cap q^{(k)}=\powAst (\Gamma^{(k)})\cap q^{(k)}$. Hence,
whenever $\gamma (k)$ is the successor of $\gamma (k-1)$, (x) can be rephrased as
$$\vert\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]})) \cap  q^{
[\gamma(k)]}\vert =\vert \powAst (\Gamma^{(k)})\cap q^{(k)}\vert.$$
\item Naturally, (ix) belongs to the structural properties that a
formative process has to fulfill in order to
simulate another one, although it can be obtained from (i) and (x).
\item Assume that (viii) holds at the beginning of the process.
Then (iii) entails (viii); therefore, in order to prove inductively
the previous properties, it suffices to show that (viii) holds at the outset.
The same argument holds for (x), which can be obtained from (ii), (iii) and (x)
of the preceding step.
\end{itemize}
\end {myremark}

%\begin{mylemma}\label{formimit-imit}
%Assume $\big(\Sigma_\mu\big)_{\mu\leqslant\xi}$ imitates
%$\big(\Sigma'_\mu\big)_{\mu\leqslant\xi}$
%if moreover $\Sigma_0$ imitates $\Sigma_0'$ then $\Sigma_{\xi}$ imitates
%$\Sigma_{\xi}'$
% \end{mylemma}

In a sense the initial conditions are very strong requests: in fact,
whenever they are satisfied we can imitate any formative process
that has one of them as starting point, as the following lemma shows.

\begin{mylemma}\label{pasting}
Let $\left(\{q^{(\mu)}\}_{q\in\Places}\right)_{\mu\leqslant\xi},
(\bullet),\TARGETS,\REDS,\POWNODES$ be a {colored $\Places$-process},
$(\widehat{\Sigma},\widehat{\mathcal{G}})$ be a {$\widehat{\Sigma}$-board}
whose $\widehat{\Sigma}$ is equipped with a Minus-Surplus
partitioning,
$q\mapsto \widehat{q}$ be a bijection from $\Places$
to $\widehat{\Places}$, and
${\mathcal C}$ be a closed collection of green blocks.
Assume that $k'\leqslant\xi$, and that
$\widehat{\Sigma}$ weakly imitates $\Sigma_{k'}$ upwards.
Define $\widehat{\Sigma}=\widehat{\Sigma}_{\gamma(k')}$ and, for all
$q\in\widehat{\Places}$,
$\widehat{q}=\widehat{q}^{[\gamma(k')]}$.
Then for all ordinals
$k''$ such that $k''\leqslant\xi$ and $\vert [k',k'']\vert <\omega$,
one can construct a formative process
$\big(\{\widehat{q}^{[\alpha]}\}_{\widehat{q}
\in\widehat{\Places}}\big)_{\gamma(k')\leqslant\mu\leqslant\gamma(k'')}$
imitating the segment $[k',k'']$ of
$\left(\{q^{(\mu)}\}_{q\in\Places}\right)_{\mu\leqslant\xi},
(\bullet),\TARGETS,\REDS,\POWNODES$.
\end{mylemma}
\begin{proof}
We construct a formative process satisfying the conditions (i)--(x) by induction.

Concerning the base case $\mu =\gamma (k')$,
(i), (vii), (viii), (x) hold by hypothesis, and
(ix) holds by Remark~\ref{rem1}, since (i) and (x) hold.
Assume $k'\ne \GE(A_{k'})$; then,
using (ix) and hypothesis (a), we can define a partition
$\bigcup_{q\in\Sigma}(\Delta
^{[\gamma(k')]}(q)$ of
$$\powAst (\text{Minus}
^{[\gamma(k')]}(\widehat{A_{k'}}))\setminus\bigcup _{q\in\Sigma}q^{[\gamma(k')]}$$
such that (ii) and (v) hold, as well.
If $k'=\GE(A_{k'})$ and $\text{Surplus}(\widehat{q}^{[\gamma(k')]})\neq\emptyset
$ for some $q\in A_{k'}$
(otherwise we proceed as before, and condition
(vi) is automatically satisfied),  then,
using (b), interchanging $\bigcup \text{Minus}(\widehat{A_{k'}}^{[\gamma(k')]})$ with
$\bigcup A^{[\gamma(k')]}$, (vi) is satisfied.

If $A_{k'}\in\POWNODES$ and $\widehat{A_{k'}}=\text{Minus}(\widehat{A_{k'}})$, proceed as
before (in this case (iv) holds by a straight checking
of cardinality starting from (ix)).
Otherwise, since (viii) holds,
there must exist a local trash
$q\in {\mathcal C}$ for $A_{k'}$.
Then, construct the partition as before, except
for $\Delta^{[\gamma(k')]}\text{Surplus}(\widehat{q})$, in which  we put
the whole remainder
$$(\powAst (\widehat{A_{k'}}^{[\gamma(k')]})
\setminus \bigcup _{q\in\Sigma}q^{[\gamma(k')]})\setminus
\bigcup_{q\in\Sigma}\Delta^{[\gamma(k')]} \text{Minus}(\widehat{q}),$$
so satisfying
(iii) and (iv).

Now, assume all the inductive hypotheses for $\gamma(k)$. Our aim
is to demonstrate
the case $\gamma(k+1)$.
By Remark~\ref{rem1}, provided that (iii)[$\gamma(k+1)$] is proven,
(viii) automatically holds.
Plainly (i)[$\gamma(k)$] and (ii)[$\gamma(k)$] entail
(x)[$\gamma(k+1)$] and (i)[$\gamma(k+1)$]. The latter
in its turn implies the following for all $\Gamma\subseteq\Sigma$\/:
\begin{equation}
\label{pow2}
\vert\powAst (\text{Minus} ^{[\gamma(k+1)]}\widehat{\Gamma}))\vert=\vert
\powAst (\Gamma^{(k+1)})\vert.
\end{equation}

In order to show (ix) we observe that,
since
\begin{eqnarray*}
\lefteqn{\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k+1)]})\setminus
\bigcup _{q\in\Sigma}q^{[\gamma(k+1)]}}\\
&=& (\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k+1)]})
\setminus\powAst (\text{Minus}(\Gamma^{[\gamma(k)]}))
\setminus
\bigcup _{q\in\Sigma}q^{[\gamma(k+1)]})\cup \\
&& \cup(\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))
\setminus
\bigcup _{q\in\Sigma}q^{[\gamma(k+1)]}),
\end{eqnarray*}
it follows that
\begin{eqnarray*}
\lefteqn{\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k+1)]}))\setminus
\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))
\setminus
\bigcup _{q\in\Sigma}q^{[\gamma(k+1)]}}\\
&=&\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k+1)]}))
\setminus\powAst (\text{Minus}(\Gamma^{[\gamma(k)]})).
\end{eqnarray*}
Therefore,
\begin{eqnarray*}
\lefteqn{\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k+1)]}))\setminus
\bigcup _{q\in\Sigma}q^{[\gamma(k+1)]}}\\
&=&\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k+1)]}))
\setminus\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))
\cup\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))
\setminus
\bigcup _{q\in\Sigma}q^{[\gamma(k+1)]}.
\end{eqnarray*}
Reasoning in the same way, we obtain
\begin{eqnarray*}
\lefteqn{\powAst (\Gamma)^{(k+1)}\setminus\bigcup_{q\in\Sigma}q^{(k+1)}}\\
&=& \powAst (\Gamma)^{(k+1)}\setminus\powAst (\Gamma)^{(k)}\cup\powAst (\Gamma)^{(k)}
\setminus\bigcup _{q\in\Sigma}q^{(k+1)}.
\end{eqnarray*}
By the induction hypothesis (i)[$\gamma(k)$] we have
$\vert\powAst (\text{Minus} ^{[\gamma(k)]}\widehat{\Gamma}))\vert=\vert
\powAst (\Gamma^{(k)})\vert$ and, by
equation~\eqref{pow2},
$$\vert\powAst (\text{Minus} ^{[\gamma(k+1)]}\widehat{\Gamma}))\vert=\vert
\powAst (\Gamma^{(k+1)})\vert,$$
which in its turn implies
$$\vert\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k+1)]}))\setminus\powAst
(\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))\vert=\vert\powAst (\Gamma)^{(k+1)}\setminus
\powAst (\Gamma)^{(k)}\vert.$$

Hence we are left to prove the equality
\begin{equation}
\label{pow3}
\vert\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))
\setminus
\bigcup _{q\in\Sigma}q^{[\gamma(k+1)]}\vert=\vert\powAst (\Gamma)^{(k)}
\setminus\bigcup _{q\in\Sigma}q^{(k+1)}\vert.
\end{equation}
Observe that
$$\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))
\setminus
\bigcup _{q\in\Sigma}q^{[\gamma(k+1)]}=\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))
\setminus\bigcup _{q\in\Sigma}
q^{[\gamma(k)]}\setminus\bigcup _{q\in\Sigma}\Delta^{[\gamma (k)]}\text{Minus}(q).$$
If $\Gamma\neq A_{k}$, by the disjointness of $\powAst$ we get
$$\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))
\setminus\bigcup _{q\in\Sigma}
q^{[\gamma(k)]}\setminus\bigcup _{q\in\Sigma}\Delta^{[\gamma (k)]}\text{Minus}(q)=
\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))\setminus\bigcup _{q\in\Sigma}
q^{[\gamma(k)]}.$$
Plainly, the same is true in the $\_ ^{()}$ version, thus \eqref{pow3}
holds for $\gamma(k)$, by virtue of (ix).
Otherwise, since $\bigcup _{q\in\Sigma}\Delta^{[\gamma (k)]}\text{Minus}(q)$
is a partition of a subset extract from
$$\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))
\setminus
\bigcup _{q\in\Sigma}q^{[\gamma(k)]},$$
we have that
\begin{eqnarray*}
\lefteqn{\left\vert\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))
\setminus\bigcup _{q\in\Sigma}
q^{[\gamma(k)]}\setminus\bigcup _{q\in\Sigma}\Delta^{[\gamma (k)]}
\text{Minus}(q)\right\vert}\\
&=&\left\vert\powAst (\text{Minus}(\widehat{\Gamma}^{[\gamma(k)]}))
\setminus\bigcup _{q\in\Sigma}
q^{[\gamma(k)]}\vert -\sum _{q\in\Sigma}\vert\Delta^{[\gamma (k)]}
\text{Minus}(q)\right\vert\,.
\end{eqnarray*}
Again, the same holds in the $\_ ^{()}$ version, and
\eqref{pow3} is reached by (i)[$\gamma(k)$] and (ii)[$\gamma(k)$].
This concludes the proof of (ix)[$\gamma(k+1)$].

Concerning (vii)[$\gamma(k+1)$], observe that
$q^{[\gamma(k+1)]}=q^{[\gamma(k)]}\cup\Delta^{[\gamma (k)]}(q)$.
By the induction hypothesis (vii)[$\gamma(k)$],
$$q^{[\gamma(k)]}=\text{Minus}(q^{[\gamma(k)]}).$$
On the other side,
since (iii)[$\gamma(k)$] holds and ${\mathcal C}$
is composed of green places only,
$$\Delta^{[\gamma (k)]}(q)=\Delta^{[\gamma (k)]}\text{Minus}(q),$$
which implies (vii)[$\gamma(k+1)$].

Regarding (ii)[$\gamma(k+1)$]-(vi)[$\gamma(k+1)$], the argument goes like
in the base case.
\end{proof}
\qed


The following theorem shows that our requests are well done, that means that they are sufficient for the role we are expected to play.
Indeed, they produce transitive partitions that model the same \MLSSP literals.


\begin{mytheorem}\label{upwards}
\begin{sloppypar}
    Let
$(\left(\{q^{(\mu)}\}_{q\in\Places}\right)_{\mu\leqslant\xi},
(\bullet),\TARGETS,\REDS,\POWNODES)$
be a {colored $\Places$-process}. Moreover, let
$\big(\{\widehat{q}^{[\alpha]}\}_{\widehat{q}\in
\widehat{\Places}}\big)_{\alpha\leqslant\xi '}$ be another formative process,
equipped with a Minus-Surplus partitioning.
Assume that, for some $k'\leqslant\xi$ and $m\leqslant\xi '$,
\end{sloppypar}
\begin{itemize}
\item $\widehat{\Sigma}_{m}$ {weakly imitates}
$\Sigma_{k'}$ {upwards};
\item the process
$\big(\{\widehat{q}^{[\alpha]}\}_{\widehat{q}\in\widehat{\Places}}
\big)_{\alpha\in\gamma [k',\xi]}$ {imitates}
$\big(\{q^{(\mu)}\}_{q\in\Places}\big)_{k'\leqslant\mu\leqslant\xi}$, where $\gamma$ is an
injective map from $[k',\xi]$ to $[m,\xi ']$;
\item $\widehat{\Sigma}_{\xi '}$ has the same targets as $\Sigma_{\xi}$;
\item for all $\mu >m$ such that $\mu\notin\gamma [k',\xi]$, the following holds:
$\Delta^{[\mu]}(\widehat{q})\subseteq\Delta^{[\mu]}\text{Surplus}(\widehat{q})$;
\item
if $\beta$ is the largest ordinal
such that
$\beta\in\gamma[k',\xi]\wedge\beta\leqslant\mu$, if
$q$ is a local trash of ${A}_{\mu}$, and if $\GE(A_{\mu})>\gamma^{-1}(\beta)$,
then $\bigcup\widehat{A_\mu}^{[\xi ']}\notin
\Delta^{[\mu]}\text{Surplus}(\widehat{q})$.
\end{itemize}
%[MANCA DEFINIZIONE
%LOCAL TRASH RELATIVO AD UN ORDINALE] relatively to $\gamma (\mu)$ where
%$\gamma (\mu)$ is the max of the following set $\{\gamma [k',\xi]\cap
%[0,\mu] \}$

Consider an \MLSSPF-formula $\Phi$,
a set-valued assignment ${\mathcal M}\in\{\:\mbox{\rm sets}\:\}^{{\mathcal X}_{\Phi}}$
defined on the collection ${\mathcal X}_{\Phi}$
of variables in $\Phi$, and assume that $\left(\{q^{(\mu)}\}_{q\in\Places}\right)_{\mu\leqslant\xi},
(\bullet),\TARGETS,\REDS,\POWNODES$
is a {colored $\Places$-process} for the \emph{$\Sigma_{{\mathcal X}_{\Phi}}$-board}.

Then, letting ${\mathcal M}'(v)=\bigcup[\Im_{{\mathcal M}}(\widehat{v})]$
for every literal in $\Phi$, the following conditions are
fulfilled:
\begin{des}
\item if the literal is satisfied by $\mathcal M$, then it is satisfied
by ${\mathcal M}'$ too;
\item if the literal is satisfied by ${\mathcal M}'$, and does not
involve $\Pow$~ or the construct $\{\anonymous,\dots,\anonymous\}$,
then it is satisfied by ${\mathcal M}$ too.
\end{des}
\end{mytheorem}
The proof of Theorem \ref{upwards} can be found in \cite{Urs06} but,
for the sake of completeness, we review it in the Appendix.

Now we are ready for the main result of this section.  We show how a
finite assignment can yield an infinite model, which satisfies the
same \MLSSP literals. To this end, we prove the following theorem,
which generalizes a result given in \cite[Theorem 38]{Urs06}.

\begin{mytheorem}\label{sufficienza}
Let $\Phi$ be a formula of \MLSSPF and
${\cal M}\in\{\:\mbox{\rm sets}\:\}^{{\mathcal X}_{\Phi}}$
a model for $\Phi^-$ together with a
$(\left(\{q^{(\mu)}\}_{q\in\Places}\right)_{\mu\leqslant\ell},
(\bullet),\TARGETS,\REDS,\POWNODES)$
{colored $\Places$-process}
for $\Sigma_{{\mathcal X}_{\Phi}}$
such that:
\begin{itemize}

\item ${\mathcal G}=(\TARGETS,\REDS,\POWNODES)$ colored
\emph{$\Sigma_{{\mathcal X}_{\Phi}}$-board} satisfies the following conditions:

There exist a ``collection of infinite'' $\Gamma$ for $\Phi$ such that
for all $\sigma\in\Gamma$ there exist a pumping chain, closure
equipped, at $\sigma$.  $\langle
(\mathcal{C},\overline{\mathcal{D}}_{0},
\mathcal{D}_{1},\ldots,\mathcal{D}_{N}),\vec m,q_0,\sigma\rangle$ with
a closure $\overline{\mathcal{C}}$.

\end{itemize}
then there exists a model for $\Phi$.
\end{mytheorem}

\proof Consider an occurrence of the literal $\neg Finite(x)$.

Since $\Gamma$ is a collection of infinite there exist a place
$\sigma\subseteq{\cal M}(x)$ and a pumping chain, $\langle
(\mathcal{C},\overline{\mathcal{D}}_{0},\mathcal{D}_{1},\ldots,\mathcal{D}_{N}),\vec
m,q_0,\sigma\rangle$ with a closure $\overline{\mathcal{C}}$.

Our goal consists in building from the original
$(\left(\{q^{(\mu)}\}_{q\in\Places}\right)_{\mu\leqslant\ell},
(\bullet),\TARGETS,\REDS,\POWNODES)$
{colored $\Places$-process}
a new one $\big(\{\widehat{q}^{[\alpha]}\}_{\widehat{q}\in
\widehat{\Places}}\big)_{\alpha\leqslant\xi '}$
in such a way $\widehat{{\cal M}}(v)=\bigcup \{\widehat{q}\wt q\in{\cal M}(v)\}$ is a model for $\Phi$.




We define, using a technique described in
\cite{CU97},
a sequence of nodes of lenght $\xi$, denoting it $\seq {\xi}$.
We shall use such a sequence
as trace for a formative process with final transitive partition
$\widehat{\Places}$ satisfying the requested properties.
The following sequence does to the purpose:
\begin{eqnarray*}
\lefteqn{A_1\dots A_{m_0 -1}\underbrace{\overbrace{C_0\dots
C_t}^{\mathcal{C}},\overbrace{D_0\dots
D_{s_1-1}}^{\overline{\mathcal{D}}_{0}}, \overbrace{C_{t+1}\dots
C_h}^{\mathcal{C}}}_{\aleph_{0} -times}, A_{\gamma(m_0)}\dots
A_{\gamma(m_1-1)}} \\
& & \overbrace{ D_{ s_0=0}\dots D_{ s_1
-1}}^{\mathcal{D}_{1}}A_{\gamma(m_1) }\dots
A_{\gamma(m_N-1)}\overbrace{D_{ s_{N-1}}\dots
D_{ s_{N}}}^{\mathcal{D}_{N}}A_{\gamma(m_N)}\dots A_{\gamma(\xi)}\,.
\end{eqnarray*}

\smallskip

\noindent Concerning nodes of the original sequence we use the capital
letter $A$, concerning nodes of the cycle ${\cal C}$ we use the capital
letter $C$, and concerning nodes of the simple path ${\cal D}$
attached to ${\cal C}$ we use the capital letter $D$.
We denote by:
\begin{itemize}
 \item $N_1$, the nodes of the sequence $ \seq {l} $;

 \item $N_2$, the nodes of the pumping cycle $({\cal C},{\cal D})$;

 \item $A_{\gamma (i)}$, a node $A_{i}$ in the pumped sequence;

  \item $A_{\gamma (i)+t}$, an
        $N_2$-node, where $\gamma (i)$ is the index of the first
        $N_1$-node before $A_{\gamma (i)+t}$.

\end{itemize}
Finally, we usually refer to a piece of a formative process, bounded by
the two indices $\alpha\leqslant\beta$,  by  ``segment of the process''.
We refer to the segments composed of $N_1$ and $N_2$
nodes in a different way, the former as ``imitating segments'', the latter
as ``pumping segments''.

In order to define a formative process we are needed only to exhibit the way to
distribute all the elements produced at each stage.
Our strategy consists in copying the old formative process until the
stage $m_0 -1 =\gamma (m_0-1)$, therefore along this segment
we define $\gamma$ as the Identity map; then ``pumping'' the cycle to create
new elements and distribute them. This procedure by transfinite induction
increases the cardinality of
the blocks inside the cycle. Unfortunately this distribution of elements could
be not propagated along the path ${\cal D}$ in order to make $\sigma$ of infinite
size.
This phenomenon depends on the fact that some of the nodes involved
could be not ``ready'' at the step when one of its block is infinite. This
obliges us to wait for the first step when it is possible. As soon as these
conditions are reached the ``infinite can be propagated'' until making
$\sigma$ of infinite size.
This procedure has in mind to preserve the cardinality
of all blocks not involved in the pumping procedure.
In order to do this we
distinguish the elements reserved for pumping procedure from those
used for mimicking the old process, creating a $\text{Surplus}$-$\text{Minus}$ partition inside all the blocks
involved in the pumping procedure, actually refining the original partition.

Assume we have copied the original formative process until $m_0-1$.

We start with the stage $\gamma (m_0-1)+1$.\\
We trigger off our pumping procedure using the property
$(i)$ of the definition of pumping
chain. Indeed, by $(i)$ ${\cal C}$ has an $q_0$ block
with a new element $t_0$.

This element, $t_0$, will generate all the elements needed for increasing
the size of all the blocks inside the cycle.

[For the details of such a construction, cf. the proof of Theorem 38 in \cite{Urs06}].

From now on we denote by $q$ places in $\mathcal{C}$, by
$\delta$ places in $\PLACES{\overline{\mathcal{D}}_{0}}$,
by $\sigma_{\Gamma}$
a place which lies in the pumping path after the node $\Gamma$,
by $\sigma^{\Gamma}$ a place which lies in the pumping path before the node
$\Gamma$.
Put $\mathcal{D}_{0} \equivAs
\mathcal{C},\overline{\mathcal{D}}_{0}$
It is possible to prolongate the formative process by
repeating the  nodes in $\NODES{\mathcal{C},\overline{\mathcal{D}}_{0}}$
$\aleph_{0}$-times in the following sequence:

$$C_0 \dots C_t,D_0\dots D_{s_1-1},C_{t+1} \dots C_h$$

\noindent in such a way as to enforce that the following holds at step $\gamma (m_0)$:

\begin{itemize}

\item[(i)] For all $\sigma\in \PLACES{\mathcal{D}_{0}}$ and
$\Gamma\in \NODES{\mathcal{D}_{0}}$, \\
$\vert\powAst (\{\text{Surplus}^{[\gamma(m_0)]}(\sigma^{\Gamma})\}\cup
(\Gamma\setminus\{\sigma^{\Gamma}\})\cap
\text{Surplus}^{[\gamma(m_0)]}q_{\Gamma}\vert\geqslant\omega$;
\item[(ii)] for all $q$,
$\text{Minus}^{[\gamma(m_0 -1)]}q=\text{Minus}^{[\gamma(m_0)]}q=_c q^{(m_0)}$ and\\
$\vert Unused(\text{Minus}^{[\gamma(m_0)]}q)\vert=\vert Unused(q)\vert$;

\item[(iii)] for all $q$, $\text{Surplus}(q) \neq\emptyset\mbox{ implies } q\in
Closure(({\cal C},{\cal D}))$;
\item[(iv)] for all $\Gamma$ in $\NODES{\mathcal{C},\mathcal{D}}$,
$\bigcup\Gamma^{[\gamma(m_0)]}\notin {\Places}^{[\gamma(m_0)]}$.
\end{itemize}

It is straightforward to verify that the conditions requested in the Lemma
\ref{pasting} are
respectively satisfied
by the \emph{colored $\Places$-process}
$\big(\Sigma_\mu\big)_{\mu\leqslant\xi},(\bullet),\TARGETS,\REDS,\POWNODES$
and the partition ${\Places}^{[\gamma(m_0)]}$ for $k=m_0$. Therefore the segment
$[m_0,m_1-1]$ can be imitated.

Using the fact that partitions $\text{Surplus}$ are never used along the segment
$[\gamma(m_0),\gamma(m_1-1)]$ and that it imitates the segment
$[m_0,m_1-1]$, we can assert that for $\Gamma$ in $\NODES{\mathcal{D}}$
$\powAst (\Gamma)^{[\gamma(m_1)-1]}\neq\emptyset$ and
$\vert \text{Surplus}^{[\gamma(m_1-1]}\delta _{s_1}\vert\geqslant\omega$.
This enables us to prolongate
the process in such a way that an analogue of (i)--(iv)
holds at the step $\gamma(m_1)$ (with $\gamma(m_1)$ in the segment $\mathcal{D}_1$).
Lemma \ref{pasting} applies again, and the process can be prolongated till
$\gamma(m_2-1)$.

In the same fashion the construction proceeds by application
the same procedure to every section of the pumping chain,
until the last node of the trace $\seq {\xi}$ is reached.
This plainly gives $\vert\widehat{\sigma}^{[\xi]}\vert\geqslant\omega$.

Now we are left to prove that the resulting transitive partition
$\widehat{\Places}^{[\xi]}$ satisfies the thesis.

To do this we invoke Theorem \ref{upwards}. It is routine verifying that the hypotheses of Theorem \ref{upwards} are met.
Therefore we can assert that the model induced by the resulting transitive partition satisfies $\Phi^-$ plus all the
literals $\neg Finite(x)$ such that in the original model ${\cal M}(x)\supseteq \sigma$ are satisfied.
Indeed, the previous procedure has made $\sigma$ of infinite size.
We are left to do the same for the other members of the collection of infinite.
This is hardly ever a limitation since all pumping chains and closures are preserved and
the formative process $\widehat{\Sigma}$ can do
the same role played by the original process before.
Therefore, the
same technique applies using a new pumping chain, till the end.

Denote the last model ${\cal M}$ and put $X=\{x\st\sigma\in\Gamma\cap {\cal M}(x)\}$.

${\cal M}$ will satisfy the following formula

$$\Phi '=\Phi ^- \wedge\bigwedge_{x\in X}\neg Finite(x)$$
since $\Gamma$ is a collection of infinite the thesis plainly follows.
\qed
Combining the results of the two sections, we achieve the main conclusion of this paper:
\begin{mytheorem}
The language \MLSSPF, namely \MLSSP extended with a finiteness
predicate, has a decidable satisfiability problem.
\end{mytheorem}

\section{Conclusions}
\label{conclusions}

We have shown that the extension \MLSSPF of the language \MLSSP with a
finiteness predicate has a decidable satisfiability problem, even though
it does not enjoy the small model property, as is the case with \MLSSP.
Such result has been achieved by showing that \MLSSPF enjoys a weaker
form of the finite model property, called ``small model witness
property.''  Roughly speaking, the small model witness property for
\MLSSPF asserts that any satisfiable \MLSSPF-formula has a model
admitting a ``small'' representation through a suitably annotated
formative process.

We plan to further extend the techniques introduced in this paper to
deal also with set-theoretic fragments involving besides the Boolean
set operators and the singleton operator, also the unionset
or the Cartesian product operators.  Notice that in such
fragments it is possible to express formulae admitting only infinite
models.

\newpage

\appendix
\vspace{1.5cm}
\noindent {\LARGE \textbf{Appendix}}

\section{Proof of Theorem \ref{upwards}}

The introduction of some additional tools makes the proof of the
Theorem \ref{upwards} more plain and fluent.  We create various levels
of similarity of transitive partitions and formative processes and
break the proof in more steps.  In the following we use conditions 1,2
and 4, defined in Section~\ref{sse_Venn}, in order to define a new
class of similarity among transitive partitions.

\begin{mydef}\label{SimBoard}\rm
Let ${\mathcal G}$ be a colored transitive $\Sigma$-board. Then
$\widehat{\Sigma}$ is said to \textsc{simulate}
$(\Sigma,{\mathcal G})$ \textsc{upwards},
when there is a bijection
$\beta\in\widehat{\Sigma}^{\Sigma}$ such that
\begin{itemize}
\item $\widehat{\Sigma}$ $\in$-simulates $\Sigma$ via
$\beta$. That is, $\bigcup\beta[X]\in\bigcup\beta[Y]$ if and only if
$\bigcup X\in\bigcup Y$, for $X,Y\subseteq\Sigma$;
\item $\widehat{\Sigma}$ $\Pow$-simulates $\Sigma$ via
$\beta$. That is, $\bigcup\beta[X]=\pow{\bigcup\beta[Y]}$ if
$\bigcup
X=\pow{\bigcup Y}$, for $Y\in\POWNODES$ $X,Y\subseteq\Sigma$;
\item $\widehat{\Sigma}$ $Red$-simulates $\Sigma$ via
$\beta$. That is,
if $\sigma\in\REDS$, then $\card{\beta(\sigma)}=\card{\sigma}$.

%$$\bigcup\beta[X]=
%\left\{\bigcup\beta[Y_{1}],\dots,\bigcup\beta[Y_{L}]\right\}\quad
%\text{iff}\quad
%\bigcup X=\left\{\bigcup Y_{1},\dots,\bigcup Y_{L}\right\},$$
%for $X,Y_{1},\dots,Y_{L}\subseteq\Sigma$ and $X\subseteq\REDS$.
\end{itemize}
\eod\end{mydef}

The following lemma shows that the previous conditions are enough to model \MLSSP clauses.

\begin{mylemma}
\label{MsatisfiesI}
Consider a formula $\Phi\in {\rm MLSSPF}$,
a set-valued assignment ${\mathcal M}\in\{\:\mbox{\rm sets}\:\}^{{\mathcal X}_{\Phi}}$
defined on the collection ${\mathcal X}_{\Phi}$
of variables in $\Phi$, together with the
colored transitive $\Sigma_{{\mathcal X}_{\Phi}}$-board
${\mathcal G}=(\TARGETS,\REDS,\POWNODES)$.
Define $\Phi^-$ as the formula $\Phi$ without literals of the type $Finite(x)$
or $\neg Finite(x)$.
Moreover, let $\widehat{\Sigma}$ be a partition and $\beta$ be a
bijection between $\Sigma_{{\mathcal X}_{\Phi}}$ and $\widehat{\Sigma}$ such that
$\widehat{\Sigma}$ simulates
$(\Sigma,{\mathcal G})$ upwards via
$\beta$, and let ${\mathcal M}'(v)=\bigcup\beta[\Im_{{\mathcal M}}(v)]$.
Then, for every literal in $\Phi^-$, the following conditions are
fulfilled:
\begin{des}
\item if the literal is satisfied by $\mathcal M$, then it is satisfied
by ${\mathcal M}'$ too;
\item if the literal is satisfied by ${\mathcal M}'$, and does not
involve $\Pow$~ or the construct $\{\anonymous,\dots,\anonymous\}$,
then it is satisfied by ${\mathcal M}$ too;
\item if the literal $Finite(x)$ appears in $\Phi$ and is satisfied by
$\mathcal M$, then it is satisfied
by ${\mathcal M}'$ too.
\end{des}
\end{mylemma}

\begin{proof}
The thesis can be recast as follows. For $u,v,w$ and $w_{i}$ in
${\mathcal X}_{\Phi}$, the following conditions hold for all literals in $\Phi$:
\begin{itemize}
\item[(1)] $\bigcup\Im(v)\;\Re\;\bigcup\Im(w)$ iff
$\bigcup\beta[\Im(v)]\;\Re\;\bigcup\beta[\Im(w)]$,
 for $\Re$ in $\{\:=\,,\:\in\,,\:\subseteq\:\}$;
\item[(2)] $\bigcup\Im(v)=\bigcup\Im(u)\:\star\:\bigcup\Im(w)$ iff
 $\bigcup\beta[\Im(v)]=\bigcup\beta[\Im(u)]\:\star\:
 \bigcup\beta[\Im(w)]$,
 for $\star$ in $\{\:\cap\,,\:\setminus\,,\:\cup\:\}$, and
$\bigcup\Im(v)=\emptyset$ iff
$\bigcup\beta[\Im(v)]=\emptyset$;
\item[(3)] if $\bigcup\Im(v)=\pow{\bigcup\Im(w)}$, then
$\bigcup\beta[\Im(v)]=\pow{\bigcup\beta[\Im(w)]}$;
\item[(4)] if
$\bigcup\Im(v)=\{\,\bigcup\Im(w_{1}),\dots,\bigcup\Im(w_{H})\,\}$,
then\\ $\bigcup\beta[\Im(v)]=\{\,\bigcup\beta[\Im(w_{1})],\dots,
\bigcup\beta[\Im(w_{H})]\,\}$;
\item[(5)] if $Finite(v)$ appears in $\Phi$ then
$\vert\bigcup\Im(v)\vert=\vert\bigcup\beta[\Im(v)]\vert$.
\end{itemize}
Property $(1)_{\in}$ (here $\Re$ is meant to be $\in$) follows from $\in$-simulates in
\defn{SimBoard}. $(3)$ follows from the assumption $\Im(v)\in\POWNODES$ and the
notion of $\Pow$-simulates given in the same definition.
Condition $(5)$ plainly follows from definition of $Red$-simulates.

We are left to prove that $(4)$ hold.
Observe that $\Im(v)\subseteq\REDS$, then consider $\Im(v)$
as the set $X$ and $Y_i$ as the sets $\Im(w_{i})$. Hence we can assume that
$\bigcup X=\{\bigcup Y_1,\dots, \bigcup Y_L\}$, $X\subseteq\REDS$, and
$Y_1,\dots, Y_L$ are distinct. We must check that
$\bigcup\beta[X]=\{\bigcup\beta[Y_1],\dots,$ $\bigcup\beta[Y_L]\}$.
Since $\widehat{\Sigma}$ $Red$-simulates
$(\Sigma,{\mathcal G})$ and $X\subseteq\REDS$,
and $\card{\beta(\sigma)}=\card{\sigma}$ for
each $\sigma\in X$, the desired conclusion easily follows.
Indeed, by property (1) of Def.~\ref{SimBoard},
$\bigcup\beta[Y_i]\in\beta(\sigma)$
if and only if
$\bigcup Y_i\in\sigma$, and $\beta[Y_1],\dots,\beta[Y_L]$
(and, accordingly, $\bigcup\beta[Y_1],\dots,\bigcup\beta[Y_L]$)
are pairwise distinct.

The proofs of remaining bi-implications go exactly as in \cite[Lemma 10.1]
{COU02}
\end{proof}
\qed
The next definition is a level of similarity of transitive partitions defined in a more combinatorial way; in the sequel we show how
these definitions are interrelated.

\begin{mydef}
\label{defImitation}\rm
Consider a colored $\Sigma$-board ${\mathcal G}=(\TARGETS,\REDS,\POWNODES)$.
A partition $\widehat{\Sigma}$ is said to \textsc{imitate}
$(\Sigma,{\mathcal G})$ when there is a bijection $\beta\in
\widehat{\Sigma}^{\Sigma}$ such that, for
$\Gamma\subseteq\Sigma$, $\sigma\in\Sigma$,
\begin{itemize}
\item[(1)] $\beta(\sigma)\cap\powast{\beta[\Gamma]}\neq\emptyset$ holds [if
and]
only if $\sigma\cap\powast{\Gamma}\neq\emptyset$;
\item[(2)] $\bigcup\beta[\Gamma]\in\beta(\sigma)$ holds if and only if $\bigcup
\Gamma\in\sigma$;
\item[(3)] if $\Gamma\in\POWNODES$ holds, then
$\powast{\beta[\Gamma]}\subseteq\bigcup\widehat{\Sigma}$;
\item[(4)]  if
$\sigma\in\REDS$ holds, then $\card{\beta(\sigma)}<\aleph_0$.
\end{itemize}
We will say that $\widehat{\Sigma}$
\textsc{imitates} $(\Sigma,{\mathcal G})$
\textsc{upwards} when the following
additional condition holds, for all $\sigma\in\Sigma$:
\begin{itemize}
\item[(4$'$)] if
$\sigma\in\REDS$, then $\card{\beta(\sigma)}=\card{\sigma}$.\eod
\end{itemize}
\end{mydef}
\begin{mylemma}\label{imitaSimula}
Consider a colored \emph{$\Sigma$-board} ${\mathcal G}=(\TARGETS,\REDS,\POWNODES)$
assume that a transitive partition $\widehat{\Sigma}$ {imitates} $(\Sigma,{\mathcal G})$
 {upwards}
then it {simulates}
$(\Sigma,{\mathcal G})$ {upwards}.
\end{mylemma}

\begin{proof}
Let $\Sigma$ and $\widehat{\Sigma}$ be transitive partitions, and
let ${\mathcal G}$ be a colored \emph{$\Places$-board} induced by
$\Sigma$. Assume that $\widehat{\Sigma}$ {imitates}
$(\Sigma,{\mathcal G})$ {upwards}
via the bijection $\beta\in
(\widehat{\Sigma})^{\Sigma}$.
Finally, let $X, Y \subseteq \Sigma$.

Then we have: $\bigcup\beta[X]\in\bigcup\beta[Y]$ iff
$(\exists\,\widehat{\sigma}\in\beta[Y])(\bigcup\beta[X]\in\widehat{\sigma})$
iff $(\exists\,\sigma\in
Y)(\bigcup\beta[X]\in\beta(\sigma))$
iff $(\exists\,\sigma\in
Y)(\bigcup X\in\sigma)$ iff $\bigcup X\in\bigcup Y$.

Assuming now that $\bigcup X=\pow{\bigcup Y}$, $Y\in\POWNODES$, let us
prove that
$\pow{\bigcup\beta[Y]}\subseteq\bigcup \beta[X]$.  Indeed, suppose
$t\subseteq\bigcup\beta[Y]$ and let $\widehat{\Sigma}_{t}$ be the
subset of $\widehat{\Sigma}$ for which
$t\in\powast{\widehat{\Sigma}_{t}}$ (so that
$\widehat{\Sigma}_{t}\subseteq \beta[Y]$, which implies
$\widehat{\Sigma}_{t}\in\POWNODES$ by the hereditarily closedness by inclusion
of $\POWNODES$).  As
$\beta^{-1}[\widehat{\Sigma}_{t}] \subseteq Y$,
it follows that
$\powast{\beta^{-1}[\widehat{\Sigma}_{t}]} \subseteq
\pow{\bigcup Y} =
\bigcup X \subseteq \bigcup \Sigma$.
Therefore, by the fact that
$\widehat{\Sigma}$ {imitates}
$(\Sigma,{\mathcal G})$ {upwards} and $\widehat{\Sigma}_{t}\in\POWNODES$,
it follows that
$\powast{\widehat{\Sigma}_{t}} \subseteq \bigcup \widehat{\Sigma}$,
so that $t \in \bigcup \widehat{\Sigma}$.  Let $\widehat{\sigma}_{t}$
be the block in $\widehat{\Sigma}$ to which $t$ belongs, and let
$\sigma_{t}$ be the block in $\Sigma$ for which
$\beta(\sigma_{t})=\widehat{\sigma}_{t}$.  Then, since
$\powast{\widehat{\Sigma}_{t}}\cap\widehat{\sigma}_{t}\neq\emptyset$, we
have that
$\powast{\beta^{-1}[\widehat{\Sigma}_{t}]}\cap\sigma_{t}\neq\emptyset$, which
yields $\bigcup X=\pow{\bigcup Y}\supseteq\powast{\beta^{-1}[
\widehat{\Sigma}_{t}]}$, $\bigcup X\cap\sigma_{t}\neq\emptyset$, $\sigma_{t}\in X$, and hence
$t\in\widehat{\sigma}_{t} \in\beta[X]$, which in turn yields $t \in
\bigcup \beta[X]$.

Next, assuming again
$\bigcup X=\pow{\bigcup Y}$, let us prove that $\bigcup
\beta[X]\subseteq\pow{\bigcup\beta[Y]}$.  Indeed, for each $t\in
\bigcup\beta[X]$ there is a unique $\sigma_{t}\in X$ such that
$t\in\beta(\sigma_{t})$; moreover, by the transitivity of
$\bigcup\widehat{\Sigma}$, there is a unique $\Gamma\subseteq\Sigma$ for
which $t\in\powast{\beta[\Gamma]}$. Moreover, since
$\powast{\beta[\Gamma]}\cap\beta(\sigma_{t})\neq\emptyset$, we also have that
$\powast{\Gamma}\cap\sigma_{t}\neq\emptyset$.
Thus we can take
$t'\in\sigma_{t}\cap\powast{\Gamma}$ that, as
$\sigma_{t}\subseteq\bigcup X=\pow{\bigcup Y}$, fulfills
$t'\in\powast{Z}$ for a suitable $Z\subseteq Y$.  In conclusion,
$\Gamma=Z$, and therefore
$t\subseteq\bigcup\beta[\Gamma]=\bigcup\beta[Z]\subseteq\bigcup\beta[Y]$.

\end{proof}
\qed
As an immediate consequence, we have

\begin{mycorollary}\label{MsatisfiesII}
Consider a formula $\Phi\in {\rm MLSSPF}$,
a set-valued assignment ${\mathcal M}\in\{\:\mbox{\rm sets}\:\}^{{\mathcal X}_{\Phi}}$
defined on the collection ${\mathcal X}_{\Phi}$
of variables in $\Phi$, together with the
colored transitive {$\Sigma_{{\mathcal X}_{\Phi}}$-board}
${\mathcal G}=(\TARGETS,\REDS,\POWNODES)$.
Moreover, let $\widehat{\Sigma}$ and $\beta$ be a partition and a
bijection, respectively,
such that $\widehat{\Sigma}$ {imitates} $(\Sigma,{\mathcal G})$
{upwards} via
$\beta$, and let ${\mathcal M}'(v)=\bigcup\beta[\Im_{{\mathcal M}}(v)]$,
where $\Im$ is
the function $\Im\in\pow{\Sigma}^{\mathcal X_{\Phi}}$ such that
${\mathcal M}(v)= \bigcup\Im(v)$ holds for every $v$ in $\mathcal X$.
Then, for every literal in $\Phi^-$ and any literal of the form
$Finite(x)$, the following conditions are
fulfilled:
\begin{des}
\item if the literal is satisfied by $\mathcal M$, then it is satisfied
by ${\mathcal M}'$ too;
\item if the literal is satisfied by ${\mathcal M}'$, and does not
involve $\Pow$~ or the construct $\{\anonymous,\dots,\anonymous\}$,
then it is satisfied by ${\mathcal M}$ too. \qed
\end{des}
\end{mycorollary}

We are almost ready for the desired proof of Theorem \ref{upwards}. One
more lemma is needed showing that, provided that the initial conditions
(relative to the starting transitive partition) are ``similar'' in the
sense described above, the process which imitates the initial model
satisfies the same \MLSSP clauses.

\begin{mylemma}\label{upward1}
\begin{sloppypar}
Let $\left(\{q^{(\mu)}\}_{q\in\Places}\right)_{\mu\leqslant\xi},
(\bullet),\TARGETS,\REDS,\POWNODES$
be a {colored $\Places$-process}. Moreover, let
$\big(\{\widehat{q}^{[\alpha]}\}_{\widehat{q}\in
\widehat{\Places}}\big)_{\alpha\leqslant\xi '}$ be another formative process,
equipped with a Minus-Surplus partitioning.
Assume that, for some $k'\leqslant\xi$ and $m\leqslant\xi '$,
\end{sloppypar}
\begin{itemize}
\item $\widehat{\Sigma}_{m}$ {weakly imitates}
$\Sigma_{k'}$ {upwards};
\item the process
$\big(\{\widehat{q}^{[\alpha]}\}_{\widehat{q}\in\widehat{\Places}}
\big)_{\alpha\in\gamma [k',\xi]}$ {imitates}
$\big(\{q^{(\mu)}\}_{q\in\Places}\big)_{k'\leqslant\mu\leqslant\xi}$, where $\gamma$ is an
injective map from $[k',\xi]$ to $[m,\xi ']$;
\item $\widehat{\Sigma}_{\xi '}$ has the same targets of $\Sigma_{\xi}$;
\item for all $\mu >m\wedge\mu\notin\gamma [k',\xi]$ the following holds:
$\Delta^{[\mu]}(\widehat{q})\subseteq\Delta^{[\mu]}\text{Surplus}(\widehat{q})$;
\item
if $\beta$ is the greatest ordinal
such that
$\beta\in\gamma[k',\xi]\wedge\beta\leqslant\mu$, if
$q$ is a local trash of ${A}_{\mu}$, and if $\GE(A_{\mu})>\gamma^{-1}(\beta)$,
then $\bigcup\widehat{A_\mu}^{[\xi ']}\notin
\Delta^{[\mu]}\text{Surplus}(\widehat{q})$.
\end{itemize}
%[MANCA DEFINIZIONE
%LOCAL TRASH RELATIVO AD UN ORDINALE] relatively to $\gamma (\mu)$ where
%$\gamma (\mu)$ is the max of the following set $\{\gamma [k',\xi]\cap
%[0,\mu] \}$
Then $\widehat{\Sigma}_{\xi '}$ {imitates} $\Sigma_{\xi}$ {upwards}.
\end{mylemma}

\begin{proof}
We prove that the resulting partition $\widehat{\Sigma}_{\xi '}$
fulfills the
conditions:
\begin{itemize}
\item[(0)]  $q^{(\xi)}\cap\powast{\Gamma}^{(\xi)}\neq\emptyset$
holds if and
only if $\widehat{q}^{[\xi ']}\cap\powast{\widehat{\Gamma}^{[\xi ']}}\neq\emptyset$;
\item[(1)] $\bigcup\widehat{\Gamma}^{[\xi ']}\in\widehat{q}^{[\xi ']}$
if and only if $\bigcup \Gamma^{(\xi)}\in q^{(\xi)}$;
\item[(2)] if $\Gamma\in\POWNODES$ holds, then
$\powast{\widehat{\Gamma}^{[\xi ']}}\subseteq\bigcup\widehat{\Places}^{[\xi ']}
$;
\item[(3$'$)] if
$q\in\REDS$, then $\card{\widehat{q}^{[\xi ']}}=\card{q^{(\xi)}}$.
\end{itemize}

Along the verification of properties (0)-(3$'$) we refer to (i)-(x)
of Def.~\ref{formimit}.
\begin{itemize}
\item[(0)] By the fact that the two partitions have the same targets;

\item[(1)]
In case $\bigcup\widehat{\Gamma}^{[\xi ']}\in\widehat{q}^{[\xi ']}$,
assuming that it
is distributed strictly before $m$, then $\GE(\Gamma)<k'$. Indeed,
if not so, by (vi) Def.~\ref{formimit}, since $\bigcup\Gamma^{(\GE(\Gamma))}\in
\Delta ^{(\GE(\Gamma))}(q)$,
$$\bigcup\widehat{\Gamma}^{[\xi ']}\in\widehat{q}^{[\xi ']}=
\bigcup\widehat{\Gamma}^{[\gamma (\GE(\Gamma))]}
\in\Delta^{[\gamma (\GE(\Gamma))]}\widehat{q},$$
which is impossible, due to the fact
that  $\bigcup\widehat{\Gamma}^{[\xi ']}\in\widehat{q}^{[\xi ']}$
is already in $\widehat{q}^{[\gamma (\GE(\Gamma))]}$, and
$\Delta^{[\gamma (\GE(\Gamma))]}\widehat{q}$,
by definition, is made of elements of
$\powAst (\widehat{\Gamma}^{[\gamma(\GE(\Gamma)]})
\setminus
\bigcup _{q\in\Sigma}q^{[\gamma(\GE(\Gamma))]}$.
Then, using the fact that
$\widehat{\Sigma}_{m}$
weakly simulates  $\Sigma_{k'}$, the result follows.
Concerning the right implication, we are left to prove the case when
$\bigcup\widehat{\Gamma}^{[\xi ']}$
is distributed after or in $m$.
Let $j$ be such an index. By hypothesis,
$j$ cannot be outside $\gamma [k',\xi]$, and so
$j=\gamma (k)$ for some $k$.
We show that $k=\GE(\Gamma)$. By contradiction, let us assume $k>\GE(\Gamma)$.
Then, by (vi) Def.~\ref{formimit},
$$\bigcup\widehat{\Gamma}^{[\gamma (\GE(\Gamma))]}
\in\Delta^{[\gamma (\GE(\Gamma))]}\widehat{q}.$$
Observe that, after $\gamma (\GE(\Gamma))$, $\widehat{\Gamma}$ cannot
change inside
the range of $\gamma$, on
account of (ii) and (iii) of Def.~\ref{formimit}. It
it cannot change for
an index $j$ outside, since
$\GE(\Gamma)$ is greater than the greatest ordinal $\beta$ such that
$\beta\in\gamma[k',\xi]\wedge\beta\leqslant j$.
On the other hand,
$k$ cannot be strictly less than $\GE(\Gamma)$, since in this case the same argument
used for $\bigcup\widehat{\Gamma}^{[\xi ']}$ distributed before $m$ and $\GE(\Gamma)\geqslant k'$
applies.
Therefore $k=\GE(\Gamma)$, and we are done.
We now show the left implication in the case $\GE(\Gamma)< k'$.
The hypothesis implies  that
$\bigcup\widehat{\Gamma}^{[m]}\in\widehat{q}^{[m]}$. Reasoning as before,
we conclude that $\widehat{\Gamma}$ cannot change along the process after $m$.
Finally, assuming $\GE(\Gamma)\geqslant k'$, by  Def.~\ref{formimit}(vi) we
have
$$
\bigcup\widehat{\Gamma}^{[\gamma (\GE(\Gamma))]}\in
\Delta^{[\gamma (\GE(\Gamma))]}\widehat{q}.
$$
Again $\widehat{\Gamma}$ cannot change in the sequel of the
process, either along
the imitated process, or outside.
%CREA LEMMA

\item[(2)]Follows plainly from Def.~\ref{formimit}(iv). Indeed,
$\Gamma\in\POWNODES$, therefore
$$\powast{\widehat{\Gamma}^{[\gamma (\GE(\Gamma))]}}
\subseteq\bigcup\widehat{\Places}^{[\gamma (\GE(\Gamma))]}.$$
As observed in the previous point,
after $[\gamma (\GE(\Gamma))]$, $\widehat{\Gamma}$ cannot change either
along the imitating process, by (ii) and Def.~\ref{formimit}(iii),
or outside, by hypothesis.
Thus $\powast{\widehat{\Gamma}^{[\xi ']}}\subseteq\bigcup\widehat{\Places}^{[\xi ']}$.

\item[(3$'$)]The red places cannot belong to ${\mathcal C}$.  Hence,
by the property (viii), they cannot have Surplus part, which in turns
implies that $\text{Minus}(\widehat{q}^{[\xi ']})=\widehat{q}^{[\xi ']}$.
This, combined with $\vert \text{Minus}^{[\gamma(\xi)]}(q)\vert=\vert
q^{(\xi)}\vert$, by Def.~\ref{formimit}(i), yields the thesis. \qed
\end{itemize}
\end{proof}
By combining the results in Lemma \ref{upward1} and Corollary
\ref{MsatisfiesII}, Theorem \ref{upwards} follows easily.



\newpage

%%%%%%%%%%%%%%%%%%%%%%%%BIBLIOGRAFIA%%%%%%%%%%%%%%%%%%%%%%%

\bibliographystyle{alpha}
{\small
\begin{thebibliography}{COS*03}


\bibitem[Can91]{Can91}
D.~Cantone,\newblock
Decision procedures for elementary sublanguages of Set
Theory: {X}. {M}ultilevel syllogistic extended by the singleton and powerset
  operators.
\emph{J. Automat. Reason.}
\textbf{7}(2):193--230, 1991.


\bibitem[CFO89]{CFO89}
D.~Cantone, A.~Ferro, and E.G.~Omodeo.
\newblock \emph{Computable Set Theory}.
\newblock Vol. 6 Oxford Science Publications of
\emph{International Series of Monographs in Computer Science}.
Clarendon Press, Oxford, 1989.


\bibitem[COP01]{COP01} D. Cantone, E.~G.~Omodeo, and
A.~Policriti.
\newblock \emph{Set Theory for Computing {\small --- From decision
procedures to
declarative programming with sets}}.
\newblock {M}onographs in {C}omputer {S}cience. Springer-Verlag, New York,
2001.

\bibitem[COS*03]{COSU03} D. Cantone, E.~G.~Omodeo, J.~T.~Schwartz, and
P. Ursino.  Notes from the logbook of a proof-checker's project.  In
N. Dershowitz, editor, \emph{Proc. of the International Symposium
on Verification: Theory and Practice}, volume 2772 of Lecture Notes in
Computer Science, pages 182--207, Berlin,Springer-Verlag, 2003.


\bibitem[COU02]{COU02}
D.~Cantone, E.~G.~Omodeo, and P.~Ursino. \newblock Formative
processes with applications to the decision problem in set theory:
I. Powerset and singleton operators. \emph{Inform. and
Comput.}, \textbf{172}:165--201, 2002.


\bibitem[CU97]{CU97}
D.~Cantone and P.~Ursino.
A unifying approach to computable set theory.
Proceedings of {\it Logic Colloquium 1997}, Leeds, UK, 6 - 13 July
1997.


\bibitem[Jec78]{Jec78}
T.~Jech.
\newblock {\em Set theory},
\newblock {Academic Press}, {New York}, 1978.

\bibitem[OCP*06]{OCPS06} E.~G.~Omodeo, D.~Cantone, A.~Policriti, and
J.~T.~Schwartz.  A Computerized Referee.  In M.~Schaerf and
O.~Stock, editors, \emph{Reasoning, Action and Interaction in AI
Theories and Systems - Essays dedicated to Luigia Carlucci Aiello},
volume 4155 of Lecture Notes in Artificial Intelligence, pages
117--139,  Springer Berlin/Heidelberg, 2006.

\bibitem[OS02]{OS02}
E.~G. Omodeo and J.~T. Schwartz.
\newblock A `{T}heory' mechanism for a proof-verifier based on first-order set
  theory.
\newblock In A.~Kakas and F.~Sadri, editors, {\em Computational Logic: Logic
  Programming and Beyond {\small-- Essays in honour of Bob Kowalski}, Part II},
  volume 2408 of {\em Lecture Notes in Artificial Intelligence}.
  Springer-Verlag, Berlin, 2002.

\bibitem[Urs05]{Urs06}
P.~Ursino.  \newblock A generalized small model property for languages
which force the infinity. \emph{Matematiche (Catania)},
\textbf{LX}(I):93--119, 2005.

\end{thebibliography}}
\end{document}

math0411227.extracted_bib
\begin{thebibliography}{COS*03}


\bibitem[Can91]{Can91}
D.~Cantone,\newblock
Decision procedures for elementary sublanguages of Set
Theory: {X}. {M}ultilevel syllogistic extended by the singleton and powerset
  operators.
\emph{J. Automat. Reason.}
\textbf{7}(2):193--230, 1991.


\bibitem[CFO89]{CFO89}
D.~Cantone, A.~Ferro, and E.G.~Omodeo.
\newblock \emph{Computable Set Theory}.
\newblock Vol. 6 Oxford Science Publications of
\emph{International Series of Monographs in Computer Science}.
Clarendon Press, Oxford, 1989.


\bibitem[COP01]{COP01} D. Cantone, E.~G.~Omodeo, and
A.~Policriti.
\newblock \emph{Set Theory for Computing {\small --- From decision
procedures to
declarative programming with sets}}.
\newblock {M}onographs in {C}omputer {S}cience. Springer-Verlag, New York,
2001.

\bibitem[COS*03]{COSU03} D. Cantone, E.~G.~Omodeo, J.~T.~Schwartz, and
P. Ursino.  Notes from the logbook of a proof-checker's project.  In
N. Dershowitz, editor, \emph{Proc. of the International Symposium
on Verification: Theory and Practice}, volume 2772 of Lecture Notes in
Computer Science, pages 182--207, Berlin,Springer-Verlag, 2003.


\bibitem[COU02]{COU02}
D.~Cantone, E.~G.~Omodeo, and P.~Ursino. \newblock Formative
processes with applications to the decision problem in set theory:
I. Powerset and singleton operators. \emph{Inform. and
Comput.}, \textbf{172}:165--201, 2002.


\bibitem[CU97]{CU97}
D.~Cantone and P.~Ursino.
A unifying approach to computable set theory.
Proceedings of {\it Logic Colloquium 1997}, Leeds, UK, 6 - 13 July
1997.


\bibitem[Jec78]{Jec78}
T.~Jech.
\newblock {\em Set theory},
\newblock {Academic Press}, {New York}, 1978.

\bibitem[OCP*06]{OCPS06} E.~G.~Omodeo, D.~Cantone, A.~Policriti, and
J.~T.~Schwartz.  A Computerized Referee.  In M.~Schaerf and
O.~Stock, editors, \emph{Reasoning, Action and Interaction in AI
Theories and Systems - Essays dedicated to Luigia Carlucci Aiello},
volume 4155 of Lecture Notes in Artificial Intelligence, pages
117--139,  Springer Berlin/Heidelberg, 2006.

\bibitem[OS02]{OS02}
E.~G. Omodeo and J.~T. Schwartz.
\newblock A `{T}heory' mechanism for a proof-verifier based on first-order set
  theory.
\newblock In A.~Kakas and F.~Sadri, editors, {\em Computational Logic: Logic
  Programming and Beyond {\small-- Essays in honour of Bob Kowalski}, Part II},
  volume 2408 of {\em Lecture Notes in Artificial Intelligence}.
  Springer-Verlag, Berlin, 2002.

\bibitem[Urs05]{Urs06}
P.~Ursino.  \newblock A generalized small model property for languages
which force the infinity. \emph{Matematiche (Catania)},
\textbf{LX}(I):93--119, 2005.

\end{thebibliography}