text:
\section{Introduction}

In 1982 Chandra and Harel raised the question whether there is a computation model over structures that captures PTIME rather than Turing machines that operate over strings \cite{chandra:jcss1982}. Soon later Gurevich raised the related question how to define a computation model over structures that could serve as foundation for the notion of algorithm \cite{gurevich:ams1985}. As there is typically a huge gap between the abstraction level of an algorithm and the one of Turing machines, Gurevich formulated a new thesis based on the observation that ``if an abstraction level is fixed (disregarding low-level details and a possible higher-level picture) and the states of an algorithm reflect all the relevant information, then a particular small instruction set suffices to model any algorithm, never mind how abstract, by a generalised machine very closely and faithfully''. This led to the definition of Abstract State Machines (ASMs), formerly known as evolving algebras \cite{gurevich:lipari1995}.

Nonetheless, in 1988 Gurevich formulated the conjecture that there is no logic---understood in a very general way comprising computation models over structures---capturing PTIME \cite{gurevich:cttcs1988}. If true an immediate implication would be that PTIME differs from NP. There is indeed a lot of evidence supporting this conjecture. Among the most important results in descriptive complexity theory (see Immerman's monograph \cite{immerman:1999}) are Fagin's theorem stating that the complexity class NP is captured by the existential fragment of second-order logic \cite{fagin:siam1974}, and the theorem by Immerman, Livchak and Vardi stating that over ordered structures the complexity class PTIME is captured by first-order logic plus inflationary fixed-point \cite{immerman:ic1986,livchak:cmo1982,vardi:stoc1982}. Thus, if there is a logic capturing PTIME, it must be contained in $\exists$SO and extend IFP[FO]. As an extension by increase of order can be ruled out, the argumentation concentrates on the addition of generalised quantifiers, but there is very little evidence that all of PTIME can be captured by adding a set of quantifiers to IFP[FO] (see e.g. the rather detailed discussion in Libkin's monograph \cite[204f.]{libkin:2004}).

Another strong argument supporting Gurevich's conjecture comes from the work of Blass, Gurevich and Shelah on choiceless polynomial time (CPT), which exploits a polynomial time-bounded version of deterministic ASMs supporting unbounded parallelism, but no choice \cite{blass:apal1999} (see also \cite{blass:jucs1997,blass:jsl2002}). CPT extends IFP[FO], subsumes other models of computation on structures such as relational machines \cite{abiteboul:stoc1991}, reflective relational machines \cite{abiteboul:lics1994} and generic machines \cite{abiteboul:jacm1997}, but still captures only a fragment of PTIME. As shown in \cite[Thm.42,43]{blass:apal1999} some PTIME problems such as Parity or Bipartite Matching cannot be expressed in CPT, and for extensions of CPT by adding quantifiers such as counting the perspective of capturing PTIME remains as dark as for IFP[FO], as all arguments given by Libkin in \cite[204f.]{libkin:2004} also apply to CPT.

If true, another consequence of Gurevich's conjecture would be that complexity theory could not be based as a whole on more abstract models of computations on structures such as ASMs. In particular, it would not be possible to avoid dealing with string encodings using Turing Machines. However, this consequence appears to be less evident in view of the ASM success stories. Gurevich's important sequential ASM thesis provides a purely logical definition of the notion of sequential algorithm and shows that these are captured by sequential ASMs \cite{gurevich:tocl2000}, which provides solid mathematical support for the ``new thesis'' formulated by Gurevich in 1985 \cite{gurevich:ams1985}. Generalisations of the theory have been developed for unbounded parallel algorithms\footnote{Differences to other characterisations of parallel algorithms in \cite{blass:tocl2003,blass:tocl2008,dershowitz:igpl2016} concern the axiomatic definition of the class of (synchronous) parallel algorithms; these are discussed in \cite{ferrarotti:tcs2016}.} \cite{ferrarotti:tcs2016}, recursive algorithms \cite{boerger:fi2020}, concurrent algorithms \cite{boerger:ai2016}, and for reflective algorithms \cite{schewe:tcs2020}. In addition, the usefulness of ASMs for high-level development of complex systems is stressed by B\"orger in \cite{boerger:2003}. Furthermore, logics that enable reasoning about ASMs have been developed for deterministic ASMs by St\"ark and Nanchen \cite{staerk:jucs2001} based on ideas from Glavan and Rosenzweig that had already been exploited for CPT \cite{glavan:csl1992}, and extended to non-deterministic ASMs by Ferrarotti, Schewe, Tec and Wang \cite{ferrarotti:igpl2017,ferrarotti:amai2018}, the latter work leading to a fragment of second-order logic with Henkin semantics \cite{henkin:jsl1950}.

Therefore, we dared to doubt that Gurevich's conjecture is true. However, we abandoned looking for a solution by means of additional quantifiers. Instead, our research is based on a rather simple observation made during the study of CPT. While CPT captures only a fragment of PTIME, the counter-examples used in \cite{blass:apal1999} show that non-deterministic choice cannot be avoided. In case of the Parity problem a PTIME-bounded computation is only possible, if we can select an arbitrary element from the (finite) input set, and similarly in case of bipartite matching it must be possible to select arbitrary unmatched boys and girls. In \cite{ferrarotti:tcs2016} the construction of an ASM rule capturing an abstractly given parallel algorithm draws on finite model theory (see \cite{ebbinghaus:1995} or \cite{libkin:2004}). A decisive argument is that logically indistinguishable tuples, i.e. with the same type, can only both give rise to updates in an update set or both not. In other words, it must be possible to break types, and this is only possible by using non-deterministic choice as used in non-deterministic ASMs \cite{boerger:2003}.

However, simply adding arbitrary choice to the CPT computation model would be too strong. We observed that in all cases of PTIME problems not covered by CPT the required choice is insignificant in the sense that it does not matter, which choice is made: if one selection leads to a positive outcome for the decision problem, any other selection will lead to the same outcome. Hence the idea to formalise {\em insignificant choice polynomial time} (ICPT) as an extension of the CPT computation model and to show that in this way we are able to capture PTIME. This will be the first contribution of this article.

In view of the important theorem by Immerman, Livchak and Vardi it is not too hard to see that PTIME problems can be solved by polynomial time bounded ASMs with insignificant choice, as it suffices to create an order on the set of atoms in the base set. This construction is rather specific: it exploits to choose only atoms, and it allows us to replace arbitrary insignificant choice ASMs by ASMs satisfying a {\em local insignificance condition}. We can then exploit that this condition can be expressed in the logic of non-deterministic ASMs \cite{ferrarotti:igpl2017,ferrarotti:amai2018}. To show that the extension will remain within PTIME it suffices to repeat the arguments for CPT. That is, we have to simulate PTIME ASMs with choices among atoms that satisfy the local insignificance condition by PTIME Turing machines with input strings given by the standard encoding of an ordered version of the input structure. Here the local insignificance allows us to choose always the smallest atom, and the PTIME bound results from the fact that local insignificance checking for choices among atoms can be done in polynomial time. Clearly, such a simulating Turing machine can be effectively computed from the given ASM\footnote{In fact, the specific ASMs used here are executable and can be compiled by a Turing machine.}. In this way we obtain a logic in the sense of Gurevich \cite{gurevich:cttcs1988,blass:apal1999} capturing PTIME.

The idea of insignificant choice has already appeared in Arvid's and Biswas' non-deterministic inductive operator \cite{arvind:stacs1987}, Gire's and Hoang's symmetric choice operator \cite{gire:infcomp1998} (a comparison and evaluation is contained in \cite{dawar:jlc2003}), and in van den Bussche's and van Gucht's the work on semi-determinism \cite{bussche:pods1992}. The key difference to our work here is that none of the previous attempts to capture PTIME discovered the decisive local insignificance condition, which is essential for the definition of a recursive set of sentences.

Following again the work in \cite{blass:apal1999} we can make insignificant choice ASMs time-explicit and obtain a fixed-point theorem characterising acceptance of a finite input structure by a computation using an insignificant choice ASM. Furthermore, we show that the corresponding fixed-point formula must be satisfied in one or equivalent all semi-transitive structures, i.e. structures that are closed under the operations defining active orbits.

This leads to the second contribution of this article. We show the limitations of ICPT identifying problems that cannot be solved by an ICPT computation. First we establish a limitation on permutation classes of sets that can be activated by an ICPT computation. This gives a support theorem analogous to the one proven in \cite{blass:apal1999}. It is quite plausible that such a result holds, as the added choice is locally insignificant. Exploiting supports we obtain a generic form for the objects in semi-transitive structures. Then we define generalised pebble games that can be used to separate classes of structures satisfying certain conditions by a formula of an infinitary logic into which our fixed-point logic can be embedded in a fairly standard way. We prove an inseparability theorem characterising classes of semi-transitive structures that cannot be separated by the logic. This theorem can be applied to show that SAT cannot be decided by an ICPT computation, which implies that PTIME differs from NP.

\paragraph*{Organisation of the Article.}

In Section \ref{sec:asm} we introduce the background from ASMs and define a version of non-deterministic ASMs analogous to the one in \cite{blass:apal1999}, i.e. we assume a finite input structure, and consider only hereditarily finite sets as objects. This is then used to define PTIME-bounded ASMs. Section \ref{sec:ic} is dedicated to the introduction of insignificant choice. We start with motivating examples, then formally restrict our computation model to PTIME-bounded insignificant choice ASMs, which we exploit to show the capture of PTIME. In Section \ref{sec:icpt} we continue with the logic of non-deterministic ASMs and PTIME logic analogous to the work on CPT. We modify the semantics of choice, which allows us to obtain a decidable syntax and thus a logic capturing PTIME.

In Section \ref{sec:fixpoints} we explicitly define the insignificant choice fragment of the logic of non-deterministic ASMs and show a fixed-point theorem characterising acceptance of a finite input structure by a computation using an insignificant choice ASM. We further characterise the structures, in which such a formula must be satisfied to guarantee that the problem is in PTIME. Section \ref{sec:structures} is dedicated to the investigation of these semi-transitive structures. We first prove a generalisation of the support theorem for CPT to ICPT, by means of which we obtain a restriction on the size of permutation classes of sets that can be activated in an ICPT computation. The proof follows largely the argumention in \cite{blass:apal1999} for the extended version of coloured sets. The integer constant in the support theorem motivates the definition of structures exploiting that skew-symmetric objects can be defined by molecules and forms.

Section \ref{sec:games} is dedicated to the development of games that allow us to separate classes of structures. We first show that the fixed-point formulae can be expressed in an infinitary extension of the logic of ASMs restricted to insignificant choice. For this infinitary logic we define a version of a pebble game, by means of which it becomes possible to characterise inseparability of classes of semi-transitive structures. In Section \ref{sec:separation} we address the power and limitations of ICPT. We exploit the characterisation of semi-transitive structures and the separation game characterisation for a proof of a separation theorem which characterises classes of structures over skew-symmetric objects that cannot be distinguished by the infinitary extension of the logic of ASMs restricted to insignificant choice, provided the structures are sufficiently large. Key to the proof is a winning strategy for the duplicator for the separation game defined before. Then we apply the inseparability theorem to structures defined for the SAT problem and show that for sufficiently large semi-transitive structures the satisfiable ones and the non-satisfiable ones cannot be distinguished by our logic. This implies the second main result, the inequality of PTIME and NP.

We conclude in Section \ref{sec:schluss} first summarising our results, then discussing the wider perspective of complexity theory on the grounds of ASMs, i.e. computations on isomorphism classes of structures rather than Turing machines.

\section{Abstract State Machines}\label{sec:asm}

We assume familiarity with the basic concepts of ASMs. In general, ASMs including their foundations, semantics and usage in applications are the subject of the detailed monograph by B\"orger and St\"ark \cite{boerger:2003}. In a nutshell, an ASM is defined by a signature, i.e. a finite set of function (and relation) symbols, a background, and a rule. The signature defines states as structures, out of which a set of initial states is defined. The sets of states and initial states are closed under isomorphisms. The background defines domains and fixed operations on them that appear in every state (see \cite{blass:beatcs2007} for details), and the rule defines a relation between states and successor states and thus also runs.

Here we follow the development for CPT in \cite{blass:apal1999} and adapt ASMs to the purpose of our study on complexity theory. In particular, we use hereditarily finite sets, which according to Barwise form a  rather natural domain for computation \cite{barwise:1975}.

\subsection{Signature and Background}

The {\em background} of an ASM, as we use them here, comprises logic names and set-theoretic names:

\begin{description}

\item[Logic names] These comprise the binary equality $=$, nullary function names \textbf{true} and \textbf{false} and the usual Boolean operations. All logic names are relational.

\item[Set-theoretic names] These comprise the binary predicate $\in$, nullary function names $\emptyset$ and \textit{Atoms\/}, unary function names $\bigcup$ and \textit{TheUnique\/}, and the binary function name \textit{Pair\/}.

\end{description}

We will use $\emptyset$ also to denote undefinedness, for which usually another function name \textit{undef\/} would be used. In this way we can concentrate on sets.

The signature $\Upsilon$ of an ASM, as we use them here, comprises input names, dynamic and static names:

\begin{description}

\item[Input names] These are given by a finite set of relation symbols, each with a fixed arity. Input names will be considered being static, i.e. locations defined by them will never be updated by the ASM.

\item[Dynamic names] These are given by a finite set of function symbols, each with a fixed arity, including \textit{Output\/} and a nullary function symbol \textit{Halt\/}. Some of the dynamic names may be relational.

\item[Static names] These are given by a finite set $K$ of nullary function symbols $c_f$ for all dynamic function symbols $f$.

\end{description}

\subsection{States}

States $S$ are defined as structures over the signature $\Upsilon$ plus the background signature, for which we assume specific base sets.
A {\em base set} $B$ comprises three parts: a finite set $A$ of {\em atoms}, which are not sets, the collection $B = \textit{HF\/}(A)$ of hereditarily finite sets built over $A$, and a set $K$ of constants\footnote{Note that we overload the notation here using $c_f$ both as a nullary function symbol and as a constant in the base set.} $c_f \notin B$ for all static names $c_f$.

If $\mathcal{P}$ denotes the powerset operator and we define inductively $\mathcal{P}^0(A) = A$ and $\mathcal{P}^{i+1}(A) = \mathcal{P}(\bigcup_{j \le i} \mathcal{P}^j(A))$, then we have
\[ \textit{HF\/}(A) = \bigcup_{i < \omega} \mathcal{P}^i(A) = A \cup \mathcal{P}(A) \cup \mathcal{P}(A \cup \mathcal{P}(A)) \cup \dots . \]

Each element $x \in \textit{HF\/}(A)$ has a well-defined {\em rank} $rk(x)$. We have $rk(x) = 0$, if $x = \emptyset$ or $x$ is an atom. If $x$ is a non-empty set, we define its rank as the smallest ordinal $\alpha$ such that $rk(y) < \alpha$ holds for all $y \in x$.

We also use the following terminology. The atoms in $A$ and the sets in $\textit{HF\/}(A)$ are the {\em objects} of the base set $B = HF(A) \cup K$. A set $X$ is called {\em transitive} iff $x \in X$ and $y \in x$ implies $y \in X$. If $x$ is an object, then $\textit{TC\/}(x)$ denotes the least transitive set $X$ with $x \in X$. If $\textit{TC\/}(x)$ is finite, the object $x$ is called {\em hereditarily finite}.

The logic names are interpreted in the usual way, i.e. \textbf{true} and \textbf{false} are interpreted by 1 and 0, respectively (i.e. by $\{ \emptyset \}$ and $\emptyset$). Boolean operations are undefined, i.e. give rise to the value 0, if at least one of the arguments is not Boolean.

An {\em isomorphism} is a permutation $\sigma$ of the set $A$ of atoms that is extended to sets in $B$ by $\sigma(\{ b_1, \dots, b_k \}) = \{ \sigma(b_1), \dots, \sigma(b_k) \}$ and to the constants $c_f$ by $\sigma(c_f) = c_f$. Then every isomorphism $\sigma$ will map the truth values $\emptyset$ and $\{ \emptyset \}$ to themselves.

The set-theoretic names $\in$ and $\emptyset$ are interpreted in the obvious way, and \textit{Atoms\/} is interpreted by the set of atoms of the base set. If $a_1 ,\dots, a_k$ are atoms and $b_1 ,\dots, b_\ell$ are sets, then $\bigcup \{ a_1 ,\dots, a_k, b_1 ,\dots, b_\ell \} = b_1 \cup\dots\cup b_\ell$. For $b = \{ a \}$ we have $\textit{TheUnique\/}(b) = a$, otherwise it is undefined. Furthermore, we have $\textit{Pair\/}(a,b) = \{ a, b \}$.

An input name $p$ is interpreted by a Boolean-valued function. If the arity is $n$ and $p(a_1, \dots, a_n)$ holds, then each $a_i$ must be an atom. Finally, a dynamic function symbol $f$ of arity $n$ is interpreted by a function $f_S: B^n \rightarrow B$ (or by $f_S: B^n \rightarrow \{ 0, 1 \}$, if $f$ is relational). The domain $\{ (a_1 , \dots, a_n) \mid f(a_1 ,\dots, a_n) \neq 0 \}$ is required to be finite. For the static function symbols we have the interpretation $(c_f)_S = c_f$. With such an interpretation we obtain the set of states over the signature $\Upsilon$ and the given background.

An {\em input structure} is a finite structure $I$ over the subsignature comprising only the input names.  Without loss of generality it can be assumed that only atoms appear in $I$\footnote{For this we refer to the remark in \cite[p.18]{blass:apal1999} on input structures. If the base set of a structure $I$ over the input signature contains sets, then there exists a structure $J$ isomorphic to $I$ with a base set consisting only of atoms. We may take this argument further. We can always consider an $n$-ary relation as a unary one taking $n$-tuples as arguments. These $n$-tuples can be represented by sets using the Kuratowski representation. While this produces again input structures containing sets, we can again replace them by isomorphic input structures containing only atoms. Tuples of different length can be well distinguished using colours. We will exploit this later when dealing with supports.}. If the finite set of atoms in the input structure is $A$, then $|A|$ is referred to as the {\em size} of the input. An {\em initial state} $S_0$ is a state over the base set $B = HF(A) \cup K$ which extends $I$ such that the domain of each dynamic function is empty. We call $S_0 = State(I)$ the {\em initial state generated by $I$}. To emphasise the dependence on $I$, we also write $HF(I)$ instead of $B$.

\subsection{Terms and Rules}

{\em Terms} and {\em Boolean terms} are defined in the usual way assuming a given set of variables $V$:

\begin{itemize}

\item Each variable $v \in V$ is a term.

\item If $f$ is a function name of arity $n$ (in the signature $\Upsilon$ or the background) and $t_1, \dots, t_n$ are terms, then $f(t_1, \dots, t_n)$ is a term. If $f$ is declared to be relational, the term is Boolean.

\item If $v$ is a variable, $t(v)$ is a term, $s$ is a term without free occurrence of $v$, and $g(v)$ is a Boolean term, then $\{ t(v) \mid v \in s \wedge g(v) \}$ is a term.

\end{itemize}

The set $\textit{fr\/}(t)$ of {\em free variables} in a term $t$ is defined as usual, in particular $\textit{fr\/}(\{ t(v) \mid v \in s \wedge g(v) \}) = (\textit{fr\/}(t(v)) \cup \textit{fr\/}(s) \cup \textit{fr\/}(g(v))) - \{ v \}$. Also the interpretation of terms in a state $S$ is standard.

{\em ASM rules} as we use them are defined as follows:

\begin{description}

\item[skip] \textbf{skip} is a rule.

\item[assignment] If $f$ is a dynamic function symbol in $\Upsilon$ of arity $n$ and $t_0, \dots, t_n$ are terms, then $f(t_1, \dots, t_n) := t_0$ is a rule.

\item[branching] If $\varphi$ is a Boolean term and $r_1$, $r_2$ are rules, then also \textbf{if} $\varphi$ \textbf{then} $r_1$ \textbf{else} $r_2$ \textbf{endif} is a rule.

We also use the shortcut \textbf{if} $\varphi$ \textbf{then} $r_1$ \textbf{endif} for \textbf{if} $\varphi$ \textbf{then} $r_1$ \textbf{else} \textbf{skip} \textbf{endif}.

\item[parallelism] If $v$ is a variable, $t$ is a term with $v \notin \textit{fr\/}(t)$, and $r(v)$ is a rule, then also \textbf{forall} $v \in t$ \textbf{do} $r(v)$ \textbf{enddo} is a rule.

We use the shortcut \textbf{par} $r_1 \dots r_k$ \textbf{endpar} for \textbf{forall} $i \in \{ 1,\dots,k \}$ \textbf{do} \textbf{if} $i=1$ \textbf{then} $r_1$ \textbf{else} \textbf{if} $i=2$ \textbf{then} $r_2$ \textbf{else} \dots \textbf{if} $i=k$ \textbf{then} $r_k$ \textbf{endif} \dots \textbf{endif} \textbf{enddo}.

\item[choice] If $v$ is a variable, $t$ is a term with $v \notin \textit{fr\/}(t)$, and $r(v)$ is a rule, then also \textbf{choose} $v \in \{ x \mid x \in \textit{Atoms\/} \wedge x \in t \}$ \textbf{do} $r(v)$ \textbf{enddo} is a rule.

\end{description}

Note that choice rules only permit to choose among atoms, which is a severe syntactic restriction compared to the common ASM choice rule \cite{boerger:2003}.

In the sequel we further use the shortcut \textbf{let} $x = t$ \textbf{in} $r(x)$ for \textbf{choose} $x \in \textit{Pair\/}(t,t)$ \textbf{do} $r(x)$ \textbf{enddo}.

The rule associated with an ASM must be closed. The semantics of ASM rules is defined via update sets that are built for the states of the machine. Applying an update set to a state defines a successor state.

If $f$ is dynamic function symbol in $\Upsilon$ of arity $n$, and $a_1, \dots, a_n$ are objects of the base set $B$ of a state $S$, then the pair $(f,(a_1, \dots, a_n))$ is a {\em location} of the state $S$. We use the abbreviation $\bar{a}$ for tuples $(a_1, \dots, a_n)$, whenever the arity is known from the context. For a location $\ell = (f,\bar{a})$ we write $val_S(\ell) = b$ iff $f_S(a_1, \dots, a_n) = b$; we call $b$ the value of the location $\ell$ in the state $S$.

An {\em update} is a pair $(\ell, a)$ consisting of a location $\ell$ and an object $a \in B$, and an {\em update set} (for a state $S$) is a set of updates with locations of $S$ and objects $a$ in the base set of $S$.

Now let $S$ be a state with base set $B$, and let $\zeta : V \rightarrow B$ be a variable assignment. Let $r$ be an ASM rule. We define a set of update sets $\boldsymbol{\Delta}_{r,\zeta}(S)$ on state $S$ for the rule $r$ depending on $\zeta$ as follows:

\begin{itemize}

\item $\boldsymbol{\Delta}_{\textbf{skip},\zeta}(S) = \{ \emptyset \}$.

\item For an assignment rule $r$ of the form $f(t_1 ,\dots, t_n) := t_0$ taking the location $\ell = (f, (\text{val}_{S,\zeta}(t_1) ,\dots, \text{val}_{S,\zeta}(t_n)))$ and the object $a = \text{val}_{S,\zeta}(t_0)$ we have $\boldsymbol{\Delta}_{r,\zeta}(S) = \{ \{ (\ell,a) \} \}$.

\item For a branching rule $r$ of the form \textbf{if} $\varphi$ \textbf{then} $r_1$ \textbf{else} $r_2$ \textbf{endif} we have
\[ \boldsymbol{\Delta}_{r,\zeta}(S) = \begin{cases}
\boldsymbol{\Delta}_{r_1,\zeta}(S) &\text{if}\; \text{val}_{S,\zeta}(\varphi) = 1 \\
\boldsymbol{\Delta}_{r_2,\zeta}(S) &\text{if}\; \text{val}_{S,\zeta}(\varphi) = 0
\end{cases} . \]

\item For a parallel rule $r$ of the form \textbf{forall} $v \in t$ \textbf{do} $r(v)$ \textbf{enddo} we have
\[ \boldsymbol{\Delta}_{r,\zeta}(S) = \Big \{ \bigcup_{a \in \text{val}_{S,\zeta}(t)} \Delta_a \;\mid\; \Delta_a \in \boldsymbol{\Delta}_{r(v),\zeta(v \mapsto a)}(S) \;\text{for all}\;  a \in \text{val}_{S,\zeta}(t)\Big \} . \]

\item For a choice rule $r$ of the form \textbf{choose} $v \in \{ x \mid x \in \textit{Atoms\/} \wedge x \in t \}$ \textbf{do} $r(v)$ \textbf{enddo} we have
\[ \boldsymbol{\Delta}_{r,\zeta}(S) = \bigcup_{a \in \textit{Atoms\/} \atop a \in \text{val}_{S,\zeta}(t)} \boldsymbol{\Delta}_{r(v),\zeta(v \mapsto a)}(S) . \]

\end{itemize}

\subsection{Runs of ASMs}

An update set $\Delta$ is {\em consistent} iff for any two updates $(\ell,a_1), (\ell,a_2) \in \Delta$ with the same location we have $a_1 = a_2$. This defines the notion of {\em successor state} $S^\prime = S + \Delta$ of a state $S$. For a consistent update set $\Delta \in \boldsymbol{\Delta}_{r,\zeta}(S)$ and a location $\ell$ we have
\[ \text{val}_{S^\prime}(\ell) = \begin{cases}
a &\text{for}\; (\ell,a) \in \Delta \\ \text{val}_S(\ell) &\text{else} \end{cases} . \]
In addition, let $S + \Delta = S$ for inconsistent update sets $\Delta$.

Then the (closed) rule $r$ of an ASM defines a set of successor states for each state $S$. We write $\Delta_r(S,S^\prime)$ for an update set in $\boldsymbol{\Delta}_r(S)$ with $S^\prime = S + \Delta_r(S,S^\prime)$. This allows us to define the notion of run of an ASM.

A {\em run} of an ASM $M$ with rule $r$ is a finite or infinite sequence of states $S_0, S_1, \dots$ such that $S_0$ is an initial state and $S_{i+1} = S_i + \Delta$ holds for some update set $\Delta \in \boldsymbol{\Delta}_r(S_i)$. Furthermore, if $k$ is the length of a run ($k = \omega$ for an infinite run), then \textit{Halt\/} must fail on all states $S_i$ with $i < k$.

Note that in a run all states have the same base set\footnote{See the discussion in \cite[Sect.4.5]{gurevich:tocl2000}.}, which is in accordance with requirements from the behavioural theories of sequential and parallel algorithms (see \cite{gurevich:tocl2000} and \cite{ferrarotti:tcs2016}, respectively, and \cite[Sect.2.4.4]{boerger:2003}). However, not all atoms and sets are active in the sense that they appear as value or argument of a location with defined value. We therefore define active objects\footnote{We adopt here the notion of critical and active object as defined in the work on CPT \cite{blass:apal1999}. It should be noted that there is a close relationship to critical elements in a state defined via a minimal bounded exploration witness in the sequential, recursive and parallel ASM theses (see \cite{gurevich:tocl2000,boerger:fi2020} and \cite{ferrarotti:tcs2016}, respectively), and the active objects then correspond to the closure of a bounded exploration witness under subterms.} as follows.

\begin{definition}\label{def-active}\rm

Let $S$ be a state with base set $B$. An object $a \in B$ is called {\em critical} iff $a$ is an atom or $a \in \{ 0, 1 \}$ or $a$ is the value of a location $\ell$ of $S$ or there is a location $\ell = (f, \bar{a})$ with  $\text{val}_S(\ell) \neq \emptyset$ and $a$ appears in $\bar{a}$. An object $a \in B$ is called {\em active} in $S$ iff there exists a critical object $a^\prime$ with $a \in \textit{TC\/}(a^\prime)$.

\end{definition}

In addition, if $R = S_0, S_1, \dots$ is a run of an ASM, then we call an object $a \in B$ {\em active} in $R$ iff $a$ is active in at least one state $S_i$ of $R$.

\subsection{Polynomial-Time-Bounded ASMs}

In order to define a polynomial time bound on an ASM we have to count steps of a run. If we only take the length of a run, each step would be a macrostep that involves many elementary updates, e.g. the use of unbounded parallelism does not impose any restriction on the number of updates in an update set employed in a transition from one state to a successor state. So we better take the size of update sets into account as well. Furthermore, as objects are sets, their size also matters in estimating what an appropriate microstep is. We therefore adopt the notion of PTIME bound from CPT \cite{blass:apal1999}.

\begin{definition}\label{def-pbound}\rm

A {\em PTIME (bounded) ASM} is a triple $\tilde{M} = (M, p(n), q(n))$ comprising an ASM $M$ and two integer polynomials $p(n)$ and $q(n)$. A {\em run} of $\tilde{M}$ is an initial segment of a run of $M$ of length at most $p(n)$ and a total number of at most $q(n)$ active objects, where $n$ is the size of the input in the initial state of the run.

\end{definition}

We say that a PTIME ASM $\tilde{M}$ {\em accepts} the input structure $I$ iff there is a run of $\tilde{M}$ with initial state generated by $I$ and ending in a state, in which \textit{Halt\/} holds and the value of \textit{Output\/} is $1$. Analogously, a PTIME ASM $\tilde{M}$ {\em rejects} the input structure $I$ iff there is a run of $\tilde{M}$ with initial state generated by $I$ and ending in a state, in which \textit{Halt\/} holds and the value of \textit{Output\/} is $0$.

\section{Insignificant Choice}\label{sec:ic}

PTIME bounded ASMs as defined in the previous section are the non-deterministic analog of the PTIME bounded machines used to define CPT \cite{blass:apal1999}. As such they also allow the usual set-theoretic expressions to be used freely (see \cite[Sect.6.1]{blass:apal1999}). In this section we will motivate and then define a restriction of this non-deterministic computation model.

\subsection{Examples}

We look at two rather simple problems in PTIME and their solution using PTIME ASMs, the Parity problem and the bipartite matching problem. For both problems Blass, Gurevich and Shelah showed that they are not in CPT \cite{blass:apal1999}, thus adding choice to the computation model adds strength.

\begin{example}\label{bsp-parity}

Let us consider ASMs without input names. So the input structure is just the naked set of atoms. In addition to \textit{Output\/} and \textit{Halt\/} use nullary function symbols \textit{mode\/}, \textit{set\/} and \textit{parity\/}. For the values assigned to \textit{mode\/} we use `init' and `progress' to make the rule easier to read. Instead we could have used $\emptyset$ and $\{ \emptyset \}$ to strictly satisfy the requirement that all locations in an initial state with a dynamic function symbol have a value $\emptyset$. Thus, without loss of generality we can assume that in an initial state \textit{mode\/} = init holds.

Consider the following ASM rule

\begin{tabbing}
xxx\=xxxxxx\=xxxxxx\=xxxxxx\=xxxxxx\=xxxxxx\= \kill
\> \textbf{par} \> \textbf{if} \> \textit{mode\/} = init \\
\>\> \textbf{then} \> \textbf{par} \> \textit{mode\/} := progress \\
\>\>\>\> \textit{set\/} := \textit{Atoms\/} \\
\>\>\>\> \textit{parity\/} := \textbf{false} \\
\>\>\> \textbf{endpar}\\
\>\> \textbf{endif} \\
\>\> \textbf{if} \> \textit{mode\/} = progress \\
\>\> \textbf{then} \> \textbf{if} \textit{set\/} $\neq \emptyset$ \\
\>\>\> \textbf{then} \> \textbf{choose} $x \in$ \textit{set\/} \textbf{do} \\
\>\>\>\> \textbf{par} \> \textit{set\/} := \textit{set\/} $-$ \textit{Pair\/}$(x,x)$ \\
\>\>\>\>\> \textit{parity\/} := $\neg$ \textit{parity\/} \\
\>\>\>\> \textbf{endpar} \\
\>\>\>\> \textbf{enddo} \\
\>\>\> \textbf{else} \> \textbf{par} \> \textit{Output\/} := \textit{parity\/} \\
\>\>\>\>\> \textit{Halt\/} := \textbf{true} \\
\>\>\>\> \textbf{endpar}\\
\>\>\> \textbf{endif} \\
\>\> \textbf{endif} \\
\> \textbf{endpar}
\end{tabbing}

Clearly, we obtain a PTIME bounded ASM, and \textit{Output\/} will become true iff the size of the input structure is odd. Note that the choices $x \in \textit{set\/}$ are choices among atoms, as we always have $\textit{set\/} \subseteq \textit{Atoms\/}$.

\end{example}

Without choice the solution to Parity in Example \ref{bsp-parity} would not be possible within a polynomial time bound. We could replace the choice by unbounded parallelism, but then the computation would explore all possible orderings of the set of atoms, whereas with the choice only a single ordering is considered. Note that this is sufficient for the Parity problem. Further note that the Subset Parity problem could be handled in an analogous way.

\begin{example}\label{bsp-matching}\rm

For the bipartite matching problem we are given a finite bipartite graph $(V,E)$, where the set $V$ of vertices is partitioned into two sets \textit{Boys\/} and \textit{Girls\/} of equal size. Thus, the set $E$ of edges contains sets $\{ x, y \}$ with $x \in \textit{Boys\/}$ and $y \in \textit{Girls\/}$. A {\em perfect matching} is a subset $F \subseteq E$ such that every vertex is incident to exactly one edge in $F$. A {\em partial matching} is a subset $F \subseteq E$ such that every vertex is incident to at most one edge in $F$. So the algorithm will create larger and larger partial matchings until no more unmatched boys and girls are left, otherwise no perfect matching exists.

We use functions girls\_to\_boys and boys\_to\_girls turning sets of unordered edges into sets of ordered pairs:
\begin{align*}
\text{girls\_to\_boys}(X) &= \{ (g,b) \mid b \in \textit{Boys\/} \wedge g \in \textit{Girls\/} \wedge \{ b,g \} \in X \} \\
\text{boys\_to\_girls}(X) &= \{ (b,g) \mid b \in \textit{Boys\/} \wedge g \in \textit{Girls\/} \wedge \{ b,g \} \in X \}
\end{align*}
Conversely, the function unordered turns a set of ordered pairs $(b,g)$ or $(g,b)$ into a set of two-element sets:
\[ \text{unordered}(X) = \{ \{ x, y \} \mid (x,y) \in X \} \]

We further use a predicate reachable and a function path. For the former one we have reachable$(b,X,g)$ iff there is a path from $b$ to $g$ using the directed edges in $X$. For the latter one path$(b,X,g)$ is a set of ordered pairs representing a path from $b$ to $g$ using the directed edges in $X$. Both functions are defined elsewhere.

As in the previous Example \ref{bsp-parity} we can assume without loss of generality that in an initial state \textit{mode\/} = init holds. Then an algorithm for bipartite matching is realised by an ASM with the following rule:

\begin{tabbing}
x\=xxxx\=xxxxxx\=xxxxxx\=xxxxxx\=xxxx\=xxxx\= \kill
\> \textbf{par} \> \textbf{if} \> \textit{mode\/} = init \\
\>\> \textbf{then} \> \textbf{par} \> \textit{mode\/} := examine \\
\>\>\>\> \textit{partial\_match\/} := $\emptyset$ \\
\>\>\> \textbf{endpar} \\
\>\> \textbf{endif} \\
\>\> \textbf{if} \> \textit{mode\/} = examine \\
\>\> \textbf{then} \> \textbf{if} \> $\exists b \in \textit{Boys\/} . \forall g \in \textit{Girls\/} . \{ b,g \} \notin \textit{partial\_match\/}$ \\
\>\>\> \textbf{then} \> \textit{mode\/} := build-digraph \\
\>\>\> \textbf{else} \> \textbf{par} \> \textit{Output\/} := \textbf{true} \\
\>\>\>\>\> \textit{Halt\/} := \textbf{true} \\
\>\>\>\>\> \textit{mode\/} := final \\
\>\>\>\> \textbf{endpar} \\
\>\>\> \textbf{endif} \\
\>\> \textbf{endif} \\
\>\> \textbf{if} \> \textit{mode\/} = build-digraph \\
\>\> \textbf{then} \> \textbf{par} \> \textit{di\_graph\/} := girls\_to\_boys(\textit{partial\_match\/}) \\
\>\>\>\>\>\> $\cup$ boys\_to\_girls$(E - \textit{partial\_match\/})$ \\
\>\>\>\> \textit{mode\/} := build-path \\
\>\>\> \textbf{endpar} \\
\>\> \textbf{endif} \\
\>\> \textbf{if} \> \textit{mode\/} = build-path \\
\>\> \textbf{then} \textbf{choose} \>\> $b \in \{ x \mid x \in \textit{Boys\/} \wedge \forall g \in \textit{Girls\/} . \{ b,g \} \notin \textit{partial\_match\/} \}$ \\
\>\>\> \textbf{do} \> \textbf{if} $\exists g^\prime \in \textit{Girls\/} . \forall b^\prime \in \textit{Boys\/} . \{ b^\prime , g^\prime \} \notin \textit{partial\_match\/}$ \\
\>\>\>\>\>\> $\wedge\; \text{reachable}(b, \textit{di\_graph}, g^\prime)$ \\
\>\>\>\> \textbf{then} \textbf{choose} $g \in \{ y \mid y \in \textit{Girls\/} \wedge \forall x \in \textit{Boys\/} . \{ x,y \}$ \\
\>\>\>\> $\qquad \notin \textit{partial\_match\/} \wedge\; \text{reachable}(b, \textit{di\_graph}, y) \}$ \\
\>\>\>\>\> \textbf{do} \> \textbf{par} \> \textit{path\/} := \text{path}$(b,\textit{di\_graph},g)$ \\
\>\>\>\>\>\>\> \textit{mode\/} := modify \\
\>\>\>\>\>\> \textbf{endpar} \\
\>\>\>\>\> \textbf{enddo} \\
\>\>\>\> \textbf{else} \> \textbf{par} \> \textit{Output\/} := \textbf{false} \\
\>\>\>\>\>\> \textit{Halt\/} := \textbf{true} \\
\>\>\>\>\>\> \textit{mode\/} := final \\
\>\>\>\>\> \textbf{endpar} \\
\>\>\>\> \textbf{endif} \\
\>\>\> \textbf{enddo} \\
\>\> \textbf{endif} \\
\>\> \textbf{if} \> \textit{mode\/} = modify \\
\>\> \textbf{then} \> \textbf{par} \> \textit{partial\_match\/} := $(\textit{partial\_match\/} - \text{unordered}(\textit{path\/}))$ \\
\>\>\>\>\>\>\> $\cup (\text{unordered}(\textit{path\/}) - \textit{partial\_match\/})$ \\
\>\>\>\> \textit{mode\/} := examine \\
\>\>\> \textbf{endpar} \\
\>\> \textbf{endif} \\
\> \textbf{endpar}
\end{tabbing}

Clearly, we obtain a PTIME bounded ASM, and \textit{Output\/} will become true iff there exists a perfect matching. As in the previous example the non-deterministic choice of boys and girls, respectively, are choices among atoms.

\end{example}

Again the use of choice-rules in Example \ref{bsp-matching} cannot be dispensed with. However, we observe that in both cases, i.e. for the Parity problem and the bipartite matching problem, that the choices used are insignificant in the sense that if the final output is true for one choice made, then it is also true for any other possible choice. For the case of Parity this corresponds to the implicit creation of different orderings, while for bipartite matching different perfect matchings are constructed. We will formalise this observation in the sequel.

\subsection{Insignificant Choice Polynomial Time}

We now formalise the observation above concerning insignificant choice. We further restrict PTIME ASMs, which defines the ICPT logic. In Section \ref{sec:icpt} this will be linked to the logic of non-deterministic ASMs \cite{ferrarotti:igpl2017,ferrarotti:amai2018}.

\begin{definition}\label{def-icasm}\rm

An {\em insignificant choice ASM} (for short: icASM) is an ASM $M$ such that for every run $S_0 ,\dots, S_k$ of length $k$ such that \textit{Halt\/} holds in $S_k$, every $i \in \{ 0,\dots,k-1 \}$ and every update set $\Delta \in \boldsymbol{\Delta}(S_i)$ there exists a run $S_0 ,\dots, S_i, S_{i+1}^\prime ,\dots, S_m^\prime$ such that $S_{i+1}^\prime = S_i + \Delta$, \textit{Halt\/} holds in $S_m^\prime$, and \textit{Output\/} = \textbf{true} (or \textbf{false}, respectively) holds in $S_k$ iff \textit{Output\/} = \textbf{true} (or \textbf{false}, respectively) holds in $S_m^\prime$.

A {\em PTIME (bounded) insignificant choice ASM} (for short: PTIME icASM) is a triple $\tilde{M} = (M, p(n), q(n))$ comprising an icASM $M$ and two integer polynomials $p(n)$ and $q(n)$ with runs defined as in Definition \ref{def-pbound} such that whenever an input structure $I$ is accepted by $\tilde{M}$ (or rejected, respectively) then every run on input structure $I$ is accepting (or rejecting, respectively).

\end{definition}

According to this definition whenever there exists an accepting or rejecting run, then all other runs on the same input structure, i.e. runs that result making different choices, are also accepting or rejecting, respectively.

Note that the insignificant choice restriction is a semantic one expressed by means of runs. We will see in the next section how insignificant choice can be characterised in a logical way.

\begin{definition}\label{def-icpt}\rm

The complexity class {\em insignificant choice polynomial time} (ICPT) is the collection of pairs $(K_1, K_2)$, where $K_1$ and $K_2$ are disjoint classes of finite structures of the same signature, such that there exists a PTIME icASM that accepts all structures in $K_1$ and rejects all structures in $K_2$.

\end{definition}

We also say that a pair $(K_1, K_2) \in$ ICPT is {\em ICPT separable}. As for the analogous definition of CPT a PTIME icASM may accept structures not in $K_1$ and reject structures not in $K_2$. Therefore, we also say that a class $K$ of finite structures is in ICPT, if $(K,K^\prime) \in$ ICPT holds for the complement $K^\prime$ of structures over the same signature.

Let us link the definition of ICPT to PTIME logics as defined in \cite{blass:apal1999}. In general, a logic $\mathcal{L}$ can be defined by a pair (\textit{Sen\/},\textit{Sat\/}) of functions satisfying the following conditions:

\begin{itemize}

\item \textit{Sen\/} assigns to every signature $\Upsilon$ a recursive set $\textit{Sen\/}(\Upsilon)$, the set of {\em $\mathcal{L}$-sentences of signature $\Upsilon$}.

\item \textit{Sat\/} assigns to every signature $\Upsilon$ a recursive binary relation $\textit{Sat\/}_\Upsilon$ over structures $S$ over $\Upsilon$ and sentences $\varphi \in \textit{Sen\/}(\Upsilon)$. We assume that $\textit{Sat\/}_\Upsilon(S,\varphi) \Leftrightarrow \textit{Sat\/}_\Upsilon(S^\prime,\varphi)$ holds, whenever $S$ and $S^\prime$ are isomorphic.

\end{itemize}

We say that a structure $S$ over $\Upsilon$ {\em satisfies} $\varphi \in \textit{Sen\/}(\Upsilon)$ (notation: $S \models \varphi$) iff $\textit{Sat\/}_\Upsilon(S,\varphi)$ holds.

If $\mathcal{L}$ is a logic in this general sense, then for each signature $\Upsilon$ and each sentence $\varphi \in \textit{Sen\/}(\Upsilon)$ let $K(\Upsilon,\varphi)$ be the class of structures $S$ with $S \models \varphi$. We then say that $\mathcal{L}$ is a {\em PTIME logic}, if every class $K(\Upsilon,\varphi)$ is PTIME in the sense that it is closed under isomorphisms and there exists a PTIME Turing machine that accepts exactly the standard encodings of ordered versions of the structures in the class.

We further say that a logic $\mathcal{L}$ {\em captures PTIME} iff it is a PTIME logic and for every signature $\Upsilon$ every PTIME class of $\Upsilon$-structures conincides with some class $K(\Upsilon,\varphi)$.

These definitions of PTIME logics can be generalised to three-valued logics, in which case $\textit{Sat\/}_\Upsilon(S,\varphi)$ may be true, false or unknown. For these possibilities we say that $\varphi$ {\em accepts} $S$ or $\varphi$ {\em rejects} $S$ or neither, respectively. Then two disjoint classes $K_1$ and $K_2$ of structures over $\Upsilon$ are called {\em $\mathcal{L}$-separable} iff there exists a sentence $\varphi$ accepting all structures in $K_1$ and rejecting all those in $K_2$.

In this sense, ICPT is to define a three-valued PTIME logic that separates pairs of structures in ICPT. The idea is that sentences of this logic are PTIME icASMs, for which $\Upsilon$ is the signature of the input structure. By abuse of terminology we also denote this logic as ICPT.

\paragraph*{Remark}

Here we use the definitions of logic PTIME logic and logic capturing PTIME in exactly the same way as in \cite{blass:apal1999}. As pointed out by Dawar \cite{dawar:communication2020} Gurevich's original definition in \cite{gurevich:cttcs1988} is slightly different in that he requires the existence of a Turing machine $M$ mapping sentences $\varphi \in Sen(\Upsilon)$ to PTIME Turing machines $M_\varphi$ such that a structure $S$ satisfies $\varphi$ iff $M_\varphi$ accepts (an encoding of) $S$. According to Immerman \cite[p.25]{immerman:1999} not every encoding is suitable: encoding and decoding must be ``computationally easy'', and the encoding must be ``fairly space efficient''. This is to ensure that the simulating Turing machine $M_\varphi$ has a chance to operate in polynomial time. Fortunately, the standard encoding of an ordered version of a structure $S$ (see \cite[p.88]{libkin:2004}) satisfies these requirements, so it is justified to consider just this encoding. Furthermore, the effectivity of the translation, i.e. the mapping by means of a Turing machine $M$, is not mentioned in \cite{blass:apal1999}. This is, because in the case of CPT (and analogously here for ICPT) the sentences in $ Sen(\Upsilon)$ are specific ASMs, for which it is commonly known how to translate them, e.g. using a tool such as CoreASM \cite{farahbod:fi2007}, into executable code, i.e. the requested effective translation always exists. Hence the decisive quesrtions are how a recursive syntax for ICPT can be defined and how a simulation by Turing machines in polynomial time can be achieved.

Thus, at this stage we cannot yet call ICPT a logic, as the definition of ICPT includes a semantic restriction of ASMs, so it is not yet clear that our sentences define a recursive set. We will now investigate a stricter local insignificance condition, which will suffice for the capture of PTIME. This condition will then be exploited in the next section to define also a decidable syntax for ICPT, which will remove this concern.

\begin{definition}\label{def-ic-local}\rm

An ASM $M$ satisfies the {\em local insignificance condition} if and only if the following two conditions are satisfied:

\begin{enumerate}\renewcommand{\labelenumi}{(\roman{enumi})}

\item For every state $S$ any two update sets $\Delta, \Delta^\prime \in \boldsymbol{\Delta}(S)$ are isomorphic, and we can write
\[ \boldsymbol{\Delta}(S) \;=\; \{ \sigma \Delta \mid \sigma \in G \} \; , \]
where $G \subseteq \mathcal{I}so$ is a set of isomorphisms and $\Delta \in \boldsymbol{\Delta}(S)$ is an arbitrarily chosen update set.

\item For every state $S$ with $\boldsymbol{\Delta}(S) \;=\; \{ \sigma_i \Delta_0 \mid 0 \le i \le k \}$ ($G = \{ \sigma_0 ,\dots, \sigma_k \} \subseteq \mathcal{I}so$) and the corresponding successor states $S_i = S + \sigma_i \Delta_0$ we have
\[ \boldsymbol{\Delta}(S_i) \;=\; \sigma_i \boldsymbol{\Delta}(S_0) \; . \]

\end{enumerate}

\end{definition}

\begin{lemma}\label{lem-ic-local}

If $M$ satisfies the local insignificance condition, then $M$ is an icASM.

\end{lemma}

\begin{proof}

Let $S_0, \dots, S_\ell$ be a run of $M$ such that \textit{Halt\/} holds in $S_\ell$. Choose an arbitrary $i \in \{ 0, \dots, \ell - 1 \}$ such that $S_{i+1} = S_i + \Delta_i$ with $\Delta_i \in \boldsymbol{\Delta}(S_i)$. Let $S_i^\prime = S_i$ and $\Delta_i^\prime \in \boldsymbol{\Delta}(S_i^\prime)$. Then due to Definition \ref{def-ic-local}(i) there exists an isomorphism $\sigma_i$ with $\sigma_i(\Delta_i) = \Delta_i^\prime$.

Consider another run $S_0, \dots, S_i, S_{i+1}^\prime, \dots, S_m^\prime$ with $S_{j+1}^\prime = S_j + \Delta_j^\prime$ for $j \in \{ i, \dots, m-1 \}$. According to Definition \ref{def-ic-local}(ii) all successor states of $S_i$ have pairwise isomorphis sets of update sets. Furthermore, due to Definition \ref{def-ic-local}(i) all update sets in each of these sets of update sets are pairwise isomorphic. Hence all update sets in any successor state of $S_i$ are pairwise isomorphic.

Using this argument inductively we must have $\ell = m$ and there must exist isomorphisms $\sigma_j$ with $\sigma_j(\Delta_j) = \Delta_j^\prime$ for all $j \in \{ i ,\dots, \ell - 1 \}$. This implies that if $((f,()),b) \in \Delta_j$ holds for $f = \textit{Output\/}$ or $f = \textit{Halt\/}$ and $b \in \{ 0, 1 \}$, then also $((f,()),b) \in \Delta_j^\prime$ (as truth values are invariant under isomorphisms). Hence also if $\text{val}_{S_{j+1}}(f) = b$ holds, then also $\text{val}_{S_{j+1}^\prime}(f) = b$, i.e. the conditions of Definition \ref{def-icasm} are satisfied.\qed

\end{proof}

The proof actually shows that PTIME ASMs satisfying the local insiginifance condition have a very regular behaviour, as they proceed in ``layers''. In all runs $S_0 ,\dots, S_k$ and $S_0^\prime ,\dots, S_k^\prime$ with a fixed initial state $S_0 = State(I) = S_0^\prime$ with $S_{i+1} = S_i + \Delta_i$ and $S_{i+1}^\prime = S_i^\prime + \Delta_i^\prime$ the update sets $\Delta_i$ and $\Delta_i^\prime$ are isomorphic. The isomorphisms between such update sets on the $i$'th layer form a subgroup $G_i \subseteq \mathcal{I}so$. Furthermore, choosing an arbitrary update set $\Delta_i$ in the $i$'th layer all other update sets on this layer can be written as $\sigma \Delta_i$ with some $\sigma \in G_i$. The following corollary summarises this observation.

\begin{corollary}\label{cor-ic-local}

Let $M$ be a PTIME ASM satisfying the local insignificance condition with input structure $I$. Then for $i>0$ there exists a subgroup $G_i \subseteq \mathcal{I}so$ such that all update sets on the $i$'th layer in runs $S_0 ,\dots, S_k$ and $S_0^\prime ,\dots, S_k^\prime$ with $S_0 = State(I) = S_0^\prime$ take the form $\Delta_i = g(\Delta)$ with $g \in G_i$ and an arbitrary fixed $\Delta$.

\end{corollary}

\subsection{The Capture of PTIME}

We now present our first main result, the capture of PTIME by ICPT. For the proof that ICPT is subsumed by PTIME we basically use the same arguments as in the proof of the upper bound theorem for CPT \cite[Thm.3]{blass:apal1999}. For the proof that PTIME is subsumed by ICPT we exploit the fundamental theorem by Immerman, Livchak and Vardi that over ordered structures PTIME is captured by first-order logic plus inflationary or least fixed-point, i.e. by IFP[FO] \cite{immerman:ic1986,livchak:cmo1982,vardi:stoc1982}. As CPT and hence also ICPT covers IFP[FO] we only have to show that with a PTIME icASM we can create an order.

\begin{theorem}\label{thm-capture}

ICPT captures PTIME on arbitrary finite structures, i.e. ICPT = PTIME.

\end{theorem}

\begin{proof}

\textbf{\em PTIME $\boldsymbol{\subseteq}$ ICPT.} \ Consider a PTIME problem represented by a Boolean query $\phi$ and a signature for input structures $I$ for $\phi$, for which there exists a PTIME Turing machine $T$ accepting $I$ iff $I$ satisfies $\phi$. We combine three steps. First we show that with a PTIME ASM that satisfies the local insignificance condition we can construct an arbitrary order on the set of atoms of $State(I)$, so we obtain an ordered structure $(I,<)$. Then using an ASM rule \textsc{create\_encoding} we build the binary encoding of $(I,<)$ (see \cite[p.88]{libkin:2004}), which can be done by a PTIME ASM without choice in polynomial time. In the third step we use an ASM rule \textsc{run\_simulation} to simulate $T$ (see \cite[p.289]{boerger:2003}), which defines another PTIME ASM without choice. The second and the third steps are standard. The rule of the combined PTIME icASM looks as follows:

\begin{tabbing}
xxx\=xxxx\=xxxxxx\=xxxxxx\=xxxxxx\=xxxxxx\=xxxxxx\= \kill
\> \textbf{par} \> \textbf{if} \> \textit{mode\/} = init \\
\>\> \textbf{then} \> \textbf{par} \> \textit{mode\/} := create-order \\
\>\>\>\> $A := \textit{Atoms\/}$ \\
\>\>\>\> $A^c := \emptyset$ \\
\>\>\> \textbf{endpar} \\
\>\> \textbf{endif} \\
\>\> \textbf{if} \> \textit{mode\/} = create-order \\
\>\> \textbf{then} \> \textbf{if} \> $A \neq \emptyset$ \\
\>\>\> \textbf{then} \> \textbf{choose} $a \in A$ \\
\>\>\>\> \textbf{do} \> \textbf{par} \> \textbf{forall} $a^\prime \in A^c$ \\
\>\>\>\>\>\> \textbf{do} $<(a^\prime,a) := \;\textbf{true}$ \\
\>\>\>\>\>\> \textbf{enddo} \\
\>\>\>\>\>\> $A := A - \{ a \}$ \\
\>\>\>\>\>\> $A^c := A^c \cup \{ a \}$ \\
\>\>\>\>\> \textbf{endpar} \\
\>\>\>\> \textbf{enddo} \\
\>\>\> \textbf{else} \> \textit{mode\/} := build-tm \\
\>\>\> \textbf{endif} \\
\>\> \textbf{endif} \\
\>\> \textbf{if} \> \textit{mode\/} = build-tm \\
\>\> \textbf{then} \> \textbf{par} \> \textsc{create\_encoding} \\
\>\>\>\> \textit{mode\/} := simulate-tm \\
\>\>\> \textbf{endpar} \\
\>\> \textbf{endif} \\
\>\> \textbf{if} \> \textit{mode\/} = simulate-tm \\
\>\> \textbf{then} \> \textsc{run\_simulation} \\
\>\> \textbf{endif} \\
\> \textbf{endpar}
\end{tabbing}

Clearly, this ASM only exploits choices among atoms. We show that the conditions of Definition \ref{def-ic-local} are satisfied:

\begin{enumerate}\renewcommand{\labelenumi}{(\roman{enumi})}

\item When a choice is made, an atom $a \in A$ is selected and the corresponding update set $\Delta_a$ contains updates $((<,(a^\prime,a)),\textbf{true})$ for all $a^\prime in A^c$ as well as $((A,()), A_{new})$ with $A_{new} = \text{val}_S(A) - \{ a \}$, and $((A^c,()), A_{new}^c)$ with $A_{new}^c = \text{val}_S(A^c) \cup \{ a \}$. These update sets are parameterised by the selected atom $a$. For two different choices $a_1, a_2$ let $\sigma$ be the isomorphism defined by the transposition of $a_1$ and $a_2$. Clearly $\sigma (\Delta_{a_1}) = \Delta_{a_2}$ holds.

\item According to (i) we have $\boldsymbol{\Delta}(S) = \{ \sigma_i(\Delta) \mid 1 \le i \le k \}$ with isomorphisms $\sigma_i \in \mathcal{I}so$ defined by transpositions $(a,a_i)$. Let $S_i = S + \sigma_i (\Delta)$ (and $S^\prime = S + \Delta$ using $\sigma_1 = 1$). We have two cases:

\begin{enumerate}

\item The machine makes again a choice in all $S_i$ leading to $\boldsymbol{\Delta}(S_i) = \{ \Delta_{b_i} \mid b_i \in A \}$ as in (i) with $\Delta_{b_i} = \tau_{j}(\Delta_i)$ with a transposition $\tau_j = (b_i,b_{ij}^\prime)$. This gives
\[ \sigma_i \boldsymbol{\Delta}(S^\prime) = \{ \sigma_i (\Delta_{b_i}) \mid b_i \in A \} = \{ \sigma_i \tau_j (\Delta) \mid 1 \le j \le \ell \} = \boldsymbol{\Delta}(S_i) \; . \]

\item The machine only yields a single update set $\{ ((\textit{mode\/},()),\text{build-tm}) \}$, which is invariant under all $\sigma_i$ ($1 \le i \le k$).

\end{enumerate}

\end{enumerate}

Hence the constructed ASM satisfies the local insignificance condition, so it is a PTIME icASM due to Lemma \ref{lem-ic-local}.

\paragraph*{\textbf{ICPT $\boldsymbol{\subseteq}$ PTIME}}

Assume a PTIME icASM $\tilde{M} = (M, p(n), q(n))$. Analogously to the proof of \cite[Thm.3]{blass:apal1999} we create a simulating PTIME Turing machine, which takes strings encoding ordered versions of input structures $I$ of $\tilde{M}$ as input. The bounds in set terms appearing in \textbf{forall} rules ensure that the number of immediate subcomputations is bounded by the number of active elements and thus by $q(n)$. This defines a polynomial bound on the number of steps of the simulating Turing machine. Furthermore, as the simulating Turing machine operates on encodings of ordered versions of structures, any choice is simulated by selecting the smallest element in the order. As all choices are insignificant, this has no effect on the final result.

It remains to show that checking that a choice satisfies the local insignificance condition can be done in polynomial time. A simulating Turing machine can produce encodings of all update sets in $\boldsymbol{\Delta}(S)$ and write them onto some tape. Any object appearing in an update set must be active, and there is a polynomial bound $q(n)$ on the number of active objects. Furthermore, as choices are only among atoms there are at most $n$ such update sets, and it suffices to explore at most $n-1$ isomorphisms defined by transpositions of two atoms. Applying such an isomorphism to an update set requires time linear in the size of the update set, and a follow-on check of set equality is again possible in polynomial time. Hence checking condition (i) in Definition \ref{def-ic-local} can be simulated by a Turing machine in polynomial time.

Analogously, the simulating Turing machine can produce encodings of all sets of update sets for the at most $n$ successor states. Again, the number of update sets in each $\boldsymbol{\Delta}(S_i)$ is polynomially bounded and the size of each update set is polynomially bounded, because the number of active objects is bounded by the polynomial $q(n)$. Then in the simulation at most $n-1$ isomorphisms defined by transpositions of atoms have to be applied, followed by set equality checking in polynomial time. Hence, also the check of condition (ii) in Definition \ref{def-ic-local} can be simulated by a Turing machine in polynomial time.

Finally, the length of each run is bounded by a polynomial $p(n)$, which together with the bounded nesting of choice rules defines a polynomial bound on the number of times local insignificance has to be checked.

Hence the simulating Turing machine works in polynomial time and accepts (or rejects) its input iff $\tilde{M}$ accepts the corresponding input structure or rejects it, respectively.\qed

\end{proof}

Note that the first part of the proof shows that PTIME is included in a fragment of ICPT defined by ASMs satisfying the local insignificance condition. We formulate this result as a separate corollary.

\begin{corollary}\label{cor-icpt-ptime}

PTIME is captured by the fragment ICPT$_{loc}$ of ICPT, where the separating icASM satisfies the local insignificance condition.

\end{corollary}

\begin{proof}

In the proof above of Theorem \ref{thm-capture} we explicitly constructed a PTIME ASM satisfying the local insignificance condition. Lemma \ref{lem-ic-local} implies that it is an icASM. This shows that for the capture of PTIME it suffices to use the local insignificance condition.\qed

\end{proof}

Our proof allows us to extend the observation in Corollary \ref{cor-ic-local} concerning layers in computations with ASMs satisfying the local insignificance condition. If $g = (a_1, a_2) \in G_i$ is a transposition of atoms and $\pi \in Aut(I)$ is an automorphism of the input structure defined by a permutation of the atoms, then $\pi g \pi^{-1}$ is the transposition $(\pi(a_1), \pi(a_2)) \in G_i$. This gives rise to the following corollary.

\begin{corollary}\label{cor-layer}

Let $M$ be an ASM satisfying the local insignificance condition with input structure $I$ and let $G_i$ be the $i$'th layer subgroup of $\mathcal{I}so$ from Corollary \ref{cor-ic-local}. Then for all $g \in G_i$ and all $\pi \in Aut(I)$ we have $\pi g \pi^{-1} \in G_i$.

\end{corollary}

Theorem \ref{thm-capture} is not yet fully satisfactory, because so far ICPT still depends on a semantic restriction of PTIME ASMs, in other words: we still have to show that we can obtain a recursive syntax. However, all other conditions for a logic capturing PTIME are already satisfied. Corollary \ref{cor-icpt-ptime} allows us to formalise ICPT by the local insignificance condition, which gives us a handier characterisation of ICPT. We will exploit this characterisation in the section on fixed-point definability linking ICPT to the logic of non-deterministic ASMs \cite{ferrarotti:igpl2017,ferrarotti:amai2018}.

\section{The Logic of ASMs and Insignificant Choice}\label{sec:icpt}

We now look further into the capture of PTIME by ICPT, for which we exploit the logic of non-deterministic ASMs, which we tailor to our purposes here.

\subsection{The Logic of Non-Deterministic ASMs}

The logic of ASMs introduced by St\"ark and Nanchen is a definitional extension of first-order logic that allows us to express statements about a step of a computation of a deterministic ASM, i.e. without choice-rules. Decisive for the logic are predicates $upd(r, f, \bar{x}, y)$ with a rule $r$ and a (dynamic) function symbol $f$ in the signature $\Upsilon$ of an ASM. Informally, it expresses that after application of the rule $r$ in the given state the location $(f,\bar{x})$ (so the length of the tuple $\bar{x}$ is the arity of $f$) will have the value $y$. In \cite{glavan:csl1992} and also in \cite{blass:apal1999} this predicate was written as $\textit{Update\/}_{r,f}(\bar{x},y)$ to emphasise the extra-logical character of $r$ and $f$.

The extension of the logic to the case of non-deterministic ASMs was left open due to problems concerning the expression of consistency (see the detailed discussion in \cite[p.326f.]{boerger:2003}). This gap was closed by Ferrarotti et al. first emphasising database transformations \cite{ferrarotti:igpl2017}, then in general\footnote{This includes the possibility to simulate concurrent ASMs by non-deterministic ones, which permits to exploit the logic also for reasoning about concurrent systems.} \cite{ferrarotti:amai2018}. The key idea underlying this work is to replace $upd(r, f, \bar{x}, y)$ by a new predicate $upd(r,X)$ with the informal meaning that the rule $r$ in the given state yields the update set $X$. Then $[X]\varphi$ (instead of $[r]\varphi$ in the St\"ark/Nanchen logic) is used to express that after the application of the update set $X$, i.e. in the successor state, the formula $\varphi$ will hold.

This makes the logic a fragment of second-order logic. Nonetheless, a completeness result could be achieved on the grounds of Henkin semantics for the logic \cite{ferrarotti:igpl2017}, whereas in \cite{ferrarotti:amai2018} a typed extension of first-order logic was exploited.

The logic addresses many subtleties considered necessary for reasoning about non-deterministic ASMs, but several of these are not needed for our purposes here:

\begin{itemize}

\item The ASMs supported by the logic are based on meta-finite states. Therefore, three types of function symbols are distinguished: database functions defining finite structures, algorithmic functions defining arbitrary structures, and bridge functions linking them. In Section 2 for the ASMs in this article we required that the domain of each dynamic function shall be finite in every state. With this requirement the subtle distinction obtained by meta-finite states becomes irrelevant.

\item The logic is grounded on ASMs that permit multiset functions (defined in the background) as synchronisation operators for synchronous parallelism as expressed by \textbf{forall} rules. The version of ASMs in this article, however, does not foresee such operators. Synchronisation can be handled in a different way, which will require more microsteps, but otherwise has no effect on the complexity as defined here. Therefore, we can dispense with the so-called $\varrho$-terms of the logic.

\item In order to feed the synchronisation operators the logic handles not only update sets, but also update multisets, and a corresponding predicate $upm(r,\ddot{X})$ expressing that rule $r$ yields the update multiset $\ddot{X}$ in the given state. Clearly, for our purposes here we can omit update multisets.

\end{itemize}

With these simplifications in mind we define the logic $\mathcal{L}^{nd}$ of non-deterministic ASMs. As the logic has to deal with update sets, we exploit that the signature of our ASMs contain a static constant symbol $c_f$ for each dynamic function symbol $f \in \Upsilon$, i.e. $c_f$ is not dynamic and has arity $0$. We also exploit that the base set contains elements that interpret $c_f$ in every state. By abuse of notation we wrote $({c_f})_S = c_f$. Now let $X$ be a second-order variable of arity 3. For a variable assignment $\zeta$ we say that $\zeta(X)$ {\em represents an update set} $\Delta$ iff for each $((f,\bar{a}),b) \in \Delta$ we have $(c_f, \bar{a}, b) \in \zeta(X)$ and vice versa. Here we write $\bar{a}$ for $n$-tuples, where $n$ is the arity of $f$. Using the Kuratowski representation of pairs by sets and its extension to $n$-tuples, we can think of $\bar{a}$ as being represented by a set.

As for the syntax, with this extension the terms of $\mathcal{L}^{nd}$ are ASM terms as defined in Section \ref{sec:asm}. The formulae of the logic are defined inductively as follows:

\begin{itemize}

\item If $t$ and $t^\prime$ are terms, then $t = t^\prime$ is a formula.

\item If $X$ is an $n$-ary second-order variable and $t_1 ,\dots, t_n$ are terms, then $X(t_1, \dots, t_n)$ is a formula.

\item If $r$ is an ASM rule and $X$ is a second-order variable of arity $3$, then upd$_r(X)$ is a formula.

\item If $\varphi$ and $\psi$ are formulae, then also $\neg \varphi$, $\varphi \wedge \psi$, $\varphi \vee \psi$ and $\varphi \rightarrow \psi$ are formulae.

\item If $\varphi$ is a formula, $x$ is a first-order variable and $X$ is a second-order variable, then also $\forall x . \varphi$, $\exists x . \varphi$, $\forall X . \varphi$, $\exists X . \varphi$ are formulae.

\item If $\varphi$ is a formula and $X$ is a second-order variable of arity 3, then $[X] \varphi$ is formula.

\end{itemize}

We use the usual shortcuts and parentheses when needed. We also write simply $f(t_1, \dots, t_n)$ for the formula $f(t_1, \dots, t_n) = \;\textbf{true}$ in case $f$ is relational.

For the semantics of $\mathcal{L}^{nd}$ we use Henkin structures \cite{henkin:jsl1950}. We first define Henkin prestructures.

\begin{definition}\label{def-prehenkin}\rm

A {\em Henkin prestructure} $\tilde{S}$ over signature $\Upsilon$ is a structure $S$ over $\Upsilon$ as defined in Section \ref{sec:asm} with base set $B$ together with sets of relations $D_n \subseteq \mathcal{P}(B^n)$ for all $n \ge 1$.

\end{definition}

With this definition we inherit all our specific assumptions on structures from Section \ref{sec:asm}, in particular the finiteness of the domain of all dynamic function symbols. For a consistent update set $\Delta$ we assume that $S + \Delta$ preserves the sets of relations $D_n$ of $\tilde{S}$, i.e. $\tilde{S} + \Delta$ is the Henkin prestructure $(S + \Delta, \{ D_n \}_{n \ge 1})$.

As the logic uses second-order variables we need extended variable assignments $\zeta$ into a Henkin prestructure. For first-order variables $x$ we have $\zeta(x) \in B$ as usual, but for second-order variables $X$ of arity $n$ we request $\zeta(X) \in D_n$. Then with respect to a Henkin prestructure $\tilde{S}$ and such a variable assignment terms are interpreted as usual. The interpretation $[\![ \varphi ]\!]_{\tilde{S},\zeta}$ for formulae $\varphi$ is defined as follows (we omit the interpretation for the shortcuts):

\begin{itemize}

\item If $\varphi$ has the form $t = t^\prime$, then $[\![ \varphi ]\!]_{\tilde{S},\zeta} = \begin{cases}
1 &\text{if}\; \text{val}_{S,\zeta}(t) = \;\text{val}_{S,\zeta}(t^\prime) \\ 0 &\text{else} \end{cases}$.

\item If $\varphi$ has the form $X(t_1 ,\dots, t_n)$, then
\[ [\![ \varphi ]\!]_{\tilde{S},\zeta} = \begin{cases}
1 &\text{if}\; (\text{val}_{S,\zeta}(t_1) ,\dots, \text{val}_{S,\zeta}(t_n)) \in \text{val}_{S,\zeta}(X) \\
0 &\text{else} \end{cases} . \]

\item If $\varphi$ has the form $\text{upd}_r(X)$, then
\[ [\![ \varphi ]\!]_{\tilde{S},\zeta} = \begin{cases}
1 &\text{if}\; \text{val}_{S,\zeta}(X) \;\text{represents an update set}\; \Delta \in \boldsymbol{\Delta}_{r,\zeta}(S) \\ 0 &\text{else} \end{cases} . \]

\item If $\varphi$ has the form $\neg \psi$, then $[\![ \varphi ]\!]_{\tilde{S},\zeta} = \begin{cases}
1 &\text{if}\; [\![ \psi ]\!]_{\tilde{S},\zeta} = 0 \\ 0 &\text{else} \end{cases}$.

\item If $\varphi$ has the form $\psi_1 \vee \psi_2$, then $[\![ \varphi ]\!]_{\tilde{S},\zeta} = \begin{cases}
0 &\text{if}\; [\![ \psi_1 ]\!]_{\tilde{S},\zeta} = [\![ \psi_2 ]\!]_{\tilde{S},\zeta} = 0 \\ 1 &\text{else} \end{cases}$.

\item If $\varphi$ has the form $\forall x . \psi$, then
\[ [\![ \varphi ]\!]_{\tilde{S},\zeta} = \begin{cases}
1 &\text{if}\; [\![ \psi ]\!]_{\tilde{S},\zeta[x \mapsto a]} = 1 \;\text{for all}\; a \in B \\
0 &\text{else} \end{cases} . \]

\item If $\varphi$ has the form $\forall X . \psi$ with a second-order variable $X$ of order $n$, then
\[ [\![ \varphi ]\!]_{\tilde{S},\zeta} = \begin{cases}
1 &\text{if}\; [\![ \psi ]\!]_{\tilde{S},\zeta[X \mapsto A]} = 1 \;\text{for all}\; A \in D_n \\
0 &\text{else} \end{cases} . \]

\item If $\varphi$ has the form $[X]\psi$, then
\[ [\![ \varphi ]\!]_{\tilde{S},\zeta} = \begin{cases}
0 &\text{if}\; \text{val}_{S,\zeta}(X) \; \text{represents a consistent update set}\; \Delta \\
&\text{with}\; [\![ \psi ]\!]_{\tilde{S}+\Delta,\zeta} = 0 \\
1 &\text{else} \end{cases} . \]

\end{itemize}

The last definition requires some explanation. We have $[\![ \varphi ]\!]_{\tilde{S},\zeta} = 1$, if $\text{val}_{S,\zeta}(X)$ represents an inconsistent update set $\Delta$. In this case $S + \Delta$ is not a well-defined state, so it makes sense to say that any formula is satisfied in it.

While this interpretation is defined for arbitrary Henkin prestructures, it makes sense to restrict the collections $D_n$ of $n$-ary relations to those that are closed under definability, which defines the notion of Henkin structure. We then say that a sentence is {\em valid} iff it is interpreted as 1 (i.e., true) in all Henkin structures.

\begin{definition}\label{def-henkin}\rm

A {\em Henkin structure} over signature $\Upsilon$ is a Henkin prestructure $\tilde{S} = (S, \{ D_n \}_{n \ge 1})$ that is closed under definability, i.e. for every formula $\varphi$, every variable assignment $\zeta$ and every $n \ge 1$ we have
\[ \{ (a_1 ,\dots, a_n) \in B^n \mid [\![ \varphi ]\!]_{\tilde{S},\zeta[x_1 \mapsto a_1, \dots, x_n \mapsto a_n]} = 1 \} \in D_n . \]

\end{definition}

Note that we merely need second-order variables to capture update sets and isomorphisms defined by choice rules. Therefore, the use of Henkin structures is not really a restriction.

\subsection{ICPT Restriction}

We now approach a characterisation of the semantic insignificant choice restriction in the logic $\mathcal{L}^{nd}$ defined above. First we show how to express that $X$ represents an update set, or is consistent. For these we have
\begin{align*}
\text{isUSet}(X) \equiv \forall x_1, x_2, x_3 . X(&x_1, x_2, x_3) \rightarrow \\
&\bigvee_{f \in \Upsilon_{dyn}} ( x_1 = c_f \wedge \exists y_1, \dots, y_{ar(f)}. x_2 = ( y_1, \dots, y_{ar(f)})
\end{align*}
using $ar(f)$ to denote the arity of $f$ and $\Upsilon_{dyn}$ to denote the set of dynamic function symbols and
\begin{align*}
\text{conUSet}(X) \equiv \;\text{isUSet}(X) \wedge & \forall x_1, x_2, x_3, x_4 . \\
& ( X(x_1, x_2, x_3) \wedge X(x_1, x_2, x_4) \rightarrow x_3 = x_4 ) .
\end{align*}
Next we exploit that due to Definition \ref{def-ic-local}  for a choice in state $S$ to be insignificant we need that all update sets in $\boldsymbol{\Delta}_r(S)$ are isomorphic, so we express that $X$ is an isomorphism by
\begin{align*}
\text{iso}(X) \equiv \forall x, & y_1, y_2 . ( X(x,y_1) \wedge X(x, y_2) \rightarrow y_1 = y_2 ) \wedge \\
& \forall x_1, x_2, y . ( X(x_1,y) \wedge X(x_2, y) \rightarrow x_1 = x_2 ) \wedge \\
&\qquad\qquad \forall x \exists y . X(x,y) \wedge \forall y \exists x . X(x,y) \wedge \\
&\forall x,y. [ X(x,y) \rightarrow (x \in \textit{Atoms\/} \leftrightarrow y \in \textit{Atoms\/}) \\
&\qquad\qquad \wedge \forall u . (u \in x \rightarrow \exists v . v \in y \wedge X(u,v)) \\
&\qquad\qquad \wedge \forall v . (v \in y \rightarrow \exists u . u \in x \wedge X(u,v)) ] \\
& \wedge \bigwedge_{f \in \Upsilon_{dyn}} X(c_f,c_f)
\end{align*}
This leads to the following {\em insignificance constraint} for a rule $r$ expressing that any two update sets yielded by $r$ are isomorphic. Recall that an isomorphism $\sigma$ extends to updates $((f,(a_1,\dots,a_n)),b)$ by $\sigma ((f,(a_1,\dots,a_n)),b) = ((f,(\sigma(a_1),\dots,\sigma(a_n))),\sigma(b))$ (see e.g. \cite[p.66]{boerger:2003}).
\begin{align*}
\forall X_1, X_2 . & \;\text{upd}_r(X_1) \wedge \;\text{upd}_r(X_2) \rightarrow \\
& \exists X. ( \text{iso}(X) \wedge \text{updIso}(X_1,X_2,X) \wedge \text{updIsoSet}(X_1,X_2,X) )
\end{align*}
with
\begin{align*}
\text{updIso}(X_1,& X_2,X) \equiv \\
\bigwedge_{f \in \Upsilon_{dyn}} & [ \forall \bar{x}_1, x_2, \bar{y}_1, y_2 .
( X_1(c_f, \bar{x}_1, x_2) \wedge \bigwedge_{1 \le i \le ar(f)} X(x_{1i}, y_{1i}) \wedge X(x_2,y_2) \\
& \hspace*{7cm} \rightarrow X_2(c_f, \bar{y}_1, y_2) ) \\
& \wedge \forall \bar{x}_1, x_2, \bar{y}_1, y_2 .
( X_2(c_f, \bar{x}_1, x_2) \wedge \bigwedge_{1 \le i \le ar(f)} X(x_{1i}, y_{1i}) \wedge X(x_2,y_2) \\
& \hspace*{7cm} \rightarrow X_1(c_f, \bar{y}_1, y_2) ) ]
\end{align*}
and\footnote{Note that $\text{updIsoSet}(X_1,X_2,X)$ depends on the rule $r$.}
\begin{align*}
\text{updIsoSet}(X_1,& X_2,X) \equiv & \\
\forall Y_1, Y_2 . & (\text{isUSet}(Y_1) \wedge \text{isUSet}(Y_2) \wedge \text{updIso}(Y_1,Y_2,X)) \rightarrow \\
& ([X_1]\text{upd}_r(Y_1) \leftrightarrow [X_2]\text{upd}_r(Y_2))
\end{align*}

We can use this characterisation of insignificant choice to modify the logic in such a way that a choice rule will either become an insignificant choice or interpreted as \textbf{skip}. First we recall the axiomatic definition of $\text{upd}_r(X)$ from \cite[Sect.7.2]{ferrarotti:igpl2017} (adapted to our simplifications of $\mathcal{L}^{nd}$).

\begin{description}

\item[U0] For $r = \textbf{skip}$ we have $\text{upd}_r(X) \leftrightarrow X = \emptyset$.

\item[U1] For an assignment $r$ of the form $f(t_1, \dots, t_n) := t_0$ we have
\begin{align*}
\text{upd}_r(X) \leftrightarrow &\text{isUSet}(X) \wedge \forall x_1, x_2, x_3 .  ( X(x_1, x_2, x_3) \leftrightarrow \\
&\qquad\qquad x_1 = c_f \wedge x_2 = (t_1, \dots, t_{ar(f)}) \wedge x_3 = t_0 )
\end{align*}

\item[U2] For a branching rule $r$ of the form \textbf{if} $\varphi$ \textbf{then} $r_1$ \textbf{else} $r_2$ \textbf{endif} we have
\[ \text{upd}_r(X) \leftrightarrow (\varphi \wedge \;\text{upd}_{r_1}(X)) \vee (\neg\varphi \wedge \;\text{upd}_{r_2}(X)) \]

\item[U3]  For a parallel rule $r$ of the form \textbf{forall} $v \in t$ \textbf{do} $r^\prime(v)$ \textbf{enddo} we have
\begin{align*}
\text{upd}_r(X) \leftrightarrow \; &\text{isUSet}(X) \wedge
\exists Y. [ ( \bigwedge_{f \in \Upsilon_{dyn}} \forall y, z. X(c_f,y,z) \leftrightarrow \exists x . Y(c_f,y,z,x) ) \\
\wedge \forall x . & (x \in t \rightarrow \exists Z . \text{upd}_{r^\prime(x)}(Z) \wedge \bigwedge_{f \in \Upsilon_{dyn}} \forall y,z . (Z(c_f,y,z) \leftrightarrow Y(c_f,y,z,x))) \\
& \wedge \forall x . (x \notin t \rightarrow \bigwedge_{f \in \Upsilon_{dyn}} \forall y,z . \neg Y(c_f,y,z,x)) ]
\end{align*}

\item[U4] For a choice rule of the form \textbf{choose} $v \in \{ x \mid x \in \textit{Atoms\/} \wedge x \in t \}$ \textbf{do} $r^\prime(v)$ \textbf{enddo} we have
\[ \text{upd}_r(X) \leftrightarrow \exists v. v \in \textit{Atoms\/} \wedge v \in t \wedge \;\text{upd}_{r^\prime(v)}(X) \]

\end{description}

In order to express insignificant choice introduce new formulae of the form $\text{upd}^{ic}_r(X)$. If $r$ is not a choice rule, we simply keep the definitions above in \textbf{U0}--\textbf{U3} replacing \text{upd} by \text{upd}$^{ic}$ on the right hand side of the equivalence.

\begin{description}

\item[U4$^\prime$] For a choice rule $r$ of the form \textbf{choose} $v \in \{ x \mid x \in \textit{Atoms\/} \wedge x \in t \}$ \textbf{do} $r^\prime(v)$ \textbf{enddo} we define
\begin{align*}
\text{upd}^{ic}_r(X) \leftrightarrow& \exists v. v \in \textit{Atoms\/} \wedge v \in t \wedge \;\text{upd}^{ic}_{r^\prime(v)}(X) \wedge \\
& \forall Y. (\exists x. x \in \textit{Atoms\/} \wedge x \in t \wedge \;\text{upd}^{ic}_{r^\prime(x)}(Y) ) \rightarrow \\
&\qquad \exists Z. ( \text{iso}(Z) \wedge \text{updIso}(X,Y,Z) \wedge \text{updIsoSet}(X,Y,Z) )
\end{align*}

\end{description}

Note that the definition of $\text{upd}^{ic}_r(X)$ above for a choice-rule $r$ includes the formula $\text{updIsoSet}(X,Y,Z)$, which depends on the rule $r$ and this includes $\text{upd}_r(X^\prime)$ (not $\text{upd}^{ic}_r(X^\prime)$!). We can eliminate $\text{upd}_r(X^\prime)$ using the definition in \textit{U4\/}. For $\text{upd}_{r^\prime(v)}(X^\prime)$ it would do no harm to replace it by $\text{upd}^{ic}_{r^\prime(v)}(X^\prime)$, but it is not necessary.

The axiom \textbf{U4$^\prime$} redefines the semantics of choice rules in the desired way\footnote{Analogous to \cite[Lemma~7.3]{ferrarotti:igpl2017} the axioms above for \text{upd}$^{ic}_r(X)$ further show that every formula in our logic can be written in an equivalent form not containing \text{upd}$^{ic}$ at all.}. Corollary \ref{cor-icpt-ptime} implies that for ICPT it suffices to consider PTIME ASMs satisfying the local insignificance condition. In the remainder of this article we will always consider such ASMs.

\subsection{ICPT: A Logic Capturing PTIME}

Returning to the question whether ICPT is a logic this can now be confirmed.

\begin{definition}\label{def-logic-icpt}\rm

The logic ICPT is defined as follows:

\begin{enumerate}

\item The sentences $Sen(\Upsilon_0)$ of the logic are PTIME icASMs $M$ with signature $\Upsilon_0$ for the input structures that satisfy the local insignificance condition. Syntactically, the choice rule in these icASMs is restricted to choice among atoms. The semantics is defined via $\text{upd}^{ic}_r$, i.e. choice rules either yield a set of isomorphic update sets satisfying the conditions in Definition \ref{def-ic-local} or no update set at all. We continue to denote such rules with \textbf{choose}, though these are very special choice rules.

\item $Sat(I,M)$ holds if and only if the input structure $I$ is accepted by the ASM $M$.

\end{enumerate}

\end{definition}

The specific semantics defined via $\text{upd}^{ic}_r$ guarantees decidable syntax, i.e. that $Sen(\Upsilon_0)$ is a recursive set. Then Theorem \ref{thm-capture} shows that this logic captures PTIME. The restriction of choices to atoms enables the PTIME simulation by Turing machines taking the standard encoding of an ordered version of the input structure as input, and the local insignificance condition guarantees also global insignificance, so a simulating Turing machine does not makes choices.

\section{Fixed-Point Definability}\label{sec:fixpoints}

We now address a generalisation of the fixed point theorems for CPT (see \cite[Thm.18\&19]{blass:apal1999}) to ICPT. From now we consider only icASMs that satisfy the local insignificance condition. Basically, we replace first-order logic by a fragment of $\mathcal{L}^{nd}$.

First, analogous to CPT we make our ASMs {\em time-explicit}, i.e. we replace the rule $r$ by a new rule of the form

\begin{quote}
\textbf{par} $r$ \textbf{if} \textit{Halt\/} = \textbf{false} \textbf{then} $ct := ct \cup \{ ct \}$ \textbf{endif} \textbf{endpar}
\end{quote}

\noindent
That is, we use a counter $ct$ taking non-negative integer values, which is initially set to $0$ and incremented in every step of the machine. Then for a PTIME bounded ASM $\tilde{M}$ the polynomial bounds have to be slightly adjusted, but still the time-explicit ASM will be PTIME bounded, and apart from the counter does exactly the same as the originally given ASM.

\subsection{Acceptance of Input Structures}

Now let $\tilde{M} = (M, p(n), q(n))$ be a PTIME icASM with time-explicit $M$. For an input structure $I$ let $\text{State}(I)$ denote the initial state generated by $I$. Then the base set of every state is $B = HF(A) \cup K$, where $A$ is the set of atoms of the base set of $I$ and $K = \{ c_f \mid f \in \Upsilon_{dyn} \}$. Recall that the isomorphisms permuting the update sets in one state are defined by permutations of $A$.

Then let $\textit{Active\/}(I)$ denote the set of active objects in some run starting in the initial state generated by $I$. Clearly, due to the definition of active objects $\textit{Active\/}(I)$ is a transitive set. By abuse of notation let $\textit{Active\/}(I)$ also denote the structure $(\textit{Active\/}(I) \cup K, \{ c_f \mid f \in \Upsilon_{dyn} \}, \bar{R})$ plus background structure, where $K = \{ c_f \mid f \in \Upsilon_{dyn} \}$ and $\bar{R}$ stands for the relations in the input structure $I$.

Let $S_0, S_1, \dots, S_{\ell}$ be a run of $M$ of length $\ell$. Then we have a sequence $Z_0, \dots, Z_{\ell-1}$ of update sets with $S_{i+1} = S_i + Z_i$ for $i=0,\dots,\ell-1$. For each $f \in \Upsilon_{dyn}$ we introduce a new relation symbol $D_f$ of arity 4 with the intended semantics that $D_f(i,\bar{x},y,Z)$ should hold iff $S_i \models f(\bar{x}) = y \neq 0$. Here $\bar{x}$ must be an $n$-tuple with $n = ar(f)$, which can be represented as a set, and $Z$ is either the update set $Z_{i-1}$ if it contains $((f,\bar{x}),y)$ or $Z = \emptyset$. This is needed to distinguish the different possible successors of $S_i$.

Analogous to \cite[Thm.18]{blass:apal1999} we obtain the following Theorem \ref{thm-fixpoint}. Before formulating this theorem and its proof, let us observe that without loss of generality we can write formulae of our logic in an equivalent {\em term normal form}, where all atomic subformulae that are equations with a function symbol $g$ take the form $g(\bar{u}) = t$, where $\bar{u}$ is a tuple of variables and $t$ is either a variable or a constant \textbf{true} or \textbf{false}.

\begin{theorem}[First Fixed-Point Theorem]\label{thm-fixpoint}

The relations $D_f(i,\bar{x},y,Z)$ for $f \in \Upsilon_{dyn}$ can be defined by an inflationary fixed-point formula $[\textbf{ifp}_{D_f} \phi(D_f, i, \bar{x}, y, Z)]$ independent of the input structure $I$ over the structure $\textit{Active\/}(I)$.

\end{theorem}

\begin{proof}

Let $r$ be the rule of the ASM $M$. We must have $D_f(0, \bar{x}, y, Z) \leftrightarrow false$, because in an initial state the domain of each dynamic function $f$ must be empty. For $i > 0$ the formula $\phi$ must express that either $f(\bar{x}) = y$ was already true in the previous state and $r$ does not yield an update set with a different new value $z$ for $f(\bar{x})$ or $r$ yields an update set in the previous state that contains $((f,\bar{x}),y)$. Hence we define $D_f$ by simultaneous recursion using
\begin{gather*}
D_f(i, \bar{x}, y, Z) \;\leftrightarrow\;\; \textit{PosInteger\/}(i) \wedge y \neq 0 \wedge \\
[( \exists Z^\prime . D_f(i-1, \bar{x}, y, Z^\prime ) \wedge \neg \exists X . ( U_r(i-1, X) \wedge \exists z . ( z \neq y \wedge X(c_f, \bar{x}, z) )) \wedge Z = \emptyset) \vee \\
\exists X . ( U_r(i-1, X) \wedge X(c_f, \bar{x}, y) \wedge Z = X ) ],
\end{gather*}
where $U_r(j,X)$ is the formula that results from $\text{upd}^{ic}_r(X)$ by replacing every atomic subformula of the form $g(\bar{u}) = t$ with dynamic function symbol $g$ by\footnote{Recall that $0$ also represents $\emptyset$ or $undef$.}
\[ \exists Z . (D_g(j,\bar{u},t, Z) \wedge t \neq 0) \vee (t = 0 \wedge \neg \exists z . D_g(j, \bar{u}, z, Z)) .\]
This defines the formula $\phi$ as desired.\qed

\end{proof}

The theorem actually shows that there is a sentence $\varphi$ defined in our logic plus inflationary fixed-point which asserts that a (time-explicit) PTIME ic-ASM $\tilde{M}$ accepts the input structure $I$, i.e. there exists some $i$ and some $Z$ such such $D_f(i,\textbf{true},Z)$ holds, where $f$ is \textit{Output\/} and \textit{Halt\/}.

\subsection{Active Objects}

In analogy to \cite[Thm.19]{blass:apal1999} we can extend fixed-point definability to transitive structures $T$ that subsume $\textit{Active\/}(I)$. For this we just have to show fixed-point definability of $\textit{Active\/}(I)$ over $\textit{HF\/}(I)$, where $HF(I)$ denotes the structure $(HF(I),K,\bar{R})$ plus background structure.

\begin{theorem}[Second Fixed-Point Theorem]\label{thm-active}

Consider input structures $I$ such that $\tilde{M}$ halts on runs starting in the initial state $State(I)$ generated by $I$. Then $\textit{Active\/}(I)$ can be uniformly (i.e. independent of $I$) defined by an inflationary fixed-point formula over $\textit{HF\/}(I)$.

\end{theorem}

\begin{proof}

Consider the formula (where $n_f$ is the arity of $f \in \Upsilon_{dyn}$)
\begin{align*}
\textit{critical\/}(x) \equiv &\; x \in \;\textit{Atoms\/}\;  \vee x \in \{ 0, 1 \} \vee \\
& \bigvee_{f \in \Upsilon_{dyn}} \exists i, x_0, \dots, x_{n_f}, Z . ( D_f(i, (x_1, \dots, x_{n_f}), x_0, Z) \wedge \\
& \; ( x = x_0 \vee\dots\vee x = x_{n_f} ) \wedge
\forall j, Z^\prime . ( j \in i \rightarrow \neg D_{\textit{Halt\/}}(j, \textbf{true}, Z^\prime) ) ) ,
\end{align*}
which expresses that $x$ is critical. Furthermore,
\[ \textit{transitive\/}(x) \equiv \forall y, z . (y \in x \wedge z \in y \rightarrow z \in x) \]
expresses that $x$ is transitive. Hence, we can define $\textit{Active\/}(I)$ by the formula
\[ x \in \;\textit{Active\/}(I)\; \leftrightarrow \forall y . (\textit{transitive\/}(y) \wedge \forall z . ( \textit{critical\/}(z) \rightarrow z \in y ) \rightarrow x \in y ) . \]

That is, $x$ is active if and only if it is a member of every transitive set containing all critical elements. If $x$ is in each such transitive set, then in particular $x \in TC(y)$ for some critical $y$, so $x$ is active. Conversely, for active $x$ there exists a critical $y$ with $x \in TC(y)$, and further, $x$ must be an element of   all transitive sets containing all critical elements, as these contain $TC(y)$ as subset.

As $D_f$ has been defined by an inflationary fixed-point formula, so is $\textit{Active\/}(I)$.\qed

\end{proof}

Note that we formulate the first fixed-point theorem for the structure $Active(I)$ instead of $HF(I)$, because we want to emphasise that only the active objects are decisive for deciding, if an input structure $I$ is accepted or not. The second fixed-point theorem shows that we could use any transitive substructure of $HF(I)$, as long as it contains $Active(I)$, i.e. we have characterised PTIME problems by a fixed-point formula that must hold in one or equivalently all transitive substructures of $HF(I)$ that contain all active objects. This will be exploited in Section \ref{sec:separation}.

\subsection{Active Orbits}

Isomorphisms are defined as permutations of the set of atoms that are extended to sets using $\theta(x) = \{ \theta(y) \mid y \in x \}$. Let $Aut(I)$ denote the automorphism group of $\text{State}(I)$, and let $Sym(I)$ denote the permutation group of the set of atoms of $State(I)$. Different to CPT there is more than one run with the initial state generated by $I$, and we have to take all these runs into account. For this we exploit {\em orbits} $x = Gy = \{ g(y) \mid g \in G \} \subseteq \textit{Active}(I)$ defined by an object $y$ and a subgroup $G$ of $Sym(I)$ such that $G$ commutes with each $\theta \in Aut(I)$ (see Corollary \ref{cor-layer}).

\paragraph*{Remark}

We have seen that active objects are decisive for the decision, if an input structure will be accepted by a PTIME icASM or not. In the work on CPT it was shown that active objects have a support with a size bounded by some constant $k$, and then all objects with support bounded by $k$ can be constructed out of the support. This will hardly work for ICPT, as the presence of choice---even though it is insignificant for the final result---enables longer runs lowering the chances to obtain such a bound for the support of all active objects. For instance, in the Parity Example \ref{bsp-parity} all subsets of the set of atoms are active objects, and a support is either the set itself or its complement, but for the corresponding orbits $\emptyset$ is a support.

However, active objects other than atoms must appear in some update set $\Delta$. Thus, if we have $((f,\bar{x}),y) \in \Delta \in \boldsymbol{\Delta}(S)$ for some state $S$ and $\Delta^\prime$ is another update set on the same layer, then there exists an isomorphism $\sigma \in Sym(I)$ with $((f,\sigma \bar{x}), \sigma y) \in \Delta^\prime$. Then it seems natural to collect all these isomorphic images of the active objects $\bar{x}$ and $y$. This defines an {\em orbit} as a subset $x$ of $Active(I)$ such that any two elements of $x$ are mapped to each other by an isomorphism in $Sym(I)$. If $x$ is such an orbit, then there exists an object $y$ such that $x = Gy$, where $G \subseteq Sym(I)$ is a group of isomorphisms. Then we call $y$ a {\em representative}\footnote{Note that any $y \in x$ can be used as a representative of the orbit.} of the orbit $x$, and $G$ its {\em generator}. By abuse of terminology we identify the pair $(y,G)$ with the orbit $x = Gy$.

With this we can think of the runs with initial state $State(I)$ as a computation tree, in which orbits connect objects in different branches of the tree, but with the same ``distance'' from the initial state. By looking at such orbits we will see that it is still possible to preserve and generalise the approach taken for CPT \cite{blass:apal1999}: not the active objects, but the active orbits will have a bounded support. This will allow us to construct the orbits out of the bounded support and to prove a separation theorem for structures.

Furthermore, if $\pi$ is an automorphism of the input structure $I$, then for any run with this input structure we obtain a run, in which $\pi$ is applied to every state. In particular, if we have update sets $\Delta, \sigma \Delta$ on the same layer, then we also have that $\pi \Delta, \pi \sigma \Delta$ are update sets on the same layer, and $\pi \sigma \pi^{-1}$ is the isomorphism mapping $\pi \Delta$ to $\pi \sigma \Delta$. This implies $G \pi = \pi G$, i.e. the commutativity request for orbits (see Corollary \ref{cor-layer}). The same applies to any subgroup $H \subseteq G$.

\begin{definition}\label{def-activeorbit}\rm

A {\em critical orbit} of a PTIME ic-ASM $\tilde{M} = (M, p(n), q(n))$ for an input structure $I$ is an orbit $x = Gy$ such that the representative $y$ is a critical object in some state $S_i$ in a run $S_0, S_1, \dots$ of $M$ on input structure $I$ and $G$ is the group of isomorphisms for the $i$'th layer of $M$.

If $x = Gy$ is a critical orbit, then every orbit $Gz$ with $z \in TC(y)$ is called an {\em active orbit}.

\end{definition}

The second part of this definition defines an active orbit as an orbit with generator $G$ and a representative $z$ in the transitive closure of a representative $y$ of a critical orbit with the same generator. This is analogous to defining active objects as elements of the transitive closure of a critical object (see Definition \ref{def-active}). However, orbits need not be transitive.

Note that an object may appear in different active orbits. Let $\mathcal{A}[I]$ denote the set of active orbits of $\tilde{M}$ for the input structure $I$. We call a substructure $J$ of $\textit{HF\/}(I)$ {\em semi-transitive} iff there is a transitive substructure $J^\prime$ such that $J$ contains all orbits $Gy$ with $y \in J^\prime$.

\begin{theorem}[Third Fixed-Point Theorem]\label{thm-orbit}

Consider input structures $I$ such that $\tilde{M}$ halts on runs starting in an initial state generated by $I$. Then $\mathcal{A}[I]$ can be uniformly defined by an inflationary fixed-point formula over $\textit{HF\/}(I)$.

\end{theorem}

\begin{proof}

According to Definition \ref{def-activeorbit} we should define an active orbit as an orbit with a representative $z$ and a generator $G$ such that $z$ is in the transitive closure of some $y$ such that $Gy$ is a critical orbit. We can first define an orbit using the formula
\[ \textit{orbit\/}(x) \equiv x \subseteq \textit{Active}(I) \wedge \exists y . \textit{represents\/}(y,x) \wedge \forall z . (z \in x \rightarrow \textit{represents\/}(z,x)) \]
using
\[ \textit{represents\/}(y,x) \equiv y \in x \wedge \forall z . (z \in x \rightarrow \exists \Phi . iso(\Phi) \wedge \Phi(y,z)) \; . \]
That is, we exploit that all objects in an orbit can be mapped to each other by some isomorphism, which implies that a generator $G$ exists, but is left implicit\footnote{Note that it is not possible to create an object $G$ in our logic, as this would be a set of isomorphisms contradicting the fact that the logic is only second-order.}.

Then according to Definition \ref{def-activeorbit} a critical orbit is easily defined as an orbit with a representative that is a critical object, for which we can exploit $\textit{critical\/}(x)$ as defined in the proof of Theorem \ref{thm-active}.
\begin{align*}
\textit{critical-orbit\/}(x) \equiv \textit{orbit\/}(x) \wedge \exists y .& (\textit{critical\/}(y) \wedge \textit{represents\/}(y,x) \\
&\wedge \forall z, \Phi . (\textit{iso-crit\/}(y,z,\Phi) \rightarrow z \in x )
\end{align*}
with
\begin{align*}
\textit{iso-crit\/}&(x,y,\Phi) \equiv iso(\Phi) \wedge \\
&\bigvee_{f \in \Upsilon_{dyn}} \exists i, x_0, \dots, x_{n_f}, Z_1, y_0, \dots, y_{n_f}, Z_2 . \\
& ( D_f(i,(x_1,\dots,x_{n_f}),x_0,Z_1) \wedge ( x = x_0 \vee\dots\vee x = x_{n_f} ) \wedge \\
& D_f(i,(y_1,\dots,y_{n_f}),y_0,Z_2) \wedge ( y = y_0 \vee\dots\vee y = y_{n_f} ) \wedge
\bigwedge_{0 \le j \le n_f} \Phi(x_j, y_j) )
\end{align*}

We can define an active orbit $x$ as an orbit with a representative $v$ in the transitive closure of a representative $u$ of a critical orbit $y$ with the additional requirement that both $x$ and $y$ must have the same generator.
\begin{align*}
\textit{active-orbit\/}(x) \; \equiv & \; x \subseteq \textit{Active}(I) \wedge \exists y . \textit{critical-orbit\/}(y) \wedge \\
&\exists u,v . \textit{represents\/}(u,y) \wedge \textit{represents\/}(v,x) \wedge \\
&\qquad\qquad\qquad v \in TC(u) \wedge \textit{same\_generator\/}(x,y)
\end{align*}
using
\[ x^\prime \in TC(z) \; \leftrightarrow \; \forall z^\prime . \textit{transitive\/}(z^\prime) \wedge z \subseteq z^\prime \rightarrow x^\prime \in z^\prime \; . \]

So it remains to define $\textit{same\_generator\/}(x,y)$. Two orbits $y$ and $x$ have the same generator, if for their representatives $u,v$ each isomorphism $\sigma$ satisfies $\sigma(u) \in y$ iff $\sigma(v) \in x$,
which is given by the formula
\begin{align*}
\textit{same\_generator\/}(x,y) \; & \equiv \; \forall u,v. ( \textit{represents\/}(u,y) \wedge \textit{represents\/}(v,x) \rightarrow \\
\forall \Phi . iso(\Phi) & \rightarrow
\forall z . \exists z^\prime . (z \in y \wedge \Phi(u,z) \rightarrow z^\prime \in x \wedge \Phi(v,z^\prime))
\wedge \\
& \qquad\qquad \forall z^\prime . \exists z . (z^\prime \in x \wedge \Phi(v,z^\prime) \rightarrow z \in y \wedge \Phi(u,z)) ) \qquad\quad
\end{align*}\qed

\end{proof}

Then the following corollary summarises the discussion in this subsection.

\begin{corollary}\label{cor-fixpoint}

Let $I$ be an input structure for a (time-explicit) PTIME ic-ASM $\tilde{M}$. There exists a formula $\varphi$ in the fixed-point logic {\rm IFP[$\mathcal{L}^{nd}$]} that asserts that $\tilde{M}$ accepts $I$, which is the case iff $\varphi$ holds in some or equivalently all semi-transitive substructures of $\textit{HF\/}(I)$ containing all active orbits in $\mathcal{A}[I]$.

\end{corollary}

\begin{proof}

By the first fixed-point Theorem \ref{thm-fixpoint} there exists an IFP[$\mathcal{L}^{nd}$] sentence $\varphi$ that asserts that $\tilde{M}$ accepts $I$. The sentence asserts that there is some positive integer $i$ such that $D_f(i,\textbf{true})$ holds in $\textit{Active\/}(I)$, where $f$ is \textit{Output\/} or \textit{Halt\/}. Using the third fixed-point Theorem \ref{thm-orbit} $\tilde{M}$ accepts $I$ iff $\varphi$ is true in some or equivalently all semi-transitive substructures of $\textit{HF\/}(I)$ containing all active orbits in $\mathcal{A}[I]$.\hspace*{\fill}\qed

\end{proof}

\section{Semi-Transitive Structures}\label{sec:structures}

The primary goal of this and the the next two sections is to show that SAT, i.e. the satifiability problem for a set of propositional clauses, is not in ICPT, but our method will allow us to establish further restrictions to ICPT. We will follow the argumentation path of \cite[Sect.8/9]{blass:apal1999} with a few generalisations that are necessary to capture the extension by insignificant choice.

In a nutshell, we need to show that there is no fixed-point formula over the insignificant choice fragment of the logic of non-deterministic ASMs separating the satisfiable from the non-satisfiable structures. According to the results of the preceding section summarised in Corollary \ref{cor-fixpoint} it suffices to consider semi-transitive substructures of $\textit{HF\/}(I)$ containing all objects of all active orbits in $\mathcal{A}[I]$. However, the active orbits depend on the icASM and thus indirectly on the fixed-point formula. This problem will be solved in this section. We first show a support theorem for the active orbits, which allows us to consider those semi-transitive substructures of $\textit{HF\/}(I)$ that contain the orbits with supports bounded by a constant $k$. Analogous to \cite[Sect.9]{blass:apal1999} we will show that objects can be constructed out of a support using generalised molecules and forms.

\subsection{A Support Theorem for ICPT}

Consider a PTIME ic-ASM $\tilde{M} = (M, p(n), q(n))$. Let $I$ be an input structure for $\tilde{M}$ and $\text{State}(I)$ be the initial state generated by $I$. Let $\bar{R}$ denote the set of input relations of $I$. Recall that the base set of every state contains all hereditarily finite sets built over the atoms. We also use $I$ to denote the set of atoms in the base set of the structure.

Isomorphisms are defined as permutations of the set of atoms that are extended to sets using $\theta(x) = \{ \theta(y) \mid y \in x \}$. By means of the Kuratowski representation of ordered pairs as sets, i.e. $(x,y) = \{ \{ x \} , \{ x,y \} \}$, extended to $n$-tuples using $(x_1, \dots, x_n) = (x_1, (x_2, \dots, x_n))$, we extend permutations also to tuples and thus to the input relations and update sets. If $\theta$ maps the input relations $R_i$ of $I$ onto themselves, we obtain an {\em automorphism} of $\text{State}(I)$. Let $Aut(I)$ denote the automorphism group of $\text{State}(I)$. Note that for every automorphism $\theta \in Aut(I)$ we have $\theta(c_f) = c_f$ for the special constants $c_f$ with $f \in \Upsilon_{dyn}$.

\begin{definition}\label{def-support}\rm

A set $X$ of atoms of $I$ is called a {\em support} of an object $y$ iff every automorphism of $\text{State}(I)$ that pointwise fixes $X$ also fixes $y$. A {\em support} of an orbit $(y,G)$ is a support of $G(y) = \{ \sigma(y) \mid \sigma \in G \}$.

\end{definition}

Let $\textit{Active\/}(I)$ denote the set of active objects in a run $S_0, S_1, \dots$, where the initial state $S_0$ is defined by $I$. Clearly, Definition \ref{def-active} implies that $\textit{Active\/}(I)$ is transitive and closed under $Aut(I)$. Clearly, if $y$ is active, then there exists an active orbit $(y,G)$ with $y \in G(y)$. The set of active orbits $\mathcal{A}[I]$ is also closed under $Aut(I)$. Our aim is to generalise the support theorem for CPT (see \cite[Thm.24 \& Cor.33]{blass:apal1999}) to ICPT, i.e. to show that every active orbit in $\mathcal{A}[I]$ has a support bounded by a fixed positive integer $k$.

For the sake of generality we assume that the unary relations in $\bar{R}$ define a partition of $I$; we refer to all sets in the partition as {\em colours}. In the following let $C$ denote the set of colours. For a real number $\varepsilon > 0$, we call $C$ {\em $\varepsilon$-level} iff $| c | > \varepsilon \cdot n$ holds for every colour $c \in C$ and $n = | I |$. Then each $\theta \in Aut(I)$ preserves the colours.

We will next exploit a sequence of lemmata similar to those that have been proven in \cite[Sect.8]{blass:apal1999} for the case of CPT with input structures over an empty signature, i.e. naked sets, and for an extension to coloured sets. We assume that our set $C$ of colours is $\varepsilon$-level for some $\varepsilon > 0$. The first lemma is a purely combinatorical lemma on so-called $\Delta$-systems. A {\em $\Delta$-system} is a collection $K$ of sets such that all pairs of sets $X, Y \in K$ with $X \neq Y$ have the same intersection $X \cap Y$. The second lemma allows us to minimize supports (see also \cite[Lemma 26]{blass:apal1999}).

\begin{lemma}[{\cite[Lemma 25]{blass:apal1999}}]\label{lem-delta}
Every family $\{ X_j \}_{j \in J}$ of sets with $| X_j | \le \ell$ for all $j \in J$ and $| J | \ge \ell ! p^{\ell+1}$ contains a $\Delta$-system $K$ with $| K | = p$.
\end{lemma}

\begin{lemma}\label{lem-support1}

Let $X_1$ and $X_2$ support $(y,G) \in \mathcal{A}[I]$ with $(I - (X_1 \cup X_2)) \cap c \neq \emptyset$ for all colours $c \in C$. Then also $X_1 \cap X_2$ is a support of $(y,G)$.

\end{lemma}

\begin{proof}

For each $c \in C$ fix an atom $a_c \in I - (X_1 \cup X_2)$, and let $b_c$ range over atoms in $( I - (X_1 \cap X_2) ) \cap c$. Let $\pi_{b_c}$ be a transposition swapping $a_c$ and $b_c$, so it is an automorphism of $I$. We have $b_c \notin X_1$ or $b_c \notin X_2$. In the former case $\pi_{b_c}$ pointwise fixes $X_1$, in the latter case it pointwise fixes $X_2$. As $X_1$ and $X_2$ both support $G(y)$, we derive $\pi_{b_c}(G(y)) = G(y)$ in both cases. Transpositions generate all permutations, and consequently all these transpositions $\pi_{b_c}$ generate all automorphisms of $I$ that pointwise fix $X_1 \cap X_2$. Therefore, all these automorphisms fix $G(y)$, and thus $X_1 \cap X_2$ supports $(y,G)$.\qed

\end{proof}

For an active orbit $(y,G) \in \mathcal{A}[I]$ with a support $X$ such that $|X \cap c | < |c|/2$ holds for all colours $c \in C$. Lemma \ref{lem-support1} justifies to define
\[ \text{Supp}(y,G) = \bigcap \{ X \mid X \;\text{supports}\; (y,G) \;\text{and}\; |X \cap c | < |c|/2 \;\text{for all}\; c \in C \} , \]
which gives the smallest support of $(y,G)$.

Let $n = | I |$. As $\tilde{M}$ is a PTIME ic-ASM, we have $| \mathcal{A}[I] | \le n^{k^\prime}$ for some positive integer $k^\prime$. Consider only input structures $I$, for which $n$ is so large that $\dbinom{\lceil \varepsilon n \rceil}{k^\prime + 1} > n^{k^\prime}$ holds. In the following let $k = k^\prime \cdot | C |$. This leads to the next lemma (see also \cite[Lemma 27]{blass:apal1999}).

\begin{lemma}\label{lem-support2}

If $(y,G) \in \mathcal{A}[I]$ has a support $X$ with $|X \cap c | < |c|/2$ for all colours $c \in C$, then $| \text{Supp}(y,G) \cap c | \le k^\prime$ and $| \text{Supp}(y,G) | \le k$.

\end{lemma}

\begin{proof}

Let $Q = G(y)$. For an automorphism $\theta$ with $\theta(Q) = Q^\prime$ we also have $\theta(\text{Supp}(Q)) = \text{Supp}(Q^\prime)$ and $\theta(\text{Supp}(Q) \cap c) = \text{Supp}(Q^\prime) \cap c$ for every colour $c \in C$. Let $s_c = | \text{Supp}(Q) \cap c |$ and assume $s_c > k^\prime$. This implies the contradiction
\begin{gather*}
n^{k^\prime} \ge | \mathcal{A}[I] |
\ge | \{ \theta(Q) \cap c \mid \theta \in Aut(I) \} | \\
\ge | \{ \theta(\text{Supp}(Q) \cap c) \mid \theta \in Aut(I) \} |
= \dbinom{\lceil \varepsilon n \rceil}{ s_c }
\ge \dbinom{\lceil \varepsilon n \rceil}{k^\prime + 1} > n^{k^\prime} .
\end{gather*}
Hence $s_c \le k^\prime$ and further $| \text{Supp}(Q) | \le | C | \cdot k^\prime = k$ holds.\qed

\end{proof}

To reach our claim it only remains to show that the prerequisite in Lemma \ref{lem-support2} is always satisfied. This will be done by the next lemma (see also \cite[Lemma 28]{blass:apal1999}).

\begin{lemma}\label{lem-support3}

If $n = | I |$ is sufficiently large, then every active orbit $(y,G) \in \mathcal{A}[I]$ has a support $X$ with $|X \cap c | < |c|/2$ for all colours $c \in C$.

\end{lemma}

Note that in the following proof the arguments are the same as in the proof of \cite[Lemma 28]{blass:apal1999} except for claim I.

\begin{proof}

Let $k$ and $k^\prime$ be as above, let $n^\prime = \min \{ | c | \mid c \in C \}$ and take $m = \lfloor n^\prime / 4 k^\prime \rfloor$. Assume that there is an orbit $(x,G)$ with no support $X$ with $|X \cap c | < |c|/2$ for all colours $c \in C$. We choose such an orbit such that $x$ has minimal rank. Then $x$ must be a set. Otherwise if $x$ were an atom, $G(x)$ would be a set of atoms with support $\{ x \}$.

\paragraph*{Claim I}

There exists a sequence of quintuples $(\theta_j, y_j, z_j, Y_j, Z_j)$ ($1 \le j \le m$) satisfying the following conditions:

\begin{itemize}

\item $\theta_j \in Aut(I)$ is an automorphism, $Y_j = \text{Supp}(y_j,G)$, $Z_j = \text{Supp}(z_j,G)$;

\item $y_j \in x$ and $z_j \notin x$;

\item $\theta_j(y_j) = z_j$, and $\theta_j(Y_j) = Z_j$;

\item $\theta_j$ pointwise fixes $Y_i \cup Z_i$ for all $i < j$.

\end{itemize}

\paragraph*{Proof of the claim}

We construct the sequence by induction on $j$. For $j = 1$ there exists an automorphism $\theta_1$ with $\theta_1(x) \neq x$---otherwise $\emptyset$ would be a support of $G(x)$, as every automorphism $\theta$ would satisfy $\theta(x) = x$ and hence also $\theta(\sigma(x)) = \sigma^\prime(\theta(x)) =\sigma^\prime(x) \in G(x)$ for all $\sigma \in G$ and $\sigma^\prime = \theta \sigma \theta^{-1}$. Then there exists an $y_1 \in x$ such that $z_1 = \theta_1(y_1) \notin x$. With $Y_1 = \text{Supp}(y_1,G)$ and $Z_1 = \text{Supp}(z_1,G)$ we get $\theta_1(Y_1) = \theta_1(\text{Supp}(G(y_1))) = \text{Supp}(\theta_1(G(y_1))) = \text{Supp}(G(z_1)) = Z_1$ and all required conditions are satisfied.

Next suppose that $(\theta_i, y_i, z_i, Y_i, Z_i)$ ($1 \le i < j$) satisfying all the conditions of the claim has been constructed. As $x$ has minimal rank and $y_i \in x$ holds, the support $Y_i$ of $(y_i,G)$ satisfies $|Y_i \cap c | < |c|/2$ for all colours $c \in C$. As $z_i$ and $Z_i$ are automorphic images, the same holds for $Z_i$. In Lemma \ref{lem-support2} we showed $| Y_i \cap c | \le k^\prime$, hence also $| Z_i \cap c | \le k^\prime$.

Define $X_j = \bigcup_{i < j} (Y_i \cup Z_i)$. Then
\[ | X_j \cap c | \le (j-1) \cdot 2 \cdot k^\prime < m \cdot 2 \cdot k^\prime \le \frac{n^\prime}{4 k^\prime} \cdot 2 \cdot k^\prime = \frac{n^\prime}{2} \le \frac{| c |}{2} \]
for all $c \in C$.

Hence there must exist an automorphism $\theta_j$ that pointwise fixes $X_j$ with $\theta_j(x) \neq x$---otherwise $X_j$ would be a support for $G(x)$ with $|X_j \cap c | < |c|/2$ for all colours $c \in C$ contradicting our assumption above. Then there exists an $y_j \in x$ such that $z_j = \theta_j(y_j) \notin x$. With $Y_j = \text{Supp}(y_j,G)$ and $Z_j = \text{Supp}(z_j,G)$ we get $\theta(Y_j) = Z_j$ as above. Hence $(\theta_j, y_j, z_j, Y_j, Z_j)$ satisfies the conditions above, which proves the claim.

For a given value of $n$ let $p$ be the largest integer with $(2k)! \cdot p^{2k+1} \le m$. For increasing values of $n$ both $m$ and $p$ increase, but $k$ remains fixed. Therefore, for sufficiently large $n$ we
have
\[ n^k < ((m+1) \cdot 4 k^\prime)^k \le ( (2k)! p^{2k+1} \cdot 4 k^\prime )^k < 2^{p-1} \; , \]
so we can also ensure $2^{p-1} > n^k$.

\paragraph*{Claim II}

There exists a sequence of quintuples $(\theta_j, y_j, z_j, Y_j, Z_j)$ ($1 \le j \le p$) satisfying the conditions from the previous claim such that the sets $Y_i \cup Z_i$ form a $\Delta$-system.

\paragraph*{Proof of the claim}

Let $(\theta_j, y_j, z_j, Y_j, Z_j)$ ($1 \le j \le m$) be the sequence guaranteed by claim I. According to Lemma \ref{lem-support2} we have $| Y_i | \le k$. As $Z_i$ is an automorphic image, we also get $| Z_i | \le k$ and thus $| Y_i \cup Z_i | \le 2k$. As we have $(2k)! \cdot p^{2k+1} \le m$, we can apply Lemma \ref{lem-delta} with $\ell = 2k$ to obtain a subsequence of length $p$, in which the sets $Y_i \cup Z_i$ form a $\Delta$-system. This proves the claim.

Now fix a sequence $(\theta_j, y_j, z_j, Y_j, Z_j)$ ($1 \le j \le p$) as in claim II, and define $X_0 = (Y_i \cup Z_i) \cap (Y_j \cup Z_j)$ with $1 \le i \neq j \le p$. As we have a $\Delta$-system, $X_0$ is uniquely determined independent of the choice of $i \neq j$. Let $U = \{ 2, \dots, p \}$. Then for any $i \in U$ $\theta_i$ pointwise fixes $Y_1 \cup Z_1$ and hence pointwise fixes also $X_0$.

\paragraph*{Claim III}

For each $V \subseteq U$ there exists an automorphism $\theta_V$ such that $z_i = \theta_V(z_i)$ for $i \in V$ and $z_i = \theta_V(y_i)$ for $i \in U - V$.

\paragraph*{Proof of the claim}

We construct a permutation $\pi$ of atoms as follows. For $a \in X_0$ or $a \in Y_i \cup Z_i$ for some $i \in V$ let $\pi(a) = a$. For $a \in Y_i - X_0$ let $\pi(a) = \theta_i(a)$. Then $\pi$ extends to an automorphism, which we denote as $\theta_V$. Due to this construction $\pi$ pointwise fixes $Z_i = \text{Supp}(z_i,G)$ for $i \in V$, which implies $\pi(z_i) = z_i$ and hence $\theta_V(z_i) = z_i$ for $i \in V$.

Furthermore, $\theta_V$ and $\theta_i$ coincide on $Y_i = \text{Supp}(y_i,G)$ for $i \notin V$, which implies $\theta_V^{-1} (\theta_i(y_i)) = y_i$. Hence $\theta_V(y_i) = \theta_i(y_i) = z_i$, which proves the claim.

Finally, fix the automorphisms $\theta_V$ in claim III for all $V \subseteq U$.

\paragraph*{Claim IV}

Let $V,W \subseteq U$ with $V \neq W$. Then $\theta_V(x) \neq \theta_W(x)$ and $\theta_V(G(x)) \neq \theta_W(G(x))$.

\paragraph*{Proof of the claim}

Without loss of generality let $V - W \neq \emptyset$, then take any $i \in V - W$. Claim III implies $\theta_V(z_i) = z_i$. As $z_i \notin x$, we have $z_i = \theta_V(z_i) \notin \theta_V(x)$. Claim III further implies $\theta_W(y_i) = z_i$. As $y_i \in x$, we have $z_i = \theta_W(y_i) \in \theta_W(x)$, which completes the proof of the claim.

Due to claim IV there are $2^{p-1}$ different automorphic images of $G(x)$. This implies the contradiction
\[ | \mathcal{A}[I] | \ge 2^{p-1} > n^k \ge | \mathcal{A}[I] | \; , \]
which completes the proof of the lemma.\qed

\end{proof}

With Lemmata \ref{lem-support2} and \ref{lem-support3} we get a positive integer $k$ such that every active orbit $(y,G) \in \mathcal{A}[I]$ has support $\text{Supp}(y,G)$ of size $| \text{Supp}(y,G) | \le k$. This completes the proof of the support theorem.

\begin{theorem}[Support Theorem]\label{thm-support}
There exists a positive integer $k$ such that for sufficiently large $I$ and $\epsilon$-level colours every active orbit $(y,G) \in \mathcal{A}[I]$ has a support of cardinality at most $k$.

\end{theorem}

Note that the input relations did not enter the proofs in this subsection. We obtain the bound for the support of orbits from the fact that the runs are PTIME bounded, and PTIME runs are defined in terms of active objects. How the active objects are built is not important for this argumentation.

\subsection{Skew-Symmetric Objects}

As in the previous subsection let $C$ be the set of colours, and assume that $C$ is $\varepsilon$-level for some $\varepsilon > 0$. Given a positive integer $k$ we call an object $x \in \textit{HF\/}(I)$ {\em $k$-skew-symmetric} iff there exists an orbit $(y,G)$ with $x = Gy$ and transitive $y$ such that for every object $z \in TC(y)$ the orbit $(z,G)$ has a support $\le k$.

In the following let $\tilde{I}_k$ denote the set of $k$-skew-symmetric objects in $\textit{HF\/}(I)$, and let $\bar{I}_k$ denote the set of all transitive $y \in \textit{HF\/}(I)$ such that $Gy \in \tilde{I}_k$.

According to \cite[Sect.9]{blass:apal1999} an object is called {\em $k$-symmetric} iff every $z \in TC(x)$ has a support $\le k$. Clearly, if $x$ is a $k$-symmetric set, it is also $k$-skew-symmetric. Thus, our definition extends the corresponding one in the work on CPT.

The main result of this subsection will be that every $x \in \tilde{I}_k$ can be constructed out of its support, which will be represented by an ordered sequence of $k$ distinct atoms called {\em $k$-molecule}, by means of a so-called {\em $k$-form}. For this we adapt again the work in \cite{blass:apal1999}. This will be the basis for a separation theorem in Section \ref{sec:separation}, which characterises when classes of structures  over $\bar{I}_k$ and $\bar{J}_k$ are $\mathcal{L}^{ic,m}_{\infty\omega}$-inseparable.

\begin{definition}\rm

A {\em $k$-molecule} is an injective mapping $\sigma: k \rightarrow I$, i.e. a sequence of $k$ distinct atoms.

\end{definition}

Now let $\bar{\sigma} = (\sigma_0, \dots, \sigma_{\ell-1})$ be a finite sequence of $k$-molecules of length $\ell$. The {\em configuration} $\textit{conf\/}(\bar{\sigma})$ of $\bar{\sigma}$ is a pair $(\sim_{\bar{\sigma}}, col_{\bar{\sigma}})$, where

\begin{itemize}

\item $\sim_{\bar{\sigma}}$ is an equivalence relation on $\ell \times k$ defined by
\[ (i,p)\; \sim_{\bar{\sigma}} \; (j,q) \;\Leftrightarrow\; \sigma_i(p) = \sigma_j(q) \; , \]

\item $col_{\bar{\sigma}}$ is a function $\ell \times k \rightarrow C$ with
\[ col_{\bar{\sigma}}(i,p) = c \;\Leftrightarrow\; \sigma_i(p) \in c \; . \]

\end{itemize}

A configuration describes how the $k$-molecules in the sequence $\bar{\sigma}$ overlap. We see that $\textit{conf\/}(\bar{\sigma})$ is uniquely determined by the configurations $\textit{conf\/}(\sigma_i, \sigma_j)$ for $i \neq j$. We now define a more abstract notion of configuration.

\begin{definition}\rm

For $\ell \in \mathbb{N}$, $\ell \neq 0$ an {\em abstract $\ell$-configuration} is a pair $(\sim,col)$, where $\sim$ is an eqivalence relation on $\ell \times k$ satisfying $(i,p) \sim (i,q) \Leftrightarrow p = q$, and $col: \ell \times k \rightarrow C$ is a function such that $(i,p) \sim (j,q) \Rightarrow col(i,p) = col(j,q)$.

\end{definition}

Clearly, every configuration $\textit{conf\/}(\bar{\sigma})$ is an abstract $\ell$-configuration. Conversely, given an abstract $\ell$-configuration $(\sim, col)$, choose a different atom $x_{(i,p)} \in c$ for the equivalence class $[(i,p)]_{\sim}$ with $c = col(i,p)$. Then using $\sigma_i(p) = x_{(i,p)}$ we define a configuration $\bar{\sigma} = (\sigma_0, \dots, \sigma_{\ell-1})$ that realises the abstract $\ell$-configuration.

\begin{definition}\rm

The set of {\em $k$-forms} is the smallest set $\mathcal{F}$ with

\begin{itemize}

\item $\{ c_0, \dots, c_{k-1} \} \subseteq \mathcal{F}$, where the $c_p$ are new symbols,

\item whenever $\varphi_1, \dots, \varphi_n \in \mathcal{F}$ and $E_1, \dots, E_n$ are abstract $2$-configurations, then the set of pairs $\varphi = \{ (\varphi_i, E_i) \mid 1 \le i \le n \}$ is a form in $\mathcal{F}$.

\end{itemize}

\end{definition}

Each $k$-form $\varphi \in \mathcal{F}$ has a {\em rank} $rk(\varphi)$. We have $rk(c_p) = 0$ and
\[ rk(\{ (\varphi_i, E_i) \mid 1 \le i \le n \}) = 1 + \max \{ rk(\varphi_i) \mid 1 \le i \le n \} \; . \]

We extend the definition of $k$-forms to {\em orbit-forms} $(\varphi,G,H)$, where $\varphi \in \mathcal{F}$ and $G, H \subseteq Sym(I)$ are groups of isomorphisms commuting with $Aut(I)$ with $H \subseteq G$. We keep the notation $\mathcal{F}$ for the set of all $k$-orbit-forms.

Following the idea in \cite[Sect.9.2]{blass:apal1999} a $k$-molecule $\sigma$ together with a $k$-form $\varphi \in \mathcal{F}$ define a unique object $\varphi * \sigma \in \textit{HF\/}(I)$:

\begin{itemize}

\item For $\varphi = c_p$ we have $\varphi * \sigma = \sigma(p)$;

\item For $\varphi = \{ (\varphi_i, E_i) \mid 1 \le i \le n \}$ we have
\[ \varphi * \sigma = \{ \varphi_i * \tau \mid E_i = \textit{conf\/}(\tau, \sigma) \} \; . \]

\end{itemize}

This extends to orbit-forms by $(\varphi,G,H) * \sigma = G ( \bigcup_{h \in H} \varphi * h \sigma)$. For $G = 1$ we obviously have $(\varphi,G,H) * \sigma = \varphi * \sigma$. For $\varphi = c_p$ and $H \neq 1$ we understand $\varphi * h \sigma$ as $\{ c_p * h \sigma \}$.

By taking $\varphi * h \sigma$ we use different $k$-molecules $h \sigma$, so the resulting object will contain different atoms. By building the union over $h \in H$ we enable to define larger sets. However, these are bundled into orbits by applying $G$ to them.

\begin{lemma}\label{lem-form}

For any automorphism $\pi \in Aut(I)$ we have $\pi((\varphi,G,H) * \sigma) = (\varphi,G,H) * \pi \sigma$.

\end{lemma}

\begin{proof}

As we have $\pi((\varphi,G,H) * \sigma) = \pi (G (\bigcup_{h\in H} \varphi * h \sigma)) = G (\pi (\bigcup_{h\in H} \varphi * h \sigma)) = G (\bigcup_{h\in H} \pi (\varphi * h \sigma))$ and $(\varphi,G,H) * \pi \sigma = G ( \bigcup_{h\in H} \varphi * h \pi \sigma) = G ( \bigcup_{h\in H} \varphi * \pi h \sigma)$, it suffices to consider $G = H = 1$, for which we proceed by induction over $\varphi$.

We have $\pi (c_p * \sigma) = \pi \sigma(p) = c_p * \pi \sigma$ covering the base case $\varphi = c_p$. If $\varphi = \{ (\varphi_i, E_i) \mid 1 \le i \le n \}$ is a set, we get
\begin{align*}
\pi (\varphi * \sigma) &= \pi \{ \varphi_i * \tau \mid E_i = \textit{conf\/}(\tau, \sigma) \} \\
&= \{ \pi (\varphi_i * \tau) \mid E_i = \textit{conf\/}(\tau, \sigma) \} \\
&= \{ \varphi_i * \pi \tau \mid E_i = \textit{conf\/}(\tau, \sigma) \} \qquad \text{(by induction hypothesis)} \\
&= \{ \varphi_i * \rho \mid E_i = \textit{conf\/}(\pi^{-1} \rho, \sigma) \} \qquad (\rho = \pi \tau) \\
&= \{ \varphi_i * \rho \mid E_i = \textit{conf\/}(\rho, \pi \sigma) \} \qquad \text{(to be shown)} \\
&= \varphi * \pi \sigma
\end{align*}

It remains to show that $\textit{conf\/}(\pi^{-1} \rho, \sigma) = \textit{conf\/}(\rho, \pi \sigma)$. For the equivalence relations we have
\begin{gather*}
(0,p) \sim_{(\pi^{-1} \rho, \sigma)} (1,q) \Leftrightarrow \pi^{-1} \rho (p) = \sigma(q) \Leftrightarrow \\
\rho (p) = \pi \sigma(q) \Leftrightarrow (0,p) \sim_{(\rho, \pi \sigma)} (1,q) \; ,
\end{gather*}
i.e. $\sim_{(\pi^{-1} \rho, \sigma)} = \sim_{(\rho, \pi \sigma)}$.
As automorphisms preserve colours, we further have
\[ col_{(\pi^{-1} \rho, \sigma)}(0,p) = c \Leftrightarrow \pi^{-1} \rho (p) \in c \Leftrightarrow \rho (p) \in c \Leftrightarrow col_{(\rho, \pi \sigma)} (0,p) = c \]
and
\[ col_{(\pi^{-1} \rho, \sigma)}(1,q) = c \Leftrightarrow \sigma(q) \in c \Leftrightarrow \pi \sigma (q) \in c \Leftrightarrow col_{(\rho, \pi \sigma)} (1,q) = c \; ,\]
which completes the proof.\qed

\end{proof}

\begin{corollary}\label{cor-form}

Every object $(\varphi,G,H) * \sigma$ is $k$-skew-symmetric and thus an object in $\tilde{I}_k$.

\end{corollary}

\begin{proof}

If $\pi \in Aut(I)$ pointwise fixes $range(\sigma)$, Lemma \ref{lem-form} implies
\[ \pi ((\varphi, G, H) * \sigma) = (\varphi,G,H) * \pi \sigma = (\varphi,G,H) * \sigma \; , \]
i.e. $range(\sigma)$ is a support for $(\varphi,G,H) * \sigma = G (\bigcup_{h \in H} \varphi * h \sigma)$.

As every element $z \in TC(\bigcup_{h \in H} \varphi * h \sigma)$ has the form $z = \bigcup_{h \in H} \psi * h \tau$ and $G z = (\psi,G,H) * \tau$, also $Gz$ has a support of size $\le k$.\qed

\end{proof}

Now we are ready to prove the main result of this subsection.

\begin{theorem}\label{thm-form}

Every $k$-skew-symmetric object $x = Gy \in \tilde{I}_k$ can be written in the form $x = (\varphi,G,H) * \sigma$ with a $k$-orbit-form $ (\varphi,G,H)$ and a $k$-molecule $\sigma$.

\end{theorem}

\begin{proof}

As $x = Gy$ is $k$-skew-symmetric, every orbit $(z,G)$ with $z \in TC(y)$ has a support $\le k$. We proceed by induction over $y$. If $y \in I$ is an atom, then $y = c_0 * \sigma$ with $\sigma(0) = y$, which implies (using $H = 1$)
\[ (c_0, G, H) * \sigma = G \{ c_0 * \sigma \} = G \{ \sigma(0) \} = \{ g \sigma (0) \mid g \in G \} = Gy = x \; . \]

Now let $\sigma$ be a $k$-molecule such that $range(\sigma)$ is a support for $x = Gy$. Assume that $y$ is a set. Then $Gz$ is $k$-skew-symmetric for $z \in y$, and by the induction hypothesis we have
\[ Gz = (\psi_z, G, H_z) * \tau_z = G ( \bigcup_{h \in H_z} \psi_z * h \tau_z) \; . \]

Then we define the $k$-form $\varphi = \{ ((\psi_z, H_z, H_z), \textit{conf\/}(\tau_z,\sigma)) \mid z \in y \}$. We claim that $x = (\varphi,G,1) * \sigma$ holds.

We have
\[ (\varphi,G,1) * \sigma = G(\varphi * \sigma) = G \{ (\psi_z,H_z,H_z) * \tau \mid z \in y \} \; , \]
where $\textit{conf\/}(\tau_z,\sigma) = \textit{conf\/}(\tau,\sigma)$, and
\[ x = Gy = G \Big\{ \bigcup_{h \in H_z} \psi_z * h \tau_z \mid z \in y \Big\} = G \Big\{ (\psi_z,H_z,H_z) * \tau_z \mid z \in y \Big\} \]
with $(\psi_z,H_z,H_z) * \tau_z = \bigcup_{h \in H_z} \psi_z * h \tau_z$.
Clearly, $\tau = \tau_z$ satisfies $\textit{conf\/}(\tau_z,\sigma) = \textit{conf\/}(\tau,\sigma)$, hence $x \subseteq (\varphi,G,1) * \sigma$ holds.

To show also $(\varphi,G,1) * \sigma \subseteq x$ let $\rho u \in (\varphi,G,1) * \sigma$ with $\rho \in G$ and $u = \{ (\psi_z,H_z,H_z) * \tau \mid z \in y \}$ with $\textit{conf\/}(\tau_z,\sigma) = \textit{conf\/}(\tau,\sigma)$. We construct an automorphism $\pi \in Aut(I)$ with $\pi(y) = u$, which pointwise fixes $range(\sigma)$. Then $\pi$ fixes $x$, as $range(\sigma)$ is a support for $x$. Hence $\rho u = \rho \pi (y) = \pi \rho^\prime(y)$ for some $\rho^\prime \in G$ and thus also $\rho u \in \pi (G y) = \pi(x) = x$.

It remains to construct the automorphism $\pi$ with the desired properties. For this define first $\pi_0: range(\tau_z) \cup range(\sigma) \rightarrow I$ by
\[ \pi_0(a) \; = \; \begin{cases} \tau(p) &\text{if}\; a = \tau_z(p) \\
\sigma(q) &\text{if}\; a = \sigma(q) \end{cases} \; . \]

As $\textit{conf\/}(\tau,\sigma)) = \textit{conf\/}(\tau_z,\sigma))$ holds, we get $\sim_{(\tau,\sigma)} = \sim_{(\tau_z,\sigma)}$. This implies that $\pi_0$ is {\em well defined}, as we have
\[ \tau_z(p) = \sigma(q) \Rightarrow (0,p) \sim_{(\tau_z,\sigma)} (1,q) \Rightarrow (0,p) \sim_{(\tau,\sigma)} (1,q) \Rightarrow \tau(p) = \sigma(q) \; . \]

Furthermore, we must have $col_{(\tau,\sigma)} = col_{(\tau_z,\sigma)}$, which implies that $\pi_0$ {\em preserves colours}. This is trivial for $a = \sigma(q)$. For $a = \tau_z(p)$ we have $\pi_0(a) = \tau(p)$ and thus
\[ \tau_z(p) \in c \Rightarrow col_{(\tau_z,\sigma)}(0,p) = c \Rightarrow col_{(\tau,\sigma)}(0,p) = c \Rightarrow \tau(p) \in c \; . \]

We can further show that $\pi_0$ is {\em injective}. For $\pi_0(a) = \tau(p_1) = \tau(p_2) = \pi_0(b)$ we get $p_1 = p_2$, as $\tau$ is injective and hence $a = \tau_z(p_1) = \tau_z(p_2) = b$. For $\pi_0(a) = \sigma(q_1) = \sigma(q_2) = \pi_0(b)$ we trivially have $a = \sigma(q_1) = \sigma(q_2) = b$. For $\pi_0(a) = \tau(p) = \sigma(q) = \pi_0(b)$ we have $(0,p) \sim_{(\tau,\sigma)} (1,q)$ and thus $(0,p) \sim_{(\tau_z,\sigma)} (1,q)$, which implies $a = \tau_z(p) = \sigma(q) = b$.

As $\pi_0$ is injective and colour-preserving, it extends to an automorphism $\pi \in Aut(I)$. By the definition of $\pi_0$ above $\pi$ pointwise fixes $range(\sigma)$ and $\pi \tau_z = \tau$. As $range(\sigma)$ is a support for $x$, we have $\pi(x) = x$ and hence using Lemma \ref{lem-form} we get
\begin{align*} \pi(y) &= \{ \pi(z) \mid z \in y \}
= \Big\{ \pi (\bigcup_{h \in H_z} \psi_z * h \tau_z) \mid z \in y \Big\} = \Big\{ \bigcup_{h \in H_z} \psi_z * \pi h \tau_z \mid z \in y \Big\} \\
&= \Big\{ \bigcup_{h \in H_z} \psi_z * h \pi \tau_z \mid z \in y \Big\} = \Big\{ \bigcup_{h \in H_z} \psi_z * h \tau \mid z \in y \Big\}  = u \; ,
\end{align*}
which shows our claim above and completes the proof. \qed

\end{proof}

\subsection{Relations over Forms and Configurations}

We can now express relationships between elements of $k$-skew-symmetric objects using relations over forms and abstract configurations that do not depend on the input structure. The decisive point is that the $k$-molecules needed to construct the $k$-skew-symmetric objects only enter via their configurations. The following lemma was already proven in \cite[Sect.9.3]{blass:apal1999}; it deals with $k$-skew-symmetric objects of the form $\varphi * \sigma$, so in all orbit-forms we assume a trivial group $G = 1$. Due to its importance for our generalised separation theorem in Section \ref{sec:separation} we repeat the proof here.

\begin{lemma}\label{lem-relations}

There exist ternary relations $In$, $Eq$ and $Sub$ such that for every input structure $I$ we have
\begin{align}
\psi * \tau \in \varphi * \sigma \quad &\Leftrightarrow \quad In(\psi,\varphi,\textit{conf\/}(\tau,\sigma)) \label{eq-in} \\
\psi * \tau = \varphi * \sigma \quad &\Leftrightarrow \quad Eq(\psi,\varphi,\textit{conf\/}(\tau,\sigma)) \label{eq-eq} \\
\psi * \tau \subseteq \varphi * \sigma \quad &\Leftrightarrow \quad Sub(\psi,\varphi,\textit{conf\/}(\tau,\sigma)) \label{eq-sub}
\end{align}
for all $k$-forms $\varphi, \psi$ and all $k$-molecules $\sigma, \tau$.

\end{lemma}

\begin{proof}

We explicitly define the relations $In$, $Eq$ and $Sub$ recursively. For an $n$-ary configuration $Q$ and $0 \le i,j \le n-1$ we use the notation $Q_{i,j}$ for the binary configuration resulting from projection of $Q$ to $\{ i,j \} \times k$ and re-indexing, i.e. $(0,p) \sim_{Q_{i,j}} (1,q)$ holds iff $(i,p) \sim_{Q} (j,q)$ holds, and $col_{Q_{i,j}}(0,p) = col_Q(i,p)$ and $col_{Q_{i,j}}(1,q) = col_Q(j,q)$. Now define

\begin{itemize}

\item $In(\psi,\varphi,E)$ holds iff $\varphi$ is a set and there exists a $k$-form $\chi$ and a ternary configuration $Q$ with $Q_{1,2} = E$ such that $(\chi,Q_{0,2}) \in \varphi$ and $Eq(\chi,\psi,Q_{0,1})$ hold.

\item $Eq(\psi,\varphi,E)$ holds iff either $\psi = c_p$ and $\varphi = c_q$ hold for some $p,q \in k$ with $(0,p) \sim_E (1,q)$ or $\varphi, \psi$ are sets and for all $k$-forms $\chi$ and all ternary configurations $Q$ with $Q_{1,2} = E$ we have
\begin{align*}
& (\chi,Q_{0,2}) \in \varphi \Rightarrow In(\chi,\psi,Q_{0,1}) \; \text{and}\\
& (\chi,Q_{0,1}) \in \psi \Rightarrow In(\chi,\varphi,Q_{0,2}) \; .
\end{align*}

\item $Sub(\psi,\varphi,E)$ holds iff $\varphi, \psi$ are sets and for all $k$-forms $\chi$ and all ternary configurations $Q$ with $Q_{1,2} = E$ we have
\[ (\chi,Q_{0,1}) \in \psi \Rightarrow In(\chi,\varphi,Q_{0,2}) \; . \]

\end{itemize}

We now proceed by simultaneous induction over the sum of ranks of $\psi$ and $\varphi$.

\begin{trivlist}

\item \textbf{(1)} For $\varphi = c_p$ both the left and right hand sides of (\ref{eq-in}) are false. Therefore, let $\varphi$ be a set.

Assume that $\psi * \tau \in \varphi * \sigma$ holds. Then there exists a pair $(\chi,\textit{conf\/}(\rho,\sigma)) \in \varphi$ with a $k$-form $\chi$ and a $k$-molecule $\rho$ such that $\psi * \tau = \chi * \rho$ holds. By the induction hypothesis we have $Eq(\psi,\chi,\textit{conf\/}(\tau,\rho))$. Use the ternary configuration $Q = \textit{conf\/}(\rho,\tau,\sigma)$, for which obviously $Q_{1,2} = \textit{conf\/}(\tau,\sigma)$ holds. Furthermore, $(\chi,Q_{0,2}) = (\chi,\textit{conf\/}(\rho,\sigma)) \in \varphi$, and $Eq(\chi,\psi,Q_{0,1})$ holds, because $Q_{0,1} = \textit{conf\/}(\rho,\tau)$. So by definition we infer $In(\psi,\varphi,\textit{conf\/}(\tau,\sigma))$.

Conversely, assume that $In(\psi,\varphi,\textit{conf\/}(\tau,\sigma))$ holds. Then according to our definition above there exists a $k$-form $\chi$ and a ternary configuration $Q$ with $Q_{1,2} = \textit{conf\/}(\tau,\sigma)$ such that $(\chi,Q_{0,2}) \in \varphi$ and $Eq(\chi,\psi,Q_{0,1})$ hold. By Lemma \ref{lem-conf-ext} there exists a $k$-molecule $\rho$ such that $Q = \textit{conf\/}(\rho,\tau,\sigma)$ holds. Then we have $(\chi,\textit{conf\/}(\rho,\sigma)) = (\chi,Q_{0,2}) \in \varphi$, and $Eq(\chi,\psi,\textit{conf\/}(\rho,\tau))$ because of $Q_{0,1} = \textit{conf\/}(\rho,\tau)$. By the induction hypothesis we get $\chi * \rho = \psi * \tau$ and hence $\psi * \tau \in \varphi * \sigma$.\\

\item \textbf{(2)} Both sides of (\ref{eq-eq}) are false, if one of $\varphi, \psi$ is symbol $c_p$, while the other one is a set. For the case $\varphi = c_q$ and $\psi = c_p$ we have
\[ \psi * \tau = \varphi * \sigma \Leftrightarrow \tau(p) = \sigma(q) \Leftrightarrow (0,p) \sim_{\tau,\sigma} (1,q) \Leftrightarrow Eq(\psi,\varphi,\textit{conf\/}(\tau,\sigma)) \; . \]

Thus, it remains to consider the case, where both $\varphi$ and $\psi$ are sets. First assume $\psi * \tau = \varphi * \sigma$. Let $\chi$ be an arbitrary $k$-form and $Q$ an arbitrary ternary configuration $Q$ with $Q_{1,2} = \textit{conf\/}(\tau,\sigma)$. Assume that $(\chi,Q_{0,2}) \in \varphi$ holds. By Lemma \ref{lem-conf-ext} there exists a $k$-molecule $\rho$ such that $Q = \textit{conf\/}(\rho,\tau,\sigma)$ holds. Then we get $(\chi,\textit{conf\/}(\rho,\sigma)) = (\chi,Q_{0,2}) \in \varphi$, and hence $\chi * \rho \in \varphi * \sigma = \psi * \tau$. By the induction hypothesis $In(\chi,\psi,\textit{conf\/}(\rho,\tau))$ holds, i.e. $In(\chi,\psi,Q_{0,1})$. The second implication required in our definition above follows analogously, hence $Eq(\psi,\varphi,\textit{conf\/}(\tau,\sigma))$ holds.

Conversely, assume that $Eq(\psi,\varphi,\textit{conf\/}(\tau,\sigma))$ holds. We only show $\psi * \tau \subseteq \varphi * \sigma$; the proof of the other subset-relationship is completely analogous. Let $\chi * \rho \in \psi * \tau$ for $(\chi,\textit{conf\/}(\rho,\tau) \in \psi$. Use the ternary configuration $Q = \textit{conf\/}(\rho,\tau,\sigma)$ with $Q_{1,2} = \textit{conf\/}(\tau,\sigma)$. By our definition of $Eq$ above we must have $(\chi,Q_{0,1}) \in \psi \Rightarrow In(\chi,\varphi,Q_{0,2})$. As $(\chi,Q_{0,1}) = (\chi, \textit{conf\/}(\rho,\tau)) \in \psi$, we get $In(\chi,\varphi,Q_{0,2})$. As $Q_{0,2} = \textit{conf\/}(\rho,\sigma)$ holds, we have $In(\chi,\varphi,\textit{conf\/}(\rho,\sigma))$. By the induction hypothesis this implies $\chi * \rho \in \varphi * \sigma$ as required.\\

\item \textbf{(3)} Both sides of (\ref{eq-sub}) are false, if one of $\varphi, \psi$ is a symbol $c_p$, so we can assume that both $\varphi, \psi$ are sets. Then the proof is completely analogous to \textbf{(2)}.\qed

\end{trivlist}

\end{proof}

For our purposes here we need a generalisation of Lemma \ref{lem-relations} to all objects in $\bar{I}_k$ that are not atoms. These elements take the form $g \bigcup_{h \in H} \varphi * h \sigma$, because they are members of $k$-skew-symmetric sets, which according to Theorem \ref{thm-form} can be written in the form $(\varphi,G,H) * \sigma \in \tilde{I}_k$, where $G$ is a group of isomorphisms and $H \subseteq G$ is a subgroup, both commuting with $Aut(I)$.

Lemma \ref{lem-form} shows the effect of applying an automorphism $\pi \in Aut(I)$ to an object $(\varphi,G,H) * \sigma$. This does not generalise directly to isomorphisms, as isomorphisms do not preserve colours, but this is the only relevant difference. If $C$ is the set of colours partitioning $I$ and $\phi$ is an isomorphism, then $\phi(C) = \{ \phi(c) \mid c \in C \}$ defines a different partition of $I$. We can therefore define an {\em abstract $\phi$-$\ell$-configuration} as a pair $(\sim,col)$, where $\sim$ is an eqivalence relation on $\ell \times k$ satisfying $(i,p) \sim (i,q) \Leftrightarrow p = q$, and $col: \ell \times k \rightarrow \phi(C)$ is a function such that $(i,p) \sim (j,q) \Rightarrow col(i,p) = col(j,q)$.

If $\bar{\sigma} = (\sigma_0, \dots, \sigma_{\ell-1})$ is a finite sequence of $k$-molecules of length $\ell$, then the $\phi$-$\ell$-configuration defined by $\bar{\sigma}$ is $\textit{conf\/}^\phi(\bar{\sigma}) = (\sim_{\bar{\sigma}}, col_{\bar{\sigma}})$, where

\begin{itemize}

\item $\sim_{\bar{\sigma}}$ is the equivalence relation on $\ell \times k$ defined by
\[ (i,p)\; \sim_{\bar{\sigma}} \; (j,q) \;\Leftrightarrow\; \sigma_i(p) = \sigma_j(q) \; , \]

\item $col_{\bar{\sigma}}$ is the function $\ell \times k \rightarrow \phi(C)$ with
\[ col_{\bar{\sigma}}(i,p) = \phi(c) \;\Leftrightarrow\; \sigma_i(p) \in \phi(c) \; . \]

\end{itemize}

Clearly, applying an isomorphism $\phi$ to an $\ell$-configuration $E = (\sim_E,col_E)$ yields a $\phi$-$\ell$-configuration $\phi(E) = (\sim_E, col_{\phi(E)})$, which differs only by the assignment of colours.

Furthermore, let us define objects $\varphi *^\phi \sigma$ by $\varphi *^\phi \sigma = \sigma(p)$ for $\varphi = c_p$ and $\varphi *^\phi \sigma = \{ \varphi_i * \tau \mid \phi(E_i) = \textit{conf\/}^\phi(\tau, \sigma) \}$ for $\varphi = \{ (\varphi_i, E_i) \mid 1 \le i \le n \}$. Then we get:

\begin{lemma}\label{lem-form-iso}

For every isomorphism $\phi$ we have $\phi (\varphi * \sigma) = \varphi *^\phi \phi \sigma$.

\end{lemma}

\begin{proof}

We have $\phi (c_p * \sigma) = \phi \sigma(p) = c_p *^\phi \phi \sigma$ covering the base case $\varphi = c_p$. If $\varphi = \{ (\varphi_i, E_i) \mid 1 \le i \le n \}$ is a set, we get
\begin{align*}
\phi (\varphi * \sigma) &= \phi \{ \varphi_i * \tau \mid E_i = \textit{conf\/}(\tau, \sigma) \} \\
&= \{ \phi (\varphi_i * \tau) \mid E_i = \textit{conf\/}(\tau, \sigma) \} \\
&= \{ \varphi_i *^\phi \phi \tau \mid E_i = \textit{conf\/}(\tau, \sigma) \} \qquad \text{(by induction hypothesis)} \\
&= \{ \varphi_i *^\phi \rho \mid E_i = \textit{conf\/}(\phi^{-1} \rho, \sigma) \} \qquad (\rho = \phi \tau) \\
&= \{ \varphi_i *^\phi \rho \mid \phi(E_i) = \textit{conf\/}^\phi(\rho, \phi \sigma) \} \qquad \text{(to be shown)} \\
&= \varphi *^\phi \phi \sigma
\end{align*}

It remains to show $\phi(\textit{conf\/}(\phi^{-1} \rho, \sigma)) = \textit{conf\/}^\phi(\rho, \pi \sigma)$. For the equivalence relations we have
\begin{gather*}
(0,p) \sim_{(\phi^{-1} \rho, \sigma)} (1,q) \Leftrightarrow \phi^{-1} \rho (p) = \sigma(q) \Leftrightarrow \\
\rho (p) = \phi \sigma(q) \Leftrightarrow (0,p) \sim_{(\rho, \phi \sigma)} (1,q) \; ,
\end{gather*}
i.e. $\sim_{(\phi^{-1} \rho, \sigma)} = \sim_{(\rho, \phi \sigma)}$.
Then we further have
\[ col_{(\phi^{-1} \rho, \sigma)}(0,p) = c \Leftrightarrow \phi^{-1} \rho (p) \in c \Leftrightarrow \rho (p) \in \phi(c) \Leftrightarrow col_{(\rho, \phi \sigma)} (0,p) = \phi(c) \]
and
\[ col_{(\phi^{-1} \rho, \sigma)}(1,q) = c \Leftrightarrow \sigma(q) \in c \Leftrightarrow \phi \sigma (q) \in \phi(c) \Leftrightarrow col_{(\rho, \phi \sigma)} (1,q) = \phi(c) \; ,\]
which completes the proof.\qed

\end{proof}

With this extension we can generalise Lemma \ref{lem-relations} as follows.

\begin{lemma}\label{lem-relations-ext1}

For every isomorphism $\phi$ there exist ternary relations $In^\phi$, $Eq^\phi$ and $Sub^\phi$ such that for every input structure $I$ we have
\begin{align}
\psi * \tau \in \phi(\varphi * \sigma) \quad &\Leftrightarrow \quad In^\phi(\psi,\varphi,\textit{conf\/}^\phi(\tau,\phi \sigma)) \label{eq-inphi} \\
\psi * \tau = \phi(\varphi * \sigma) \quad &\Leftrightarrow \quad Eq^\phi(\psi,\varphi,\textit{conf\/}^\phi(\tau,\phi \sigma)) \label{eq-eqphi} \\
\psi * \tau \subseteq \phi(\varphi * \sigma) \quad &\Leftrightarrow \quad Sub^\phi(\psi,\varphi,\textit{conf\/}^\phi(\tau,\phi \sigma)) \label{eq-subphi}
\end{align}
for all $k$-forms $\varphi, \psi$ and all $k$-molecules $\sigma, \tau$.

\end{lemma}

\begin{proof}

The proof is completely analogous to the proof of Lemma \ref{lem-relations}. We just define the ternary relations $In^\phi$, $Eq^\phi$ and $Sub^\phi$ explicitly:

\begin{itemize}

\item $In^\phi(\psi,\varphi,E)$ holds iff $\varphi$ is a set and there exists a $k$-form $\chi$ and a ternary configuration $Q$ with $\phi(Q_{1,2}) = E$ such that $(\chi,Q_{0,2}) \in \varphi$ and $Eq(\chi,\psi,Q_{0,1})$ hold.

\item $Eq^\phi(\psi,\varphi,E)$ holds iff either $\psi = c_p$ and $\varphi = c_q$ hold for some $p,q \in k$ with $(0,p) \sim_E (1,q)$ or $\varphi, \psi$ are sets and for all $k$-forms $\chi$ and all ternary configurations $Q$ with $\phi(Q_{1,2}) = E$ we have
\begin{align*}
& (\chi,Q_{0,2}) \in \varphi \Rightarrow In(\chi,\psi,Q_{0,1}) \; \text{and}\\
& (\chi,Q_{0,1}) \in \psi \Rightarrow In(\chi,\varphi,Q_{0,2}) \; .
\end{align*}

\item $Sub^\phi(\psi,\varphi,E)$ holds iff $\varphi, \psi$ are sets and for all $k$-forms $\chi$ and all ternary configurations $Q$ with $\phi(Q_{1,2}) = E$ we have
\[ (\chi,Q_{0,1}) \in \psi \Rightarrow In(\chi,\varphi,Q_{0,2}) \; .\]\qed

\end{itemize}

\end{proof}

Next we extend Lemma \ref{lem-relations} to elements of $k$-skew-symmetric sets.

\begin{lemma}\label{lem-relations-ext2}

We have
\begin{align*}
\bigcup_{h \in H} \psi * h \tau & \in  \bigcup_{h^\prime \in H^\prime} \varphi * h^\prime \sigma
\Leftrightarrow \\
& \exists h^\prime \in H^\prime, \psi^\prime, \tau^\prime . In(\psi^\prime, \varphi, \textit{conf\/}(\tau^\prime, h^\prime \sigma)) \wedge \\
& \forall h \in H . Sub(\psi, \psi^\prime, \textit{conf\/}(h \tau, \tau^\prime)) \wedge \\
& \forall \chi, \alpha . ( In(\chi, \psi^\prime, \textit{conf\/}(\alpha,\tau^\prime)) \rightarrow
\exists h \in H . In(\chi, \psi, \textit{conf\/}(\alpha, h \tau))) \\
\bigcup_{h \in H} \psi * h \tau & = \bigcup_{h^\prime \in H^\prime} \varphi * h^\prime \sigma
\Leftrightarrow \\
& \forall h \in H, \chi, \alpha . ( In(\chi, \psi, \textit{conf\/}(\alpha, h \tau)) \rightarrow \exists h^\prime \in H^\prime . In(\chi, \varphi, \textit{conf\/}(\alpha, h^\prime \sigma))) \wedge \\
& \forall h^\prime \in H^\prime, \chi, \alpha . ( In(\chi, \varphi, \textit{conf\/}(\alpha, h^\prime \sigma)) \rightarrow \exists h \in H . In(\chi, \psi, \textit{conf\/}(\alpha, h \tau))) \\
\bigcup_{h \in H} \psi * h \tau & \subseteq \bigcup_{h^\prime \in H^\prime} \varphi * h^\prime \sigma
\Leftrightarrow \\
& \forall h \in H, \chi, \alpha . ( In(\chi, \psi, \textit{conf\/}(\alpha, h \tau)) \rightarrow \exists h^\prime \in H^\prime . In(\chi, \varphi, \textit{conf\/}(\alpha, h^\prime \sigma)))
\end{align*}

\end{lemma}

\begin{proof}

We simply exploit that we deal with sets. Thus, $\bigcup_{h \in H} \psi * h \tau \in  \bigcup_{h^\prime \in H^\prime} \varphi * h^\prime \sigma$ holds iff there exists some $h^\prime \in H^\prime$ with $h^\prime (\varphi * h^\prime \sigma) = \bigcup_{h \in H} \psi * h \tau$. In addition, elements in $h^\prime (\varphi * h^\prime \sigma)$ have the form $\psi^\prime * \tau^\prime$, so we must have $In(\psi^\prime, \varphi, \textit{conf\/}(\tau^\prime, h^\prime \sigma))$ according to Lemma \ref{lem-relations}. We must have further $\bigcup_{h \in H} \psi * h \tau \subseteq \psi^\prime * \tau^\prime$, which is expressed by $Sub(\psi, \psi^\prime, \textit{conf\/}(h \tau, \tau^\prime))$, and further $\psi^\prime * \tau^\prime \subseteq \bigcup_{h \in H} \psi * h \tau$, which is expressed by
\[ In(\chi, \psi^\prime, \textit{conf\/}(\alpha,\tau^\prime)) \rightarrow
\exists h \in H . In(\chi, \psi, \textit{conf\/}(\alpha, h \tau)) \]
for all forms $\chi$ and all molecules $\alpha$.

Analogously, for the equality and subset relations the given formulae just formulate set equality or subset relationship, respectively, and this is expressed using Lemma \ref{lem-relations} with the predicate $In$.\qed

\end{proof}

Finally, we can combine Lemmata \ref{lem-relations-ext1} and \ref{lem-relations-ext2}. It suffices to express the relationships between sets of the form $\bigcup_{h \in H} \psi * h \tau$ and $\phi (\bigcup_{h^\prime \in H^\prime} \varphi * h^\prime \sigma)$.

\begin{corollary}\label{cor-relations-ext}

For every isomorphism $\phi$ we have
\begin{align*}
\bigcup_{h \in H} \psi * h \tau & \in \phi( \bigcup_{h^\prime \in H^\prime} \varphi * h^\prime \sigma)
\Leftrightarrow \\
& \exists h^\prime \in H^\prime, \psi^\prime, \tau^\prime . In^\phi(\psi^\prime, \varphi, \textit{conf\/}^\phi(\tau^\prime, \phi h^\prime \sigma)) \wedge \\
& \forall h \in H . Sub(\psi, \psi^\prime, \textit{conf\/}(h \tau, \tau^\prime)) \wedge \\
& \forall \chi, \alpha . ( In(\chi, \psi^\prime, \textit{conf\/}(\alpha,\tau^\prime)) \rightarrow
\exists h \in H . In(\chi, \psi, \textit{conf\/}(\alpha, h \tau))) \\
\bigcup_{h \in H} \psi * h \tau & = \phi ( \bigcup_{h^\prime \in H^\prime} \varphi * h^\prime \sigma )
\Leftrightarrow \\
& \forall h \in H, \chi, \alpha . ( In(\chi, \psi, \textit{conf\/}(\alpha, h \tau)) \rightarrow \exists h^\prime \in H^\prime . In^\phi (\chi, \varphi, \textit{conf\/}^\phi (\alpha, \phi h^\prime \sigma))) \wedge \\
& \forall h^\prime \in H^\prime, \chi, \alpha . ( In^\phi (\chi, \varphi, \textit{conf\/}^\phi(\alpha, \phi h^\prime \sigma)) \rightarrow \exists h \in H . In(\chi, \psi, \textit{conf\/}(\alpha, h \tau)))
\end{align*}
\begin{align*}
\bigcup_{h \in H} \psi * h \tau & \subseteq \phi ( \bigcup_{h^\prime \in H^\prime} \varphi * h^\prime \sigma )
\Leftrightarrow \\
& \forall h \in H, \chi, \alpha . ( In(\chi, \psi, \textit{conf\/}(\alpha, h \tau)) \rightarrow \exists h^\prime \in H^\prime . In^\phi (\chi, \varphi, \textit{conf\/}^\phi (\alpha, \phi h^\prime \sigma)))
\end{align*}

\end{corollary}

Let us summarise the results on relations over forms and configurations in the following theorem.

\begin{theorem}\label{thm-relations}

Set membership, equality and set inclusion between objects in $\bar{I}_k$ can be expressed by the relations $In^\phi$, $Eq^\phi$ and $Sub^\phi$ and $\phi$-$\ell$-configurations, where $\phi$ is any isomorphism on $I$.

\end{theorem}

Note that the relations $In$, $Eq$ and $Sub$ are included by letting $\phi$ be the identity isomorphism.

\subsection{Extension of Configurations}

Now let $m \ge 3$ and assume $| I | \ge km$. The following lemma shows that if the configurations of two sequences of $k$-molecules of length $\ell < m$ over different structures $I$ and $J$ coincide, then the sequences can be uniformly extended.

\begin{lemma}\label{lem-conf-ext}

Let $\bar{\sigma} = \sigma_1, \dots \sigma_\ell$ and $\bar{\tau} = \tau_1, \dots, \tau_\ell$ be sequences of $k$-molecules over $I$ and $J$, respectively, with $\ell < m$. If $\textit{conf\/}(\bar{\sigma}) = \textit{conf\/}(\bar{\tau})$ holds and $\sigma_0$ is another $k$-molecule over $I$, then there exists another $k$-molecule $\tau_0$ over $J$ with $\textit{conf\/}(\sigma_0,\bar{\sigma}) = \textit{conf\/}(\tau_0,\bar{\tau})$.

\end{lemma}

\begin{proof}

For $1 \le p \le k$ and $1 \le i \le \ell$ we clearly must have $\tau_0(p) = \tau_i(q_i)$, if $(0,p) \sim_{\sigma_0,\bar{\sigma}} (i,q_i)$ holds. Therefore, we define a partial molecule $\tau_0^\prime(p) = \tau_i(q_i)$ for such $p$ and $q_i$. This partial molecule $\tau_0^\prime$ is well defined: if $(0,p) \sim_{\sigma_0,\bar{\sigma}} (i,q_i)$ and $(0,p) \sim_{\sigma_0,\bar{\sigma}} (j,q_j)$ hold, we must have $(i,q_i) \sim_{\bar{\sigma}} (j,q_j)$ and hence $\tau_i(q_i) = \tau_j(q_j)$.

For $(0,p) \sim_{\sigma_0,\bar{\sigma}} (i,q_i)$ we also have $\sigma_0(p) = \sigma_i(q_i)$. As $col_{\bar{\sigma}}(i,q_i) = col_{\bar{\tau}}(i,q_i)$ holds, we also get that $\tau_0^\prime(p)$ and $\sigma_0(p)$ have the same colour.

Furthermore, $\tau_0^\prime$ is injective. If we have $\tau_0^\prime(p_1) = \tau_0^\prime(p_2)$, then we get $\tau_i(q_i) = \tau_j(q_j)$ for $(0,p_1) \sim_{\sigma_0,\bar{\sigma}} (i,q_i)$ and $(0,p_2) \sim_{\sigma_0,\bar{\sigma}} (j,q_j)$. Hence $(i,q_i) \sim_{\bar{\sigma}} (j,q_j)$ and consequently $(0,p_1) \sim_{\sigma_0,\bar{\sigma}} (0,p_2)$ and $p_1 = p_2$.

So we can can extend $\tau_0^\prime$ to a $k$-molecule $\tau_0$ over $J$ such that \ $\tau_0^\prime(p)$ and $\sigma_0(p)$ have the same colour for all $1 \le p \le k$. This is possible, because there are enough elements for each colour.\qed

\end{proof}

We now show that relationships between elements in $k$-skew-symmetric sets generated from such sequences as in Lemma \ref{lem-conf-ext} are preserved by the extension of the configurations. First we consider the case, where no isomorphism is applied, so we deal with configurations with colour assignment in $C$.

\begin{lemma}\label{lem-extension-relations}

Let $\bar{\sigma} = \sigma_0, \dots \sigma_\ell$ and $\bar{\tau} = \tau_0, \dots, \tau_\ell$ be sequences of $k$-molecules over $I$ and $J$, respectively, with $\ell < m$ such that $\textit{conf\/}(\bar{\sigma}) = \textit{conf\/}(\bar{\tau})$ holds. For objects $x_i = \bigcup_{h \in H_i} \varphi_i * h \sigma_i$ and $y_i = \bigcup_{h \in H_i} \varphi_i * h \tau_i$ we have
\begin{align*}
x_i \in x_j \; &\Leftrightarrow \; y_i \in y_j \\
x_i = x_j \; &\Leftrightarrow \; y_i = y_j \\
x_i \subseteq x_j \; &\Leftrightarrow \; y_i \subseteq y_j
\end{align*}

\end{lemma}

\begin{proof}

First consider set membership; assume $x_i \in x_j$. According to Lemma \ref{lem-relations-ext2} there exists some $h_j \in H_j$, a form $\psi$ and a molecule $\tau$ such that
\[ In(\psi, \varphi_j, \textit{conf\/}(\tau, h_j \sigma_j)) \]
holds. In addition, we have
\begin{gather*}
\forall h \in H_i . Sub(\varphi_i, \psi, \textit{conf\/}(h \sigma_i, \tau)) \wedge \\
\forall \chi, \alpha . ( In(\chi, \psi, \textit{conf\/}(\alpha,\tau)) \rightarrow
\exists h \in H_i . In(\chi, \varphi_i, \textit{conf\/}(\alpha, h \sigma_i))) \; .
\end{gather*}

First define $\tau^\prime(p) = h_j \tau_j (q)$ for all $p, q$ with $(0,p) \sim_{(\tau, h_j \sigma_j)} (1,q)$. This already implies
\[ (0,p) \sim_{(\tau^\prime, h_j \tau_j)} (1,q) \Leftrightarrow \tau^\prime(p) = h_j \tau_j (q) \Leftrightarrow (0,p) \sim_{(\tau, h_j \sigma_j)} (1,q) \; . \]
Furthermore, we have
\begin{gather*}
col_{(\tau^\prime, h_j \tau_j)} (0,p) = c \Leftrightarrow \tau^\prime(p) \in c \Leftrightarrow h_j \tau_j (q) \in c \Leftrightarrow \\
h_j \sigma_j (q) \in c \Leftrightarrow col_{(\tau, h_j \sigma_j)} (1,q) = c \Leftrightarrow col_{(\tau, h_j \sigma_j)} (0,p) = c
\end{gather*}
and
\begin{gather*}
col_{(\tau^\prime, h_j \tau_j)} (1,q) = c \Leftrightarrow h_j \tau_j (q) \in c \Leftrightarrow col_{(\tau, h_j \sigma_j)} (1,q) = c \; ,
\end{gather*}
which imply $\textit{conf\/}(\tau^\prime, h_j \tau_j) = \textit{conf\/}(\tau, h_j \sigma_j)$, hence $In(\psi, \varphi_j, \textit{conf\/}(\tau^\prime, h_j \tau_j))$ holds.

Next let $h \in H_i$ be arbitrary, so $Sub(\varphi_i, \psi, \textit{conf\/}(h \sigma_i, \tau))$ holds. Let us extend the definition of $\tau^\prime$ by $\tau^\prime(q) = h \tau_i (p)$, whenever $(0,p) \sim_{(h \sigma_i, \tau)} (1,q)$ holds. If this does not conflict with the definition of $\tau^\prime$ above, we have
\[ (0,p) \sim_{(h \tau_i, \tau^\prime)} (1,q) \Leftrightarrow h \tau_i(p) = \tau^\prime(q) \Leftrightarrow (0,p) \sim_{(h \sigma_i, \tau)} (1,q) \]
and furthermore
\[ col_{(h \sigma_i, \tau)} (0,p) = c \Leftrightarrow h \sigma_i(p) \in c \Leftrightarrow h \tau_i(p) \in c \Leftrightarrow col_{(h \tau_i, \tau^\prime)} (0,p) = c \; , \]
which also implies $col_{(h \sigma_i, \tau)} (1,q) = col_{(h \tau_i, \tau^\prime)} (1,q)$, as we defined $\tau^\prime(q) = h \tau_i (p)$ only for $(0,p) \sim_{(h \sigma_i, \tau)} (1,q)$. So we get $\textit{conf\/}(h \sigma_i, \tau) = \textit{conf\/}(h \tau_i, \tau^\prime)$, which implies that $Sub(\varphi_i, \psi, \textit{conf\/}(h \tau_i, \tau^\prime))$ holds.

We still have to show that $\tau^\prime$ is well-defined. We defined
\[ \tau^\prime(p) \; = \; \begin{cases} h_j \tau_j (q) &\text{if}\; (0,p) \sim_{(\tau, h_j \sigma_j)} (1,q) \\
h \tau_i (q) &\text{if}\; (0,p) \sim_{(\tau, h \sigma_i)} (1,q) \end{cases} \]
with the given $h_j \in H_j$ and arbitrary $h \in H_i$. So we get
\[ h_j \sigma_j(q) = h \sigma_i(q) \Leftrightarrow (0,q) \sim_{(h_j \sigma_j, h \sigma_i)} (1,q) \Leftrightarrow (0,q) \sim_{(h_j \tau_j, h \tau_i)} (1,q) \Leftrightarrow h_j \tau_j(q) = h \tau_i(q) \; . \]

Finally, take an arbitrary form $\chi$ and a molecule $\alpha$ such that $In(\chi, \psi, \textit{conf\/}(\alpha,\tau^\prime))$ holds. Choose a form $\alpha^\prime$ with $\textit{conf\/}(\alpha^\prime,\tau) = \textit{conf\/}(\alpha,\tau^\prime)$. Then we have $In(\chi, \psi, \textit{conf\/}(\alpha^\prime,\tau))$, which implies that $In(\chi, \varphi_i, \textit{conf\/}(\alpha^\prime, h_i \sigma_i))$ holds for some $h_i \in H_i$. As we have $\textit{conf\/}(h \sigma_i, \tau) = \textit{conf\/}(h \tau_i, \tau^\prime)$ for all $h \in H_i$, we get also $\textit{conf\/}(\alpha^\prime, h_i \sigma_i) = \textit{conf\/}(\alpha, h_i \tau_i)$. Hence we also have $In(\chi, \varphi_i, \textit{conf\/}(\alpha, h_i \tau_i))$.

Together we have now shown that
\begin{gather*}
In(\psi, \varphi_j, \textit{conf\/}(\tau^\prime, h_j \tau_j)) \wedge \forall h \in H_i . Sub(\varphi_i, \psi, \textit{conf\/}(h \tau_i, \tau^\prime)) \wedge \\
\forall \chi, \alpha . ( In(\chi, \psi, \textit{conf\/}(\alpha,\tau^\prime)) \rightarrow
\exists h \in H_i . In(\chi, \varphi_i, \textit{conf\/}(\alpha, h \tau_i)))
\end{gather*}
holds, which by Lemma \ref{lem-relations-ext2} implies $y_i \in y_j$ as claimed. The converse showing that $y_i \in y_j$ implies $x_i \in x_j$ is completely analogous.

Next assume that $x_i = x_j$ holds. Then according to Lemma \ref{lem-relations-ext2} we have
\begin{gather*}
\forall h \in H_i, \chi, \alpha . ( In(\chi, \varphi_i, \textit{conf\/}(\alpha, h \sigma_i)) \rightarrow \exists h^\prime \in H_j . In(\chi, \varphi_j, \textit{conf\/}(\alpha, h^\prime \sigma_j))) \wedge \\
\forall h^\prime \in H_j, \chi, \alpha . ( In(\chi, \varphi_j, \textit{conf\/}(\alpha, h^\prime \sigma_j)) \rightarrow \exists h \in H_i . In(\chi, \varphi_i, \textit{conf\/}(\alpha, h \sigma_i)))
\end{gather*}

Let $h \in H_i$ be arbitrary, and let $\chi$ be a form and $\alpha$ be a molecule such that $In(\chi, \varphi_i, \textit{conf\/}(\alpha, h \tau_i))$ holds. Then there exists a form $\alpha^\prime$ with $\textit{conf\/}(\alpha^\prime, h \sigma_i)) = \textit{conf\/}(\alpha, h \tau_i))$, hence $In(\chi, \varphi_i, \textit{conf\/}(\alpha^\prime, h \sigma_i))$ holds. This implies $In(\chi, \varphi_j, \textit{conf\/}(\alpha^\prime, h_j \sigma_j)))$ for some $h_j \in H_j$, and we must have $\textit{conf\/}(\alpha^\prime, h_j \sigma_j)) = \textit{conf\/}(\alpha, h_j \tau_j))$. Hence $In(\chi, \varphi_j, \textit{conf\/}(\alpha, h_j \tau_j)))$ holds, which shows $y_i \subseteq y_j$.

