A Tenth Hilbert Problem-like Result: The Decidability of MLS with Unordered Cartesian Product

TL;DR

This paper proves the decidability of MLS with unordered Cartesian product using formative processes and provides a combinatorial characterization of satisfiable formulas.

Contribution

It introduces a new decidability result for MLS with unordered Cartesian product and offers a combinatorial description of satisfiable formulas.

Findings

Decidability of MLS with unordered Cartesian product established.

A combinatorial characterization of satisfiable formulas provided.

Method based on formative processes enhances understanding of the problem.

Abstract

Using the technique of formative processes, I solve the decidability problem of MLS with unordered cartesian product in the positive. Moreover I give a pure combinatorial description of the satisfiable MLS with unordered cartesian product-formulas for a given number of variables.

Equations

$$\textstyle\bigcup\Sigma\subseteq\bigcup\bigcup(\Sigma\cup\{\sigma^{*}\})\subseteq{\mathscr{P}}\big{(}{\bigcup\bigcup(\Sigma\cup\{\sigma^{*}\})}\big{)}=\bigcup(\Sigma\cup\{\sigma^{*}\})\,.$$

$$\textstyle\bigcup(\Sigma\setminus\{\sigma^{*}\})\subseteq\bigcup\bigcup\Sigma\subseteq{\mathscr{P}}\big{(}{\bigcup\bigcup\Sigma}\big{)}=\bigcup\Sigma\,.$$

$$\mathcal{T}\in \mathcal{P}(\mathcal{P}{)}^{\mathcal{P}(\mathcal{P})}$$

$$\mathcal{T}(B)=\{q\in \mathcal{P}\mid q^{(\bullet )}\cap {\mathcal{P}}^{\ast }(B^{(\bullet )})\ne \varnothing \}$$

$$\Sigma \ne {\Sigma }^{\prime },\text{mbox}and\bigcup {\Sigma }^{\prime }\setminus \bigcup \Sigma \subseteq {\mathcal{P}}^{\ast }(\Gamma )\text{mbox}forsome\Gamma \subseteq \Sigma ,$$

$$\begin{array}[]{lcl}\tau^{(\mu)}&:=&\mbox{the unique $\sigma\in\mathcal{P}_{\mu}$ such that $\sigma\subseteq\tau$, if any exists, else $\emptyset$}.\end{array}$$

$${\mathcal{P}}^{\ast }(\Gamma )\cap \left(\bigcup {\mathcal{P}}_{\nu +1}\setminus \bigcup {\mathcal{P}}_{\nu }\right)\ne \varnothing \text{mbox}implies\left({\mathcal{P}}^{\ast }(\Gamma )\setminus \bigcup {\mathcal{P}}_{\nu +1}\right)\cap \bigcup {\mathcal{P}}_{\xi }=\varnothing .$$

$$\begin{array}[]{lcl}p^{(\mu)}&:=&\left({p^{(\bullet)}}\right)^{(\mu)}\\ B^{(\mu)}&:=&\{q^{(\mu)}\,\texttt{:}\>q\in B\}\\ B^{(\bullet)}&:=&\{q^{(\bullet)}\,\texttt{:}\>q\in B\}\\ \Delta^{(\nu)}(p)&:=&p^{(\nu+1)}\setminus\bigcup\mathcal{P}_{\nu}\\ A_{\nu}&:=&\mbox{the set $A\subseteq\mathcal{P}$ for which $\bigcup\mathcal{P}_{\nu+1}\setminus\bigcup\mathcal{P}_{\nu}\subseteq{\mathscr{P}}^{\ast}\big{(}{A^{(\nu)}}\big{)}$}\\ T_{\nu}&:=&\{p\in\mathcal{P}\mid\Delta^{(\nu)}(p)\cap(\bigcup\mathcal{P}_{\nu+1}\setminus\bigcup\mathcal{P}_{\nu})\neq\emptyset\}.\end{array}$$

$$s\subseteq t\text{/},s=t\text{/},s\in t\text{/},$$

$$\begin{array}[]{rcl}\hbox{\sf rk}\;(M)&:=&\hbox{\sf rk}\;(\bigcup M[V])\end{array}$$

$$M\varnothing$$

$$M(s\cup t)$$

$$M(s\cap t)$$

$$M(s\setminus t)$$

$$M(s\otimes t)$$

$$(s\in t{)}^M$$

$$(s\subseteq t{)}^M$$

$$(\Phi \wedge \Psi {)}^M$$

$$(\Phi \to \Psi {)}^M$$

$$t_1\cup t_2,t_1\cap t_2,t_1\setminus t_2,t_1\otimes t_2,$$

$$\displaystyle\begin{array}[]{l@{~~~~~~~~}l@{~~~~~~~~}l@{~~~~~~~~}l@{~~~~}l}x=y\cup z\/,\hfil~{}~{}~{}~{}~{}~{}~{}~{}&x=y\cap z\/,\hfil~{}~{}~{}~{}~{}~{}~{}~{}&x=y\setminus z\/,\hfil~{}~{}~{}~{}~{}~{}~{}~{}\\ x=y\/,\hfil~{}~{}~{}~{}~{}~{}~{}~{}&x\neq y\/,\hfil~{}~{}~{}~{}~{}~{}~{}~{}\\ x=y\otimes z\/,\hfil~{}~{}~{}~{}~{}~{}~{}~{}&x\in y\/,\hfil~{}~{}~{}~{}~{}~{}~{}~{}&x\notin y\/,\hfil~{}~{}~{}~{}~{}~{}~{}~{}&x\subseteq y\/,\hfil~{}~{}~{}~{}&x\not\subseteq y\/,\end{array}$$

$$x=y\cup z\text{/},x=y\setminus z\text{/},x\in y\text{/},s\otimes t$$

$$M_{{}_{\mathfrak{I}}}v:=\bigcup \mathfrak{I}(v)\text{/},\text{for v∈V/.}$$

$${\mathfrak{I}}_{{}_M}(v):=\{\sigma \in {\Sigma }_M\text{|}\sigma \subseteq Mv\}\text{/},\text{for v∈V.}$$