Conversely, let $h \in H_j$ be arbitrary, and let $\chi$ be a form and $\alpha$ be a molecule such that $In(\chi, \varphi_j, \textit{conf\/}(\alpha, h \tau_j)))$ holds. Take a form $\alpha^\prime$ with $\textit{conf\/}(\alpha^\prime, h \sigma_j)) = \textit{conf\/}(\alpha, h \tau_j))$, hence $In(\chi, \varphi_i, \textit{conf\/}(\alpha^\prime, h \sigma_j))$ holds. This implies $In(\chi, \varphi_i, \textit{conf\/}(\alpha^\prime, h_i \sigma_i)))$ for some $h_i \in H_i$, and we must have $\textit{conf\/}(\alpha^\prime, h_i \sigma_i)) = \textit{conf\/}(\alpha, h_i \tau_i))$. Hence $In(\chi, \varphi_i, \textit{conf\/}(\alpha, h_i \tau_i)))$ holds, which shows $y_j \subseteq y_i$, and thus $y_i = y_j$. The proof of the other direction showing that $y_i = y_j$ implies $x_i = x_j$ is completely analogous.

This leaves the case of the subset relationship, which is shown analogously to the first part of the equality case, which completes the proof of the lemma.\qed

\end{proof}

We can extend Lemma \ref{lem-extension-relations} to relationships that involve isomorphisms. The proof of Corollary \ref{cor-extension-relations} is analogous to the proof of Lemma \ref{lem-extension-relations} with the only difference that we exploit Corollary \ref{cor-relations-ext} instead of Lemma \ref{lem-relations-ext2}.

\begin{corollary}\label{cor-extension-relations}

Let $\bar{\sigma} = \sigma_0, \dots \sigma_\ell$ and $\bar{\tau} = \tau_0, \dots, \tau_\ell$ be sequences of $k$-molecules over $I$ and $J$, respectively, with $\ell < m$ such that $\textit{conf\/}(\bar{\sigma}) = \textit{conf\/}(\bar{\tau})$ holds. For objects $x_i = \bigcup_{h \in H_i} \varphi_i * h \sigma_i$ and $y_i =\bigcup_{h \in H_i} \varphi_i * h \tau_i$ and an isomorphism $\phi$ we have
\begin{align*}
x_i \in \phi(x_j) \; &\Leftrightarrow \; y_i \in \phi(y_j) \\
x_i = \phi(x_j) \; &\Leftrightarrow \; y_i = \phi(y_j) \\
x_i \subseteq \phi(x_j) \; &\Leftrightarrow \; y_i \subseteq \phi(y_j)
\end{align*}

\end{corollary}

We will exploit Lemma \ref{lem-extension-relations} and Corollary \ref{cor-extension-relations} in Section \ref{sec:separation} for the construction of a winning strategy, which will show the inseparabilty of classes $(\bar{I}_k,\bar{R}_1)$ and $(\bar{I}_k,\bar{R}_2)$ for sufficiently large $I$.