$$h(v)=\{\begin{array}{l}h(\varnothing ):=0\\ h(B):=max\{h(q)|q\in B\},\forall B\subseteq \mathcal{P}\wedge \varnothing \ne B\in {\mathcal{G}}_{WF}\\ h(q):=max\{h(B)|q\in T(B)\}+1,\forall q\in \mathcal{P}\cap {\mathcal{G}}_{WF}.\end{array}$$

$$\left|{\mathfrak{N}}_W=\{\mu \mid W{F}_{\mathcal{H}}^{(\xi )}(A_{\mu })\}\right|\le \left|\Sigma \right|\uparrow \uparrow (h^{\ast }+1),$$

$$\left|{\mathfrak{M}}_W=\{\mu \mid W{F}_{\mathcal{H}}^{(\mu )}(A_{\mu })\}\right|\le 2\uparrow \uparrow (\left|\Sigma \right|+1).$$

$$rk(\bigcup A_{{\mu }^{(\bullet )}})\le max\{h_{\mu }(q)\mid q\in A_{\mu }\}\le \left|\Sigma \right|$$

$$\left|{\mathfrak{M}}_W\right|\le {\mathcal{V}}_{|\Sigma |+1}=2\uparrow \uparrow (\left|\Sigma \right|+1).$$

$$x=y\cup z,x=y\setminus z,x\ne y,x\in y,x\notin y,x\subseteq y\otimes z$$

$$\Sigma /\mathfrak{I}\models \ell ⟹\hat{\Sigma }/\overline{\mathfrak{I}}\models \ell ,$$

$$\bigcup \beta [X]\subseteq \bigcup \beta [Y]\otimes \bigcup \beta [Z]\text{mbox}if\bigcup X\subseteq \bigcup Y\otimes \bigcup Z\text{mbox},forX,Y,Z\subseteq \Sigma$$

$$\bigcup X\subseteq \bigcup Y\otimes \bigcup Z$$

Full text

Introduction

In the eighties, the decidability problem of $\textnormal{{MLS}}\otimes$ was originally posed by Domenico Cantone (actually in its ordered cartesian product-version) during the realization of his Ph.D thesis under the supervision of J.T.Schwartz. By a personal communication M.Davis quoted this problem as a Tenth Hilbert Problem(THP)-like one. Indeed, some years later, Cutello Cantone and Policriti [CCP89] proved that extending $\textnormal{{MLS}}\otimes$ with cardinalities equality one finds a set theoretic reduction to THP (see [Mat70] for undecidability of THP). Both the opinion of M.Davis and the meaning of the above result went in the direction of the undecidability of $\textnormal{{MLS}}\otimes$. Until now, as far as I know, there are no proofs of this result or its negation. On the contrary it seemed that following how the model grows, it was possible to trace the structure of the assignment to the variables. This allows extra information to be obtain in order to reach decidability. Indeed, there is a significant difference between natural numbers and sets, while the former have no inner structure, the latter bring the history of their formation inside themselves. These ideas led to the birth of the technique of formative processes. This technique allows us to deal with languages which forces some formulas to have infinite models [Urs05] [CU14],[CU18]. Roughly speaking, the formative processes show how a model becomes infinite through its finite structure. Recently in many fields of mathematics combinatorial properties of substructures are used to infer properties of the entire infinite structure, for example extreme amenability of an infinite structure arises from Ramsey Property of its finite substructures (see for example [KPT]).

The main content of the present paper is the proof of the decidability of $\textnormal{{MLS}}\otimes$, a secondary one consists in relating this approach with THP.

In the meanwhile I give a finite combinatorial description of the model and this fact lights up the intimate structure of decidability and undecidability through the study of the behaviour of the cycles of finite structure which generates the model.

In few words, the undecidability arises whenever the number of times, that one can repeat a cycle, is superimposed from outside. On the contrary, the problem stays decidable whenever the bound of the number of times, one can repeat the cycle, emerges from the structure. For this reason I believe that starting from this point it could be possible to give a pure combinatorial description of THP.

The article is composed of four sections:

The first is devoted to show all known tools which are useful in the proof of the main result.

The second shows supplementary unknown essential results in order to reach our goal.

The third contains the final proof of the decidability of $\textnormal{{MLS}}\otimes$.

The fourth contains a short discussion about the connections between $\textnormal{{MLS}}\otimes$ and THP.

1 Preliminaries

All the notions in this section are widely explained in [CU18]. In order to make the reading of the present article easier, I briefly resume those among them which are useful in the following.

1.1 $\mathcal{P}$-graphs and Formative Processes

Definition 1**.**

*A partition $\Sigma$ is a collection of pairwise disjoint non-null sets, called the blocks of $\Sigma$. The union $\bigcup\Sigma$ of a partition $\Sigma$ is the domain of $\Sigma$. A partition is transitive if so is its domain. Likewise, a partition is hereditarily finite if so is its domain.         *

If a partition $\Sigma$ is non-transitive, then we can obtain a transitive partition containing $\Sigma$ as a subset, by adding to it as a new block the set $\mathsf{TrCl}(\bigcup\Sigma)\setminus\bigcup\Sigma$ ($\mathsf{TrCl}(\bigcup\Sigma)$ denotes the transitive closure of $\Sigma$). In fact, it can be shown that $\Sigma\cup\{\mathsf{TrCl}(\bigcup\Sigma)\setminus\bigcup\Sigma\}$ is the minimal transitive partition containing $\Sigma$ as a subset.

Definition 2**.**

The transitive completion of a non-transitive partition $\Sigma$ is the partition $\Sigma\cup\{\mathsf{TrCl}(\bigcup\Sigma)\setminus\bigcup\Sigma\}$.

*I agree that the transitive completion of a transitive partition $\Sigma$ is the partition itself.         *

For technical reasons, it will be more convenient to consider a stronger kind of completion. Let $\Sigma$ be a partition, and $\sigma^{*}$ any (non-null) set disjoint from $\bigcup\Sigma$ and such that the following chain of inclusions and equalities are fulfilled:

[TABLE]

Then, setting $\Sigma^{*}:=\Sigma\cup\{\sigma^{*}\}$, we have:

1. (I)

$\Sigma^{*}$ is a transitive partition, and 2. (II)

${\mathscr{P}}({\bigcup\Gamma})\subseteq\bigcup\Sigma^{*}$, for each $\Gamma\subseteq\Sigma$.

Upon calling internal the blocks in $\Sigma^{*}$ distinct from $\sigma^{*}$, constraint (II) just asserts that the domain of the partition $\Sigma^{*}$ contains the powerset of every possible union of internal blocks.

I shall interchangeably refer to the block $\sigma^{*}$ (sometimes denoted also by $\overline{\sigma}$) either as the external block of $\Sigma$ (relative to the ${\mathscr{P}}$-completion $\Sigma^{*}$) or as the special block of $\Sigma^{*}$. Additionally, we shall refer to the partition $\Sigma^{*}$ as the ${\mathscr{P}}$-completion of $\Sigma$.

Definition 3** (${\mathscr{P}}$-partition).**

A partition $\Sigma$ is said to be a ${\mathscr{P}}$-partition if it contains a block $\sigma^{*}$ such that

[TABLE]

As is expected, the ${\mathscr{P}}$-completion of a given partition $\Sigma$ is a ${\mathscr{P}}$-partition.

In the following, unless specified, we manage with ${\mathscr{P}}$-partition, therefore, in order to simplify the notation, we omit the prefix ${\mathscr{P}}$.

Now we consider a finite set $\mathcal{P}$, whose elements are called places (or syntactical Venn regions)111Roughly speaking, the intended meaning of places and blocks is that the former are empty boxes, instead the latter are, the same boxes, filled. By abuse of language, occasionally, we shall use the same notation for both of them, relying on the context to distinguish them. and whose subsets are called nodes, denoted by $\mathcal{N}$. we assume that $\mathcal{P}\cap\mathcal{N}=\emptyset$, so that no node is a place, and vice versa. we shall use these places and nodes as the vertices of a directed bipartite graph $\mathcal{G}$ of a special kind, called $\mathcal{P}$-graph or $\mathcal{P}$-board.

The edges issuing from each place $q$ are exactly all pairs $\langle q,B\rangle$ such that $q\in B\subseteq\mathcal{P}$: these are called membership edges. The remaining edges of $\mathcal{G}$, called distribution edges, go from nodes to places; hence, $\mathcal{G}$ is fully characterized by the function

[TABLE]

associating with each node $B$ the set of all places $t$ such that $\langle B,t\rangle$ is an edge of $\mathcal{G}$. The elements of $\mathcal{T}({B})$ are the targets of $B$, and $\mathcal{T}$ is the target function of $\mathcal{G}$. Thus, we usually represent $\mathcal{G}$ by $\mathcal{T}$.

Definition 4** (Compliance with a $\mathcal{P}$-graph).**

A ${\mathscr{P}}$-partition $\Sigma$ is said to comply with a syllogistic $\mathcal{P}$-graph $\mathcal{G}$ (and, symmetrically, the syllogistic $\mathcal{P}$-graph $\mathcal{G}_{\Sigma}$ is said to be induced by the ${\mathscr{P}}$-partition $\Sigma$) via the map $q\mapsto q^{(\bullet)}$, where $|\Sigma|=|\mathcal{P}|$ and $q\mapsto q^{(\bullet)}$ belongs to $\Sigma^{\mathcal{P}}$, if

1. (a)

the map $q\mapsto q^{(\bullet)}$ is bijective, and 2. (b)

the target function $\mathcal{T}$ of $\mathcal{G}$ satisfies

[TABLE]

*for every $B\subseteq\mathcal{P}$.       ** * **

Definition 5**.**

A $\mathcal{P}$-graph is realizable if there exists a transitive partition complying with it.

Definition 6**.**

A transitive partition $\Sigma$ (and its $\mathcal{P}$-graph $\mathcal{G}_{\Sigma})$ is computable if it has a formative process with length bounded by a computable function in ${\left|{\Sigma}\right|}$.

In [COU02] it is showed that all partitions are computable.

Example 1**.**

Here we show a couple of realizable $\mathcal{P}$-graphs:

The following are instead not realizable $\mathcal{P}$-graphs:

Now we introduce the technique of formative processes which allows to create transitive partition step by step starting from the empty partition.

Definition 7** (Formative processes).**

Let $\Sigma,\Sigma^{\prime}$ be partitions such that

• •

every block $\sigma\in\Sigma$ has a block $\sigma^{\prime}\in\Sigma^{\prime}$ for which $\sigma\subseteq\sigma^{\prime}$;

• •

$\sigma_{0},\sigma_{1}\subseteq\tau$ implies $\sigma_{0}=\sigma_{1}$ when $\sigma_{0},\sigma_{1}\in\Sigma$ and $\tau\in\Sigma^{\prime}$.

Then we say that $\Sigma^{\prime}$ frames $\Sigma$(in some articles extend). When $\Sigma^{\prime}$ frames $\Sigma$, and moreover

[TABLE]

then the ordered pair $\langle\Sigma,\Sigma^{\prime}\rangle$ is called an action (via $\Gamma$)(in some articles prolongation).

A (formative) process is a sequence \big{(}\mathcal{P}_{\mu}\big{)}_{\mu\leqslant\xi} of partitions, where $\xi$ can be any ordinal and, for every ordinal $\nu<\xi$,

• •

$\mathcal{P}_{\nu}=\emptyset$ if $\nu=0$;

• •

$\langle\mathcal{P}_{\nu}\/,\mathcal{P}_{\nu+1}\rangle$ is an action;

• •

$\mathcal{P}_{\lambda}$ frames $\mathcal{P}_{\nu}$, and $\bigcup\mathcal{P}_{\lambda}\subseteq\bigcup\{\bigcup\mathcal{P}_{\gamma}\,\texttt{:}\>\gamma<\lambda\}$, for every limit ordinal $\lambda$ such that $\nu<\lambda\leqslant\xi$.

For all $\mu\leqslant\xi$ and $\tau\in\mathcal{P}_{\xi}$, we put

[TABLE]

Notice that $\tau^{(\mu)}=\tau\cap\bigcup\mathcal{P}_{\mu}$ holds.

A process \big{(}\mathcal{P}_{\mu}\big{)}_{\mu\leqslant\xi} is said to be greedy (in some articles coherence requirement) if, for all $\nu<\xi$ and $\Gamma\subseteq\mathcal{P}_{\nu}$, the following holds:

[TABLE]

To stress the fact that no greediness assumption is made for a given formative process \big{(}\mathcal{P}_{\mu}\big{)}_{\mu\leqslant\xi}, this may be referred to as a weak process.

Then, for all $\mu\leqslant\xi$, $\nu<\xi$, $p\in\mathcal{P}$, $B\subseteq\mathcal{P}$, we will designate by $p^{(\mu)},B^{(\mu)},B^{(\bullet)},\Delta^{(\nu)}(p),A_{\nu}$, respectively, the unique sets such that

[TABLE]

we shall call

• •

$A_{\nu}$, the $\nu$-th move of the process;

• •

$\mathfrak{T}=(A_{\nu})_{\nu<\xi}$, the trace of the process, $\mathfrak{T}_{\mu}=(A_{\nu})_{\nu\leq\mu<\xi}$ the $\mu$-partial trace of the process;

• •

$(A_{\nu},T_{\nu})_{\nu<\xi}$, the history of the process (or, sometimes, the history of the final partition $\mathcal{P}_{\xi}$.

I give some definitions regarding formative processes which will be useful in the prosecution

Definition 8**.**

Let $\mathcal{H}:=<(\mathcal{P}^{\mu})_{\mu<\xi},(\bullet),\mathcal{T}>$ be a (greedy) formative process with trace $(A_{\mu})_{\mu<\xi}$ for a given transitive partition $\Sigma=\mathcal{P}^{(\xi)}$ and let $\mathcal{G}_{\xi}$ be the $\mathcal{P}$-graph induced by $\Sigma$. Then

• •

$FCr(A\rightarrow\delta)$* for $A\subseteq\mathcal{P},\delta\in\mathcal{P}$ is equal to the $\min\{\mu\mid\Delta^{(\mu)}(\delta)\neq\emptyset\wedge A_{\mu}=A\}$*

• •

$LE(\sigma)$* for $\sigma\in\mathcal{P}$ is equal to the $\sup\{\mu\mid\sigma^{(\mu)}=\emptyset\}$*

• •

$FE(\sigma)\subseteq\mathcal{P}$* for $\sigma\in\mathcal{P}$ is equal to a node $A$ such that $FCr(A\rightarrow\sigma)=LE(\sigma)$*

• •

$\mathfrak{N}(A)=\{\mu\mid A=A_{\mu}\}$**

• •

$Aff(\sigma)=\{A\mid\sigma\in\mathcal{T}(A)\}$**

• •

If $x\in\Delta^{(\mu)}(q)$ for some $q$ then $x$ is ${\bf new}$ at the step $\mu$. we denote by $New^{(\mu)}$ the collection of all new objects at the step $\mu$

• •

If Suppose $x\in\sigma\in A$ and $x\notin\mathsf{TrCl}({\mathscr{P}}^{\ast}({A^{(\mu)}})\cap\bigcup_{p\in\mathcal{T}(A)}p^{(\mu)})$ then $x$ is ${\bf unused}$ at the step $\mu$ for the node $A$. we denote by $Unused^{(\mu)}(A)$ the collection of all unused objects for $A$ at the step $\mu$ (obviously a new object at the step $\mu$ is, in particular, unused at the step $\mu$).

All the above notations have to specify the formative process to which they refer.

Remark 1**.**

Obviously a new element at the step $\mu$ is unused wherever it appears. On the converse an unused element could be not new. In a greedy process $Unused^{(\mu)}(A_{\mu})$ cannot be unused at the step $\mu+1$. Moreover any element $y\in{\mathscr{P}}^{\ast}({A^{(\mu)}})$ which contains an $x\in Unused^{(\mu)}(A)$ cannot be inside $\bigcup\mathcal{P}^{(\mu)}$ by disjointness of nodes and the unused condition.

In few words new elements at the step $\mu$ are just created, instead unused ones are not still used to build objects.

1.2 The Theory $\textnormal{{MLS}}\otimes$

Following [CU18] it should be enough just saying that $\textnormal{{MLS}}\otimes$ is a subtheory of the theory $\mathcal{S}$, but in order to make self-contained the article I give a brief description of $\textnormal{{MLS}}\otimes$. The details can be found in the same text.

1.3 Syntax and semantics of $\textnormal{{MLS}}\otimes$

The symbols of the language of $\textnormal{{MLS}}\otimes$ are:

• •

infinitely many set variables $x,y,z$, …;

• •

the constant symbol $\varnothing$;

• •

the set operators $\cdot\cup\cdot$, $\cdot\cap\cdot$, $\cdot\setminus\cdot$,$\cdot\otimes\cdot$;222By $\otimes$ we denote the unordered Cartesian product, where we have S\otimes T:=\big{\{}\{s,t\}\mid s\in S,t\in T\big{\}}.

• •

the set predicates $\cdot\subseteq\cdot$, $\cdot=\cdot$, $\cdot\in\cdot$.

The set of $\textnormal{{MLS}}\otimes$-terms is the smallest collection of expressions such that:

• •

all variables and the constant $\emptyset$ are $\textnormal{{MLS}}\otimes$-terms;

• •

if $s$ and $t$ are $\textnormal{{MLS}}\otimes$-terms, so are $s\cup t$, $s\cap t$, $s\setminus t$, $s\otimes t$.

$\textnormal{{MLS}}\otimes$-atoms have the form

[TABLE]

where $s,t$ are $\textnormal{{MLS}}\otimes$-terms.

$\textnormal{{MLS}}\otimes$-formulae are propositional combinations of $\textnormal{{MLS}}\otimes$-atoms, by means of the usual logical connectives $\wedge$ (conjunction), ${\bf\vee}$ (disjunction), ${\bf\neg}$ (negation), ${\bf\rightarrow}$ (implication), ${\bf\leftrightarrow}$ (bi-implication), etc. $\textnormal{{MLS}}\otimes$-literals are $\textnormal{{MLS}}\otimes$-atoms and their negations.

For an $\textnormal{{MLS}}\otimes$-formula or $\textnormal{{MLS}}\otimes$-term $\Phi$, we denote by $\mathrm{Vars}(\Phi)$ the collection of the set variables occurring in $\Phi$ (similarly for $\textnormal{{MLS}}\otimes$-terms). The size or length of $\Phi$, written $|\Phi|$, is defined as the number of nodes in the syntactic tree of $\Phi$.

The semantics of $\textnormal{{MLS}}\otimes$ is defined in the more natural way. A set assignment $M$ is any map from a collection $V$ of set variables (called the variables domain of $M$) into the universe $\mathcal{V}$ of all sets (in short, M\in\mbox{\boldmath\mathcal{V}}^{V} or $M\in\{\>\mbox{\rm sets}\>\}^{V}$). The set domain of $M$ is the set $\bigcup M[V]=\bigcup_{v\in V}Mv$ and the rank of $\mathcal{M}$ is the rank of its set domain, namely,

[TABLE]

(so that, when $V$ is finite, $\hbox{\sf rk}\;(M)=\max_{v\in V}~{}\hbox{\sf rk}\;(Mv)$). A set assignment $M$ is finite, if so is its set domain.

Let $M$ be a set assignment and $V$ its variables domain. Also, let $s,t,s_{1},\ldots,s_{n}$ be $\textnormal{{MLS}}\otimes$-terms whose variables occur in $V$. we put, recursively,

[TABLE]

In addition, for all $\textnormal{{MLS}}\otimes$-formulae $\Phi$, $\Psi$ such that $\mathrm{Vars}(\Phi),\mathrm{Vars}(\Psi)\subseteq V$, we put:

[TABLE]

(where, plainly, ${\bf t}$ and ${\bf f}$ stand the truth-values true and false, respectively), and

[TABLE]

The set assignment $M$ is said to satisfy an $\textnormal{{MLS}}\otimes$-formula $\Phi$ if $\Phi^{M}={\bf t}$ holds, in which case we also write $M\models\Phi$ and say that $M$ is a model for $\Phi$. If $\Phi$ has a model, we say that $\Phi$ is satisfiable; otherwise, we say that $\Phi$ is unsatisfiable. If $\Phi$ has a finite model, we say that it is finitely satisfiable. If $\Phi$ has a model $M$ such that $Mx\neq My$ for all distinct variables $x,y\in\mathrm{Vars}(\Phi)$, we say that it is injectively satisfiable. If $M^{\prime}\models\Phi$ for every set assignment $M^{\prime}$ defined over $\mathrm{Vars}(\Phi)$, then $\Phi$ is said to be true. Two $\textnormal{{MLS}}\otimes$-formulae $\Phi$ and $\Psi$ are said to be equisatisfiable if $\Phi$ is satisfiable if and only if so is $\Psi$.

1.3.1 The decision problem for $\textnormal{{MLS}}\otimes$

The decision problem (or satisfiability problem, or satisfaction problem) for $\textnormal{{MLS}}\otimes$ is the problem of establishing algorithmically whether any given $\textnormal{{MLS}}\otimes$-formula is satisfiable. If the decision problem for $\textnormal{{MLS}}\otimes$ is solvable, then $\textnormal{{MLS}}\otimes$ is said to be decidable. A decision procedure (or satisfiability test) for $\textnormal{{MLS}}\otimes$ is any algorithm which solves the decision problem for $\textnormal{{MLS}}\otimes$. The finite satisfiability problem for $\textnormal{{MLS}}\otimes$ is the problem of establishing algorithmically whether any given $\textnormal{{MLS}}\otimes$-formula is finitely satisfiable. The injective satisfiability problem for $\textnormal{{MLS}}\otimes$ is the problem of establishing algorithmically whether any given $\textnormal{{MLS}}\otimes$-formula is injectively satisfiable.

By making use of the disjunctive normal form, the satisfiability problem for $\textnormal{{MLS}}\otimes$ can be readily reduced to the same problem for conjunctions of $\textnormal{{MLS}}\otimes$-literals. In addition, by suitably introducing fresh set variables to name subterms of the following types

[TABLE]

where $t_{1},t_{2},t$ are $\textnormal{{MLS}}\otimes$-terms, the satisfiability problem for $\textnormal{{MLS}}\otimes$ can further be reduced to the satisfiability problem for conjunctions of $\textnormal{{MLS}}\otimes$-literals of the following types

[TABLE]

where $x,y,z$ stand for set variables or the constant $\emptyset$.

Finally, by applying the simplification rules illustrated in [CU18] the satisfiability problem for $\textnormal{{MLS}}\otimes$ can be reduced to the satisfiability problem for conjunctions of $\textnormal{{MLS}}\otimes$-atoms of the following types:

[TABLE]

which we call normalized conjunctions of $\textnormal{{MLS}}\otimes$.

1.3.2 Satisfiability by partitions

Let $V$ be a finite collection of set variables and $\Sigma$ a finite partition. Also, let $\mathfrak{I}\colon V\rightarrow{\mathscr{P}}({\Sigma})$. The map $\mathfrak{I}$ induces in a very natural way a set assignment $M_{{}_{\mathfrak{I}}}$ over $V$ by putting

[TABLE]

Definition 9**.**

Given a map $\mathfrak{I}\colon V\rightarrow{\mathscr{P}}({\Sigma})$ over a finite collection $V$ of set variables, with $\Sigma$ a finite partition, for any $\textnormal{{MLS}}\otimes$-formula $\Phi$ such that $\mathrm{Vars}(\Phi)\subseteq V$, the partition $\Sigma$ satisfies $\Phi$ via the map $\mathfrak{I}$, and write $\Sigma/\mathfrak{I}\models\Phi$, if the set assignment $M_{{}_{\mathfrak{I}}}$ induced by $\mathfrak{I}$ satisfies $\Phi$. we say that $\Sigma$ satisfies $\Phi$, and write $\Sigma\models\Phi$, if $\Sigma$ satisfies $\Phi$ via some map $\mathfrak{I}\colon V\rightarrow{\mathscr{P}}({\Sigma})$, with $\mathrm{Vars}(\Phi)\subseteq V$.

Thus, if an $\textnormal{{MLS}}\otimes$-formula $\Phi$ is satisfied by some partition, then it is satisfied by some set assignment. The converse holds too. Indeed, let us assume that $M\models\Phi$, for some set assignment $M$ over a given collection $V$ of set variables. Let $\Sigma_{M}$ be the Venn partition induced by $M$ and $\mathfrak{I}_{{}_{M}}\colon V\rightarrow{\mathscr{P}}({\Sigma_{M}})$ the map defined by putting

[TABLE]

Plainly, the set assignment induced by $\mathfrak{I}_{{}_{M}}$ is just $M$. Thus $\Sigma_{M}/\mathfrak{I}_{{}_{M}}\models\Phi$, so that $\Sigma_{M}\models\Phi$, proving that $\Phi$ is satisfied by some partition.

Therefore the notions of satisfiability by set assignments and that of satisfiability by partitions coincide.

2 The Technique of Cycles

In the present section I develop the technique of cycles in formative processes.

In a sense a $\mathcal{P}$-graph is a plumbing system, therefore there is a big difference between a plumbing system empty or partially empty and completely filled. A realizable $\mathcal{P}$-graph is a plumbing system that we can ensure that it could be completely filled.

The cycles are some kind of hydraulic pumps that guarantee that the part of system, which starts from them, could be filled anyway.

2.1 Well-Founded vertices

I may assume that:

• •

any $\mathcal{P}$-graph contains the empty node ;

• •

all vertices in a $\mathcal{P}$-graph are reachable from the empty node ;

• •

every node in a $\mathcal{P}$-graph has some target.

Definition 10**.**

The set of well-founded vertices333This notion could be omitted keeping just the weak version without affecting the proof of the main claim. Although I decide to maintain it anyway since it is definitely more natural and makes the approach to the principal one more gradual. of a $\mathcal{P}$-graph $\mathcal{G}$ is the minimal set $S$ of vertices of $\mathcal{G}$ such that, for each vertex $v$ in $\mathcal{G}$, if all the immediate predecessors of $v$ are in $S$, then so is $v$444Equivalently, a vertex of $\mathcal{G}$ is well-founded if it is not reachable from any cycle.

Definition 11**.**

Let be $v$ a vertex of a $\mathcal{P}$-graph $\mathcal{G}$ the branch of $v$ $Br(v)$ is the subgraph obtained by following the arrows in the reverse direction, having $v$ as a starting point.

Definition 12**.**

The subgraph of a $\mathcal{P}$-graph $\mathcal{G}$ induced by its well-founded vertices is the well-founded part of $\mathcal{G}$ and is denoted $\mathcal{G}_{WF}$.

Plainly, $\mathcal{G}_{WF}$ is acyclic and contains the empty node $\emptyset$. In addition, if $\mathcal{G}$ is acyclic, then $\mathcal{G}_{WF}=\mathcal{G}$. By assuming that membership edges have null weight, whereas propagation edges have unitary weight, we obtain the following definition of height $h(v)$ for the well-founded vertices of a $\mathcal{P}$-graph $\mathcal{G}_{WF}$ with target function $\mathcal{T}$:

[TABLE]

I use the ‘arrow’ notation $v^{\prime}\rightarrow v^{\prime\prime}$ to denote that $(v^{\prime},v^{\prime\prime})$ is an edge of a given $\mathcal{P}$-graph $\mathcal{G}_{WF}$ with target function $\mathcal{T}$, namely, that either

• •

$v^{\prime}$ is a place, $v^{\prime\prime}$ is a node, and $v^{\prime}\in v^{\prime\prime}$, or

• •

$v^{\prime}$ is a node, $v^{\prime\prime}$ is a place, and $v^{\prime\prime}\in T(v^{\prime})$

Thus, if $v_{1}\rightarrow v_{2}\rightarrow v_{3}$, for well-founded vertices $v_{1},v_{2},v_{3}$ then

• •

$h(v_{1})\leq h(v_{2})\leq h(v_{3})$, and

• •

$h(v_{1})<h(v_{3})$.

Here is an example of a $\mathcal{P}$-graph with the assigned height to the vertices.

Lemma 1**.**

Let $\Sigma$ be a transitive partition complying with a given $\mathcal{P}$-graph $\mathcal{G}$ via the map $q\rightarrow q^{(\bullet)}\in\Sigma^{\mathcal{P}}$. Then

(a)

$rk(q^{(\bullet)})\leq h(q)$, for every well-founded place $q\in\mathcal{P}$;

(b)

$rk(\bigcup B^{(\bullet)})\leq h(B)$**

Proof.

It is enough to observe that $p^{(\bullet)}\subseteq\bigcup{\mathscr{P}}^{\ast}[\mathcal{T}^{-1}(p)]=\bigcup_{B\rightarrow p}{\mathscr{P}}^{\ast}(B^{(\bullet)})$ where $\mathcal{T}$ is the target function of $\mathcal{G}$. Then,

• •

$rk(\emptyset^{(\bullet)})=0$

• •

$rk(q^{(\bullet)})\leq\max_{B\rightarrow p}(rk(B^{(\bullet)}))\leq\max_{B\rightarrow p}(h(B))+1)=h(q)$

• •

$rk(\bigcup B^{(\bullet)})\leq\max_{q\in B}(h(q))=h(B)$.

Using the notion of $WF$ vertices we ”prune” either the formative process and the $\mathcal{P}$-graph.

Definition 13** (Notation).**

Let $\mathcal{H}:=<(\mathcal{P}^{\mu})_{\mu<\xi},(\bullet),\mathcal{T}>$ be a (greedy) formative process with trace $(A_{\mu})_{\mu<\xi}$ for a given transitive partition $\Sigma=\mathcal{P}^{(\xi)}$ and let $\mathcal{G}_{\xi}$ be the $\mathcal{P}$-graph induced by $\Sigma$. Then we can define a flag function for vertices of a $\mathcal{P}$-graph related to the condition of a vertex $p$ at the stage $\mu$ in the following way

$WF^{(\mu)}_{\mathcal{H}}(p)=1$* iff $\sigma^{(\mu)}$ is well-founded in $\mathcal{G}_{\mu}$, $WF^{(\mu)}_{\mathcal{H}}(p)=0$ otherwise.*

Lemma 2**.**

Let $\mathcal{H}:=<(\mathcal{P}^{\mu})_{\mu<\xi},(\bullet),\mathcal{T}>$ be a (greedy) formative process with trace $(A_{\mu})_{\mu<\xi}$ for a given transitive partition $\Sigma=\mathcal{P}^{(\xi)}$ and let $\mathcal{G}_{\xi}$ be the $\mathcal{P}$-graph induced by $\Sigma$. Then

[TABLE]

where the $\uparrow\uparrow$ denotes the iterated exponentiation in Knuth’s uparrow notation and $h^{*}:=max\{h(q)\mid q\mbox{ is a well-founded place of }\mathcal{G}_{\xi}\}.$

Proof.

It is enough to observe that $h(q)\leq h^{*}$, for every well-founded place $q\in\mathcal{G}_{\xi}$. Therefore, if $A_{\mu}$ is well-founded, step $\mu$ in the formative process $\mathcal{H}$ will distribute elements in $\mathcal{H}$, and we have ${\left|{\mathcal{V}_{h^{*}+1}}\right|}=2\uparrow\uparrow(h^{*}+1)$.

Lemma 3**.**

Let $\mathcal{H}:=<(\mathcal{P}^{\mu})_{\mu<\xi},(\bullet),\mathcal{T}>$ be a (greedy) formative process with trace $(A_{\mu})_{\mu<\xi}$ for a given transitive partition $\Sigma=\mathcal{P}^{(\xi)}$ and let $\mathcal{G}_{\mu}$ be the $\mathcal{P}$-graph induced by $\mathcal{P}^{(\mu)}$ for $\mu\leq\xi$. Then

[TABLE]

Proof.

For $\mu\leq\xi$, let $h_{\mu}$ be the height function relative to the syllogistic graph $\mathcal{G}_{\mu}$. If $A_{\mu}$ is well-founded in $\mathcal{G}_{\mu}$, then

[TABLE]

Thus, $A_{\mu}$ will distribute elements in $\mathcal{V}_{{\left|{\Sigma}\right|}+1}$, and therefore

[TABLE]

Theorem 1**.**

Let $\mathcal{H}:=<(\mathcal{P}^{(\mu)})_{\mu<\xi},(\bullet),\mathcal{T}>$ be a (greedy) formative process with trace $(A_{\mu})_{\mu<\xi}$. Let $E:i\rightarrow\mu_{i}$ be the increasing ordinal enumeration of the set of ordinals $\mathfrak{M}_{W}$ Let $\xi_{W}:=dom(E)$. Then $(A_{\mu_{i}})_{i<\xi_{W}}$ is a trace of a greedy partial formative process $<(\mathcal{P}^{[\mu_{j}]})_{j<\xi_{W}},(\bullet),\mathcal{T}>$ such that:

• •

$q^{[j]}\subseteq q^{(\mu_{j})}$, for $j\leq\xi_{W}$ and $q\in\mathcal{P}$; in addition, if $q$ is well-founded in $\mathcal{G}_{\mu_{j}}$ , then $q^{[j]}=q^{(\mu_{j})}$

• •

${\mathscr{P}}^{\ast}(A_{\mu_{i}}^{[i]})\cap\bigcup\mathcal{P}^{[i+1]}={\mathscr{P}}^{\ast}(A_{\mu_{i}}^{(\mu_{i})})\cap\bigcup\mathcal{P}^{(\mu_{i}+1)}$**

[Sketch of the proof.

]

It is sufficient to prove that for all $q\in\mathcal{P}$ if $WF(q)^{\mu_{i+1}}_{\mathcal{H}}$ then for all $i$ $q^{(\mu_{i}+1)}=q^{(\mu_{i+1})}$ and that ${\mathscr{P}}^{\ast}(A_{\mu_{i+1}}^{(\mu_{i}+1)})\setminus\mathcal{P}^{(\mu_{i}+1)}={\mathscr{P}}^{\ast}(A_{\mu_{i+1}}^{(\mu_{i+1})})\setminus\mathcal{P}^{(\mu_{i+1})}$.

The key of the proof relies on that nothing happens to $WF$ vertices along the segment $\mu_{i}-\mu_{i+1}$.

Observe that in this segment of the process we call just $\neg WF$ nodes therefore their targets are either $\neg WF$ or they become $\neg WF$ at that step. This in turn implies that none of places feeded along $\mu_{i}-\mu_{i+1}$ can be $WF$ at the step $\mu_{i+1}$.

The second assert depends on the fact that different nodes have disjoint ${\mathscr{P}}^{\ast}$.

The $\mathcal{P}$-graph which results from this selection has all $WF$ nodes of $\mathcal{G}$ by Remark 5.

Hence $\mathcal{G}_{\mathfrak{M}_{W}}\supseteq\mathcal{G}_{WF}$.

Example 2**.**

Consider a transitive partition with the following $\mathcal{P}$-graph.

After pruning it can become

or this

depending on the transitive partition.

2.2 cart-imitate and weakly cart-imitate

I introduce a modification of $\mathcal{P}$-graph by introducing a new kind of arrow.

Definition 14**.**

I denote by ${\mathscr{P}}^{\ast}({A})_{1,2}$ the collection of elements of ${\mathscr{P}}^{\ast}({A})$ of cardinality 1 and 2.

I know that in a $\mathcal{P}$-graph generated by a partition $\Sigma$ there exists an arrow between a node $A$ and a place $q$ if and only if $q^{(\bullet)}\cap{\mathscr{P}}^{\ast}({B^{(\bullet)}})\neq\emptyset$. I require a filter on this set and we label an arrow by $\otimes$ if and only if the following happens $q^{(\bullet)}\cap{\mathscr{P}}^{\ast}({B^{(\bullet)}})_{1,2}\neq\emptyset$. I call such kind of arrow cart-arrow.

Remark 2**.**

The introduction of a new kind of arrow determines a new phenomenology. Indeed, the result of [COU02] does not hold for $\mathcal{P}$-graph with cart-arrows. This is because the realizability of such graphs is not anymore guaranteed from the fact that the usual one is realizable. A $\mathcal{P}$-graph could be realizable with the usual arrows instead it could fail to be true if we introduce cart-arrows, as the following example shows.

Example 3**.**

The following $\mathcal{P}$-graph is realizable. You find also, joined with the name of the vertex, its distance from the empty node.

Instead the following is not.

The above example, far from being just a curiosity, singles out a deep difference between the two different structures. This difference is determined from the inability of cartesian product to produce as many elements as exponential does. This has been the principal reason for the unfruitful attempts to solve the decidability of $\textnormal{{MLS}}\otimes$.

I have to adapt all the previous morphism theorems to the new context. This will make new sufficient conditions of a partition arise. These conditions allow a partition to inherit the capability to model $\otimes$-literals from another one.

Definition 15**.**

A partition $\widehat{\Sigma}$ is said to weakly cart-imitate another partition, $\Sigma$, when there is a bijection $\beta\colon\Sigma\rightarrow\widehat{\Sigma}$ such that, for $X\subseteq\Sigma$ and $\sigma\in\Sigma$,

1. (i)

if ${\mathscr{P}}^{\ast}({\beta[X]})\cap\beta(\sigma)\neq\emptyset$, then ${\mathscr{P}}^{\ast}({X})\cap\sigma\neq\emptyset$; 2. (ii)

$\bigcup\beta[X]\in\beta(\sigma)$* if and only if $\bigcup X\in\sigma$;* 3. (iii)

${\mathscr{P}}^{\ast}({\beta[X]})_{1,2}\cap\beta(\sigma)\neq\emptyset$* if and only if ${\mathscr{P}}^{\ast}({X})_{1,2}\cap\sigma\neq\emptyset$ and*

${\mathscr{P}}^{\ast}({\beta[X]})\setminus{\mathscr{P}}^{\ast}({\beta[X]})_{1,2}\cap\beta(\sigma)\neq\emptyset$* if and only if ${\mathscr{P}}^{\ast}({X})\setminus{\mathscr{P}}^{\ast}({X})_{1,2}\cap\sigma\neq\emptyset$*

The following lemma shows the above cited connection between weakly cart-imitation and satisfiability of $\otimes$-literals.

Lemma 4**.**

Let $\Sigma$ and $\widehat{\Sigma}$ be partitions such that $\widehat{\Sigma}$ weakly cart-imitates $\Sigma$ via an injective map $\beta\colon\Sigma\rightarrowtail\widehat{\Sigma}$, and let $\mathfrak{I}\colon V\rightarrow{\mathscr{P}}({\Sigma})$ be a map over a given finite collection $V$ of set variables. Then, for every literal $\ell$ of any of the following types

[TABLE]

(where $x,y,z$ stand for set variables in $V$), we have

[TABLE]

*where $\overline{\mathfrak{I}}:=\overline{\beta}\circ\mathfrak{I}$ and $\overline{\beta}$ is the image-map related to $\beta$.         *

Proof.

By Lemma 3.11 and 3.13 in [CU18] we are left to prove just $\otimes$-literals case.

If the following property

[TABLE]

holds we are done. Indeed, if $\mathfrak{I}$ satisfies $\otimes$-literals, then $\bigcup\beta[X]\subseteq\bigcup\beta[Y]\otimes\bigcup\beta[Z]$, which in turns implies that $\overline{\mathfrak{I}}$ satisfies the same literals.

Let us prove property 10.

Assume

[TABLE]

Let $t\in\bigcup\beta[X]$ then $t\in\beta(\sigma)$ for some $\sigma\in X$. By transitivity of $\Sigma$ there exists $B\subseteq\Sigma$ such that $t\in\beta(\sigma)\cap{\mathscr{P}}^{\ast}({\beta[B]})$, hence, from Definition 15 (i), we get $\sigma\cap{\mathscr{P}}^{\ast}({B})\neq\emptyset$.

By hypothesis, $B$ is equal to $\{p,q\}$ for some $p\in Y$ and $q\in Z$. If $t\in{\mathscr{P}}^{\ast}({\beta(p),\beta(q)})\setminus{\mathscr{P}}^{\ast}({\beta(p),\beta(q)})_{1,2}$ then, by Definition 15(iii), ${\mathscr{P}}^{\ast}({p,q})\setminus{\mathscr{P}}^{\ast}_{1,2}({p,q})\cap\sigma\neq\emptyset$. This last fact contradicts initial hypothesis.

Definition 16**.**

A node $A$ is saturated in the process $\mathcal{H}:=<(\mathcal{P}^{\mu})_{\mu<\xi},(\bullet),\mathcal{T}>$ iff ${\mathscr{P}}^{\ast}({A^{(\xi)}})\subseteq\bigcup\mathcal{P}^{\xi}$.

If we limit this condition to the unordered pairs, we say that $A$ is cart-saturated in $\mathcal{H}:=<(\mathcal{P}^{\mu})_{\mu<\xi},(\bullet),\mathcal{T}>$.

we omit to indicate the process whenever it is clear from the context. If there exists a $\lambda<\xi$ such that $A^{(\lambda)}=A^{(\xi)}$ then we say that $A$ is saturated (or cart-saturated) at $\lambda$.

Remark 3**.**

Transitivity and saturation are dual properties. The former is needed to prove the first inclusion of the $\otimes$-literals, the latter the reverse one.

Definition 15 is not enough to prove the whole equality, therefore, in order to guarantee the satisfiability of $\otimes$-literals, we need the following extra condition.

Definition 17**.**

Assume $\widehat{\Sigma}$ weakly cart-imitate $\Sigma$, if moreover it satisfies

• (iv)

*[cart-saturated condition] if ${\mathscr{P}}^{\ast}_{1,2}({X})\subseteq\bigcup\Sigma$, then ${\mathscr{P}}^{\ast}_{1,2}({\beta[X]})\subseteq\bigcup\beta[\Sigma]$. *

then $\widehat{\Sigma}$ is said to cart-imitate $\Sigma$

In this case the following holds

[TABLE]

Proof.

Assume $\bigcup X\supseteq\bigcup Y\otimes\bigcup Z$ and $\{w,w^{\prime}\}\in\bigcup\beta[Y]\otimes\bigcup\beta[Z]$ then there exist $p\in Y$ and $q\in Z$ such that $\{w,w^{\prime}\}\in{\mathscr{P}}^{\ast}_{1,2}({\beta(p),\beta(q)})$. By hypothesis ${\mathscr{P}}^{\ast}_{1,2}({p,q})$ is entirely distributed and by Definition (iv) ${\mathscr{P}}^{\ast}_{1,2}({\beta[p,q]})\subseteq\bigcup\beta[\Sigma]$. Hence there exists $\sigma$ such that $\{w,w^{\prime}\}\in\beta(\sigma)$. By Definition 15 (iii) and initial hypothesis ${\mathscr{P}}^{\ast}_{1,2}({p,q})\cap\sigma\neq\emptyset$ and $\sigma\in X$ therefore $\{w,w^{\prime}\}\in\bigcup\beta[X]$ as claimed.

Resuming,

Theorem 2**.**

Let $\mathfrak{I}\colon V\rightarrow{\mathscr{P}}({\Sigma})$ be a map over a given finite collection $V$ of set variables, which is a model of $\Phi\in\textnormal{{MLS}}\otimes$, $\Sigma$ the transitive partition related to the model $\mathfrak{I}$ and $\mathcal{G}_{\Sigma}$ its $\mathcal{P}$-graph with cart-arrows. Let $\Sigma^{\prime}$ be a transitive partition such that $\Sigma^{\prime}$ (Weakly) cart-imitates $\Sigma$ via an injective map $\beta\colon\Sigma\rightarrowtail\Sigma^{\prime}$, then the assignment $\overline{\mathfrak{I}}$ of $\Sigma^{\prime}$ inherited from $\mathfrak{I}$ is a model for $\Phi$ (if weakly for $\Phi^{-}$).

Remark 4**.**

Observe that compared with the original notion of imitate the cart-imitation requires to preserve more structure than before since a new kind of arrow appears. An immediate consequence of this fact is that if a node $B$ has a cart arrow then it has to be composed of not more than 2 places. A less immediate consequence is that this notion can force the cardinality of places.

Indeed, if the principal target condition must be satisfied through a cart arrow then the principal union has to be a couple. It turns out that the two places of $B$ have both cardinality 1. I call such places blocked places. Whenever such places are involved in a cycle this cannot be repeated more than once, for this reason we shall call such cycles blocked cycles.

The two inclusions related to $\otimes$-literals, $x\subseteq y\otimes z$ and $x\supseteq y\otimes z$ could be satisfied through Definitions (iii)15 and 17. The former depends only on the arrows therefore it suffices coping a process to satisfy the property. Instead, the latter could trigger off a circular phenomenon which makes the property impossible to satisfy in a finite number of steps. Indeed, trying to saturate a node you could make another one to be saturated. Then you try to saturate the other one and so on. This can produce a circular request. The following example shows this pathology.

Example 4**.**

\begin{array}[]{l}\left(\begin{array}[]{c}\alpha^{(\mu)}\\ \beta^{(\mu)}\end{array}\right)_{\mu\leq 4}=\left(\begin{array}[]{c|c|c|c|c|c}\emptyset&\emptyset^{1}&\emptyset^{1}&\emptyset^{1}&\emptyset^{1}&\dotsc\\ \emptyset&\emptyset&\emptyset^{2}&\{\emptyset^{1},\emptyset^{2}\}&\{\{\emptyset^{1},\emptyset^{2},\emptyset^{3},\{\emptyset^{1},\emptyset^{2}\}\}\}&\dots\end{array}\right)\\ \end{array}**

with history

\begin{array}[]{l}\left(\begin{array}[]{c}A_{\mu}\\ T_{\mu}\end{array}\right)_{\mu<4}=\left(\begin{array}[]{c|c|c|c}\emptyset&\{\alpha\}&\{\beta\}&\{\beta\}\\ \{\alpha\}&\{\beta\}&\{\beta\}&\{\beta\}\end{array}\right)\\ \end{array}.

In this last case there is just one way to saturate the node: pumping cycle technique. That means to infinitely iterate the cycle many times, until a limit ordinal step is reached. Such a technique has been originally developed in [Urs05] then refined in [CU14].

This is the reason why satisfying a formula of $\textnormal{{MLS}}\otimes$ could require necessarily an infinite model.

In those cases the only way to achieve a finite assignment which ensures the existence of a model is to create a $\mathcal{P}$-graph with cycles which, at request, can be iterated until the saturation is reached. Those assignments are usually called a finite representation of the infinite or model which witnesses the infinite, as the following definition explains.

Definition 18**.**

For a given partition $\Sigma$ if the partition $\widehat{\Sigma}$ has a formative process \big{(}\mathcal{P}_{\mu}\big{)}_{\mu\leqslant\xi} which ensures that a new partition $\widehat{\Sigma}^{\prime}$ which cart-imitates $\Sigma$ can be created then $\widehat{\Sigma}$ witnesses cart-simulation of $\Sigma$.

2.3 Weakly Well-Founded Vertices

The main goal of the definition of well-founded vertex consists in relating the structure of $P$-graph with its production of elements. This concept glues the semantics and the syntactics of $P$-graphs. Indeed, starting from this notion, I have inferred the the maximal cardinality of calls of a node, using its distance from the empty node. Unfortunately this concept prevents the existence of cycles in the branch of a well-founded node, because this fact usually causes an uncontrolled production of elements and therefore of calls.

In this section I motivate a slight extension of the above definition to a more flexible one. There are various reasons to try to extend the notion of distance from the empty node. As I pointed out, a fairly general setting is that the distance between a vertex and the empty node cannot be defined whenever I have a cycle. However if a cycle cannot be repeated uncontrolled many times, this argument is no longer an obstacle in the definition of distance from the empty node. This question takes substance from the existence of the already mentioned kind of cycle, the blocked one. Although there is another type of cycle that falls into this series: the so called ”asphyxiated” cycle.

Hence the question is whether there is a good notion of distance from empty node which takes into account those kinds of phenomena.

The new definition of distance, the distance from the empty node of ”weakly well founded” vertices, that I am going to introduce, serves the purpose.

However, at first, I eliminate at least one of the pathological cycles through the linearization procedure, a pure technical artifice.

2.3.1 The elimination of blocked cycle through linearization procedure

The blocked cycles are not real ones since they cannot be repeated more than once, this is the reason why the linearization makes sense. Indeed, I cannot follow up the cart-Principal Target arrow (the so called ”funnel” arrow) more than once. Indeed, after passing it I can run across the cycle only until this arrow appears again (without passing it one more time). In few words the blocked cycle can be run across less than twice.

Practically, the linearization procedure simply transforms the cycle in a simple path of double the length that of the cycle.

I will refer to the application of such a procedure as linearizating or untying of a cycle.

I set the scene by outlining the modification of a formative process which creates a blocked cycle. As soon as a blocked cycle begins to repeat itself I introduce new copies, by a labelling procedure, of places and elements involved in the cycle at that stage of the process. For example, suppose to replace $\sigma$ with $\sigma_{a}$, as well as all its elements $x$ with $x_{a}$. Going on, one just uses the version $*_{a}$ of the objects in place of $*$ ones. Since the cycle cannot be repeated more than once, no more than one copy can be created. The $\mathcal{P}$-graph, related to this new process, has not blocked cycles.

Obviously one can achieve again the original $\mathcal{P}$-graph and process simply by quotient $*_{a}=*$.

This procedure applies to a process whenever a blocked cycle appears. Therefore, without loss of generality, I can assume that all $\mathcal{P}$-graphs do not contain any blocked cycle.

2.3.2 Asphyxiated Cycle

At first and intuitive sight it seems that a cycle is a path that can be repeated infinitely many times and, in its semantic counterpart, can create infinitely many elements. Unfortunately the structure of our language provides at least two counterexamples which contradict such intuitive approach. The first one was already considered and solved in the previous section. The blocked cycle cannot be repeated an infinite amount of times because it has at least one funnel. Therefore we might think that whenever there is not such a funnel, the capability to produce infinitely many elements is restored again. This is in a sense true. Indeed, the asphyxiated cycle could produce an unbounded quantity of elements but it cannot distribute them along some designated arrows. In particular, the cardinality of the new elements, that can be distributed along such arrows, is computable and depends only on the distance of the cycle from the empty node. The core argument for defining weakly well-found vertices lies exactly on this. Example 5.8 in [CU18] provides a meaningful instance of this phenomenon.

In this case there is just one new element that can be used either to repeat the cycle or to trigger off the external branch, but not together. This fact causes the pathology.

This strange phenomenon maintains the capability of the cycle to produce infinite many elements but not to create an increasing amount of new elements step by step. In a sense even if an increasing amount of elements is generated the cardinality of the new ones stay constant.

Luckily, in spite of its colloquial nature, this argument can be perfectly defined in a formal way in terms of $\textnormal{{MLS}}\otimes$. Indeed, there is a necessary and sufficient condition that depicts it properly.

In practice, whenever such a cycle receives $k$ new elements from an external branch it is not capable of increasing this $k$ during its iteration. This in particular determines its own way to propagate along external branch. This shadow process cannot differ too much from the oracle one. Indeed, if the oracle process uses $k$ new elements to propagate along cart external branch, the shadow one must do the same. In other words the shadow process can copy the oracle process as it does in the well-founded part of the $\mathcal{P}$-graph, this is the reason why all nodes attached to asphyxiate cycles and well-founded nodes can be considered analogues of well-founded nodes and, for this reason, designated as weakly well-founded nodes.

Definition 19**.**

An asphyxiate cycle $\mathbf{C}$ is a cycle that in its iteration does not change the number of its unused elements (i.e. $Unused^{(\mu)}(A)\ A\in\mathbf{C}$). we denote the collection of maximal asphyxiated cycles by $\mathfrak{AC}$.

The following lemma expresses in a formal way the characteristic of this object:

Lemma 5**.**

A cycle is asphyxiated iff all the arrows of the cycle are cart-type, moreover all the places of nodes of the cycle not involved in the cycle contain at most one element.

Proof.

The proof is trivial. Indeed, if a cycle has new elements, operator ${\mathscr{P}}^{\ast}$ does not increase their number iff the cycle has only cart-arrows and the place not involved in the cycle has exactly one element.

In view of recent considerations it is natural to introduce a generalized notion of well-founded node. Indeed, for our scopes it turns out to be useful to include among the well-founded nodes those ones which in their branch have not cycles but the asphyxiated ones. Moreover they can be attached to the cycles only through cart arrows. This is because a normal arrow does not control the combinatorial explosion of elements, as we shall soon see.

Definition 20**.**

Consider a cycle $\mathbf{C}$ we define

• •

$\mathcal{T}(\mathbf{C})=\bigcup_{A\in\mathcal{N}\cap\mathbf{C}}\mathcal{T}(A)\setminus\{\sigma\mid\sigma\in\mathbf{C}\}$, External Targets of $\mathbf{C}$;

• •

$Aff(\mathbf{C})=\{A\mid A\in Aff(\sigma)\wedge\sigma\in\mathcal{C}\wedge A\notin\mathcal{C}\}$, Afferent of $\mathbf{C}$;

• •

$AffPl(\mathbf{C})=\{\sigma\mid\sigma\in A\in\mathbf{C}\wedge\sigma\notin\mathbf{C}\}$, Afferent places of $\mathbf{C}$;

• •

$Out(\mathbf{C})=\{A\rightarrow\sigma\mid A\in\mathbf{C}\wedge\sigma\notin\mathbf{C}\}$, Out-arrows of $\mathbf{C}$;

• •

$In(\mathbf{C})=\{A\rightarrow\sigma\mid\sigma\in\mathbf{C}\wedge A\in Aff(\mathbf{C})\}$, In-arrows of $\mathbf{C}$.

Definition 21**.**

A vertex $v$ is recursively defined as weakly well-founded ($WWF$) if the following hold:

$Branch(v)$* does not contain cycles but asphyxiated ones,* 2. 2.

For any asphyxiated cycle $\mathbf{C}$ in $Branch(v)$, $Out(\mathbf{C})$, restricted to $Branch(v)$, is composed only of cart-arrows. 3. 3.

If $v=\mathbf{C}$ asphyxiated cycle, then $In(\mathbf{C})$ and $AffPl(\mathbf{C})$ are composed of only $WWF$ vertices.

This means that an asphyxiated cycle could behave in two different ways: as an asphyxiated cycle along cart-arrows in $Out(\mathbf{C})$, as an usual pumping cycle along the remainder of $Out(\mathbf{C})$.

In order to extend the definition of distance from the empty node in the weakly well-founded context we need first to set the distance of an asphyxiated cycle from the empty node. Actually it is sufficient to deal with such a cycle as a generalized $\mathcal{P}$-node. we consider only maximal asphyxiated cycle that is the maximal equivalent component.

I now introduce some auxiliary definitions. we shall use an analogue of Notation13 for $WWF$, namely $WWF^{(\mu)}_{\mathcal{H}}(A)$ stands for $A\in\mathcal{N}$ $WWF$ in $\mathcal{G}^{\mu}$ for a process $\mathcal{H}$.

If $v$ is a $WF$ vertex not $WWF$ we define its distance from the empty node as usual.

Otherwise if $\mathbf{C}$ is a $WWF$ asphyxiated cycle we define its distance from the empty node in the following way

[TABLE]

Where $v=q$ is a place or $v=B$ is a node in $\mathcal{C}$, then

[TABLE]

Otherwise

[TABLE]

Observe that vertices in an asphyxiated cycle are not $WWF$.

3 $\textnormal{{MLS}}\otimes$ is Decidable

First I extend all results of Section 2 to $WWF$-context.

By ”calling a cycle $\mathbf{C}$” I mean calling for distributing along $Out(\mathbf{C})$ a node of $\mathbf{C}$. Whenever I deal with an asphyxiated one this must happen through a cart-arrow.

Let introduce some notations useful in the following.

Let $\mathcal{H}:=<(\mathcal{P}^{\mu})_{\mu<\xi},(\bullet),\mathcal{T}>$ be a (greedy) formative process with trace $(A_{\mu})_{\mu<\xi}$ for a given transitive partition $\Sigma=\mathcal{P}^{(\xi)}$, $\mathfrak{T}$ its trace and $\mathcal{G}_{\mu}$ the $\mathcal{P}$-graph induced by $\mathcal{P}^{(\mu)}$ for $\mu\leq\xi$.

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

Lemma 6**.**

Let $\mathcal{H}:=<(\mathcal{P}^{\mu})_{\mu<\xi},(\bullet),\mathcal{T}>$ be a (greedy) formative process with trace $(A_{\mu})_{\mu<\xi}$ for a given transitive partition $\Sigma=\mathcal{P}^{(\xi)}$ and let $\mathcal{G}_{\mu}$ be the $\mathcal{P}$-graph induced by $\mathcal{P}^{(\mu)}$ for $\mu\leq\xi$. Let $H={\left|{\Sigma}\right|}^{2}2^{{\left|{\Sigma}\right|}}$ then

[TABLE]

where $l$ is the maximum distance of a vertex or an asphyxiated cycle WWF from the empty node.

Proof.

We observe that

[TABLE]

At first consider a node $A$ such that $WWF^{\xi}(A)=1$, let estimate $\mathfrak{M}_{A}$.

Remark 5**.**

Let $\mathcal{H}:=<(\mathcal{P}^{(\mu)})_{\mu<\xi},(\bullet),\mathcal{T}>$ be a greedy formative process with trace$(A_{\mu})_{\mu<\xi}$ for a given transitive partition $\Sigma=\mathcal{P}^{(\xi)}$, and let $\mathcal{G}_{\mu}$ be the $\mathcal{P}$-graph induced by $\mathcal{P}^{(\mu)}$, for $\mu\leq\xi$. Let us put

[TABLE]

and let $W_{\mu}$ be the set of well-founded places in $\mathcal{G}_{\mu}$. Then, for every $\mu<\nu<\rho\leq\xi$, we have:

• •

$(W_{\nu}\setminus W_{\mu})\cap W_{\rho}=\emptyset$**

(namely, when a place becomes non-well-founded, it will remain non-well-founded)

• •

$W_{\mu}\cap\mathcal{P}_{\nu}\subseteq W_{\nu}$**

(namely, any well-founded place at stage $\mu$ which is active at a later stage $\nu$ is also well-founded at stage $\nu$)

Suppose we are able to calculate ${\left|{\mathfrak{N}_{A}}\right|}$ (of course ${\left|{\mathfrak{N}_{A,\mu}}\right|}$, as well).

By the previous remark the following holds

[TABLE]

Therefore we can compute the $WWF$-side of the formula 14.

We are left to prove the $\neg WWF$-side

Consider a node $A$ such that such that $WWF^{(\xi)}(A)=0$, let compute $\mathfrak{M}_{A}$.

Possibly $A$ is such that $WWF^{(\mu)}(A)=1$ for some $\mu<\xi$. Let $\mu$ the last stage such that this holds. After $\mu$, as consequence of this, $A$ will not appear anymore in $\mathfrak{M}$ therefore $\mathfrak{M}_{A}=\mathfrak{M}_{A,\mu}$.

Moreover $WWF^{(\mu)}(A)=1$ therefore the above arguments hold again, then $\mathfrak{N}_{A,\mu}=\mathfrak{M}_{A,\mu}$, which in turn implies $\mathfrak{M}_{A}=\mathfrak{M}_{A,\mu}=\mathfrak{N}_{A,\mu}$, which we have assumed to be computable. Therefore the $\neg$WWF-side of the formula 14 can be computed and we are done.

To finish the proof we have to show how calculating ${\left|{\mathfrak{N}_{A}}\right|}$. Actually we show that ${\left|{\mathfrak{N}_{A}}\right|}\leq H^{l}$ with $l$ the maximum distance from the empty node. We proceed by induction on $n\leq l$. The base case is obvious.

Suppose by inductive hypothesis that all node $A$ such that $WWF^{(\xi)}(A)=1$ with distance $m<n$ cannot appear in $\mathfrak{N}_{A}$ more than $H^{m}$-times and we prove that a node $A$ such that $WWF^{(\xi)}(A)=1$ with distance $n$ cannot appear in $\mathfrak{N}_{A}$ more than $H^{n}$-times.

A node can be call at most as many times as a single place receives elements.

Likely a $WWF$ asphyxiated cycle can be called as many times as a single place of the cycle receives elements from abroad. This is because the number of unused elements of a single node of the cycle does not increase by repeating the cycle. Moreover the places of the nodes in the cycle which do not belong to the cycle itself cannot contain more than one element therefore, once the cycle is activated, they cannot receive anymore elements.

$p$ is $WWF$. A place can be supplied at most by $2^{{\left|{\Sigma}\right|}}$ nodes or asphyxiated cycles with distance from the empty node less than $n$. By induction hypothesis each of them can be called not more than $H^{n-1}$-times. Therefore $p$ can be called not more than ${\left|{\Sigma}\right|}2^{{\left|{\Sigma}\right|}}H^{n-1}$-times therefore less than $H^{n}$-times. 2. 2.

$p$ is an $WWF$ asphyxiated cycle.

This cycle can be called as many times as receives new elements therefore it depends from the nodes which come in the cycle from abroad. Each of them is $WWF$ and they have distance less than $n$ therefore each of them can be called not more than ${\left|{\Sigma}\right|}2^{{\left|{\Sigma}\right|}}H^{n-1}$. Considering all possible such nodes not more than ${\left|{\Sigma}\right|}^{2}2^{{\left|{\Sigma}\right|}}H^{n-1}$ therefore this cycle cannot be called to distribute not more than $H^{n}$-times.

Theorem 3**.**

Let $\mathcal{H}:=<(\mathcal{P}^{(\mu)})_{\mu<\xi},(\bullet),\mathcal{T}>$ be a (greedy) formative process with trace $(A_{\mu})_{\mu<\xi}$. Let $E:i\rightarrow\mu_{i}$ be the increasing ordinal enumeration of the set of ordinals in $\mathfrak{M}$

Let $\xi_{WW}:=dom(E)$. Then $(A_{\mu_{i}})_{i<\xi_{WW}}$ is a trace of a greedy partial formative process $<(\mathcal{P}^{[\mu_{j}]})_{j<\xi_{WW}},(\bullet),\mathcal{T}>$ such that:

• •

$q^{[j]}\subseteq q^{(\mu_{j})}$, for $j\leq\xi_{WW}$ and $q\in\mathcal{P}$; in addition, if $q$ is WWF in $\mathcal{G}_{\mu_{j}}$ , then $q^{[j]}=q^{(\mu_{j})}$

• •

${\mathscr{P}}^{\ast}(A_{\mu_{i}}^{[i]})\cap\bigcup\mathcal{P}^{[i+1]}={\mathscr{P}}^{\ast}(A_{\mu_{i}}^{(\mu_{i})})\cap\bigcup\mathcal{P}^{(\mu_{i}+1)}$**

Proof.

Sketch of the proof

In order to follow the oracle formative process building the shadow process step by step in the usual manner(see [CU18] for constructing a shadow process from an oracle one) we need to preserve the following properties:

Cardinality of $WWF$ places. 2. 2.

Cardinality of ${\left|{q\cap pow^{*}A}\right|}$ when $A\in WWF$. 3. 3.

Cardinality of unused elements of $WWF$ asphyxiated cycles.

If a node $A$ does not belong to an asphyxiated we construct the partition which distribute elements along the targets, as usual. Otherwise suppose the oracle process call at the step $\mu_{i}$ a node $A_{\mu_{i}}$ of a $WWF$ asphyxiated cycle $\mathbf{C}$ which distributes outside of the cycle through a cart-arrow. The cardinality of unused elements inside the cycle are preserved therefore $Unused^{(\mu_{i})}(\mathbf{C})=Unused^{[i]}(\mathbf{C})$. What we don’t know is where those elements are. No matter in which node of the cycle the unused elements are, we call the cycle until the designated node $A_{\mu_{i}}$. Since the number of unused elements do not increase, in the step $(\mu_{i})$ the unused elements are the same, therefore $A_{\mu_{i}}$ can distribute exactly as the oracle process does. Then we can copy step $\mu_{i}$ with the step $[i]$. In particular $\Delta^{[\ ]}(\sigma)=\Delta^{(\ )}(\sigma)$ along the cart-arrow outside the cycle therefore the listed properties are maintained.

Definition 22**.**

Let $\mathcal{G}$ be the $\mathcal{P}$-graph realized by a given greedy formative process $\mathcal{H}:=<(\mathcal{P}^{(\mu)})_{\mu<\xi},(\bullet),\mathcal{T}>$ and $\mathcal{G}_{WW}$ the $\mathcal{P}$-graph realized by the formative process $\mathcal{H^{\prime}}:=<(\mathcal{P}^{[\mu]})_{\mu<\xi_{WW}},(\bullet),\mathcal{T}>$ described in the preceding lemma. we call it the weakly-well-founded part of $\mathcal{G}$ relative to $\mathcal{H}$. (When $\mathcal{H}$ is understood, we shall just call it the weakly well-founded part of $\mathcal{G}$.)

Now we are going to show that the $WWF$ side of the graph can create a partition which complies with the whole graph

Let define the following relationship among cycles.

Definition 23**.**

Given two cycles $\mathcal{C}_{1},\mathcal{C}_{2}$, if there exists a path starting from $\mathcal{C}_{1}$ and containing $\mathcal{C}_{2}$ then we write $\mathcal{C}_{1}\leq\mathcal{C}_{2}$. Moreover if $\mathcal{C}_{1}\leq\mathcal{C}_{2}$ but $\neg(\mathcal{C}_{1}\leq\mathcal{C}_{2})$ then we write $\mathcal{C}_{1}<\mathcal{C}_{2}$, viceversa we write $\mathcal{C}_{1}\equiv\mathcal{C}_{2}$, which is an equivalence equation.

We first observe that an asphyxiated cycle cannot be equivalent to a usual cycle, hence its maximal component has to be an asphyxiated cycle too. Moreover a WWF asphyxiated cycle $\mathbf{C}$ cannot have in its branch an usual cycle, but since it can behave in a duplex way, as $WWF$ along its cart out arrow as usual pumping cycle along its usual out arrow, it could happen $\mathbf{C}<\mathcal{D}$ for a pumping $\mathcal{D}$.

Definition 24** (Minimal System of Generators(MSG)).**

Given a realizable $P$-graph $G$, let consider the equivalence classes of equivalence relation $\equiv$. Select a collection of minimal classes respect the relationship $\leq$ and for a given formative process consider for each minimal class the first cycle formed along the process. We call such a selection $\mathcal{BG}=\{\mathcal{C}_{1},\dots,\mathcal{C}_{n}\}$ a Minimal System of Generators(MSG) for a graph $\mathcal{G}$ and a formative process $\mathcal{H}$.

Lemma 7**.**

Let $\mathcal{G}$ be the $\mathcal{P}$-graph realized by a given greedy formative process $\mathcal{H}:=<(\mathcal{P}^{(\mu)})_{\mu<\xi},(\bullet),\mathcal{T}>$, and let $\mathcal{G}_{WW}$ be the weakly well-founded part of $\mathcal{G}$ (relative to $\mathcal{H}$). Then $\mathcal{G}_{WW}$ contains a minimal system $\mathcal{BG}$ of generators for $\mathcal{G}$.

Proof.

Let $\mathcal{C}$ the first cycle of $\mathcal{BG}$ realized by $\mathcal{H}$. Let $\mu$ be such a step, $WWF^{(\mu)(A_{\mu})}=1$, otherwise either $\mathcal{C}$ would be not minimal or the first cycle of $\mathcal{BG}$ achieved by $\mathcal{H}$.

Therefore $\mu\in\mathfrak{M}$ using the fact that $\mathcal{BG}$ and its cycles belong to different equivalence classes, We prove in an analogue way for all the other cycles of $\mathcal{BG}$.

Theorem 4**.**

. Let $\mathcal{G}$ be the $\mathcal{P}$-graph realized by a given greedy formative process $\mathcal{H}:=<(\mathcal{P}^{(\mu)})_{\mu<\xi},(\bullet),\mathcal{T}>$, and let $\mathcal{G}_{WW}$ be the weakly-well-founded part of $\mathcal{G}$ (relative to $\mathcal{H}$). Then starting from $\mathcal{H^{\prime}}:=<(\mathcal{P}^{[\mu]})_{\mu<\xi_{WW}},(\bullet),\mathcal{T}>$ it is possible to generate a greedy formative process $\mathcal{H^{\prime\prime}}$ for a $\mathcal{P}$-graph $\mathcal{G^{\prime}}$ which weakly cart-simulates $\mathcal{G}$. We call $\mathcal{H^{\prime\prime}}$ the weak cart-process of $\mathcal{H}$.

Proof.

We start with the process $\mathcal{H^{\prime}}:=<(\mathcal{P}^{[\mu]})_{\mu<\xi_{WW}},(\bullet),\mathcal{T}>$ and we try to prolong it in order to achieve the original $\mathcal{G}$.

W.L.O.G. We can assume that all paths starting from a generator has a vertex with at least $|\mathcal{P}|^{k}$ new elements, $k$ max length of a path without repetitions of $\mathcal{G}$. This number of elements guarantees that we can follow all the paths until the end.

Consider the following set of ordinals.

[TABLE]

Sort this set with an increasing order inherited from the oracle process $<\mu_{1},\mu_{2}\dots\mu_{l}>$ and let proceed to create those arrows step by step

Let $\mu_{1}=FCr(A_{1}\rightarrow\delta)$, if $A$ have not an empty place then it has at least $|\mathcal{P}|^{k}$ unused elements. We distribute $|\mathcal{P}|^{k-1}$ such elements to each target of $A$. In this way we create all the arrows which start from $A$, taking care of the element composed of general union of places, which has to be assigned to the Principal Target, if there’s any. By contradiction suppose there exists a place $\sigma$ in $A_{1}$ such that $\sigma^{[\xi_{WW}]}=\emptyset$, this in turn implies that $WWF^{(\xi_{WW})}_{\mathcal{H^{\prime}}}(\sigma)=0$, then $FNE(\sigma)=FCr(B\rightarrow\sigma)$ for some $B$ and $FCr(B\rightarrow\sigma)<\mu_{1}$, contradiction.

Let $\mu_{2}=FCr(A_{2}\rightarrow\delta)$ if $A_{2}$ have not an empty place then, since it $WWW^{(\xi_{WW})}$ either has a place which is a target of $A_{1}$ and then it has at least $|\mathcal{P}|^{k-1}$ unused elements or it has a place in a pumping cycle and then it has at least $|\mathcal{P}|^{k}$. In the former it can distribute at least $|\mathcal{P}|^{k-2}$ for each target in case of latter at least $|\mathcal{P}|^{k-1}$ and we proceed as in the previous step. The case of an empty place is solved exactly as step 1, as well.

We proceed in the same fashion step by step. We are sure that we have elements at all times to trigger off new arrows since $k$ is the length of the longest simple path.

Since we have produced a transitive partition which weakly cart-simulate the oracle by Theorem 2 this solves the decidability problem for $\textnormal{{MLS}}\otimes^{-}$.

In order to finish out the proof of our main result we just need to saturate the $x=y\otimes z$ literals. This can be done using the pumping technique used to solve the decidability problem for MLSSPF [CU14].

Indeed, we pump to the infinity the cycles with cart arrows in order to saturate the nodes involved, then we close Principal Target in the usual way.

Theorem 5**.**

We can extend the process created in Theorem 4 in order to create a partition which cart-simulates the oracle one.

Proof.

Let $A$ be a node with $LC$ saturated in the oracle process and not saturated in the weak cart-process. Observe that in the oracle process after its $LC$ a saturated node cannot have one of its places fed. The same happens in the weak cart-process. Indeed, $LC(A)$ has been selected in the creation of the weak cart-process. In that step the weak cart-process discharges all the unused elements of $A$, then at that stage $A$ is saturated. It can change its condition only if one of its places is feeded in the prosecution of the process, which is impossible since the oracle does not feed any. Indeed, the weak cart-process distributes elements along arrows only if the oracle does.

Let $A$ be a node without $LC$, saturated in oracle process and not saturated in the weak cart-process. In this case $A$ is saturated in a limit ordinal, this means that $A$ has a pumping cycle and that after this limit ordinal this node cannot be called anymore.

I briefly outline the construction.

Since the node $A$ is saturated in a limit ordinal $\lambda$ we can assume both that a cycle including $A$ is repeated infinitely many times cofinally in $\lambda$ and all nodes involved in such cycle have Last Call greater than $\lambda$. This implies that all $\mu_{i}$ related to the first creation of the arrows of the cycle have to be less than $\lambda$. Pick the maximum one. Repeat the cycle for saturating $A$ after this step of weak cart-process. Observe that since is not saturated it has new unused elements to trigger off the cycle therefore it is a pumping cycle.

The pumping technique was originally introduced in [Urs05], [CU14] and widely described in [CU18].

Example 5**.**

An example of infinite saturation. Consider the following formula in $\textnormal{{MLS}}\otimes$ $\psi:x=x\otimes x\wedge x\neq\emptyset$ and its model $Mx=\{\emptyset,\emptyset^{1},\{\emptyset,\emptyset^{1}\}\dots\{\emptyset^{n},\emptyset^{m}\}\dots\}$ where $\emptyset^{n}$ stands for $\emptyset$ with $n$ brackets. It has the following $\mathcal{P}$-graph

and formative process with the following trace and targets ($T_{\mu}$ are targets of node $A_{\mu}$)

\begin{array}[]{l}\left(\begin{array}[]{c}A_{\mu}\\ T_{\mu}\end{array}\right)_{\mu<\omega}=\left(\begin{array}[]{c|c|c|c}\emptyset&\{\sigma_{0}\}&\{\sigma_{0}\}&\dots\\ \{\sigma_{0}\}&\{\sigma_{0}\}&\{\sigma_{0}\}&\dots\end{array}\right)\\ \end{array}.

Corollary 1**.**

$MLS\otimes$* is decidable.*

Proof.

We have showed that whenever $\Phi\in MLS\otimes$ has model there must be another one, bounded by a countable function in ${\left|{\Sigma}\right|}$, which witnesses the cart-simulation. This in turn implies decidability of $MLS\otimes$.

4 A Brief Remark on THP

The language $\textnormal{{MLS}}\otimes$ with cardinality equality, studied in Cutello Cantone and Policriti [CCP89], cannot have small model property since $\textnormal{{MLS}}\otimes$ admits infinite models, but it cannot have even witness small model property since it is equivalent to THP.

The reason seems to rely on a particular property of cycles in a $\mathcal{P}$-graph. In a sense when you try to make the cardinality of two assignments equal by pumping a cycle of one of them, you could increase the cardinality of the other one. This would make the combinatorics of the model grow. The above argument suggests that, in case undecidability arises, the cycles involved must be interconnected. In a sense undecidability and a special property of cycles could be related in some sense.

Therefore I cannot rule out that a property of cycles could single out a subclass of decidable formulas (and integer polynomials) greater than $\textnormal{{MLS}}\otimes$.

Mainly, Davis-Matyasevich-Robinson approach moves from Mathematical Logic to Number Theory using the fact that listable set has an exponential Diophantine representation [DPR61]. Indeed, Matyasevich finishes the proof by constructing the first example of a relation of exponential growth. Nowadays it is often reffered to as DPRM-Theorem:

”Every listable set of m-tuples of natural numbers has a Diophantine representation”.

This theorem implies, in particular, the undecidability of Hilbert’s tenth problem:

”There is no algorithm for deciding whether a given Diophantine equation has a solution”.

My Set Computable approach would go in a different direction. It should deduct from a finite combinatorial properties of finite $\mathcal{P}$-graphs the undecidability of THP.

For those reasons I conjecture a pure countable Set Theory fashion proof of the undecidability of THP.

Moreover I hope to show, in a pure combinatorial context, from where the undecidability comes.

5 Acknowledgments

The author is grateful to Domenico Cantone for helpful comments and suggestions on preliminary versions of the paper and Martin Davis who kindly gave his permission to cite his personal communication.

Appendix

In this Appendix, as a graphic example, I show the first cases of realizable standard $\mathcal{P}$-graphs. This taxonomy is strictly related with satisfiable formulas with an assigned number of variables. Standard $\mathcal{P}$-graphs are related with MLSP-like language.

In $\textnormal{{MLS}}\otimes$ case, as I have showed along the present paper, a new kind of arrow is needed, then new combinatorial structures arise.

Since a formula with $n$ variables has $2^{n}-1$ venn regions in order to have a $\mathcal{P}$-graph which depicts a model you need 1 place for 1 variable 3 places for 2 variables and so on. For $\textnormal{{MLS}}\otimes$ formulas you need a modified $\mathcal{P}$-graph with cart-arrow so the graphs are definitely more than the usual ones.

In this context it is impossible to give all this phenomenology, I just give few examples with one and two places.

Considering example with one place.

With places, $\alpha$ and $\beta$, and one node $\{\alpha\}$:

[TABLE]

With places $\alpha$ and $\beta$, and two nodes, $\{\alpha\},\{\beta\}$:

[TABLE]

With places $\alpha$ and $\beta$ and two nodes, $\{\alpha\},\{\alpha,\beta\}$:

[TABLE]