\subsection{Forms for Relations}

For the winning strategy we also have to take care of the input relations, which so far have not been dealt with throughout this section. Let the input relations be $\bar{R} = \{ R_1, \dots, R_m \}$, where the arity of $R_i$ is $n_i \le \ell$. For indices $i_1 ,\dots, i_q \in \{ 1, \dots, m \}$ such that $n_{i_x} = n_{i_y}$ we build
\[ R_{i_1 ,\dots, i_q} = \bigcap_{1 \le j \le q} R_{i_j} - \bigcup_{i \notin \{ i_1 ,\dots, i_q \}} R_i \; , \]
where we may omit those $R_{i_1 ,\dots, i_q}$ that by definition must be empty. In this way we partition the sets of tuples over $I$ including $I$ itself. We refer to these relations as {\em colours}, which extends our previous definition of colours. Let $C$ denote the set of all colours. As before, we call a structure {\em $\varepsilon$-level} iff $| c | > \varepsilon \cdot n^{n_i}$ holds for all colours $c \in C$, where $n_i$ is the arity of the colour $c$, and $n$ is the size of the set of atoms.

If $\bar{a} = (a_1,\dots,a_\ell)$ is an $\ell$-tuple of atoms ($\ell > 1$), then by means of the Kuratowski representation of pairs, which is canonically extended to arbitrary tuples, we can consider $\bar{a}$ as a set in $\textit{HF\/}(I)$. For $\ell \le m$ we then find an $m$-form $\phi_{\bar{a}}$ and an $m$-molecule $\sigma$ with $\bar{a} = \phi * \sigma$.

For $\ell = 2$ and $a_1 \neq a_2$ take $\sigma(0) = a_1$ and $\sigma(1) = a_2$ with an arbitrary extension to an $m$-molecule $\sigma$. For $a_1 = a_2$ take $\sigma(0) = a_1$ and extend $\sigma$ arbitrarily to an $m$-molecule. In the former case let $p_1 = 0$ and $p_2 = 1$; in the latter case let $p_1 = p_2 = 0$. Furthermore, define
\[ \varphi_{(a_1,a_2)} = \{ ( \{ (c_{p_1}, E) \}, E), ( \{ (c_{p_1}, E), (c_{p_2}, E) \}, E ) \} \]
where $\sim_E$ satisfies $(0,p) \sim_E (1,p)$ for $p \in \{ 0, 1 \}$. Then we get
\[ \varphi * \sigma = \{ \{ \sigma(p_1) \}, \{ \sigma(p_1), \sigma(p_2) \} \} = \bar{a} \; . \]

We extend this construction to arbitrary tuples by induction. Note that $\phi_{\bar{a}}$ only depends on the pattern of the tuple $\bar{a}$, not on the actual values---these values are captured by the molecule $\sigma$.

Next consider an $\ell$-ary relation $R$, in which all tuples are composed from $m$ distinct atoms $a_0,\dots,a_{m-1}$. Let $\sigma$ be the $m$-molecule defined by $\sigma(p) = a_p$. Then there exsts a form $\varphi_R = \{ (\varphi_{\bar{a}}, E) \mid \bar{a} \in R \}$ such that $R = \varphi_R * \sigma$ holds, where we $\sim_E$ satisfies $(0,p) \sim_E (1,p)$ for all $p \in \{ 0, \dots, m-1 \}$.

If we are given a colour $c \in C$ defined by the input relations of arity $n_i$, then any given $m$ atoms $a_0,\dots,a_{m-1}$ define a subrelation of $c$, and this subrelation can be written in the form $\varphi * \sigma$ with a form $\varphi$ as constructed and a molecule $\sigma$ defined by the distinct atoms among the given ones (and then arbitrarily extended). In this case we call $\varphi$ an {\em $m$-pattern} of the colour $c$. We will exploit this representation of subrelations of colours in Section \ref{sec:separation}.

With our representation of tuples we can take the expression of relationships as in Lemmata \ref{lem-relations} and \ref{lem-relations-ext1} further to components of tuples.

\begin{lemma}\label{lem-components}

For every $\ell > 0$ there exist ternary relations $\Pi^{(j)}$ for $1 \le j \le \ell$ such that $\varphi * \sigma$ is the $j$'th component of the $\ell$-tuple $\chi * \alpha$ iff $\Pi^{(j)}(\varphi, \chi, \textit{conf\/}(\sigma, \alpha))$ holds.

\end{lemma}

\begin{proof}

According to our considerations above we can write
\[ \chi = \{ ( \{ (\chi_1, E) \}, E), ( \{ (\chi_1, E), (\chi_2, E) \}, E ) \} \; . \]

Then $\varphi * \sigma$ is the first component of the $\ell$-tuple $\chi * \alpha$ iff $\varphi * \sigma = \chi_1 * \alpha$, so we define $\Pi^{(1)}(\varphi, \chi, Q) = Eq(\varphi, \chi_1, Q)$. With this the claim for $j=1$ follows immediately from Lemma \ref{lem-relations}.

For $j > 1$ we have that $\varphi * \sigma$ is the $j$'th component of $\chi * \alpha$ iff it is the $(j-1)$'th component of the $(\ell-1)$-tuple $\chi_2 * \alpha$. So we define $\Pi^{(j)}(\varphi, \chi, Q) = \Pi^{(j-1)}(\varphi, \chi_2, Q)$. With this the claim for $j > 1$ follows by induction. \qed

\end{proof}

\begin{corollary}\label{cor-components}

For every $\ell > 0$ and every isomorphism $\Phi$ there exist ternary relations $\Pi^{(j)}_\Phi$ for $1 \le j \le \ell$ such that $\Phi^{-1}(\varphi * \sigma)$ is the $j$'th component of the $\ell$-tuple $\chi * \alpha$ iff $\Pi^{(j)}_\Phi(\varphi, \chi, \textit{conf\/}^\Phi(\sigma, \alpha))$ holds.

\end{corollary}

\begin{proof}

Again we have
\[ \chi = \{ ( \{ (\chi_1, E) \}, E), ( \{ (\chi_1, E), (\chi_2, E) \}, E ) \} \; . \]

Then $\Phi^{-1}(\varphi * \sigma)$ is the first component of $\chi * \alpha$ iff $\varphi * \sigma = \Phi(\chi_1 * \alpha)$, so we define $\Pi^{(1)}_\Phi(\varphi, \chi, Q) = Eq^\Phi(\varphi, \chi_1, Q)$. With this the claim for $j=1$ follows immediately from Lemma \ref{lem-relations-ext1}.

As the $j$'th component of $\chi * \alpha$ is the $(j-1)$'th component of the $(\ell-1)$-tuple $\chi_2 * \alpha$, the claim for $j > 1$ follows by induction. \qed

\end{proof}

\section{Separation Games on ICPT}\label{sec:games}

This section continues with the question how the separation of classes of (semi-transitive) structures by an inflationary fixed-point formula over the insignificant fragment $\mathcal{L}^{ic}$ of the logic $\mathcal{L}^{nd}$ can be characterised. For this we first analyse the formulae used in proofs of the Fixed-Point Theorems \ref{thm-fixpoint} and \ref{thm-orbit}, which will give us a precise definition of $\mathcal{L}^{ic}$. Then we use a fairly standard embedding of IFP$[\mathcal{L}^{ic}]$ into an infinitary logic $\mathcal{L}^{ic,\omega}_{\infty\omega}$. For the finite variable fragment $\mathcal{L}^{ic,m}_{\infty\omega}$ we then define a pebble game in the spirit of the Ehrenfeucht-Fra\"{\i}ss\'{e} method that characterises separability of classes of structures satisfying some conditions. This game characterisation will be the main result of this section.

\subsection{The Finite Variable Infinitary Logic $\mathcal{L}^{ic,m}_{\infty\omega}$}

In the Fixed-Point Theorems \ref{thm-fixpoint}, \ref{thm-active} and \ref{thm-orbit} we only require a fragment $\mathcal{L}^{ic}$ of the logic $\mathcal{L}^{nd}$ of non-deterministic ASMs. Concerning the terms we permit the 4-ary relation symbols $D_f$ with $f \in \Upsilon_{dyn}$. These relation symbols are derived and thus could be eliminated. The formulae of the logic $\mathcal{L}^{ic}$ are defined as follows:

\begin{enumerate}

\item If $t$ and $t^\prime$ are terms, then $t = t^\prime$ is a formula of $\mathcal{L}^{ic}$.

\item If $X$ is a second-order variable of arity $n \in \{ 2, 3, 4 \}$ and $t_1 ,\dots, t_n$ are terms, then $X(t_1, \dots, t_n)$ is a formula of $\mathcal{L}^{ic}$.

\item If $r$ is an ASM rule, $j \ge 0$ and $X$ is a second-order variable of arity $3$, then $U_r(j,X)$ is a formula of $\mathcal{L}^{ic}$, where\footnote{as in Theorem \ref{thm-fixpoint}} $U_r(j,X)$ is the formula that results from $\text{upd}^{ic}_r(X)$ by replacing every atomic subformula of the form $g(\bar{u}) = t$ with dynamic function symbol $g$ by
\[ \exists Z . (D_g(j,\bar{u},t, Z) \wedge t \neq 0) \vee (t = 0 \wedge \neg \exists z . D_g(j, \bar{u}, z, Z)) .\]

\item If $\varphi$ and $\psi$ are formulae of $\mathcal{L}^{ic}$, then also $\neg \varphi$, $\varphi \wedge \psi$, $\varphi \vee \psi$ and $\varphi \rightarrow \psi$ are formulae of $\mathcal{L}^{ic}$.

\item If $\varphi$ is a formula of $\mathcal{L}^{ic}$ and $x$ is a first-order variable, then also $\forall x . \varphi$ and $\exists x . \varphi$ are formulae of $\mathcal{L}^{ic}$.

\item If $\varphi$ is a formula of $\mathcal{L}^{ic}$ and $X$ is a second-order variable of arity 2, then also $\forall X . \text{iso}(X) \rightarrow \varphi$ and $\exists X . \text{iso}(X) \wedge \varphi$ are formulae of $\mathcal{L}^{ic}$.

\item If $\varphi$ is a formula of $\mathcal{L}^{ic}$and $X$ is a second-order variable of arity 3, then also $\forall X . \text{isUSet}(X) \rightarrow \varphi$ and $\exists X . \text{isUSet}(X) \wedge \varphi$ are formulae of $\mathcal{L}^{ic}$.

\end{enumerate}

Note that we also have quantification over second-order variables of arity 4, but this only occurs inside formulae of the form upd$_r^{ic}(X)$, where $r$ is a \textbf{forall} rule. Furthermore, a formula upd$_r^{ic}(X)$, where $r$ is a \textbf{choose} rule, contains subformulae of the form $[X^\prime]\text{upd}_r(Y)$; the formulae involve universal quantification over such $X^\prime$ that are isomorphic, as well as quantification over $Y$ that are also isomorphic. This applies in the same way to formulae $U_r(j,X)$.

All abbreviating formulae $\text{isUSet}(X)$, $\text{ConUSet}(X)$, $\text{iso}(X)$, $\text{updIso}(X_1,X_2,X)$, $\text{updIsoSet}(X_1,X_2,X)$, the formula $\phi(D_f, i, \bar{x}, y, Z)$ used in the fixed-point formula in Theorem \ref{thm-fixpoint}, $\textit{critical\/}(x)$, $\textit{transitive\/}(x)$, $\textit{orbit\/}(x)$, $\textit{represents\/}(y,x)$, $\textit{critical-orbit\/}(x)$, $\textit{iso-crit\/}(x,y,X)$, $\textit{active-orbit\/}(x)$ and $\textit{same\_generator\/}(x,y)$ can be represented in $\mathcal{L}^{ic}$. Therefore, in the following we can concentrate on the inflationary fixed-point logic $\text{IFP}[\mathcal{L}^{ic}]$.

Every formula $\varphi \in \mathcal{L}^{ic}$ has a {\em modal rank} $\text{mod-rk}(\varphi)$. If $\varphi$ does not contain a subformula of the form $[X]\text{upd}_r(Y)$, the $\text{mod-rk}(\varphi) = 0$. Otherwise
\[ \text{mod-rk}(\varphi) = \max \{ \text{mod-rk}(\psi) \mid [X]\psi \;\text{is a subformula of}\; \varphi \;\text{for some}\; X \} + 1 \; . \]

In the remainder of this section we investigate the expressiveness of the fixed-point logic IFP[$\mathcal{L}^{ic}$]. Following \cite[Ch.11]{libkin:2004} we embed the logic into an infinitary extension of $\mathcal{L}^{ic}$, then in the next subsection we develop a pebble game by means of which we can characterise classes of structures that cannot be separated by formulae of the logic. We will use this later for the investigation of the limitations of ICPT.

As usual let $\mathcal{L}^{ic}_{\infty\omega}$ be the logic that extends $\mathcal{L}^{ic}$ by infinitary conjunctions $\bigwedge$ and disjunctions $\bigvee$, i.e. in addition to the rules above defining formulae in $\mathcal{L}^{ic}$ we need the following rule for formulae in $\mathcal{L}^{ic}_{\infty\omega}$:

\begin{enumerate}\setcounter{enumi}{7}

\item If all $\varphi_i$ ($i \in I$) are formulae, then also $\bigwedge_{i \in I} \varphi_i$ and $\bigvee_{i \in I} \varphi_i$ are formulae, provided that the sets $\{ r \mid U_r(j,X) \;\text{is a subformula of}\; \varphi_i \}$ are finite and identical for all $i \in I$ (then also $\max \{ \text{mod-rk}(\varphi_i) \mid i \in I \}$ exists).

\end{enumerate}

Let $\mathcal{L}^{ic,m}_{\infty\omega}$ denote the fragment of $\mathcal{L}^{ic}_{\infty\omega}$ with formulae that contain at most $m$ variables, and let $\mathcal{L}^{ic,\omega}_{\infty\omega}$ be the fragment of formulae that contain only finitely many variables, i.e.
\[ \mathcal{L}^{ic,\omega}_{\infty\omega} = \bigcup_{m \in \mathbb{N}} \mathcal{L}^{ic,m}_{\infty\omega} . \]

Now let $[\textbf{ifp}_R \; \varphi(R,\bar{X},\bar{x})](\bar{X},\bar{x})$ be a formula in IFP[$\mathcal{L}^{ic}$]. Assume that $\varphi$ in addition to the second-order variables $\bar{X}$ and the first-order variables $\bar{x} = (x_1, \dots, x_m)$ uses also first-order variables $\bar{z} = (z_1, \dots, z_\ell)$. We use additional first-order variables $\bar{y} = (y_1, \dots, y_m)$ to inductively define formulae $\varphi^\beta(\bar{X},\bar{x})$ for each ordinal $\beta$. For finite structures it suffices to consider $\beta \in \mathbb{N}$. For $\beta=0$ let $\varphi^0(\bar{X},\bar{x}) \equiv \neg (x_1 = x_1)$, which is equivalent to \textbf{false}. Then define $\varphi^{\beta+1}(\bar{X},\bar{x})$ replacing in $\varphi(R,\bar{X},\bar{x})$ each occurrence $R(u_1, \dots, u_m)$, where $u_1, \dots, u_m$ are variables among $\bar{x}$ and $\bar{z}$ by
\[ \exists \bar{y} . \bar{y} = \bar{u} \wedge \exists \bar{x} . ( \bar{x} = \bar{y} \wedge \varphi^\beta(\bar{X},\bar{x}) ) . \]
For a limit ordinal $\gamma$ we simply have $\varphi^{\gamma}(\bar{X},\bar{x}) \equiv \bigvee\limits_{\beta < \gamma} \varphi^\beta(\bar{X},\bar{x})$.

Then for each ordinal $\beta$ the formula $\varphi^\beta(\bar{X},\bar{x})$ represents $R$ in the $\beta$'th stage of the fixed-point iteration. Hence $[\textbf{ifp}_R \; \varphi(R,\bar{X},\bar{x})](\bar{X},\bar{x})$ is equivalent to $\bigvee_\beta \varphi^\beta(\bar{X},\bar{x})$.

Note that at most the number of first-order variables is doubled, whereas the number of second-order variables remains unchanged. In particular, the conditions required in (8) are satisfied for all infinitary conjunctions and disjunctions.

For complex nested fixed-point formulae we proceed by induction. We can use the same replacement as above to define $\varphi^{\beta+1}(\bar{X},\bar{x})$; the only difference is that $\varphi^\beta(\bar{X},\bar{x})$ is already a formula that includes infinitary connectives. The same holds for limit ordinals.

With this embedding of IFP[$\mathcal{L}^{ic}$] into $\mathcal{L}^{ic,\omega}_{\infty\omega}$ we can rephrase Corollary \ref{cor-fixpoint} as follows:

\begin{theorem}\label{thm-fixpoint2}

Let $I$ be an input structure for a (time-explicit) PTIME ic-ASM $\tilde{M}$. There exists a formula $\varphi$ in $\mathcal{L}^{ic,m}_{\infty\omega}$ for some $m \in \mathbb{N}$ that asserts that $\tilde{M}$ accepts $I$, which is the case iff $\varphi$ holds in some or equivalently all semi-transitive substructures of $\textit{HF\/}(I)$ containing all objects of all active orbits in $\mathcal{A}[I]$.

\end{theorem}

For later use we recall the notion of {\em quantifier rank} of a formula. For a formula $\varphi$ of $\mathcal{L}^{ic,m}_{\infty\omega}$ we define $qr(\varphi)$ as follows:

\begin{itemize}

\item for an atomic formula $\varphi$ we have $qr(\varphi) = 0$;

\item for Boolean connectives we have $qr(\neg\varphi) = qr(\varphi)$ and $qr(\varphi \wedge \psi) = qr(\varphi \vee \psi) = qr(\varphi \rightarrow \psi) = \max \{ qr(\varphi), qr(\psi) \}$;

\item for infinitary connectives we have $qr(\bigwedge\limits_{i \in I} \varphi_i) = qr(\bigvee\limits_{i \in I} \varphi_i) = \sup\limits_{i \in I} qr(\varphi_i)$;

\item for quantified formulae we have $qr(\exists x . \varphi) = qr(\forall x . \varphi) = qr(\exists X . \varphi) = qr(\forall X . \varphi) = qr(\varphi) + 1$.

\end{itemize}

Note that in general a formula of the form $\text{upd}_r^{ic}(X)$ has a quantifier rank $> 0$ due to the definition of $\text{upd}_r^{ic}$.

\subsection{Separation Games}

Equivalence of structures with respect to infinitary logics with finitely many variables can be characterised by pebble games (see \cite[Sect.11.2]{libkin:2004}). We will now define an analogous pebble game for $\mathcal{L}^{ic,m}_{\infty\omega}$. However, we are not concerned with a characterisation of equivalence of two structures, but instead with the separability of two classes of structures, i.e. roughly speaking with the existence of sentences that take different interpretations for some structures in the two classes\footnote{Dawar argues convincingly that $\mathcal{L}^{ic,m}_{\infty\omega}$-equivalence of structures is meaningless \cite{dawar:communication2020}, as it is well known that any two ordered structures can be separated by a formula of the infinitary extension $\mathcal{L}^m_{\infty\omega}$ of first-order logic for some constant $m$ \cite{dawar:csl1996} and hence any two (unordered) structures can be separated by a formula of $\mathcal{L}^{ic,m}_{\infty\omega}$, because $\mathcal{L}^{ic}$ permits to generate an arbitrary order. As a consequence, it is plausible that an equivalence theorem as in the case of CPT \cite{blass:apal1999} stating that all sufficiently large symmetric structures will become equivalent (in case of a winning strategy of the duplicator) cannot hold. However, this does not imply that the separating formula is always the same for all pairs of structures. It may still be possible that for classes of structures no formula of $\mathcal{L}^{ic,m}_{\infty\omega}$ exists separating them, and in fact this is all we need to find examples of problems that cannot be decided by ICPT and thus do not lie in PTIME.}.

We may concentrate on structures, where the signature $\Upsilon$ contains a constant $\emptyset$ and set membership $\in$ in addition to finitely many relation symbols. Denote such structures as $\mathcal{A} = (T,\in,\emptyset,\bar{R})$, where $\bar{R}$ stands for the finite set of relations over $T$. Assume that $T$ contains a finite set of special constants $c_f$ corresponding to dynamic functions symbols $f$, each with an arity $n$. The presence of such constants allows us to talk about {\em update sets} in $\mathcal{A}$, i.e. sets of updates in the form of triples $(c_f, \bar{a}, b)$, where the length of the tuple $\bar{a}$ equals the arity of $f$.

Separation games are played over a pair $(C_1, C_2)$, where each $C_i$ is a non-empty class of structures over a common signature $\Upsilon$ subject to the following conditions:

\begin{itemize}

\item The signature $\Upsilon$ satisfies the conditions in Section \ref{sec:asm}.

\item All structures $\mathcal{A} \in C_1$ have the same base set $B_1 = HF(A_1) \cup \{ c_f \mid f \in \Upsilon_{dyn} \}$.

\item All structures $\mathcal{B} \in C_2$ have the same base set $B_2 = HF(A_2) \cup \{ c_f \mid f \in \Upsilon_{dyn} \}$.

\item $C_1$ and $C_2$ are both closed under isomorphisms and the application of update sets.

\item $C_1$ and $C_2$ are disjoint.

\end{itemize}

We will call such a pair $(C_1, C_2)$ a {\em separation candidate}.

We say that a separation candidate $(C_1,C_2)$ is {\em partitioned} into separation candidates $(C_{1i},C_{2i})$ with $i \in I$ iff all classes $C_{1i}$ ($i \in I$) are pairwise disjoint, all classes $C_{2i}$ ($i \in I$) are pairwise disjoint, $C_1 = \bigcup_{i \in I} C_{1i}$, and $C_2 = \bigcup_{i \in I}^n C_{2i}$.

Partitions are ordered by $\mathcal{P}_1 \rhd \mathcal{P}_2$ iff for each $(C^1_{1i}, C^1_{2i}) \in \mathcal{P}_1$ there exists a $(C^2_{1j}, C^2_{2j}) \in \mathcal{P}_2$ with $C^1_{1i} \subseteq C^2_{1j}$ and $C^1_{2i} \subseteq C^2_{2j}$.

\begin{definition}\label{def-sep}\rm

Let $(C_1, C_2)$ be a separation candidate.

\begin{enumerate}

\item $(C_1, C_2)$ is called {\em $\mathcal{L}^{ic,m}_{\infty\omega}$-separable} if and only if there exists a sentence $\varphi \in \mathcal{L}^{ic,m}_{\infty\omega}$ such that $\mathcal{A} \models \varphi$ holds for all $\mathcal{A} \in C_1$ and $\mathcal{B} \models \neg \varphi$ holds for all $\mathcal{B} \in C_2$.

\item $(C_1, C_2)$ is called {\em $\mathcal{L}^{ic,m}_{\infty\omega}$-inseparable} if and only if  for all sentences $\varphi \in \mathcal{L}^{ic,m}_{\infty\omega}$ we have that $\mathcal{A} \models \varphi$ holds for some $\mathcal{A} \in C_1$ if and only if $\mathcal{B} \models \varphi$ holds for some $\mathcal{B} \in C_2$.

\end{enumerate}

\end{definition}

Theorem \ref{thm-fixpoint2} states that if a decision problem is in PTIME, there exists a sentence $\varphi \in \mathcal{L}^{ic,m}_{\infty\omega}$ that separates all semi-transitive structures satisfying $\varphi$ from all those semi-transitive structures not satisfying $\varphi$. Thus, in order to show that a decision problem is not in PTIME we have to show the inseparability of the classes of semi-transitive structures satisfying $\varphi$ or not, respectively. In fact, it suffices to show inseparability for classes that are sufficiently large. This is what we will do in the next section. Here we concentrate on the characterisation of separability by a game. We first need a specific form of partial isomorphisms between structures.

\begin{definition}\label{def-po}\rm

Let $(C_1, C_2)$ be a separation candidate, and let $\mathcal{A}\in C_1$ and $\mathcal{B} \in C_2$.

\begin{itemize}

\item Let $\bar{\boldsymbol{\Delta}} = (\Delta_1 ,\dots, \Delta_k)$ and $\bar{\boldsymbol{\Delta}}^\prime = (\Delta_1^\prime ,\dots, \Delta_k^\prime)$ be finite sequences of update sets of equal length over $\mathcal{A}$ and $\mathcal{B}$, respectively.

\item Let $\bar{a} = (a_1 ,\dots, a_\ell)$ and $\bar{b} = (b_1 ,\dots, b_\ell)$ be finite, equally long sequences of elements of $\mathcal{A}$ and $\mathcal{B}$, respectively, not including the special constants $c_f$.

\item Let $\bar{\boldsymbol{\Phi}} = (\Phi_1 ,\dots, \Phi_p)$ and $\bar{\boldsymbol{\Psi}} = (\Psi_1,\dots, \Psi_p)$ be finite sequences of isomorphisms of equal length over $\mathcal{A}$ and $\mathcal{B}$, respectively.

\end{itemize}

Then $(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$ and $(\bar{\boldsymbol{\Delta}}^\prime, \bar{b}, \bar{\boldsymbol{\Psi}})$ define a {\em partial isomorphism} between structures\footnote{Note that this definition of partial isomorphism does not only include structures, but also update sets and isomorphisms defined over the structures, so in a sense it extends to all structures in runs with the same initial state.} $\mathcal{A}$ and $\mathcal{B}$ iff the following conditions hold:

\begin{enumerate}

\item for all $i,j \le k$ we have $\Delta_i = \Delta_j$ iff $\Delta_i^\prime = \Delta_j^\prime$, and $\Delta_i \subseteq \Delta_j$ iff $\Delta_i^\prime \subseteq \Delta_j^\prime$;

\item for all $i,j \le \ell$ we have $a_i = a_j$ iff $b_i = b_j$, $a_i \in a_j$ iff $b_i \in b_j$, and $a_i \subseteq a_j$ iff $b_i \subseteq b_j$;

\item for $f \in \Upsilon_{dyn}$, $i \le k$, $i_0 \le \ell$ and all sequences $(i_1 ,\dots, i_n)$ of indices $i_j \le \ell$ we have $(c_f, (a_{i_1} ,\dots, a_{i_n}), a_{i_0}) \in \Delta_i$ iff $(c_f, (b_{i_1} ,\dots, b_{i_n}), b_{i_0}) \in \Delta_i^\prime$;

\item for all sequences $(i_1 ,\dots, i_n)$ of indices $i_j \le \ell$ and all relation symbols $R \in \Upsilon_0$ of arity $n$ we have $R^{\mathcal{A}}(a_{i_1} ,\dots, a_{i_n})$ iff $R^{\mathcal{B}}(b_{i_1} ,\dots, b_{i_n})$;

\item for all $i_1, i_2 \le \ell$ and $j \le p$ we have that $\Phi_j(a_{i_1}, a_{i_2})$ holds iff $\Psi_j(b_{i_1}, b_{i_2})$ holds.

\end{enumerate}

\end{definition}

Note that these conditions imply that for all $i_1, i_2 \le k$ and $j \le p$ we have that $\Phi_j(\Delta_{i_1}) = \Delta_{i_2}$ holds iff $\Psi_j(\Delta_{i_1}^\prime) = \Delta_{i_2}^\prime$ holds.

Then a {\em separation game} over separation candidates $(C_1, C_2)$ is played by two players, called {\em spoiler} and {\em duplicator}, both having $m$ pebbles marked by numbers $1, \dots, m$. In every round first the spoiler makes a move, which is either an {\em (update) set move}, an {\em object move} or an {\em isomorphism move}, and the duplicator reacts with a set move, an object move or an isomorphism move, respectively:

\begin{description}

\item[(update) set move] The spoiler chooses a class $C_1$ or $C_2$ and places one of his pebbles (regardless, if used or not) on an update set over the common base set of the chosen class. The duplicator reacts by placing his pebble with the same number on an update set of the other class.

\item[object move] The spoiler chooses a class $C_1$ or $C_2$ and places one of his pebbles (regardless, if used or not) on an object of the common base set of the chosen class. The duplicator reacts by placing his pebble with the same number on an object of the other class.

\item[isomorphism move] The spoiler chooses a class $C_1$ or $C_2$ and places one of his pebbles (regardless, if used or not) on an isomorphism on the chosen class ($\Phi: B_1 \rightarrow B_1$ or $\Psi: B_2 \rightarrow B_2$, respectively). The duplicator reacts by placing his pebble with the same number on an isomorphism on the other class.

\end{description}

After each round, if $k$ update sets, $\ell$ objects and $p$ isomorphisms are marked by pebbles (with $k + \ell + p \le m$), the following conditions are checked:

\begin{itemize}

\item for each structure $\mathcal{A} \in C_1$ there exists a structure $\mathcal{B} \in C_2$ such that the sequences defined by the pebbles define a partial isomorphism between $\mathcal{A}$ and $\mathcal{B}$;

\item for each structure $\mathcal{B} \in C_2$ there exists a structure $\mathcal{A} \in C_1$ such that the sequences defined by the pebbles define a partial isomorphism between $\mathcal{A}$ and $\mathcal{B}$.

\end{itemize}

If both conditions are satisfied, the game continues with another round, otherwise the game is terminated and the spoiler has won. If the game continues forever, the duplicator wins.

Thus, we say that the duplicator has a {\em winning strategy} for a separation game iff he can ensure that after each move of the spoiler he is able to react with a move satisfying the two conditions above. If this is the case, we write $C_1 \equiv_{\infty\omega}^{ic,m} C_2$.

Note that for our purposes here we need to include the case of infinite structures\footnote{A similar pebble game has been exploited for CPT in \cite{blass:apal1999}, where also infinite structures had to be taken into account. However, the emphasis was on characterising equivalence of two structures.}, because Theorem \ref{thm-fixpoint2} shows that a formula expressing acceptance of an input structure $I$ is to hold in semi-transitive substructures of $\textit{HF\/}(I)$ containing all objects of active orbits in $\mathcal{A}[I]$, and these structures are not necessarily finite.

\subsection{Characterisation of Separability}

We can now approach the main result of this section. Let $B_1$ and $B_2$ denote the base sets of the structures $\mathcal{A} \in C_1$ and $\mathcal{B} \in C_2$, respectively. We have to consider partial maps $g: A \rightarrow B$ on objects as well as partial maps
\[ f: \mathcal{P}(\{ c_f \mid f \in \Upsilon_{dyn} \} \times \bigcup_{n \in \mathbb{N}} B_1^n \times B_1) \rightarrow \mathcal{P}(\{ c_f \mid f \in \Upsilon_{dyn} \} \times \bigcup_{n \in \mathbb{N}} B_2^n \times B_2) \]
on update sets, partial maps $q: Sym(A_1) \rightarrow Sym(A_2)$ on isomorphisms,and their union $h = g \oplus f \oplus q$. Let $dom(h)$ and $rng(h)$ denote the domain and the range of such partial functions, respectively.

As separation games may require infinitely many rounds, we consider ordinals denoted as $\alpha, \beta, \dots$. Let $(C_1, C_2)$ be a separation candidate. For an ordinal $\beta$ let $\mathcal{I}_\beta$ denote a set of partial isomorphisms between some $\mathcal{A} \in C_1$ and some $\mathcal{B} \in C_2$, and let $\mathcal{J}_\alpha = \{ \mathcal{I}_\beta \mid \beta < \alpha \}$. By abuse of terminology we call $\mathcal{I}_\beta$ a set of partial isomorphisms between $C_1$ and $C_2$.

\begin{definition}\label{def-backforth}\rm

The set $\mathcal{J}_\alpha$ of sets of partial isomorphisms has the {\em $m$-back-and-forth property} iff the following are satisfied:

\begin{enumerate}

\item For every $\beta < \alpha$ all structures $\mathcal{A} \in C_1$ and $\mathcal{B} \in C_2$ appear in $\mathcal{I}_\beta$.

\item $\mathcal{I}_\gamma \subseteq \mathcal{I}_\beta$ holds for $\beta < \gamma$.

\item Each set $\mathcal{I}_\beta$ is downward-closed, i.e. for $h \in \mathcal{I}_\beta$ and $h^\prime \subseteq h$ (i.e. $dom(h^\prime) \subseteq dom(h)$ and $h, h^\prime$ coincide on $dom(h^\prime)$) also $h^\prime \in \mathcal{I}_\beta$.

\item For every $h = g \oplus f \oplus q \in \mathcal{I}_{\beta + 1}$ with $| dom(h) | < m$ the following two conditions hold:

\begin{description}

\item[forth] for every object $a \in B_1$, every update set $\Delta$ over $B_1$ and every isomorphism $\Phi \in Sym(A_1)$ there is a $h^\prime \in \mathcal{I}_\beta$ with $h \subseteq h^\prime$ and $a \in dom(h^\prime)$ (then $h^\prime = g^\prime \oplus f \oplus q$) or $\Delta \in dom(h^\prime)$ (then $h^\prime = g \oplus f^\prime \oplus q$) or $\Phi \in dom(h^\prime)$ (then $h^\prime = g \oplus f \oplus q^\prime$), respectively;

\item[back] for every object $b \in B_2$, every update set $\Delta^\prime$ over $B_2$ and every isomorphism $\Psi \in Sym(A_2)$ there is a $h^\prime \in \mathcal{I}_\beta$ with $h \subseteq h^\prime$ and $b \in rng(h^\prime)$ (then $h^\prime = g^\prime \oplus f \oplus q$) or $\Delta^\prime \in rng(h^\prime)$ (then $h^\prime = g \oplus f^\prime \oplus q$), or $\Psi \in rng(h^\prime)$ (then $h^\prime = g \oplus f \oplus q^\prime$), respectively.

\end{description}

\end{enumerate}

\end{definition}

In the Ehrenfeucht-Fra\"{\i}ss\'{e} method games are just a reformulation of the back-and-forth property and vice versa. Indeed, the partial isomorphisms in $\mathcal{I}_\beta$ represent configurations of the game, when there are $\beta$ rounds left to play. For this properties (i)-(iii) in Definition \ref{def-backforth} are obvious, and property (iv) expresses that whatever move the spoiler may make, the duplicator finds a suitable reaction that establishes a partial isomorphism.

Recall that the semantics of the logic of non-deterministic ASMs has been defined as a Henkin semantics, i.e. in variable assignments $\zeta$ we have $\zeta(X) \in D_n$ for second-order variables $X$ of arity $n$. Update sets $X$ in formulae appearing within formulae $\text{upd}_r^{ic}(X)$ are then uniquely determined by the rules $r$, and thus their number is bounded by the bounded nesting of the rules.

\begin{theorem}\label{thm-pebble}

Two classes of structures forming a separation candidate $(C_1, C_2)$ are $\mathcal{L}^{ic,m}_{\infty\omega}$-inseparable for $m \in \mathbb{N}$ iff $C_1 \equiv_{\infty\omega}^{ic,m} C_2$ holds.

\end{theorem}

\begin{proof}

Due to our considerations above it suffices to show equivalence of the following two conditions:

\begin{enumerate}

\item For every formula $\varphi(\bar{X},\bar{x},\bar{Y})$ of $\mathcal{L}^{ic,m}_{\infty\omega}$ of quantifier rank $\beta < \alpha$ and $\text{mod-rk}(\varphi) = n$ there exists a sequence of partitions $\mathcal{P}_n \rhd \mathcal{P}_{n-1} \rhd\dots\rhd \mathcal{P}_0 = \{ (C_1, C_2) \}$ such that for all $\mathcal{A} \in C^n_{1i}$, $\mathcal{B} \in C^n_{2i}$ and all partial isomorphisms $h = g \oplus f \oplus q$ between $\mathcal{A}$ and $\mathcal{B}$ we have
\[ \mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}}) \quad\Leftrightarrow\quad \mathcal{B} \models\varphi(f(\bar{\boldsymbol{\Delta}}),g(\bar{a}),q(\bar{\boldsymbol{\Phi}})) \]
and $\mathcal{P}_j \rhd\dots\rhd \mathcal{P}_0$ is the sequence with the same property for all subformulae $\psi$ of $\varphi$ with $\text{mod-rk}(\psi) = j$.

\item There is a family $\mathcal{J}_\alpha = \{ \mathcal{I}_\beta \mid \beta < \alpha \}$ of sets of partial isomorphisms between $C_1$ and $C_2$ with the $m$-back-and-forth property.

\end{enumerate}

\paragraph*{\textbf{Part I: (1) $\Rightarrow$ (2)}}

For $\beta < \alpha$ we define $\mathcal{I}_\beta$ as the union of sets $\mathcal{I}_\beta(\psi)$, where $\psi(\bar{X},\bar{x},\bar{Y})$ is a subformula of $\varphi \in\mathcal{L}^{ic,m}_{\infty\omega}$ with quantifier rank $qr(\psi) \le \beta < \alpha$ and $\text{mod-rk}(\psi) = j$, and $\mathcal{I}_\beta(\psi)$ is the set of all partial isomorphisms $h = g \oplus f \oplus q$ between structures $\mathcal{A} \in C^j_{1i}$ and $\mathcal{B} \in C^j_{2i}$ with $| dom(h) | < m$, such that for every $(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}})$ contained in $dom(h)$ we have
\[ \mathcal{A} \models \psi(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}}) \quad\Leftrightarrow\quad \mathcal{B} \models \psi(f(\bar{\boldsymbol{\Delta}}),g(\bar{a}),q(\bar{\boldsymbol{\Phi}})) \; . \]
We show that $\mathcal{J}_\alpha = \{ \mathcal{I}_\beta \mid \beta < \alpha \}$ has the $m$-back-and-forth property.

The empty partial isomorphism between arbitrary $\mathcal{A} \in C^j_{1i}$ and $\mathcal{B} \in C^j_{2i}$ is in $\mathcal{I}_\beta$, which gives property (1) of Definition \ref{def-backforth}. The containment property (2) and the downward closure property (3) are immediate consequences of the definition of $\mathcal{I}_\beta$. Therefore, it remains to show property (4).

\paragraph*{\textbf{forth}}

Assume that there exists some $h = g \oplus f \oplus q \in \mathcal{I}_{\beta + 1}$ with $\beta + 1 < \alpha$ and $| dom(h) | < m$ violating the \textbf{forth} condition. Consider three cases:

\begin{description}

\item[Case a] First assume that there are structures $\mathcal{A} \in C^j_{1i}$ and $\mathcal{B} \in C^j_{2i}$ such that there is an object $a \in B_1$, but there is no object $b \in B_2$ such that $h$ can be extended to $h^\prime \in \mathcal{I}_\beta$ with $h^\prime(a) = b$. By the definition of $\mathcal{I}_\beta$ for every object $b \in B_2$ we find a formula $\varphi_b^{\mathcal{B}}(\bar{X},x_0,\bar{x},\bar{Y})$ of $\mathcal{L}^{ic,m}_{\infty\omega}$ with $qr(\varphi^{\mathcal{B}}_b) \le \beta$ such that for some $\bar{\boldsymbol{\Delta}}$, $\bar{a}$ and $\bar{\boldsymbol{\Phi}}$ contained in $dom(h)$ we have
\[ \mathcal{A} \models \varphi_b^{\mathcal{B}}(\bar{\boldsymbol{\Delta}}, a, \bar{a}, \bar{\boldsymbol{\Phi}}) \quad\text{and}\quad \mathcal{B} \models \neg\varphi_b^{\mathcal{B}}(f(\bar{\boldsymbol{\Delta}}),b,g(\bar{a}),q(\bar{\boldsymbol{\Phi}})) . \]
Define the formulae
\[ \varphi^{\mathcal{B}}(\bar{X},\bar{x},\bar{Y}) \;\equiv\; \exists x_0 . \bigwedge_{b \in B_2} \varphi_b^{\mathcal{B}}((\bar{X},x_0,\bar{x},\bar{Y}) \quad\text{and}\quad
\varphi(\bar{X},\bar{x},\bar{Y}) \;\equiv\; \bigwedge_{\mathcal{B} \in C^j_{2i}} \varphi^{\mathcal{B}}(\bar{X},\bar{x},\bar{Y}) \; . \]
Due to our assumption on the sequence $\mathcal{P}_j \rhd\dots\rhd \mathcal{P}_0$ of partitions these formulae are well-defined in $\mathcal{L}^{ic,m}_{\infty\omega}$.

Then we have $qr(\varphi) \le \beta + 1$ and $\mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}})$, but $\mathcal{B} \models \neg \varphi(f(\bar{\boldsymbol{\Delta}}),g(\bar{a}),q(\bar{\boldsymbol{\Phi}}))$ for all $\mathcal{B}\in C^j_{2i}$, which contradicts $h = g \oplus f \oplus q \in \mathcal{I}_{\beta + 1}$.

\item[Case b] Next assume that there are structures $\mathcal{A} \in C^j_{1i}$ and $\mathcal{B} \in C^j_{2i}$ such that there is an update set $\Delta$ over $B_1$, but no update set $\Delta^\prime$ over $B_2$ such that $h$ can be extended to $h^\prime \in \mathcal{I}_\beta$ with $h^\prime(\Delta) = \Delta^\prime$. By the definition of $\mathcal{I}_\beta$ for every update set $\Delta^\prime$ over $B_2$ we find a formula $\varphi_{\Delta^\prime}^{\mathcal{B}}(X,\bar{X},\bar{x},\bar{Y})$ of $\mathcal{L}^{ic,m}_{\infty\omega}$ with $qr(\varphi^{\mathcal{B}}_{\Delta^\prime}) \le \beta$ such that for some $\bar{\boldsymbol{\Delta}}$, $\bar{a}$ and $\bar{\boldsymbol{\Phi}}$ contained in $dom(h)$ we have
\[ \mathcal{A} \models \varphi_{\Delta^\prime}^{\mathcal{B}}(\Delta, \bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}}) \quad\text{and}\quad \mathcal{B} \models \neg\varphi_{\Delta^\prime}^{\mathcal{B}}(\Delta^\prime, f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}})) . \]
Define the formulae
\[ \varphi^{\mathcal{B}}(\bar{X},\bar{x},\bar{Y}) \;\equiv\; \exists X . \bigwedge_{\Delta^\prime} \varphi_{\Delta^\prime}^{\mathcal{B}}((X, \bar{X}, \bar{x}, \bar{Y}) \quad\text{and}\quad
\varphi(\bar{X},\bar{x},\bar{Y}) \;\equiv\; \bigwedge_{\mathcal{B} \in C^j_{2i}} \varphi^{\mathcal{B}}(\bar{X},\bar{x},\bar{Y}) \; . \]
Due to our assumption on the sequence $\mathcal{P}_j \rhd\dots\rhd \mathcal{P}_0$ of partitions these formulae are well-defined in $\mathcal{L}^{ic,m}_{\infty\omega}$.

Then we have $qr(\varphi) \le \beta + 1$ and $\mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}})$, but $\mathcal{B} \models \neg \varphi(f(\bar{\boldsymbol{\Delta}}),g(\bar{a}),q(\bar{\boldsymbol{\Phi}}))$ for all $\mathcal{B}\in C^j_{2i}$, which contradicts $h = g \oplus f \oplus q \in \mathcal{I}_{\beta + 1}$.

\item[Case c] Thirdly, assume that there are structures $\mathcal{A} \in C^j_{1i}$ and $\mathcal{B} \in C^j_{2i}$ such that there is an isomorphism $\Phi: A_1 \rightarrow A_1$, but there is no isomorphism $\Psi: A_2 \rightarrow A_2$ such that $h$ can be extended to $h^\prime \in \mathcal{I}_\beta$ with $h^\prime(\Phi) = \Psi$. By the definition of $\mathcal{I}_\beta$ for every isomorphism $\Psi: A_2 \rightarrow A_2$ we find a formula $\varphi_{\Psi}^{\mathcal{B}}(\bar{X},\bar{x},Y,\bar{Y})$ of $\mathcal{L}^{ic,m}_{\infty\omega}$ with $qr(\varphi^{\mathcal{B}}_{\Psi}) \le \beta$ such that for some $\bar{\boldsymbol{\Delta}}$, $\bar{a}$ and $\bar{\boldsymbol{\Phi}}$ contained in $dom(h)$ we have
\[ \mathcal{A} \models \varphi_{\Psi}^{\mathcal{B}}(\bar{\boldsymbol{\Delta}}, \bar{a}, \Phi, \bar{\boldsymbol{\Phi}}) \quad\text{and}\quad \mathcal{B} \models \neg\varphi_{\Psi}^{\mathcal{B}}(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), \Psi, q(\bar{\boldsymbol{\Phi}})) . \]
Define the formulae
\[ \varphi^{\mathcal{B}}(\bar{X},\bar{x},\bar{Y}) \;\equiv\; \exists Y . \bigwedge_{\Psi} \varphi_{\Psi}^{\mathcal{B}}((\bar{X}, \bar{x}, Y, \bar{Y}) \quad\text{and}\quad
\varphi(\bar{X},\bar{x},\bar{Y}) \;\equiv\; \bigwedge_{\mathcal{B} \in C^j_{2i}} \varphi^{\mathcal{B}}(\bar{X},\bar{x},\bar{Y}) \; . \]
Due to our assumption on the sequence $\mathcal{P}_j \rhd\dots\rhd \mathcal{P}_0$ of partitions these formulae are well-defined in $\mathcal{L}^{ic,m}_{\infty\omega}$.

Then we have $qr(\varphi) \le \beta + 1$ and $\mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}})$, but $\mathcal{B} \models \neg \varphi(f(\bar{\boldsymbol{\Delta}}),g(\bar{a}),q(\bar{\boldsymbol{\Phi}}))$ for all $\mathcal{B}\in C^j_{2i}$, which contradicts $h = g \oplus f \oplus q \in \mathcal{I}_{\beta + 1}$.

\end{description}

Next assume that there exists some $h = f \oplus g \in \mathcal{I}_{\beta + 1}$ with $| dom(h) | < m$ violating the \textbf{back} condition. We proceed analogously to the case of the forth condition. Again we have three cases:

\begin{description}

\item[Case a] First assume that there are structures $\mathcal{A} \in C^j_{1i}$ and $\mathcal{B} \in C^j_{2i}$ such that there is an object $b \in B_2$, but no object $a \in B_1$ such that $h$ can be extended to $h^\prime \in \mathcal{I}_\beta$ with $h^\prime(a) = b$. By the definition of $\mathcal{I}_\beta$ for every object $a \in B_1$ we find a formula $\varphi_a^{\mathcal{A}}(\bar{X},x_0,\bar{x},\bar{Y})$ of $\mathcal{L}^{ic,m}_{\infty\omega}$ with $qr(\varphi^{\mathcal{A}}_a) \le \beta$ such that for some $\bar{\boldsymbol{\Delta}}$, $\bar{a}$ and $\bar{\boldsymbol{\Phi}}$ contained in $dom(h)$ we have
\[ \mathcal{A} \models \neg \varphi_a^{\mathcal{A}}(\bar{\boldsymbol{\Delta}}, a, \bar{a}, \bar{\boldsymbol{\Phi}}) \quad\text{and}\quad \mathcal{B} \models \varphi_a^{\mathcal{A}}(f(\bar{\boldsymbol{\Delta}}), b, g(\bar{a}), q(\bar{\boldsymbol{\Phi}})) . \]
Define the formulae
\[ \varphi^{\mathcal{A}}(\bar{X},\bar{x},\bar{Y}) \;\equiv\; \exists x_0 . \bigwedge_{a \in B_1} \varphi_a^{\mathcal{A}}((\bar{X},x_0,\bar{x},\bar{Y}) \quad\text{and}\quad
\varphi(\bar{X},\bar{x},\bar{Y}) \;\equiv\; \bigwedge_{\mathcal{A} \in C^j_{1i}} \varphi^{\mathcal{A}}(\bar{X},\bar{x},\bar{Y}) \; . \]
Due to our assumption on the sequence $\mathcal{P}_j \rhd\dots\rhd \mathcal{P}_0$ of partitions these formulae are well-defined in $\mathcal{L}^{ic,m}_{\infty\omega}$.

Then we have $qr(\varphi) \le \beta + 1$ and $\mathcal{A} \models \neg \varphi(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}})$ for all $\mathcal{A}\in C^j_{1i}$, but $\mathcal{B} \models \neg \varphi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$, which contradicts $h = g \oplus f \oplus q \in \mathcal{I}_{\beta + 1}$.

\item[Case b] Next assume that there are structures $\mathcal{A} \in C^j_{1i}$ and $\mathcal{B} \in C^j_{2i}$ such that there is an update set $\Delta^\prime$ over $B_2$, but there is no update set $\Delta$ over $B_1$ such that $h$ can be extended to $h^\prime \in \mathcal{I}_\beta$ with $h^\prime(\Delta) = \Delta^\prime$. By the definition of $\mathcal{I}_\beta$ for every update set $\Delta$ over $B_1$ we find a formula $\varphi_{\Delta}^{\mathcal{A}}(X,\bar{X},\bar{x},\bar{Y})$ of $\mathcal{L}^{ic,m}_{\infty\omega}$ with $qr(\varphi^{\mathcal{A}}_{\Delta}) \le \beta$ such that for some $\bar{\boldsymbol{\Delta}}$, $\bar{a}$ and $\bar{\boldsymbol{\Phi}}$ contained in $dom(h)$ we have
\[ \mathcal{A} \models \neg \varphi_{\Delta}^{\mathcal{A}}(\Delta, \bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}}) \quad\text{and}\quad \mathcal{B} \models \varphi_{\Delta^\prime}^{\mathcal{B}}(\Delta^\prime, f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}})) . \]
Define the formulae
\[ \varphi^{\mathcal{A}}(\bar{X},\bar{x},\bar{Y}) \;\equiv\; \exists X . \bigwedge_{\Delta} \varphi_{\Delta}^{\mathcal{A}}((X, \bar{X}, \bar{x}, \bar{Y}) \quad\text{and}\quad
\varphi(\bar{X},\bar{x},\bar{Y}) \;\equiv\; \bigwedge_{\mathcal{A} \in C^j_{1i}} \varphi^{\mathcal{A}}(\bar{X},\bar{x},\bar{Y}) \; . \]
Due to our assumption on the sequence $\mathcal{P}_j \rhd\dots\rhd \mathcal{P}_0$ of partitions these formulae are well-defined in $\mathcal{L}^{ic,m}_{\infty\omega}$.

Then we have $qr(\varphi) \le \beta + 1$ and $\mathcal{A} \models \neg \varphi(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}})$  for all $\mathcal{A}\in C^j_{1i}$, but $\mathcal{B} \models \varphi(f(\bar{\boldsymbol{\Delta}}),g(\bar{a}),q(\bar{\boldsymbol{\Phi}}))$, which contradicts $h = g \oplus f \oplus q \in \mathcal{I}_{\beta + 1}$.

\item[Case c] Thirdly, assume that there are structures $\mathcal{A} \in C^j_{1i}$ and $\mathcal{B} \in C^j_{2i}$ such that there is an isomorphism $\Psi: A_2 \rightarrow A_2$, but no isomorphism $\Phi: A_1 \rightarrow A_1$ such that $h$ can be extended to $h^\prime \in \mathcal{I}_\beta$ with $h^\prime(\Phi) = \Psi$. By the definition of $\mathcal{I}_\beta$ for every isomorphism $\Phi: A_1 \rightarrow A_1$ we find a formula $\varphi_{\Phi}^{\mathcal{A}}(\bar{X},\bar{x},Y,\bar{Y})$ of $\mathcal{L}^{ic,m}_{\infty\omega}$ with $qr(\varphi^{\mathcal{A}}_{\Phi}) \le \beta$ such that for some $\bar{\boldsymbol{\Delta}}$, $\bar{a}$ and $\bar{\boldsymbol{\Phi}}$ contained in $dom(h)$ we have
\[ \mathcal{A} \models \neg \varphi_{\Phi}^{\mathcal{A}}(\bar{\boldsymbol{\Delta}}, \bar{a}, \Phi, \bar{\boldsymbol{\Phi}}) \quad\text{and}\quad \mathcal{B} \models \varphi_{\Phi}^{\mathcal{A}}(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), \Psi, q(\bar{\boldsymbol{\Phi}})) . \]
Define the formulae
\[ \varphi^{\mathcal{A}}(\bar{X},\bar{x},\bar{Y}) \;\equiv\; \exists Y . \bigwedge_{\Phi} \varphi_{\Phi}^{\mathcal{A}}((\bar{X}, \bar{x}, Y, \bar{Y}) \quad\text{and}\quad
\varphi(\bar{X},\bar{x},\bar{Y}) \;\equiv\; \bigwedge_{\mathcal{A} \in C^j_{1i}} \varphi^{\mathcal{A}}(\bar{X},\bar{x},\bar{Y}) \; . \]
Due to our assumption on the sequence $\mathcal{P}_j \rhd\dots\rhd \mathcal{P}_0$ of partitions these formulae are well-defined in $\mathcal{L}^{ic,m}_{\infty\omega}$.

Then we have $qr(\varphi) \le \beta + 1$ and $\mathcal{A} \models \neg \varphi(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}})$ for all $\mathcal{A}\in C^j_{1i}$, but $\mathcal{B} \models \varphi(f(\bar{\boldsymbol{\Delta}}),g(\bar{a}),q(\bar{\boldsymbol{\Phi}}))$, which contradicts $h = g \oplus f \oplus q \in \mathcal{I}_{\beta + 1}$.

\end{description}

\paragraph*{\textbf{Part II: (2) $\Rightarrow$ (1)}}

Now assume that there is a family $\mathcal{J}_\alpha = \{ \mathcal{I}_\beta \mid \beta < \alpha \}$ of sets of partial isomorphisms between $C_1$ and $C_2$ with the $m$-back-and-forth property. We use transfinite induction over $\beta < \alpha$ to show that for every formula $\varphi(\bar{X},\bar{x},\bar{Y})$ of $\mathcal{L}^{ic,m}_{\infty\omega}$ with $qr(\varphi) \le \beta$ satisfies (1).

For the induction base let $\beta = 0$. Then $\varphi$ is a Boolean or infinitary combination of atomic formulae. We may exclude formulae of the form $U_r(j,X)$, as these represent complex second-order formula (see the axioms \textbf{U0}-\textbf{U3} and \textbf{U4}$^\prime$ in Section 4.2) with quantifier rank $> 0$.

Let the partition $\mathcal{P}_0$ be trivial containing only the separation candidate $(C_1,C_2)$.
For a Boolean combination for each $\mathcal{A} \in C_1$ and each $\mathcal{B} \in C_2$, if $h = g \oplus f \oplus q \in \mathcal{I}_\beta$ is a partial isomorphism between $\mathcal{A}$ and $\mathcal{B}$, then
\[ \mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}}) \quad\Leftrightarrow\quad \mathcal{B} \models\varphi(f(\bar{\boldsymbol{\Delta}}),g(\bar{a}),q(\bar{\boldsymbol{\Phi}})) \]
follows immediately from the conditions of Definition \ref{def-po}.
For a formula $\varphi \equiv \bigvee_{i \in I} \varphi_i$ we must have $qr(\varphi_i) = 0$ for all $i \in I$. So each $\varphi_i$ is a Boolean combination of atomic formulae, and the required condition follows again from the conditions of Definition \ref{def-po}.

For the induction step let $\beta > 0$ and assume that the induction hypothesis holds for all formulae with quantifier rank $\gamma < \beta$. If $\beta$ is a limit ordinal and $qr(\varphi) = \beta$ holds, this is only possible, if $\varphi$ is an infinite disjunction or conjunction, say $\varphi \equiv \bigvee_{i \in I} \varphi_i$ or $\varphi \equiv \bigwedge_{i \in I} \varphi_i$. Then we must have $qr(\varphi_i) < qr(\varphi)$ for all $i \in I$. Furthermore, $\text{mod-rk}(\varphi_i) = \text{mod-rk}(\varphi)$ for all $i \in I$.

According to our induction hypothesis there is a fixed sequence of partitions $\mathcal{P}_j \rhd\dots\rhd \mathcal{P}_0$ (with $j = \text{mod-rk}(\varphi)$) such that for all $\mathcal{A} \in C^j_{1i}$, $\mathcal{B} \in C^j_{2i}$ and all partial isomorphisms $h = g \oplus f \oplus q$ between $\mathcal{A}$ and $\mathcal{B}$ we have
\[ \mathcal{A} \models \varphi_\imath(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}}) \quad\Leftrightarrow\quad \mathcal{B} \models\varphi_\imath(f(\bar{\boldsymbol{\Delta}}),g(\bar{a}),q(\bar{\boldsymbol{\Phi}})) \]
for all $\imath \in I$, which immediately implies
\[ \mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}}) \quad\Leftrightarrow\quad \mathcal{B} \models\varphi(f(\bar{\boldsymbol{\Delta}}),g(\bar{a}),q(\bar{\boldsymbol{\Phi}})) \; . \]

Assume from now on that $\beta$ is not a limit ordinal. If $\varphi$ is a Boolean or infinitary combination, we proceed by structural induction. The case of Boolean combinations follows immediately from the induction hypothesis, as the partition sequence to be used for $\varphi$ is the same as the partition sequence for all subformulae in the Boolean combination. Likewise, for an infinite combination $\varphi \equiv \bigvee_{i \in I} \varphi_i$, if $qr(\varphi_i) = \beta$ holds for all at least one $i \in I$, then $\beta$, we can exploit the induction hypothesis for all $\varphi_i$ ($i \in I$) using a fixed sequence of partitions.

For quantified formulae we have to consider the cases

\begin{enumerate}

\item $\varphi(\bar{X}, \bar{x}, \bar{Y}) \equiv \exists x_0 . \psi(\bar{X}, x_0, \bar{x}, \bar{Y})$,

\item $\varphi(\bar{X},\bar{x}) \equiv \exists X_0 . \text{isUSet}(X_0) \wedge \psi(X_0, \bar{X}, \bar{x}, \bar{Y})$ and

\item $\varphi(\bar{X},\bar{x}, \bar{Y}) \equiv \exists Y_0 . \text{iso}(Y_0) \wedge \psi(\bar{X}, \bar{x}, Y_0, \bar{Y})$.

\end{enumerate}

\begin{description}

\item[\textbf{(1)}] First consider the case of first-order quantification, i.e. we have $\varphi(\bar{X},\bar{x}) \equiv \exists x_0 . \psi(\bar{X}, x_0, \bar{x}, \bar{Y})$ with $qr(\varphi) = \beta + 1 < \alpha$ and $qr(\psi) = \beta$. Without loss of generality we can assume that $x_0$ does not occur in $\bar{x}$ and thus $k + \ell + p < m$, where $k$ is the length of $\bar{X}$, $\ell$ the length of $\bar{x}$ and $p$ is the length of $\bar{Y}$. If $\text{mod-rk}(\varphi) = n$, then also $\text{mod-rk}(\psi) = n$. By induction let $\mathcal{P}_n \rhd\dots\rhd \mathcal{P}_0$ be the sequence of partitions defined by $\psi$.

Let $h = g \oplus f \oplus q \in \mathcal{I}_{\beta+1}$ be a partial isomorphism between $\mathcal{A} \in C^n_{1i}$ and $\mathcal{B} \in C^n_{2i}$, and take a sequence $\bar{\boldsymbol{\Delta}} = \Delta_1, \dots, \Delta_k$ of update sets over $\mathcal{A}$, a sequence $\bar{a} = (a_1, \dots, a_\ell)$ of objects of $\mathcal{A}$, and a sequence $\bar{\boldsymbol{\Phi}} = \Phi_1, \dots, \Phi_p$ of isomorphisms over $\mathcal{A}$. As $\mathcal{I}_{\beta+1}$ is downward-closed, we can assume $dom(h) = \{ \Delta_1, \dots, \Delta_k, a_1, \dots, a_\ell, \Phi_1,$ $\dots, \Phi_p \}$.

If $\mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$ holds, we get $\mathcal{A} \models \psi(\bar{\boldsymbol{\Delta}}, a_0, \bar{a}, \bar{\boldsymbol{\Phi}})$ for some object $a_0 \in B_1$. Using the \textbf{forth} property for $h$ we find an extension $h^\prime \in \mathcal{I}_\beta$ with $a_0 \in dom(h^\prime)$. Applying the induction hypothesis for $\psi$ we derive $\mathcal{B} \models \psi(f(\bar{\boldsymbol{\Delta}}), h^\prime(a_0), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$ and further $\mathcal{B} \models \varphi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$.

Conversely, if $\mathcal{B} \models \varphi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$ holds, we get $\mathcal{B} \models \psi(f(\bar{\boldsymbol{\Delta}}), b_0, g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$ for some object $b_0 \in B_2$. Using the \textbf{back} property for $h$ we find an extension $h^\prime \in \mathcal{I}_\beta$ with $b_0 \in rng(h^\prime)$, say $b_0 = h^\prime(a_0)$. Applying the induction hypothesis for $\psi$ we derive $\mathcal{A} \models \psi(\bar{\boldsymbol{\Delta}}, a_0, \bar{a}, \bar{\boldsymbol{\Phi}})$ and further $\mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$.

\item[\textbf{(2)}] Next consider second-order quantification over update sets, i.e. $\varphi(\bar{X},\bar{x}, \bar{Y}) \equiv \exists X_0 . \text{isUSet}(X_0) \wedge \psi(X_0, \bar{X}, \bar{x}, \bar{Y})$ with $qr(\varphi) = \beta + 1 < \alpha$ and $qr(\psi) = \beta$, in particular $X_0$ has arity 3. Without loss of generality we can assume that $X_0$ does not occur in $\bar{X}$ and thus $k + \ell + p < m$, where $k$ is the length of $\bar{X}$, $\ell$ the length of $\bar{x}$ and $p$ is the length of $\bar{Y}$. If $\text{mod-rk}(\varphi) = n$, then also $\text{mod-rk}(\psi) = n$. By induction let $\mathcal{P}_n \rhd\dots\rhd \mathcal{P}_0$ be the sequence of partitions defined by $\psi$.

Let $h = g \oplus f \oplus q \in \mathcal{I}_{\beta+1}$ be a partial isomorphism between $\mathcal{A} \in C^n_{1i}$ and $\mathcal{B} \in C^n_{2i}$. Then take a sequence $\bar{\boldsymbol{\Delta}} = \Delta_1, \dots, \Delta_k$ of update sets over $\mathcal{A}$, a sequence $\bar{a} = (a_1, \dots, a_\ell)$ of objects of $\mathcal{A}$ and a sequence $\bar{\boldsymbol{\Phi}} = \Phi_1, \dots, \Phi_p$ of isomorphisms over $\mathcal{A}$. As $\mathcal{I}_{\beta+1}$ is downward-closed, we can assume $dom(h) = \{ \Delta_1, \dots, \Delta_k, a_1, \dots, a_\ell, \Phi_1,$ $\dots, \Phi_p \}$.

If $\mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$ holds, we get $\mathcal{A} \models \psi(\Delta_0, \bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$ for some update set $\Delta_0$ over $\mathcal{A}$. Using the \textbf{forth} property for $h$ we find an extension $h^\prime \in \mathcal{I}_\beta$ with $\Delta_0 \in dom(h^\prime)$. Applying the induction hypothesis for $\psi$ we derive $\mathcal{B} \models \psi(h^\prime(\Delta_0), f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$ and further $\mathcal{B} \models \text{isUSet}(h^\prime(\Delta_0))$ and $\mathcal{B} \models \varphi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$.

Conversely, if $\mathcal{B} \models \varphi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$ holds, we get $\mathcal{B} \models \psi(\Delta_0^\prime, f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$ for some update set $\Delta_0^\prime$ over $\mathcal{B}$. Using the \textbf{back} property for $h$ we find an extension $h^\prime \in \mathcal{I}_\beta$ with $\Delta_0^\prime \in rng(h^\prime)$, say $h^\prime(\Delta_0) = \Delta_0^\prime$. Applying the induction hypothesis for $\psi$ we derive $\mathcal{A} \models \psi(\Delta_0, \bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$ and hence $\mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$.

\item[\textbf{(3)}] Next consider second-order quantification over isomorphisms, i.e. $\varphi(\bar{X},\bar{x}, \bar{Y})$ $\equiv \exists Y_0 . \text{iso}(Y_0) \wedge \psi(\bar{X}, \bar{x}, Y_0, \bar{Y})$ with $qr(\varphi) = \beta + 1 < \alpha$ and $qr(\psi) = \beta$, in particular $Y_0$ has arity 2. Without loss of generality we can assume that $Y_0$ does not occur in $\bar{Y}$ and thus $k + \ell + p < m$, where $k$ is the length of $\bar{X}$, $\ell$ the length of $\bar{x}$ and $p$ is the length of $\bar{Y}$. If $\text{mod-rk}(\varphi) = n$, then also $\text{mod-rk}(\psi) = n$. By induction let $\mathcal{P}_n \rhd\dots\rhd \mathcal{P}_0$ be the sequence of partitions defined by $\psi$.

Let $h = g \oplus f \oplus q \in \mathcal{I}_{\beta+1}$ be a partial isomorphism between $\mathcal{A} \in C^n_{1i}$ and $\mathcal{B} \in C^n_{2i}$. Then take a sequence $\bar{\boldsymbol{\Delta}} = \Delta_1, \dots, \Delta_k$ of update sets over $\mathcal{A}$, a sequence $\bar{a} = (a_1, \dots, a_\ell)$ of objects of $\mathcal{A}$ and a sequence $\bar{\boldsymbol{\Phi}} = \Phi_1, \dots, \Phi_p$ of isomorphisms over $\mathcal{A}$. As $\mathcal{I}_{\beta+1}$ is downward-closed, we can assume $dom(h) = \{ \Delta_1, \dots, \Delta_k, a_1, \dots, a_\ell, \Phi_1,$ $\dots, \Phi_p \}$.

If $\mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$ holds, we get $\mathcal{A} \models \psi(\bar{\boldsymbol{\Delta}}, \bar{a}, \Phi_0, \bar{\boldsymbol{\Phi}})$ for some isomorphism $\Phi_0$ over $\mathcal{A}$. Using the \textbf{forth} property for $h$ we find an extension $h^\prime \in \mathcal{I}_\beta$ with $\Phi_0 \in dom(h^\prime)$. Applying the induction hypothesis for $\psi$ we derive $\mathcal{B} \models \text{iso}(h^\prime(\Phi_0))$ and $\mathcal{B} \models \psi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), h^\prime(\Phi_0),  q(\bar{\boldsymbol{\Phi}}))$, hence $\mathcal{B} \models \varphi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$.

Conversely, if $\mathcal{B} \models \varphi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$ holds, we get $\mathcal{B} \models \psi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), \Psi_0, q(\bar{\boldsymbol{\Phi}}))$ for some isomorphism $\Psi_0$ over $\mathcal{B}$. Using the \textbf{back} property for $h$ we find an extension $h^\prime \in \mathcal{I}_\beta$ with $\Psi_0 \in rng(h^\prime)$, say $h^\prime(\Phi_0) = \Psi_0$. Applying the induction hypothesis for $\psi$ we derive $\mathcal{A} \models \psi(\bar{\boldsymbol{\Delta}}, \bar{a}, \Phi, \bar{\boldsymbol{\Phi}})$ and hence $\mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$.

\end{description}

This leaves the case, where $\varphi(\bar{X},\bar{x},\bar{Y}) \equiv U_r(j,X)$ with $j \ge 0$ and a second-order variable $X$ of arity $3$, which results from $\text{upd}_r^{ic}(X)$ by replacing every atomic subformula of the form $g(\bar{u}) = t$ with dynamic function symbol $g$ by
\[ \exists Z . (D_g(j,\bar{u},t, Z) \wedge t \neq 0) \vee (t = 0 \wedge \neg \exists z . D_g(j, \bar{u}, z, Z)) .\]
According to the definition of $\text{upd}_r^{ic}(X)$ these formulae include subformulae of the form $\varphi \equiv [X^\prime] \text{upd}_r(Y)$ hold (see the axioms \textbf{U0}-\textbf{U3} and \textbf{U4}$^\prime$ in Section 4.2). That is, such formulae represent complex second-order formulae, and we proceed by structural induction over $r$.

\begin{description}

\item[skip] For $r = \;\textbf{skip}$ we have $\text{upd}^{ic}_r(X) \leftrightarrow \forall x, y, z. \neg X(x,y,z)$. There is nothing to be substituted, so this case is already covered by first-order quantification.

\item[assignment] If $r$ is an assignment rule $f(t_1, \dots, t_n) := t_0$ we have
\begin{align*}
\text{upd}^{ic}_r(X) \leftrightarrow & \text{isUSet}(X) \wedge \forall x_1, x_2, x_3 . ( X(x_1, x_2, x_3) \leftrightarrow \\
& \hspace*{3.5cm} x_1 = c_f \wedge x_2 = (t_1, \dots, t_n) \wedge x_3 = t_0 ) \; ,
\end{align*}
so again the cases of first-order quantification and Boolean combinations suffice to cover this case as well.

\item[branching] For $r$ of the form \textbf{if} $\varphi$ \textbf{then} $r_1$ \textbf{else} $r_2$ \textbf{endif} we have that $\text{upd}^{ic}_r(X)$ is a Boolean combination of atomic formulae and $\text{upd}^{ic}_{r_1}(X)$ and $\text{upd}^{ic}_{r_2}(X)$. Then also $U_r(j,X)$ is a Boolean combination of atomic formulae and $U_{r_1}(j,X)$ and $U_{r_2}(j,X)$, so the claim follows immediately by induction using the sequence of partitions defined by $\text{upd}^{ic}_{r_1}(X)$ and $\text{upd}^{ic}_{r_2}(X)$.

\item[parallelism] Let $r$ be a rule \textbf{forall} $v \in t$ \textbf{do} $r^\prime(v)$ \textbf{enddo}. Then we have
\begin{align*}
\text{upd}_r^{ic}(X) \leftrightarrow \; &\text{isUSet}(X) \wedge
\exists Y. [ ( \bigwedge_{f \in \Upsilon_{dyn}} \forall y, z. X(c_f,y,z) \leftrightarrow \exists x . Y(c_f,y,z,x) ) \\
\wedge \forall x . & (x \in t \rightarrow \exists Z . \text{upd}_{r^\prime(x)}^{ic}(Z) \wedge \bigwedge_{f \in \Upsilon_{dyn}} \forall y,z . (Z(c_f,y,z) \leftrightarrow Y(c_f,y,z,x))) \\
& \wedge \forall x . (x \notin t \rightarrow \bigwedge_{f \in \Upsilon_{dyn}} \forall y,z . \neg Y(c_f,y,z,x)) ]
\end{align*}
Then we obtain $U_r(X)$ by replacing $\text{upd}_{r^\prime(x)}^{ic}(Z)$ on the right hand side by $U_{r^\prime(x)}(Z)$.

Consider the sequence $\mathcal{P}_n \rhd\dots\rhd \mathcal{P}_0$ defined by $\text{upd}_{r^\prime(x)}^{ic}(Z)$, which exists by induction and satisfies the property in (1). Take $h = g \oplus f \oplus q \in \mathcal{I}_{\beta+1}$ with $\bar{\boldsymbol{\Delta}}, \bar{a} \in dom(h)$. Let $\mathcal{A} \in C^n_{1i}$ and $\mathcal{B} \in C^n_{2i}$.

First assume that we have $\mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$. Then without loss of generality we have $\mathcal{A} \models \text{isUSet}(\Delta_1)$, and there exists a set $U$ with the following properties:

\begin{itemize}

\item $\bigwedge\limits_{f \in \Upsilon_{dyn}} \forall y,z . (c_f,y,z) \in \Delta_1 \leftrightarrow \exists x. (c_f,y,z,x) \in U$.

\item For all $x$ with $\mathcal{A} \models x \in t$ there exists a set $U_x$ with
\[ \mathcal{A} \models U_{r^\prime(x)} (j,U_x) \wedge \bigwedge_{f \in \Upsilon_{dyn}} \forall y,z. ( (c_f,y,x) \in U_x \leftrightarrow (c_f,y,z,x) \in U ) \; . \]

\item For all $x$ with $\mathcal{A} \models x \notin t$ we have $\mathcal{A} \models \bigwedge\limits_{f \in \Upsilon_{dyn}} \forall y,z. (c_f,y,z,x) \notin U$.

\end{itemize}

The last two of these properties imply $U = \bigcup \{ (c_f,y,z,x) \mid \mathcal{A} \models x \in t,\; f \in \Upsilon_{dyn}, \; (c_f,y,x) \in U_x \}$. Let $T = \{ x \mid \mathcal{A} \models x \in t \}$ and $k = |T|$. Then the first property further implies $\Delta_1 = \bigcup\limits_{x \in T} U_x$.

As we have $\mathcal{A} \models \bigwedge\limits_{x \in T} U_{r^\prime(x)}(j,U_x) (\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$, we can use induction for the rules $r^\prime(x)$ and apply $k$ times the \textbf{forth} property to extend $h$ to $h^\prime \in \mathcal{I}_\gamma$ ($\gamma < \beta$) such that $\mathcal{B} \models \bigwedge\limits_{x \in T} U_{r^\prime(x)}(j,h^\prime(U_x)) (h(\bar{\boldsymbol{\Delta}}), h(\bar{a}), h(\bar{\boldsymbol{\Phi}}))$. Then with $\Delta_1^\prime = \bigcup\limits_{x \in T} h^\prime(U_x) = h(\Delta_1)$ (due to the properties of partial isomorphisms) we get $\mathcal{B} \models \varphi(h(\bar{\boldsymbol{\Delta}}), h(\bar{a}), h(\bar{\boldsymbol{\Phi}}))$.

Conversely, assume that we have $\mathcal{B} \models \varphi(h(\bar{\boldsymbol{\Delta}}), h(\bar{a}), h(\bar{\boldsymbol{\Phi}}))$, and without loss of generality we have $\mathcal{B} \models \text{isUSet}(h(\Delta_1))$. Then there exists a set $V$ with the following properties:

\begin{itemize}

\item $\bigwedge\limits_{f \in \Upsilon_{dyn}} \forall y,z . (c_f,y,z) \in h(\Delta_1) \leftrightarrow \exists x. (c_f,y,z,x) \in V$.

\item For all $x$ with $\mathcal{B} \models x \in t$ there exists a set $V_x$ with
\[ \mathcal{B} \models U_{r^\prime(x)} (j,V_x) \wedge \bigwedge_{f \in \Upsilon_{dyn}} \forall y,z. ( (c_f,y,x) \in V_x \leftrightarrow (c_f,y,z,x) \in V ) \; . \]

\item For all $x$ with $\mathcal{B} \models x \notin t$ we have $\mathcal{B} \models \bigwedge\limits_{f \in \Upsilon_{dyn}} \forall y,z. (c_f,y,z,x) \notin V$.

\end{itemize}

The last two of these properties imply $V = \bigcup \{ (c_f,y,z,x) \mid \mathcal{B} \models x \in t,\; f \in \Upsilon_{dyn}, \; (c_f,y,x) \in V_x \}$. Let $T = \{ x \mid \mathcal{B} \models x \in t \}$ and $k = |T|$. Then the first property further implies $h(\Delta_1) = \bigcup\limits_{x \in T} V_x$.

As we have $\mathcal{B} \models \bigwedge\limits_{x \in T} U_{r^\prime(x)}(j,V_x) (h(\bar{\boldsymbol{\Delta}}), h(\bar{a}), h(\bar{\boldsymbol{\Phi}}))$, we can use induction for the rules $r^\prime(x)$ and apply $k$ times the \textbf{back} property to extend $h$ to $h^\prime \in \mathcal{I}_\gamma$ ($\gamma < \beta$) such that $h^\prime(U_x) = V_x$, so we get $\mathcal{A} \models \bigwedge\limits_{x \in T} U_{r^\prime(x)}(j,U_x) (\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$. Then with $\Delta_1 = \bigcup\limits_{x \in T} U_x$ we get $\mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$.

\item[choice] For a choice rule $r$ of the form \textbf{choose} $v \in \{ x \mid x \in \textit{Atoms\/} \wedge x \in t \}$ \textbf{do} $r^\prime(v)$ \textbf{enddo} we have
\begin{align*}
\text{upd}&^{ic}_r(X) \leftrightarrow \exists v. v \in \textit{Atoms\/} \wedge v \in t \wedge \;\text{upd}^{ic}_{r^\prime(v)}(X) \wedge \\
& \forall Y. (\exists x. x \in \textit{Atoms\/} \wedge x \in t \wedge \;\text{upd}^{ic}_{r^\prime(x)}(Y) ) \rightarrow
\exists Z. ( \text{iso}(Z) \wedge \\
& \hspace*{3.5cm} \textit{updIso\/}(X,Y,Z) \wedge \textit{updIsoSet\/}(X,Y,Z) )
\end{align*}
according to axiom \textbf{U4}$^\prime$ and further
\begin{align*}
\text{updIso}(X,& Y,Z) \equiv \\
\bigwedge_{f \in \Upsilon_{dyn}} & [ \forall \bar{x}_1, x_2, \bar{y}_1, y_2 .
( X(c_f, \bar{x}_1, x_2) \wedge \bigwedge_{1 \le i \le ar(f)} Z(x_{1i}, y_{1i}) \wedge Z(x_2,y_2) \\
& \hspace*{7cm} \rightarrow Y(c_f, \bar{y}_1, y_2) ) \\
& \wedge \forall \bar{x}_1, x_2, \bar{y}_1, y_2 .
( Y(c_f, \bar{x}_1, x_2) \wedge \bigwedge_{1 \le i \le ar(f)} Z(x_{1i}, y_{1i}) \wedge Z(x_2,y_2) \\
& \hspace*{7cm} \rightarrow X(c_f, \bar{y}_1, y_2) ) ]
\end{align*}
and
\begin{align*}
\text{updIsoSet}(X,& Y, Z) \equiv & \\
\forall Y_1, Y_2 . & (\text{isUSet}(Y_1) \wedge \text{isUSet}(Y_2) \wedge \text{updIso}(Y_1,Y_2,Z)) \rightarrow \\
& ([X]\text{upd}_r(Y_1) \leftrightarrow [Y]\text{upd}_r(Y_2))
\end{align*}

We obtain $U_r(j,X)$ by replacing in the first of these formulae $\text{upd}^{ic}_{r^\prime(v)}(X)$ by $U_{r^\prime(v)}(j,X)$ and $\text{upd}^{ic}_{r^\prime(x)}(Y)$ by $U_{r^\prime(x)}(j,Y)$, and by replacing in $\text{updIsoSet}(X, Y, Z)$ the subformula $[X]upd_r(Y_1)$ by $[X]U_r^\prime(j,Y_1)$ with $U_r^\prime(j,Y_1) \equiv \exists v. v \in \textit{Atoms\/} \wedge v \in t \wedge \;U_{r^\prime(v)}(j,Y_1)$ and likewise $[Y]\text{upd}_r(Y_2)$ by $[Y]U_r^\prime(j,Y_2)$ with $U_r^\prime(j,Y_2) \equiv \exists v. v \in \textit{Atoms\/} \wedge v \in t \wedge \;U_{r^\prime(v)}(j,Y_2))$. Then we must have $\beta = \gamma + 2$ for some ordinal $\gamma$.

To all occurrences of subformulae of the form $\psi \equiv U_{r^\prime(x)}(j,Y)$ we can apply the induction hypothesis. Let $\mathcal{P}_n \rhd\dots\rhd \mathcal{P}_0$ be the sequence of partitions guaranteed by the induction hypothesis for these subformulae. Then for any structures $\mathcal{A} \in C^n_{1i}$ and $\mathcal{B} \in C^n_{2i}$ and any partial isomorphism $h = g \oplus f \oplus q \in \mathcal{I}_\beta$ between $\mathcal{A}$ and $\mathcal{B}$ we have
\[ \mathcal{A} \models \psi(\bar{\boldsymbol{\Delta}},\bar{a},\bar{\boldsymbol{\Phi}}) \quad\Leftrightarrow\quad \mathcal{B} \models\psi(f(\bar{\boldsymbol{\Delta}}),g(\bar{a}),q(\bar{\boldsymbol{\Phi}})) \; . \]

This will still hold for structures $\mathcal{A} \in C^{n+1}_{1i}$ and $\mathcal{B} \in C^{n+1}_{2i}$, if we refine the partition $\mathcal{P}_n$, i.e. extend the sequence by $\mathcal{P}_{n+1} \rhd \mathcal{P}_n$.

Consider now the subformulae of the form $\chi \equiv [X] U_r^\prime(j,Y)$. First take a structure $\mathcal{A} \in C^n_{1i}$ with $\mathcal{A} \models \chi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$, so without loss of generality we may assume $\mathcal{A} \models [\Delta_1] U^\prime_r(j,\Delta_2)$. Then there are are two possibilities:

\begin{enumerate}

\item $\Delta_1$ is inconsistent, i.e. $\mathcal{A} \models \neg \text{ConUSet}(\Delta_1)$. The formula $\psi(\bar{X},\bar{x}) \equiv \text{ConUSet}(X_1)$ has quantifier rank 2 and uses only first-order quantification. Using the already proven cases for Boolean combinations and first-order quantification we can take any structure $\mathcal{B} \in C^n_{2i}$ such that $h$ is a partial isomorphism between $\mathcal{A}$ and $\mathcal{B}$, and obtain $\mathcal{B} \models \neg \text{ConUSet}(h(\Delta_1))$, i.e. $\mathcal{B} \models \chi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$.

\item $\Delta_1$ is consistent, i.e. $\mathcal{A} \models \text{ConUSet}(\Delta_1)$, and $\mathcal{A} + \Delta_1 \models U^\prime_r(j,\Delta_2)$. As $\mathcal{A} + \Delta_1 \in C^n_{2i}$, then by the induction hypothesis we get $\mathcal{B}^\prime \models U_r^\prime(j,f(\Delta_2))$ for all $\mathcal{B}^\prime \in C^n_{2i}$, provided that $h$ defines a partial isomorphism between $\mathcal{A} + \Delta_1$ and $\mathcal{B}^\prime$. Clearly, there are structures $\mathcal{B} \in C^n_{2i}$ (invert the updates in $f(\Delta_1)$) with $\mathcal{B} + f(\Delta_1) = \mathcal{B}^\prime$. For these we get $\mathcal{B} \models \text{ConUSet}(f(\Delta_1))$ and further $\mathcal{B} \models [ f(\Delta_1) ] U_r^\prime (j, f(\Delta_2))$, i.e. $\mathcal{B} \models \chi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$.

\end{enumerate}

Conversely, let $\mathcal{B} \in C^n_{2i}$ with $\mathcal{B} \models \chi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}}))$. Without loss of generality we can assume that $\mathcal{B} \models [ f(\Delta_1) ] U_r^\prime (j, f(\Delta_2))$ holds. Then again we have two possibilities:

\begin{enumerate}\setcounter{enumi}{2}

\item $f(\Delta_1)$ is inconsistent, i.e. $\mathcal{B} \models \neg \text{ConUSet}(f(\Delta_1))$. Again we can take any structure $\mathcal{A} \in C^n_{1i}$ such that $h$ is a partial isomorphism between $\mathcal{A}$ and $\mathcal{B}$, and obtain $\mathcal{A} \models \neg \text{ConUSet}(\Delta_1)$, hence also $\mathcal{A} \models \chi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$.

\item $f(\Delta_1)$ is consistent, i.e. $\mathcal{B} \models \text{ConUSet}(f(\Delta_1))$, and $\mathcal{A} + f(\Delta_1) \models U^\prime_r(j,f(\Delta_2))$. By induction we get $\mathcal{A}^\prime \models U_r^\prime(\Delta_2)$ for all $\mathcal{A}^\prime \in C^n_{1i}$, provided that $h$ defines a partial isomorphism between $\mathcal{A}^\prime$ and $\mathcal{B} + f(\Delta_1)$. There are structures $\mathcal{A} \in C^n_{1i}$ with $\mathcal{A} + \Delta_1 = \mathcal{A}^\prime$, and for these we get $\mathcal{A} \models \text{ConUSet}(\Delta_1)$ and further $\mathcal{A} \models [ \Delta_1 ] U_r^\prime (j, \Delta_2)$, i.e. $\mathcal{A} \models \chi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$.

\end{enumerate}

However, subformulae of the form $\chi \equiv [X] U_r^\prime(j,Y)$ appear only in the subformula $\text{updIsoSet}(X, Y, Z)$ (with the substitution), and in order to lift the argument we need to consider simultaneously all update sets that are isomorphic to $\Delta_1$ (or $f(\Delta_1))$, respectively. That is, the structure $\mathcal{B}$ in (2) must satisfy $\mathcal{B} + f(\Delta) = \mathcal{B}^\prime_\Delta$ for all $\Delta$ isomorphic to $\Delta_1$, where $\mathcal{B}^\prime_\Delta \in C^n_{2i}$ is defined by $\mathcal{A}$, $\Delta$ and $h$. Analogously, the structure $\mathcal{A}$ in (4) must satisfy $\mathcal{A} + \Delta = \mathcal{A}^\prime_{\Delta^\prime}$ for all $\Delta^\prime$ isomorphic to $f(\Delta_1)$, where $\mathcal{A}^\prime_{\Delta^\prime} \in C^n_{1i}$ is defined by $\mathcal{B}$, $\Delta^\prime$ and $h$.

We therefore consider the following property for structures $\mathcal{A} \in C^n_{1i}$ and $\mathcal{B} \in C^n_{2i}$:

\begin{quote}

\textbf{(*)} Whenever $h = g \oplus f \oplus q$ is a partial isomorphism between $\mathcal{A} + \Delta$ and $\mathcal{B} + f(\Delta)$ satisfying
\[ \mathcal{A} + \Delta \models \varphi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}}) \Leftrightarrow \mathcal{B} + f(\Delta) \models \varphi(f(\bar{\boldsymbol{\Delta}}), g(\bar{a}), q(\bar{\boldsymbol{\Phi}})) \; , \]
then for any $\Delta^\prime$ that is isomorphic to $\Delta$ $h$ is also a partial isomorphism between $\mathcal{A} + \Delta^\prime$ and $\mathcal{B} + f(\Delta^\prime)$ satisfying the same property, and the same holds for update sets isomorphic to $f(\Delta)$.

\end{quote}

Then we observe the following properties:

\begin{itemize}

\item For every $\mathcal{A} \in C^n_{1i}$ there exists some $\mathcal{B} \in C^n_{2i}$ (and for every $\mathcal{B} \in C^n_{2i}$ there exists some $\mathcal{A} \in C^n_{1i}$) satisfying the property \textbf{(*)}.

\item If $(\mathcal{A}, \mathcal{B})$ satisfy the property \textbf{(*)}, then also $(\mathcal{A}^\prime, \mathcal{B}^\prime)$ satisfy \textbf{(*)}, where $\mathcal{A}^\prime$ is isomorphic to $\mathcal{A}$ and $\mathcal{B}^\prime$ is isomorphic to $\mathcal{B}$.

\item If $(\mathcal{A}, \mathcal{B})$ satisfy the property \textbf{(*)}, then also $(\mathcal{A} + \Delta, \mathcal{B} + \Delta^\prime)$ satisfy \textbf{(*)}.

\end{itemize}

We use property \textbf{(*)} to define a partition $\mathcal{P}_{n+1}$, where $(\mathcal{A}, \mathcal{B})$ satisfy the property \textbf{(*)}, whenever $\mathcal{A} \in C^{n+1}_{1i}$ and $\mathcal{B} \in C^{n+1}_{2i}$ hold for the same $i$. By the first observed property choosing pairs $(\mathcal{A}, \mathcal{B})$ satisfying \textbf{(*)} gives rise to a partition, by the second observed property all $C^{n+1}_{1i}$ and $C^{n+1}_{2i}$ are closed under isomorphisms, and by the third observed property these sets of structures are also closed under the application of update sets. Hence all $(C^{n+1}_{1i},C^{n+1}_{2i})$ are separation candidates.

Now let $\mathcal{A} \in C^{n+1}_{1i}$ and $\mathcal{B} \in C^{n+1}_{2i}$. Let $h \in \mathcal{I}_{\beta+1}$ be a partial isomorphism with $\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}} \in dom(h)$. First assume that $\mathcal{A} \models \varphi(\bar{\boldsymbol{\Delta}}, \bar{a}, \bar{\boldsymbol{\Phi}})$ holds, so without loss of generality we have $\mathcal{A} \models U_r(j,\Delta_1)$.

Consider the subformulae
\begin{align*}
\psi(X,v) & \equiv v \in \textit{Atoms\/} \wedge v \in t \wedge \;U_{r^\prime(v)}(j,X) \wedge \\
& \forall Y. (\exists x. x \in \textit{Atoms\/} \wedge x \in t \wedge \;U_{r^\prime(x)}(j,Y) ) \rightarrow
\exists Z. ( \text{iso}(Z) \wedge \\
& \hspace*{3.5cm} \textit{updIso\/}(X,Y,Z) \wedge \textit{updIsoSet\/}(X,Y,Z) )
\end{align*}
and
\begin{align*}
\chi(X)  & \equiv \forall Y. (\exists x. x \in \textit{Atoms\/} \wedge x \in t \wedge \;U_{r^\prime(x)}(Y) ) \rightarrow
\exists Z. ( \text{iso}(Z) \wedge \\
& \hspace*{4cm} \textit{updIso\/}(X,Y,Z) \wedge \textit{updIsoSet\/}(X,Y,Z) ) .
\end{align*}

Then we have $\mathcal{A} \models \psi(\Delta_1,a)$ for some atom $a \in A_1$, so we have $\mathcal{A} \models a \in t$, $\mathcal{A} \models U_{r^\prime(a)}(j,\Delta_1)$ and $\mathcal{A} \models \chi(\Delta_1)$. We apply the \textbf{forth} property to extend $h$ to $h_1 \in \mathcal{I}_\beta$ with $h_1(a) = b$. Then by induction we obtain $\mathcal{B} \models b \in \textit{Atoms\/} \wedge b \in t$ and $\mathcal{B} \models U_{r^\prime(b)}(h(\Delta_1))$. We have to show that also $\mathcal{B} \models \chi(h(\Delta_1))$ holds.

For this take an arbitrary update set $\Delta^\prime$ over $\mathcal{B}$ and assume that $\mathcal{B} \models \exists x . x \in \textit{Atoms\/} \wedge x \in t \wedge U_{r^\prime(x)}(j,\Delta^\prime)$ holds. Then we have $\mathcal{B} \models b^\prime \in \textit{Atoms\/} \wedge b^\prime \in t \wedge U_{r^\prime(b^\prime)}(\Delta^\prime)$ for some atom $b^\prime \in A_2$.

As we have $\beta = \gamma + 2$, we can apply the \textbf{back} property twice (for $b^\prime$ and $\Delta^\prime$) to extend $h_1$ to $h_2 \in \mathcal{I}_\gamma$ with $h_2(\Delta^{\prime\prime}) = \Delta^\prime$ and $h_2(a^\prime) = b^\prime$ for some update set $\Delta^{\prime\prime}$ over $\mathcal{A}$ and some object $a^\prime \in B_1$.

Then by induction we get $\mathcal{A} \models a^\prime \in \textit{Atoms\/} \wedge a^\prime \in t \wedge U_{r^\prime(a^\prime)}(j,\Delta^{\prime\prime})$ and further $\mathcal{A} \models \exists x . x \in \textit{Atoms\/} \wedge x \in t \wedge U_{r^\prime(x)}(j,\Delta^{\prime\prime})$. As $\mathcal{A} \models \chi(\Delta_1)$ holds, we derive $\mathcal{A} \models \exists Z. ( \text{iso}(Z) \wedge \textit{updIso\/}(\Delta_1, \Delta^{\prime\prime},Z) \wedge \textit{updIsoSet\/}(\Delta_1, \Delta^{\prime\prime}, Z)$. By induction---the case of $\textit{updIsoSet\/}(\Delta_1, \Delta^{\prime\prime}, Z)$ follows from our extension of the partition sequence---we then get $\mathcal{B} \models \exists Z. ( \text{iso}(Z) \wedge \textit{updIso\/}(h(\Delta_1), h_2(\Delta^{\prime\prime}) ,Z) \wedge \textit{updIsoSet\/}(h(\Delta_1), h_2(\Delta^{\prime\prime}) ,Z))$, which implies the desired $\mathcal{B} \models \chi(h(\Delta_1))$.

Conversely, assume that $\mathcal{B} \models \varphi(h(\bar{\boldsymbol{\Delta}}), h(\bar{a}), h(\bar{\boldsymbol{\Phi}}))$ holds, so without loss of generality we have $\mathcal{B} \models U_r(j,h(\Delta_1))$. Let the subformulae $\psi(X,v)$ and $\chi(X)$ be as above.

Then we have $\mathcal{B} \models \psi(h(\Delta_1),b)$ for some atom $b \in A_2$, so we have $\mathcal{B} \models b \in t$, $\mathcal{B} \models U_{r^\prime(b)}(j,h(\Delta_1))$ and $\mathcal{B} \models \chi(h(\Delta_1))$. We apply the \textbf{back} property to extend $h$ to $h_1 \in \mathcal{I}_\beta$ with $h_1(a) = b$ for some $a \in B_1$. Then by induction we obtain $\mathcal{A} \models a \in \textit{Atoms\/} \wedge a \in t$ and $\mathcal{A} \models U_{r^\prime(a)}(\Delta_1)$. We have to show that also $\mathcal{A} \models \chi(\Delta_1)$ holds.

For this take an arbitrary update set $\Delta$ over $\mathcal{A}$ and assume that $\mathcal{A} \models \exists x . x \in \textit{Atoms\/} \wedge x \in t \wedge U_{r^\prime(x)}(j,\Delta)$ holds. Then we have $\mathcal{A} \models a^\prime \in \textit{Atoms\/} \wedge a^\prime \in t \wedge U_{r^\prime(a^\prime)}(\Delta)$ for some atom $a^\prime \in A_1$. Now we can apply the \textbf{forth} property twice (for $a^\prime$ and $\Delta$) to extend $h_1$ to $h_2 \in \mathcal{I}_\gamma$ with $h_2(\Delta) = \Delta^\prime$ and $h_2(a^\prime) = b^\prime$.

Then by induction we get $\mathcal{B} \models b^\prime \in \textit{Atoms\/} \wedge b^\prime \in t \wedge U_{r^\prime(b^\prime)}(j,\Delta^\prime)$ and further $\mathcal{B} \models \exists x . x \in \textit{Atoms\/} \wedge x \in t \wedge U_{r^\prime(x)}(j,\Delta^\prime)$. As $\mathcal{B} \models \chi(h(\Delta_1))$ holds, we derive $\mathcal{B} \models \exists Z. ( \text{iso}(Z) \wedge \textit{updIso\/}(h(\Delta_1), \Delta^\prime , Z) \wedge \textit{updIsoSet\/}(h(\Delta_1), \Delta^\prime, Z)$. By induction---the case of $\textit{updIsoSet\/}(h(\Delta_1), \Delta^\prime, Z)$ follows from our extension of the partition sequence---we then get $\mathcal{A} \models \exists Z. ( \text{iso}(Z) \wedge \textit{updIso\/}(\Delta_1, \Delta, Z) \wedge \textit{updIsoSet\/}(\Delta_1, \Delta , Z))$, which implies the desired $\mathcal{A} \models \chi(\Delta_1)$.

\end{description}

This completes the proof of the theorem.\qed

\end{proof}

Theorem \ref{thm-pebble} provides the decisive means to show limitations of ICPT, which we will exploit in the next section.

\paragraph*{Remark} If we consider the special case, where we do not use choice rules. The modal rank of all formulae of interest will be 0. In particular, there is no need to consider sequences of partitions. Furthermore, any formula of the form $\text{upd}^{ic}_r(X)$ becomes $\text{upd}_r(X)$, and there is no quantification over isomorphisms. Consequently isomorphism moves become obsolete. We could further rearrange our formulae in a way that also the use of update sets becomes obsolete, as the update set produced by a choiceless rule is uniquely determined in every state. This brings us back to the classical case of the infinitary extension of first-order logic, and our theorem degenerates to the game used for CPT in \cite{blass:apal1999}.

\section{An Inseparability Theorem for ICPT}\label{sec:separation}

We now investigate the expressiveness of the logic $\mathcal{L}^{ic,m}_{\infty\omega}$ for fixed $m$. We consider input structures $I$ over the input signature $\Upsilon_0$, which define the set $C$ of disjoint colours as used in Section \ref{sec:structures}. All colours are assumed to be $\varepsilon$-level. For fixed $k$ $I$ is extended to a structure $\bar{I}_k$ defined by all objects in the $k$-skew-symmetric sets in $\tilde{I} \subseteq HF(\tilde{I})$, i.e. we consider the signature $\{ \in, \emptyset \} \cup \Upsilon_0$. As in the previous sections we assume that all structures are large in comparison to $m$.

Let the signature $\Upsilon_0$ be fixed. The following lemma shows that $\mathcal{L}^{ic,m}_{\infty\omega}$ is quite powerful, as it is always possible to separate classes when the colours have different cardinality.

\begin{lemma}\label{lem-expressiveness}

Let $(C_1, C_2)$ be a separation candidate for $\mathcal{L}^{ic,m}_{\infty\omega}$ for $m \ge 3$ with base sets $\bar{I}_k$ and $\bar{J}_k$, respectively, such that $|\bar{I}_k| \neq |\bar{J}_k|$ holds. Then $(C_1, C_2)$ is $\mathcal{L}^{ic,m}_{\infty\omega}$-separable.

\end{lemma}

\begin{proof}

Without loss of generality we can assume $\bar{I}_k \subseteq \bar{J}_k$, so there must exist an $k$-skew-symmetric orbit $(x,G) \in \tilde{J}_k - \tilde{I}_k$. We choose such an orbit, for which $x$ is maximal. Let the spoiler start with an update set move on structure $\bar{J}_k$, such that $x$ appears as critical element in the update set $\Delta$. The duplicator has to choose an update set $\Delta^\prime$ over $\bar{I}_k$ containing a critical element $y$. If $x$ is a set, the spoiler can successively choose subsets $x_\ell \subsetneq \dots \subsetneq x_0 = x$, and whenever $x_i, x_{i+1}$ are covered by pebbles, first $x_i$, then $x_{i+1}$ appears in the update set. Then the duplicator is enforced to create analogously a sequence $y_\ell \subsetneq \dots \subsetneq y_0 = y$, such that whenever $y_i, y_{i+1}$ are covered by pebbles, first $x_i$, then $x_{i+1}$ appears in the update set $\Delta^\prime$. This is only possible, if $y$ has the same cardinality as $x$, which is not possible.

If $x$ is an atom, the spoiler step by step enlarges $\Delta$ by new updates containing new atoms. As the duplicator has to do the same, this is only possible if $\bar{I}_k$ and $\bar{J}_k$ contain the same number of atoms, which is also excluded.\qed

\end{proof}

Note that the argument in the proof could not be applied to CPT, because the support theorem for CPT \cite[Sect.8]{blass:apal1999} does not permit the creation of large sets, and this is independent of the base set. Using orbits, however, we can create such sets as elements of an orbit, even though the orbit has a bounded support. For instance, for the Parity example orbits have empty support.

Further note that if there are no input relations of arity $\ge 2$ and we have $|\bar{I}_k \cap c| = |\bar{J}_k \cap c|$ for all colours, then all structures in $C_1$ and $C_2$ are isomorphic, so one of these two classes will be empty.

Next we formulate and prove the main result of this section, the Inseparability Theorem, which basically states that if the conditions for $\mathcal{L}^{ic,m}_{\infty\omega}$-separability in Lemma \ref{lem-expressiveness} is not satisfied, then we obtain inseparability. The proof will exploit the relations over forms and configurations from Theorem \ref{thm-relations} and the representation of skew-symmetric objects from Theorem \ref{thm-form}. Formally, we also need the following {\em pattern assumption}.

\begin{definition}\rm

A separation candidate $(C_1, C_2)$ fulfills the {\em pattern assumption} iff almost all combinations of $m$-patterns occur in the colours defined by the input relations in the structures in $C_1$ and $C_2$, in particular, for every combination of $m$-patterns $\chi$ in a structure $\mathcal{A} \in C_1$ there is a structure $\mathcal{B} \in C_2$ with the same combination of $m$-patterns, and for every combination of $m$-patterns $\chi$ in a structure $\mathcal{B} \in C_2$ there is a structure $\mathcal{A} \in C_1$ with the same combination of $m$-patterns.

\end{definition}

\begin{theorem}[Inseparability Theorem]\label{thm-equivalence}

Let $k \ge 1, m \ge 3$, and let $(C_1, C_2)$ be a separation candidate for $\mathcal{L}^{ic,m}_{\infty\omega}$, where both classes contain structures over the same base set $\bar{I}_k$. If there are sufficiently many atoms and $(C_1, C_2)$ fulfills the pattern assumption, then $(C_1, C_2)$ is $\mathcal{L}^{ic,m}_{\infty\omega}$-inseparable.

\end{theorem}

\begin{proof}

According to Theorem \ref{thm-pebble} we have to show that the duplicator has a winning strategy for the separation game over $(C_1, C_2)$. After each move let $x_i, y_i$ ($0 \le i \le m-1$) be the objects, update sets or isomorphisms covered by the $i$'th pair of pebbles. By renumbering the pebbles we can assume without loss of generality that $x_0, \dots x_\ell$ and $y_0, \dots, y_\ell$ ($\ell \le m-1$) are the objects in the two sequences.

Without loss of generality we can assume that the game starts with all $2m$ pebbles used such that $x_i = y_i = \emptyset$ for $0 \le i \le m-1$. That is, initially, all pebbles are placed on objects. Concerning the objects we define the winning strategy for the duplicator in such a way that after each step there exist $k$-forms $\varphi$, groups $H_i \subseteq G_i \subseteq Sym(I)$, isomorphisms $g_i \in G_i$ and $k$-molecules $\sigma_i$, $\tau_i$ over $\tilde{I}$ and $\tilde{J}$, respectively, such that
\begin{equation}
x_i = g_i (\bigcup_{h\in H_i} \varphi_i * h \sigma_i), \quad y_i = g_i(\bigcup_{h\in H_i} \varphi_i * h \tau_i) \quad \text{and} \quad \textit{conf\/}(\bar{\sigma}) = \textit{conf\/}(\bar{\tau}) \tag{*}\label{eq-winning}
\end{equation}
hold for all $0 \le i \le \ell$.

This property is only affected by an object move. Therefore, we first consider the object move the duplicator has to perform in response to an object move by the spoiler to maintain condition (\ref{eq-winning}). The condition is obviously satisfied at the beginning of the game with $\varphi_i = \emptyset$, $g_i = 1$, $H_i = 1$, $\sigma_i = \sigma_j$ and $\tau_i = \tau_j$ for all $i,j$. Now consider a move by the spoiler. By symmetry we can assume without loss of generality that the spoiler uses the pebble 0 for $\bar{I}_k$ replacing $x_0$ by $x_0^\prime$. As $x_0^\prime \in \bar{I}_k$, Theorem \ref{thm-form} implies that there is a $k$-form $\varphi_0^\prime$, a group $G \subseteq Sym(\tilde{I})$, a subgroup $H_0 \subseteq G$ and a $k$-molecule $\sigma_0^\prime$ over $\tilde{I}$ such that $x_0^\prime \in (\varphi_0^\prime, G, H_0) * \sigma_0^\prime$.

Thus, $x_0^\prime = g_0(\bigcup_{h \in H_0} \varphi_0^\prime * h \sigma_0^\prime)$ for some $g_0 \in G$. According to Lemma \ref{lem-conf-ext} there exists a $k$-molecule $\tau_0^\prime$ such that
\[ \textit{conf\/}(\sigma_0^\prime,\sigma_1, \dots, \sigma_\ell) = \textit{conf\/}(\tau_0^\prime, \tau_1, \dots, \tau_\ell) \]
holds. Then choosing $y_0^\prime = g_0 (\bigcup_{h \in H_0} \varphi_0^\prime * h \tau_0^\prime)$ preserves the condition (\ref{eq-winning}).

We now have to show that $x_i \mapsto y_i$ defines a partial isomorphism between $\bar{I}_k$ and $\bar{J}_k$. We can assume that this is the case before the object move by the spoiler, so we need to show that we still get a partial isomorphism, when $x_0$ is replaced by $x_0^\prime$ and $y_0$ is replaced by $y_0^\prime$.

First, for the isomorphisms $\phi_{i,j} = g_i^{-1} g_j$ and $\bar{x}_i = \bigcup_{h \in H_i} \varphi_i * h \sigma_i$ and $\bar{y}_i = \bigcup_{h \in H_i} \varphi_i * h \tau_i$ we can exploit Corollary \ref{cor-extension-relations}, which gives
\begin{align*}
x_i \in x_j \Leftrightarrow\;
& g_i (\bar{x}_i) \in g_j (\bar{x}_j) \Leftrightarrow \bar{x}_i \in \phi_{i,j}(\bar{x}_j) \Leftrightarrow \\
& \bar{y}_i \in \phi_{i,j}(\bar{y}_j) \Leftrightarrow g_i (\bar{y}_i) \in g_j (\bar{y}_j) \Leftrightarrow y_i \in y_j \\
x_i = x_j \Leftrightarrow\;
& g_i (\bar{x}_i) = g_j (\bar{x}_j) \Leftrightarrow \bar{x}_i = \phi_{i,j}(\bar{x}_j) \Leftrightarrow \\
& \bar{y}_i = \phi_{i,j}(\bar{y}_j) \Leftrightarrow g_i (\bar{y}_i) = g_j (\bar{y}_j) \Leftrightarrow y_i = y_j \\
x_i \subseteq x_j \Leftrightarrow\;
& g_i (\bar{x}_i) \subseteq g_j (\bar{x}_j) \Leftrightarrow \bar{x}_i \subseteq \phi_{i,j}(\bar{x}_j) \Leftrightarrow \\
& \bar{y}_i \subseteq \phi_{i,j}(\bar{y}_j) \Leftrightarrow g_i (\bar{y}_i) \subseteq g_j (\bar{y}_j) \Leftrightarrow y_i \subseteq y_j
\end{align*}

This shows that property (2) of Definition \ref{def-po} is maintained.

Next consider the update sets; assume $x_i = \Delta_i$ and $y_i = \Delta_i^\prime$ holds for pebbles $\ell < i \le p$. As $\Delta_i$ is an update set, it can be written as a union $\Delta_i = \bigcup_{f \in \Upsilon_{dyn}} \Delta_{i,f}$, and all updates in $\Delta_{i,f}$ have the form $((f, (a_1, \dots, a_r), a_0)$ with $r = ar(f)$. The {\em update tuple} $(a_0, \dots, a_r)$ is a tuple of objects $a_j \in \bar{I}_k$, each of which takes the form $a_i = g_i \bigcup_{h \in H_i} \varphi_i * h \sigma_i$ with some group $G_i$ of isomorphisms, $g_i \in G_i$, a subgroup $H_i \subseteq G_i$, and a $k$-molecule $\sigma_i$. That is, $\Delta_{i,f}$ and also $\Delta_i$ is uniquely determined by these $g_i$, $H_i$ and the molecules $\sigma_i$.

The winning strategy of the duplicator requires to maintain that $\Delta_i^\prime = \bigcup_{f \in \Upsilon_{dyn}} \Delta^\prime_{i,f}$ holds, where the tuples $((f, (b_1, \dots, b_r), b_0) \in \Delta^\prime_{i,f}$ are built from update tuples $(b_0, \dots, b_r)$ with objects $b_j \in \bar{I}_k$ such that
\begin{align}
a_i = g_i (\bigcup_{h\in H_i} \varphi_i * h \sigma_i), \quad & b_i = g_i(\bigcup_{h\in H_i} \varphi_i * h \tau_i) \notag\\
\text{and} \quad & \textit{conf\/}^{\Phi_{i,j}}(\sigma_i, \sigma_j) = \textit{conf\/}^{\Phi_{i,j}}(\tau_i, \tau_j) \tag{$\dagger$}\label{eq-winning2}
\end{align}
holds with $\Phi_{i,j} = g_i^{-1} g_j$ for all $i,j$. We include the representations of the objects and other update sets in these configurations.

Same as for the object moves, whenever the spoiler places a pebble on a new update set---without loss of generality let this be $\Delta_p$---then $\Delta_p$ is defined by new isomorphisms $g_i^p$, groups $H_i^p$ of isomorphisms, forms $\varphi_i^p$ and molecules $\sigma_i^p$ satisfying the above property. Using Lemma \ref{lem-conf-ext} repeatedly we obtain molecules $\tau_i^p$ such that with the same $g_i^p$, $H_i^p$ and $\varphi_i^p$ property (\ref{eq-winning2}) is satisfied.

With this we show that conditions (1) and (3) of Definition \ref{def-po} are maintained. Condition (1) requires to show that if an update tuple $(a_0, \dots, a_r)$ defines an update in $\Delta_{i,f}$, then the corresponding update tuple $(b_0, \dots, b_r)$ defines an update in $\Delta^\prime_{i,f}$ (or the other way round, or both). This holds by our construction, Lemma \ref{lem-components} and Corollary \ref{cor-components}.

Condition (3) requires to show that if some $a_i$ in an update tuple equals some selected object $x_j$, then also $b_i$ equals the corresponding selected object $y_j$. This follows in the same way as for the object moves exploiting the equality of the configurations or $\Phi$-configurations as well as Lemma \ref{lem-components} and Corollary \ref{cor-components}.

Similarly, consider isomorphisms $\Phi_i$ ($p < i \le m$). We can represent $\Phi_i$ as a set of cycles of lengths $c_1^i, \dots, c_{n_i}^i$, and each such cycle can be represented as a tuple of length $c_j^i$ such that each atom appears in exactly one cycle. Then we can write $\Phi_i = \chi_{\Phi_i} * \alpha_i$, where $\alpha_i$ is a fixed molecule containing all the atoms\footnote{Note that this is an $n$-molecule, not a $k$-molecule, so $\Phi_i \notin \bar{I}_k$, but it is still an object in $\textit{HF\/}(I)$, and our constructions apply nonetheless to such molecules as well. In fact, the isomorphisms used in separation pebble games are not objects of the structures.}.

With this the winning strategy of the duplicator is to maintain with every move the following property:
\begin{equation}
\Phi_i = \chi_{\Phi_i} * \alpha_i ,\quad \Psi_i = \chi_{\Phi_i} * \beta_i ,\quad \text{and} \quad \textit{conf\/}(\bar{\sigma}, \bar{\alpha}) = \textit{conf\/}(\bar{\tau}, \bar{\beta}) \; , \tag{$\ddagger$} \label{eq-winning3}
\end{equation}
where $\bar{\sigma}$ and $\bar{\tau}$ refer to the sequences of the molecules defining the objects.

If an isomorphism move by the spoiler introduces a new isomorphism, say $\Phi_q^\prime = \chi_{\Phi_q^\prime} * \alpha_q^\prime$, then using Lemma \ref{lem-conf-ext} we find a molecule $\beta_q^\prime$ with $\textit{conf\/}(\bar{\sigma}, \bar{\alpha}, \alpha_q^\prime) = \textit{conf\/}(\bar{\tau}, \bar{\beta}, \beta_q^\prime)$. If the duplicator chooses $\Psi_q^\prime = \chi_{\Phi_q^\prime} * \beta_q^\prime$, then property (\ref{eq-winning3}) is maintained. This also holds for changes to the object sequences by an object move.

Assume that $\Phi_i(x_{i_1}, x_{i_2})$ holds with $x_{i_1} = \varphi_{i_1} * \sigma_{i_1}$ and $x_{i_2} = \varphi_{i_2} * \sigma_{i_2}$. We do not need to consider more complex forms, as only atoms appear in the isomorphisms $\Phi_i$ and $\Psi_i$. Then by Lemma \ref{lem-components} we have
\begin{align*}
\Phi_i(x_{i_1}, x_{i_2}) \; &\Leftrightarrow \; \text{for some}\; j \; x_{i_1} \;\text{is the}\; j\text{'th component of a cycle of}\; \Phi_i \;\text{and}\; x_{i_2} \; \text{is the}\\
&\qquad \text{$(j+1)$'th component of a this cycle (modulo the cycle length)} \\
&\Leftrightarrow \; \Pi^{(j)}(\varphi_{i_1}, \chi_{\Phi_i}, \textit{conf\/}(\sigma_{i_1}, \alpha_i)) \wedge
\Pi^{(j+1)}(\varphi_{i_2}, \chi_{\Phi_i}, \textit{conf\/}(\sigma_{i_2}, \alpha_i)) \\
&\qquad \text{(treat the $\sigma_{i_j}$ as $n$-molecules)} \\
&\Leftrightarrow \; \Pi^{(j)}(\varphi_{i_1}, \chi_{\Phi_i}, \textit{conf\/}(\tau_{i_1}, \beta_i)) \wedge
\Pi^{(j+1)}(\varphi_{i_2}, \chi_{\Phi_i}, \textit{conf\/}(\tau_{i_2}, \beta_i)) \\
&\Leftrightarrow \; y_{i_1} \;\text{is the}\; j\text{'th component of a cycle of}\; \Psi_i \;\text{and}\; y_{i_2} \; \text{is the}\\
&\qquad (j+1)\text{'th component of a this cycle (modulo the cycle length)} \\
&\Leftrightarrow \; \Psi_i(y_{i_1}, y_{i_2})
\end{align*}

This establishes condition (5) of Definition \ref{def-po}. As update set and isomorphism moves do not have any impact on each other, it only remains to show condition (4) of Definition \ref{def-po}.

For this consider an $\ell$-ary colour $c$ defined by the input relations in $\bar{I}_k$ and $\bar{J}_k$ with $\ell \le m$. Only atoms can appear in the tuples in $c$, so consider those $x_i$, $y_i$ that are atoms. The atoms appearing in $x_0, \dots, x_{m-1}$ define an $m$-molecule $\upsilon$, and those appearing in $y_0, \dots, y_{m-1}$ define an $m$-molecule $\omega$. Likewise, the atoms appearing in $x_0^\prime, x_1, \dots, x_{m-1}$ and $y_0^\prime, y_1, \dots, y_{m-1}$, respectively, define molecules $\upsilon^\prime$ and $\omega^\prime$. Without loss of generality we can assume that $x_0^\prime$ and $y_0^\prime$ are both atoms; otherwise there is nothing to show.

First consider the case that $x_0^\prime$ and $y_0^\prime$ are atoms replacing atoms $x_0$ and $y_0$, respectively. Then we can assume that before the move the following conditions were satisfied:

\begin{itemize}

\item for each structure $\mathcal{A} \in C_1$ there exists a structure $\mathcal{B} \in C_2$ such that the sequences defined by the pebbles define a partial isomorphism between $\mathcal{A}$ and $\mathcal{B}$;

\item for each structure $\mathcal{B} \in C_2$ there exists a structure $\mathcal{A} \in C_1$ such that the sequences defined by the pebbles define a partial isomorphism between $\mathcal{A}$ and $\mathcal{B}$.

\end{itemize}

Let $\mathcal{A} \in C_1$ be arbitrary. Then for a colour $c \in C$ the subrelation of $c^{\mathcal{A}}$ defined by the atoms in $x_0^\prime, x_1, \dots, x_\ell$ can be written in the form $\chi * \nu^\prime$, where $\nu^\prime$ is an $m$-molecule defined by the atoms in $x_0^\prime, x_1, \dots, x_\ell$. Let $\pi$ be the isomorphism defined by the transposition of $x_0$ and $x_0^\prime$. Then for $\mathcal{A}^\prime = \pi(\mathcal{A}) \in C_1$ the subrelation of $c^{\mathcal{A}^\prime}$ defined by the atoms in $x_0, \dots, x_\ell$ is $\chi * \nu$ with $\nu = \pi \nu^\prime$. Then there exists a structure $\mathcal{B}^\prime \in C_2$ such that the sequences defined by the pebbles define a partial isomorphism between $\mathcal{A}^\prime$ and $\mathcal{B}^\prime$.

In particular, $c^{\mathcal{A}^\prime}(x_{i_1}, \dots, x_{i_r})$ holds iff $c^{\mathcal{B}^\prime}(y_{i_1}, \dots, y_{i_r})$ holds. This implies that the subrelation $c^{\mathcal{B}^\prime}$ defined by the atoms in $y_0, \dots, y_\ell$ take the form $\chi * \omega$ with an $m$-molecule $\omega$ defined by the atoms in $y_0, \dots, y_\ell$. Let $\pi^\prime$ be an isomorphism such that $\omega^\prime = \pi^\prime \omega$ becomes the molecule defined by the atoms in $y_0^\prime, y_1, \dots, y_\ell$. Then $\mathcal{B} = \pi^\prime(\mathcal{B}^\prime) \in C_2$, and the subrelation of $c^{\mathcal{B}}$ defined by the atoms in $y_0^\prime, y_1, \dots, y_\ell$ is $\chi * \omega^\prime$. This implies finally
\[ c^{\mathcal{A}}(x_{i_1}, \dots, x_{i_r}) \; \Leftrightarrow \; c^{\mathcal{B}}(y_{i_1}, \dots, y_{i_r}) \; , \]
which shows the desired condition (4) of Definition \ref{def-po}.

For the second case, when $\mathcal{B} \in C_2$ is given, because the spoiler selected the class $C_2$, we proceed completely analogously.

The leaves the case of an object move creating a new atom $x_0^\prime$ (or $y_0^\prime$, but for symmetry reasons we can ignore this), while $x_0$ (or $y_0$, respectively) was not an atom. In this case, for a structure $\mathcal{A} \in C_1$ and the set $C = \{ c_1, \dots, c_p \}$ of colours let $\psi_1 * \omega, \dots, \psi_p * \omega$ with an $m$-molecule $\omega$ be the subrelations of $c_1^{\mathcal{A}}, \dots, c_p^{\mathcal{A}}$ defined by the atoms in $x_0^\prime, x_1, \dots, x_\ell$. According to the pattern assumption there exists a structure $\mathcal{B} \in C_2$ with the same combination of patterns, i.e. there exists an $m$-molecule $\nu^\prime$ such that the subrelations of $c_1^{\mathcal{B}}, \dots, c_p^{\mathcal{B}}$ are $\psi_1 * \nu^\prime, \dots, \psi_p * \nu^\prime$. Let $\nu = \pi \nu^\prime$ with some isomorphism $\pi$ such that $\nu$ is defined by the sequence of atoms in $y_0^\prime, y_1, \dots, y_\ell$, in an order corresponding to $x_0^\prime, x_1, \dots, x_\ell$. Then take the structure $\mathcal{B}^\prime = \pi(\mathcal{B}) \in C_2$. Here, $\psi_1 * \nu, \dots, \psi_p * \nu$ are the subrelations of $c_1^{\mathcal{B}^\prime}, \dots, c_p^{\mathcal{B}^\prime}$ defined by the atoms in $y_0^\prime, y_1, \dots, y_\ell$, which again shows the desired condition (4) of Definition \ref{def-po}.

The inverse direction starting from $\mathcal{B} \in C_2$ follows analogously.
This completes the proof of the inseparability theorem. \qed

\end{proof}

We now look at SAT, the satisfiability problem for a set of clauses. It is commonly known (see e.g. \cite{immerman:1999}) that the problem can be represented by a signature $\Upsilon$ with two binary relation symbols $P$ and $N$. We have $P(i,j)$, if the atom $a_j$ appears positively in the clause $c_i$, and $N(i,j)$ if the atom $a_j$ appears negatively in the clause $c_i$. Without loss of generality we can assume that we never have an atom $P(i,j)$ and $N(i,j)$ together. We apply the Inseparability Theorem \ref{thm-equivalence} to the SAT problem.

\begin{corollary}[SAT Theorem]\label{thm-sat}
The pair $(K_1,K_2)$ of satisfiable/non-satisfiable SAT structures cannot be separated by ICPT.

\end{corollary}

\begin{proof}

Let $\tilde{M}$ be a PTIME ic-ASM with input signature $\Upsilon_0 = \{ P, N \}$. According to Theorem \ref{thm-fixpoint2} there exists a formula $\varphi$ in $\mathcal{L}^{ic,m}_{\infty\omega}$ for some $m > 0$ that asserts that $\tilde{M}$ accepts an input structure $I$. This is the case, if $\varphi$ holds in some semi-transitive substructures of $HF(I)$ containing all elements of all active orbits in $\mathcal{A}[I]$. In particular, $\tilde{M}$ accepts $I$ if and only if $\bar{I}_k$ satisfies $\varphi$.

However, if $I$ is sufficiently large, then Theorem \ref{thm-equivalence} states that $\mathcal{L}^{ic,m}_{\infty\omega}$ cannot distinguish all structures in $K_1$ and $K_2$, so $\tilde{M}$ accepts both satisfiable and non-satisfiable structures. This shows that $(K_1,K_2)$ cannot be separated by ICPT.\qed

\end{proof}

As SAT is in NP and ICPT captures PTIME Theorem \ref{thm-capture} implies the following corollary.

\begin{corollary}

PTIME differs from NP.

\end{corollary}

\section{Conclusions}\label{sec:schluss}

Originally, we only wanted to study how complexity theory could be conducted in connection with ASMs, and the work on CPT \cite{blass:apal1999} was one of the few studies in this direction. We saw that CPT exploits (synchronous, parallel) ASMs to characterise the choiceless fragment of PTIME. In view of the behavioural theory of parallel algorithms, in particular using the more convincing set of postulates in \cite{ferrarotti:tcs2016}, it is indeed justified to say that CPT captures THE choiceless fragment of PTIME. This brought us to Gurevich's conjecture that there is no logic capturing PTIME \cite{gurevich:cttcs1988}, in other words that the gap between PTIME and its choiceless fragment could not be covered by a logical extension of CPT. This would also imply a negative answer to Chandra and Harel's question if there exists a computation model on structures rather than strings that can capture PTIME \cite{chandra:jcss1982}.

This study brought us to the idea of insignificant choice. Retrospectively, after showing that ICPT captures PTIME and Gurevich's conjecture does not hold despite all the supporting evidence, it appears very natural to investigate ICPT. A computation not covered by CPT must either be outside PTIME or it must contain some form of non-deterministic choice. There cannot be any PTIME elimination of the choice, as this would bring the computation back into CPT. There can also be no polynomial bound on the cumulated number of choices, because otherwise the choice could be replaced by a parallel execution of all choices, which again would lead back to CPT. However, if nonetheless a well-defined result comes out, the choice must have been insignificant.

Our first major result gives an answer to the question raised by Chandra and Harel: the appropriate model of computation on structures is the model of ASMs (formerly known as evolving algebras and occasionally also called Gurevich machines), and the particular form of ASMs needed for the capture of PTIME are the PTIME ic-ASMs, where choice is restricted to atoms and a local insignificance condition is satisfied. The corresponding Theorem \ref{thm-capture} is simple, but only becomes convincing by the logical fixed-point characterisation in Theorems \ref{thm-fixpoint} and \ref{thm-fixpoint2}, which depend on the logic of non-deterministic ASMs \cite{ferrarotti:amai2018}.

We also learnt that the idea to approach the capture of PTIME by some form of insignificant choice has been already investigated earlier (see \cite{arvind:stacs1987} and \cite{gire:infcomp1998}). However, they could not obtain a syntactic characterisation of the sentences of the logic. In our work the exploitation of ASMs made the key difference, as the state-based view allowed us to characterise ICPT by a local insignificance condition, which requires a modified definition of the semantics of choice rules. If the states in the computation are ignored, it becomes hard to see the importance of update sets, which are the decisive add-on in the logic of non-deterministic ASMs \cite{ferrarotti:igpl2017,ferrarotti:amai2018} compared to the logic of deterministic ASMs \cite{staerk:jucs2001}.

With the logical capture of PTIME it becomes quite natural to investigate also the relationship between PTIME and NP. Here we adopted first the Ehrenfeucht-Fra\"{\i}ss\'{e} method \cite{libkin:2004} and defined a pebble game that allows us to characterise inseparable classes of structures in the logic $\mathcal{L}^{ic,m}_{\infty\omega}$. To our knowledge the study of inseparability instead of equivalence of just two structures has not yet received much attention in finite model theory. Then we exploited the proof that CPT is strictly included in PTIME, which led us to the Inseparability Theorem \ref{thm-equivalence} showing under which conditions classes of structures cannot be separated by $\mathcal{L}^{ic,m}_{\infty\omega}$. As a consequence the classes of satisfiable and unsatifiable structures of the NP-complete SAT problem are inseparable by ICPT. The consequence is that PTIME differs from NP.

Besides the value of the two major technical results, the refutation of Gurevich's conjecture and the proof that PTIME and NP differ, we see a third, even more important contribution made by this article. There exist already several behavioural theories showing how particular classes of algorithms are captured by particular classes of ASMs. This justifies to qualify ASMs as THE general computation model on structures. This article shows that a presumed limitation with respect to the ability to deal with complexity theory on the level of computations on structures does not exist. To the contrary, fundamental complexity theoretical results only result when we adopt computations on structures.

Last but not least we like to remark that in this article analogous to the work by Blass, Gurevich and Shelah we adopted a rather specific view on ASMs, which brought them closer to the usual treatment in complexity theory. We see, however, no reason to stick to such a specific version of ASMs. We could as well treat ASMs on arbitrary structures, and a logical characterisation by fixed-point formulae over the logic of ASMs would still work. This offers countless opportunities for the study of descriptive complexity theory without having to refer all the time to the level of Turing machines.

\subsection*{Acknowledgements}

I am grateful to Egon B\"orger and Flavio Ferrarotti for carefully reading my manu\-script and making many suggestions for improvement. Anuj Dawar read the whole earlier manuscript and his many critical comments \cite{dawar:communication2020} helped to close gaps and remove inaccuracies. I also like to thank Jan van den Bussche and Thomas Klimpel who spotted some issues in earlier versions of the manuscript that needed clarification.

\bibliographystyle{plain}

redpajama_set_name: RedPajamaArXiv