FO logic on cellular automata orbits equals MSO logic
Guillaume Theyssier

[
    J. M. García-Regaña, I. Calvo, E. Sánchez, H. Thienpondt, J. L. Velasco and J. A. Capitán
    
=============================================================================================





  We introduce an extension of classical cellular automata (CA) to arbitrary labeled graphs, and show that FO logic on CA orbits is equivalent to MSO logic. 
  
  We deduce various results from that equivalence, including a characterization of finitely generated groups on which FO model checking for CA orbits is undecidable, and undecidability of satisfiability of a fixed FO property for CA over finite graphs. We also show concrete examples of FO formulas for CA orbits whose model checking problem is equivalent to the domino problem, or its seeded or recurring variants respectively, on any finitely generated group. For the recurring domino problem, we use an extension of the FO signature by a relation found in the well-known Garden of Eden theorem, but we also show a concrete FO formula without the extension and with one quantifier alternation whose model checking problem does not belong to the arithmetical hierarchy on group ^2.




§ INTRODUCTION



Symbolic dynamics was historically introduced as the study of one-dimensional infinite words representing discretized orbits of smooth dynamical systems through a finite partition of space <cit.>. It has since then been largely extended to higher dimensions and arbitrary Cayley graphs of finitely generated groups, and seen rich developments going way beyond the initial motivations. The field of symbolic dynamics would now be better described as the study of sets of configurations (i.e. coloring of a graph) which can be defined by local uniform constraints (subshift of finite type, sofic subshift, etc) and maps on configurations acting by a uniform and local update rule (cellular automata, and morphisms between subshifts, which are the continuous maps commuting with translations <cit.>).
 A fascinating aspects of these objects is that they are very simple to define, yet can produce very complex behaviors which make them challenging to analyze. They can be considered as a reasonable modeling tool <cit.>, but more importantly, they constitute a natural model of computation for which undecidablity and computational hardness can arise in the most simple and seemingly unrelated questions in a spectacular way <cit.>.

 In symbolic dynamics, a major trend is to relate the properties of the considered objects (cellular automata or subshifts) to the structure of the underlying graph they are defined on (usually Cayley graphs of finitely generated groups). An emblematic example is the domino problem: since the breakthrough undecidability result of Berger <cit.>, a lot of works have focused on the characterization of Cayley graphs of groups for which the domino problem is undecidable  <cit.> or other graphs with less symmetries <cit.>. Concerning cellular automata (CA),
properties of the global map that can be expressed in first-order (FO) logic (or, said differently, FO properties of their orbit graph) are already challenging. 
For instance, injectivity and surjectivity problems were shown decidable on  <cit.> and on context-free graphs <cit.>, but undecidable on ^2 <cit.>. Other FO properties of CA were studied in relation to the graph structure: 
the Gotschalk conjecture <cit.> asks whether the property “injectivity implies surjectivity” is true for all CA on all group. Besides, the garden of Eden theorem <cit.> characterizes amenability among finitely generated groups by the fact that another simple FO property[As detailed in Section <ref>, it uses an additional relation in the FO signature which doesn't break the main point of our approach, an equivalence with MSO.] is true for all CA on this group.

It turns out that many central problems considered in symbolic dynamics can actually be rephrased in monadic second order logic (MSO). It was for instance noticed in <cit.> for injectivity and surjectivity of CA. MSO is a logical language that has received enormous interest, probably for its balance between expressivity and decidability in many cases.
More precisely, for graph properties, algorithmic metatheorems <cit.> and reciprocals <cit.> relates the complexity of the MSO model checking problem to the structure of considered graph or graph family. The key parameter at play here is treewidth <cit.> which is related to the non-existence of arbitrarily large grid minors <cit.>: bounded treewidth provides positive algorithmic results, while arbitrarily large grid minors often allows lower bounds or undecidability results. For instance, on a Cayley graph of a finitely generated group, the MSO model checking problem is decidable if and only if the group is virtually free (meaning having a free group as finite index subgroup) <cit.>.

Of course, positive algorithmic results for MSO apply to the particular problems studied in symbolic dynamics, but lower bounds or undecidability results for MSO are not directly transferable. For instance, on the graph ^2, undecidability of MSO model checking follows from a straightforward encoding of Turing machines, while undecidability of the domino problem <cit.> or of injectivity problem of CA <cit.> requires detailed and non-straightforward constructions that involves ideas and tools of independent interest (aperiodic tile sets and space filling curves for instance). Moreover, it is still open to our knowledge whether both problems are undecidable on any Cayley graph of group which is not virtually free. More generally, much work remains to close the gap between the global understanding of MSO logic on arbitrary graphs and the particular MSO fragments at sake in symbolic dynamics that are mostly understood on Cayley graphs of some group families.



    Contributions of the paper.

In this paper we explore properties of CA on arbitrary labeled graphs (finite or infinite). To do this, we introduce a definition of local rules of CA that doesn't use any explicit reference to the local structure of the graph as it is classically done, but instead just relies on the notion of bounded labeled walks and multiset of possible states read at the end of these walks. In particular, we don't require the graph to be uniform nor to have bounded degree, but our notion exactly corresponds to the classical one on Cayley graphs of finitely generated groups. Moreover, a fixed CA local rule provides a well-defined CA global map on any graph with same label sets. We can thus explore the influence of the graph separately from the local rule. For instance, we can specify a graph property by a CA local rule f and a FO property ϕ of CA orbits:  the set of graphs on which the local rule f induces a global map that satisfies ϕ. Our main result (theorems <ref>, <ref> and <ref>) is then an equivalence between this approach and MSO logic, on arbitrary labeled graphs. Precisely, for every class 𝒞 of graphs, the following two conditions are equivalent:



  * there exists an MSO formula Ψ, such that G∈𝒞 GΨ,  

  * there exists a pair (ϕ,f), where ϕ is a FO formula and f is a CA local rule, such that G∈𝒞 if and only if the global map induced by f on G satisfies ϕ.

Moreover, the pair (ϕ,f) can be effectively constructed from Ψ, and conversely.

Said differently, (FO,CA) pairs and MSO formulas define exactly the same graph languages, and the corresponding model checking problems are many-one equivalent on any fixed graph. We believe that this new characterization of MSO is particularly relevant in the context of symbolic dynamics. 

First, FO properties of orbits of CA are a conjugacy invariant and were much studied as mentioned above. We obtain a characterization of the decidability of FO model checking for CA orbits on Cayley graphs (Corollary <ref>) and we show that undecidability can be obtained with a fixed FO formula (Corollary <ref>) exactly on non virtually free f.g. groups, which should be put in perspective with the Ballier-Stein conjecture <cit.>. We also obtain undecidability of a satisfiability problem for CA on finite graphs for a fixed FO formula (Corollary <ref>).

Besides, when fixing an arbitrary FO formula and letting the CA vary, we get fragments of MSO that make sense beyond the examples directly motivated by CA theory.
In particular, we show in Section <ref> that on Cayley graphs of finitely generated groups, such fragments do not depend on the choice of generators, and that the domino problem and its variants (seeded and recurring) are equivalent to the model checking problem of some simple fixed FO formula (Theorem <ref>). For this we use an additional relation in the case of the recurring domino problem that remains MSO-expressible (Lemma <ref>). Finally we obtain a FO formula with just one quantifier alternation whose model checking problem does not belong to the arithmetical hierarchy when fixing the graph ^2 (Theorem <ref>).



    Warmup examples.
 
To fix ideas and give some intuition on how FO logic on CA orbits can be used to express graph properties, let us consider two well-known MSO properties and give an informal translation into a pair made of a FO formula and a CA local rule.

[k-Colorable graphs]
  Fix k and consider an undirected graph G=(V,E). Consider the CA local rule with state set S={0,…, k-1} such that a vertex in state i changes its state to i+1 k if it has a neighbor in state i and remains in state i otherwise. It can be checked that the CA induced on G by this local rule has a fixed-point if and only if G admits a proper vertex coloring with k colors (i.e. a coloring where no two neighboring vertices have the same color).


[Connected graphs]
  Consider an undirected graph G=(V,E). Consider the state set S={0,1,a_0,a_1,a_2} and the CA local rule such that a vertex in state i∈{0,1} becomes 1-i, a vertex in state a_i becomes 0 if it has a neighbor in {0,1} and a_i+1 3 otherwise.
  We claim that G is connected if and only if the CA induced on G by this local rule has no periodic orbit of minimal period 6, which is obviously an FO property of orbits.


   If G is not connected then we can define a configuration c equal to a_0 on one component and 0 on the others: c is periodic of minimal period 6 because no vertex in a_i will ever have a neighbor in {0,1}, so these vertices will have a cyclic behavior of period 3 and those from others components, a cyclic behavior of period 2.
  If G is connected, then no periodic orbit has minimal period 6 because any configuration c in such an orbit would necessarily contain a vertex in some state a_i and another in a state from {0,1} (otherwise the minimal period would be 2 or 3) and, since G is connected, it would actually contain a vertex v in state a_i with a neighbor in a state from {0,1}. Then after one step this vertex v would become 0 and would never turn back to state a_i by definition of F: this contradicts the fact that c belongs to a periodic orbit.




    Comparison with another characterization of MSO by automata.
 Several previous works established equivalence results between logic formalism and automata theory in the context of MSO languages of graphs. As mentioned above, <cit.> already noticed that some cellular automata properties can be translated into MSO. Following this, <cit.> and <cit.> introduced tiling and automata recognizers that are equivalent to (small) fragments of MSO. In <cit.>, alternating distributed graph automata are introduced that recognize exactly the languages of graphs definable in MSO logic. These distributed automata are close to CA in the sense that they run on configurations (coloring of the input graph by states) and use finite local memory and local communication between neighboring vertices. However, they are highly non-deterministic (alternating) and their accepting mechanism uses both initialization of the run to a particular configuration, and a global knowledge of the final configuration reached (precisely the set of states present in this configuration). Restrictions of this model to deterministic or non-deterministic automata (instead of alternating) gives strictly weaker fragments.

Our goal here is not to define a single automata model equivalent to MSO. Instead our approach motivated by symbolic dynamics uses deterministic CA on one hand and quantifier alternations in a separated FO formula which plays also the role of the accepting condition on the other hand. A key aspect is that we thus get natural fragments of MSO by fixing the FO formula and letting the CA rule vary. This also makes a strong difference with distributed alternating automata in the accepting mechanism since the FO formula does not offer any direct means of initializing some computation on a particular configuration, nor to detect presence of some particular states in a final configuration. 



§ FORMAL DEFINITIONS





    Graphs.
 

 A (Σ,Δ)-labeled graph is a graph G=(V,(E_δ)_δ∈Δ,L), which can be finite or infinite, where L:V→Σ is the vertex labeling and E_δ⊆ V× V are the edges labeled by δ. 
In such a graph, given some finite word w=w_1⋯ w_k∈Δ^ ∗, a path labeled by w is a sequence of vertices v_1,…, v_k+1 such that, for any 1≤ i≤ k, (v_i,v_i+1)∈ E_w_i.
All graphs considered in this paper are simple, meaning that there is at most one edge of a given label between two given vertices[The hypothesis that our graphs are simple will be used in sections <ref> and <ref>. We choose to adopt this hypothesis across the entire paper for simplicity and clarity, however the main results from Section <ref> should also hold without this hypothesis.]. Such a graph is said to be connected if it is connected as an undirected and unlabeled graph, i.e. if G=(V,E) is connected where (v,v')∈ E if either (v,v')∈ E_δ or (v',v)∈ E_δ for some δ∈Δ. The set of connected graphs is denoted by . Σ will in some case be a singleton and can therefore be silently omitted: we speak about Δ-labeled graph in this case. 
An important class of graphs studied in symbolic dynamics is that of Cayley graphs of finitely generated (f.g.) groups. Given a f.g. group (Γ,·) and a (finite) set of generators Δ (including their inverses), the associated Cayley graph is the Δ-labeled graph where (γ,γ')∈ E_δ if and only if γ'=γ·δ. 
An undirected graph G_1 is a minor of another undirected graph G_2 if it can be obtained from G_2 by deleting edges and vertices, and by contracting edges (i.e. identifying the vertices incident to the edge without creating multiple edges).



    Cellular automata.

Given a finite set of states S and a set of vertices V, a configuration is an element of S^V. It can be seen as a coloring of vertices by S.
A CA is a map from configurations to configurations, that is induced by a uniform local rule.
It is generally studied as a dynamical system through its set of orbits, which are sequences of configurations obtained by iterating the map from an initial configuration.

CA are usually defined over a fixed Cayley graph of a (f.g.) group <cit.>.
Following this classical approach, the local rule defining a CA is formally a lookup table and is bound to a particular graph as it relies on local patterns defined over bounded balls of the graph. It also requires the graph to be uniform and of bounded degree.
More general definitions were proposed that don't stick to a particular graph <cit.>, but they still rely on the hypothesis of bounded degree and use a particular labeling by port numbers.

We introduce in this section a simple definition of CA on arbitrary labeled graphs. The key advantage of our formalism is that a given local rule actually defines a CA on any labeled graph for fixed label sets. We can therefore fix a local rule and asks on which graphs the corresponding CA has a given property (as sketched in Section <ref>): a pair made of a local rule and a property of CA dynamics actually defines a property of graphs. Moreover, on Cayley graphs of f.g. groups our formalism is equivalent to the classical one.
The CA local rules we consider can intuitively be seen as finite memory and finite distance exploring machines working as follows in parallel from each vertex v: they walk from v following all possible Δ-labeled walks up to some length r, and harvest states seen at the end of these walks and count their occurrences up to some constant k, then they decide from this information (a multiset) the new state at vertex v.
From this point of view, the edge labeling by Δ acts as local directions that give more information on the position in the graph given a labeled walk, while vertex labeling σ gives some level of non-uniformity as in non-uniform cellular automata <cit.>.


















Let us now formalize this definition.

Given v∈ V and a word w∈Δ^∗, we denote by ^w(v) the set of vertices reachable from v by a path labeled by w. If w=ϵ (empty word), then ^w(v)={v} by definition. If G is the Cayley graph of a f.g. group, then ^w(v) is always a singleton, however there are generally several paths reaching the same vertex.





The k-capped multisets over set X are the multisets where no cardinality is greater than k, and are denoted ^k(X) = {0,…,k}^X.  Given a multiset m∈^X, we denote by ^k(m) the k-capped multiset such that ^k(m)(x) = max(m(x),k). We denote by A^≤ r the words of length at most r over alphabet A including the empty word ϵ.  Given a set of states S and a configuration c∈ S^V and v∈ V, the k-capped pattern of radius r at v in c is the k-capped multiset (c,v,r,k)∈^k(Δ^≤ r× S) defined by:
  
    (c,v,r,k) = ^k((w,s)↦#{v'∈^w(v) : c_v'=s}).



  A CA local rule for (Σ,Δ)-labeled graphs of state set S, radius r and using k-capped multisets (k≥ 1) is a map 

    f : Σ×^k(Δ^≤ r× S)→ S.

 For any (Σ,Δ)-labeled graph with vertices V, the global CA map F_G,f: S^V→ S^V associated to the local map f and graph G is then defined by 

    F_G,f(c)_v = f(σ(c_v),(c,v,r,k))

for any configuration c∈ S^V and any vertex v∈ V.


In the sequel, when considering a local map f, it always implicitly comes with a specified state set S and values of r and k defining its domain and image sets.
We are mainly interested in the case where Σ is a singleton (uniform CA), but incorporating Σ in our definition allows non-uniformity in the local rule as in non-uniform CA <cit.>.


On a Cayley graph of f.g. group, (x,v,r,k) gives all the information about configuration x restricted to the ball in the graph centered in v and with radius r: indeed, in this case, (x,v,r,k)(q,w)=1 if and only if the unique vertex v'∈^w(v) is such that x_v'=q, and ^w(v) describes the entire ball when w enumerates Δ^≤ r.
From this observation it follows that in the case of Cayley graphs and when Σ is a singleton, the global CA maps from Definition <ref> are exactly the classical global CA maps (see for instance <cit.>).


Definition <ref> explains how a given CA local rule f induces a CA global map F_G,f on a given graph. F_G,f is the main object of study in CA theory, as it represents a dynamical system.

[Two definitions of Game of Life]
  Consider the famous Game of Life CA F:{0,1}^^2→{0,1}^^2 <cit.>. In this example Σ is a singleton and thus ignored to simplify notations.
  First, let G_1 be the Cayley graph of ^2 with generators n=(0,1), e=(1,0) and their inverses. Let M be the following set of words in Δ^≤ 2: n, n^-1, e, e^-1, ne, ne^-1, n^-1e, n^-1e^-1. Now define the local rule f_1 of radius 2 and using 4-capped multiset by
  
    f_1(μ) =
        
          1     if μ(1,ϵ)=0 and ∑_w∈ Mμ(1,w) = 3
    
          1     if μ(1,ϵ)=1 and  2≤∑_w∈ Mμ(1,w) ≤ 3
    
          0     otherwise.

One can check that F_G_1,f_1= F.
Now consider the undirected and unlabeled graph G_2=(^2,E) with ((i,j),(i',j'))∈ E if |i-i'|≤ 1 and |j-j'|≤ 1 and (i,j)≠ (i',j'). Here we denote Δ={u}. We then define another local rule f_2 of radius 1 and using 4-capped multiset as follows:

    f_2(μ) = 
        
          1     if μ(1,ϵ)=0 and μ(1,u) = 3
    
          1     if μ(1,ϵ)=1 and  2≤μ(1,u) ≤ 3
    
          0     otherwise.

One can again check that F_G_2,f_2 = F.




    Logics.



To make the exposition more concise, we suppose some familiarity with standard concepts of formal logic (variables, assignments, quantification, free variables, etc).
MSO logic uses first-order variables (usually denoted by lower-case letters) representing vertices and second-order variables (usually denoted by upper-case letters) representing sets of vertices.
To help reading, relations in formulas will use infix notation (x R y) while relation in the meta-language will use the set notation ((x,y)∈ R).


  The set MSO formulas over label sets (Σ,Δ) is the set of atomic formulas:
  
  
  * xLσ for x a first-order variable and σ∈Σ (meaning x has label σ),
  
  * x E_δ x' for x and x' first-order variables and δ∈Δ (meaning that there is an edge labeled δ from x to x'),
  
  * x=x' for first-order variables x and x' (meaning that x is equal to x'),
  
  * x∈ X for first-order variable x and second-order variable X (meaning that x belongs to set X),
  
  closed by the usual logic connectives (∨, ∧, ) and quantifiers (∀, ∃).
  Given an MSO formula Ψ, a (Σ,Δ)-labeled graph G and an assignment α of free variables of Ψ we define the semantics in the standard way starting from the obvious meaning of atomic formula above (see <cit.> for an in-depth introduction). We write (G,α)Ψ when Ψ is true on G with assignment α. If Ψ has no free variable, we simply write GΨ when Ψ is true on G.


We will sometimes use substitution of relations with formulas defining them. For instance we can write Ψ(X,Ψ_R(x_1,x_2)), where Ψ is a formula using an additional relation symbol R, to denote the MSO formula obtained by substituting Ψ_R for R in Ψ (with the usual precaution of renaming variables if necessary, see <cit.>).

We now define FO logic over orbits of CA: they are just formulas allowing quantifications over configurations and using two relations, equality and application of one step of the CA global rule.


  The set of FO formulas is made of atomic formulas:
  
  
  * y = y' (meaning that configuration y is equal to configuration y'),
  
  * y→ y' (meaning that the global CA map leads to y' in one step starting from y),
  
  and closed under the usual logic connectives and quantifiers. Given a FO formula ϕ, a CA global map F:S^V→ S^V and an assignment β of free variables of ϕ to configurations from S^V, we write (F,β)ϕ to denote that F satisfies ϕ with assignment β following the obvious semantics of formulas starting from the relations above. When ϕ has no free variable, we just write Fϕ.


For a CA global map F:S^V→ S^V and a FO formula ϕ with free variables (y^1,…,y^n), we use the shortcut Fϕ(c^1,…,c^n) for configurations c^1,…, c^n∈ S^V to express that (F,β)ϕ where β is the assignment given by y^i↦ c^i for 1≤ i≤ n. We will also use the FO shortcut

y^0 k y^k to represent the FO formula expressing that y^0 leads to y^k in k steps and the k+1 configurations involved in this partial orbit are pairwise different:

    y^0 k y^k∃ y^1,…, ∃ y^k : ⋀_0≤ i<ky^i→ y^i+1∧⋀_i≠ jy^i≠ y^j.


Notation convention: we will always use letter Ψ for MSO formulas, x or X for MSO variables, α for MSO assignments, ϕ for FO formulas, y for FO variables, G for graphs, f for CA local rules, F for CA global maps and c for configurations. We use notation c_v to denote state of configuration at vertex v, that's why we prefer the exponent notation c^1, c^2,… to denote several configurations.



    Combining graphs, CA and logics.


The above definitions suggest various definitions of sets of objects (or languages):
 the graph languages 
 
 
  * Ψ = {G : GΨ} and
 
  * ϕ,f = {G : F_G,fϕ},
 
and the set of CA local rules ϕ,G = {f : F_G,fϕ},


where we use the notation convention above, and where Σ and Δ are fixed so graphs are actually (Σ,Δ)-graphs and CA local rules are rules for such graphs.
Moreover, ϕ,G can be seen as decision problems where inputs are given as local maps of CA (model checking problem of ϕ on G).

 











§ TRANSLATION RESULTS





 §.§ From FO/CA pairs to MSO


Whatever the state set, a CA configuration can be represented as a tuple of vertex sets: we can code the state at a vertex by the number of sets it belongs to among the tuple. This way, FO variables can easily be translated into tuples of second-order MSO variables undergoing the same quantification and  we get an onto map from possible assignments of the tuple of second-order MSO variables onto possible assignments of the corresponding FO variable.

Under that coding, equality of configurations translates into a simple MSO formula with just one universal first-order quantifier. It remains to show that the other relation in the signature of FO, relation → which represents the application of one step of the CA global map, can also be translated into MSO: 
this boils down to checking that at each vertex the local rule is correctly applied, which itself boils down to counting up to some constant occurrences of states that can be reached by a labeled walk of bounded length.


  There is a recursive translation τ from pairs (ϕ,f) made of a FO formula ϕ and a CA local rule f to MSO formulas such that the following equivalence holds for any graph G: F_f,Gϕ Gτ(ϕ,f).




  Fix ϕ and f with state set S={1,…,n}, radius r and using k-capped multisets. Suppose that ϕ is in prenex normal form where ϕ^0(y^1,…,y^m) is the quantifier-free part (if not just compute this prenex normal form).
We will use the following map   from n-tuple of vertex sets ⊆ V to configurations of S^V:
  
    (E_1,…, E_n) = v↦#{i : 1≤ i≤ n ∧ v∈ E_i}.

  ι is an onto map. Following this coding we define the MSO formula Ψ_s-𝚜𝚝𝚊𝚝𝚎(x,X) expressing that the configuration represented by X at vertex x is in state s:
  
    Ψ_s-𝚜𝚝𝚊𝚝𝚎(x,X)⋁_A⊆ S|A|=s⋀_1≤ i≤ n x∈ X_i i∈ A.

  
For each relation y^1 Ry^2 in the FO signature, we want to define an MSO formula 
Ψ_R(X^1,X^2) where X^i are n-tuples, and with the following property: for any assignment α of this two n-tuples, and for any graph G, the assignment β which assigns (α(X^i)) to y^i verifies:

    (G,α)Ψ_R(X^1,X^2) (F_G,f,β) y^1R y^2.


First it is not difficult to write such a formula in the case of relation y^1 = y^2: 
    Ψ_=(X^1,X^2) ∀ x, ⋁_s∈ SΨ_s-𝚜𝚝𝚊𝚝𝚎(x,X^1)∧Ψ_s-𝚜𝚝𝚊𝚝𝚎(x,X^2)

For the case of relation y^1→ y^2, we first need for each w∈Δ^l an MSO formula Ψ_w(x_0,x_l) expressing that vertex x_l can be reached by a walk labeled w starting from label x_0, that can be written as:

    Ψ_w(x_0,x_l)∃ x_1,…, x_l-1 : ⋀_0≤ i<lx_iE_w_i x_i+1.

Then we define the formula Ψ_(s,w)≥ p(X,x) for each 0≤ p<k by

    Ψ_(s,w)≥ p(X,x)∃ x_1,…, x_p : ⋀_1≤ i,j≤ pi≠ jx_i≠ x_j ∧⋀_1≤ i≤ pΨ_w(x,x_i) ∧Ψ_s-𝚜𝚝𝚊𝚝𝚎(x_i,X)

which expresses that in configuration X, there are at least p occurrences of state s reachable by a walk labeled w starting from x.
We can write by Boolean combination of the above a formula Ψ_(s,w)=p expressing that in configuration X, there are exactly p occurrences of state s reachable by a walk labeled w starting from x.

We can now define the formula Ψ_→ with the property announced above with respect to the FO relation y^1→ y^2 :

    Ψ_→(X^1,X^2)∀ x,⋀_σ∈Σμ∈ M(xLσ∧⋀_s∈ Sw∈Δ^≤ rΨ_(s,w)=μ(s,w)(X,x))⇒Ψ_f(σ,μ)-𝚜𝚝𝚊𝚝𝚎(x,X^2)

where M=^k(Δ^≤ r× S). This formula is just the translation of the definition of a CA global rule from its local rule (Definition <ref>) saying that at each vertex, if the local symbol and multiset pattern are (σ,μ), then the next state should be f(σ,μ).

With these ingredients, ϕ^0(y^1,…, y^m), the quantifier free part of ϕ, is translated into an MSO formula Ψ^0(X^1,…,X^m) by replacing each occurrence of some atomic formula y^i= y^j (resp. y^i→ y^j) by Ψ_=(X^i,X^j) (resp. Ψ_→(X^i,X^j)). We still have that, for any MSO assignment α, the FO assignment β defined with a slight abuse of notations as ι∘α as above verifies:

    (G,α)Ψ^0(X^1,…,X^m) (F_G,f,β)ϕ^0(y^1,…, y^m).


Since ι is an onto map, one has also that

    (G,α')∀X^1,Ψ^0(X^1,…,X^m) (F_G,f,β')∀ y^1,ϕ^0(y^1,…, y^m)

  for any MSO assignment α' and corresponding FO assignment β' defined as ι∘α' (with a slight abuse of notations).
The same hold with the ∃ quantifier and the Theorem follows by a straightforward induction.





 §.§ From MSO to FO/CA pairs.


This converse translation is less straightforward. Let us first give a simplified overview by considering an MSO formula Ψ in prenex normal form, and describing its translation into a CA local rule f together with a FO formula ϕ.

We will use binary configurations (i.e. elements of {0,1}^V) to code either second-order variable assignments (a set coded by its indicator function) or first-order variable assignments (a singleton coded by its indicator function).
More generally, we can code several variable assignments in a configuration made of several binary components, i.e. configurations over a product alphabet S={0,1}×⋯×{0,1}.
Given a configuration made of a product of binary components coding an assignment of several variables, the truth of an atomic formula using these variables over this assignment can be checked by a CA local rule in a distributed manner. With slightly more work and using a particular FO property of orbits, we can actually test any quantifier free formula in a distributed manner.

The CA local rule together with the FO formula we are going to construct will essentially enforce an erasing process that starts from a configuration made of a product of binary components (to code an assignment of all MSO variables at once) and then removes components of the product one by one at successive steps until reaching a fixed point: on one hand having all information about variables assignment at the start allows to check the truth of the quantifier-free matrix of the MSO formula as hinted before, and, on the other hand, having components to disappear individually in successive steps allows to make a FO quantification over configurations following exactly the MSO quantification over variables. 

For instance, taking MSO formula Ψ=∀ X_1,∃ x_2, ∀ X_3, R(X_1,x_2,X_3), we construct a FO formula that is essentially of the form:

    ∀ y_1, ∃ y_2, ∀ y_3 : y_3→ y_2→[anchor=base, baseline]
         (a) y_1;
         (a) edge[loop right] (a);

and a CA local rule that will ensure that y_1≈ a_1, y_2≈ (a_1,a_2) and y_3≈ (a_1,a_2,a_3) where a_1 is an assignment for X_1, a_2 is an assignment for x_2 and a_3 is an assignment for X_3.
It will also ensure, when in configuration y_3, that the assignments (a_1,a_2,a_3) satisfy R(X_1,x_2,X_3).
It is important to note that successive choices of assignments of variables y_1, y_2 and y_3 corresponds, up to a simple product encoding, to successive choices of assignments for variables X_1, x_2 and X_3.  
Non-deterministic choices of successive assignments are possible in this construction because they correspond to going backward in time in the canonical orbit enforced by the FO formula above: there is no contradiction with the determinism of cellular automata.


To turn this overview into a concrete construction, several technical points have to be addressed:


  * the simplified behavior described above only works on some well-formed configuration; as usual in CA constructions, we will use local error detection and special error states to mark orbits of bad configurations and distinguish them from good ones: here we use two error states that oscillate with period two in order to ensure that any orbit reaching a fixed point has successfully passed all error detection mechanisms.

  * to code first-order variables, binary configurations need to have exactly one vertex in state 1 and the local nature of CA prevents from verifying this (it cannot a priori distinguish a configuration with a single 1 from a configuration with two 1s arbitrarily far away, not to mention the case of non-connected graphs). Our construction handles this through the FO formula to be satisfied using a sibling configurations counting trick combined with a particular behavior of the CA which uses additional layers of states.

  The erasing process of the CA mentioned above will therefore take several steps for first-order variables, and only one step for second-order variables.

  * checking a quantifier-free formula given an assignment of its variables encoded in a configuration is generally not doable in one step by a CA, especially on non-connected graphs that prevent the CA from communicating between components (think of the example: x∈ X∨ y∈ X) ; to solve this problem our construction will once again rely on a combination of FO logic over several steps and a particular behavior of the CA. 

We first give a solution to these technical problems that works when we restrict to connected graphs. This construction is a little simpler than the general case that we address later, and it has the benefit to induce a better controlled  dependence of the FO formula on the MSO formula (an aspect that will turn out to be useful in Section <ref>).

If Ψ is an MSO formula in prenex normal form with quantifier prefix Q_1,…, Q_n, its prefix signature is the word describing the alternance of quantifiers taking into account both the type of quantification and the order of quantified variables. More precisely, it is the word over alphabet {∀,∃}×{1,2} obtained as follows: first map each quantifier to the alphabet according to the actual type and order, then remove any repetition of consecutive identical letters.


  There are two recursive transformations τ_FO from MSO formulas to FO formulas and τ_CA from MSO formulas to CA local rules such that, for any MSO formula Ψ, the pair made of ϕ=τ_FO(Ψ) and f=τ_CA(Ψ) verifies:
  
  
  * for any connected graph G the following equivalence holds: GΨ F_G,fϕ,
  
  * if Ψ is prenex then ϕ depends only on its prefix signature.
  




Let 
Ψ = _1x_1^1,…, _1x_1^k_1,_2x_2^1,…, _2x_2^k_2,…, _nx_n^1,…, _nx_n^k_n, R(x_1^1,…,x_n^k_n)
be any MSO formula in prenex normal form where _1,…, _n are the n quantifiers types (either ∀ or ∃ and either first or second-order) forming the prefix signature, variables x_i^1,…, x_i^k_i are bound by quantifier of type _i and R(x_1^1,…,x_n^k_n) is the matrix of the prenex normal form (i.e. a quantifier free formula). We use this numbering of variables grouped by quantifiers type to obtain a more compact FO formula that only depends on the prefix signature of Ψ.
Let's write R(x_1^1,…,x_n^k_n) in disjunctive normal form:

    R(x_1^1,…,x_n^k_n) = ⋁_1≤ j≤ d C_j(x_1^1,…,x_n^k_n)

where each clause C_j is a conjunction of terms which are atomic formula or negation thereof using variables x_1^1,…,x_n^k_n.


Let  be the set of i such that _i is a first-order quantifier.



    Structure of configurations.


For each 1≤ i≤ n, let ω(i)=|∩{1,…,i}| and define (i) = i + 2·ω(i). As it will become clear below, (n) denotes the length of an orbit along which n particular configurations will be identified. Configurations along this orbit will use distinct state sets, and (i) will also denotes the number of layers of the i-th configuration. We first introduce sets S_l for 1≤ l≤(n) that will be used to hold variable assignments and translate MSO quantification over variables of first or second-order into FO quantification over configurations. S_l is a product of l layers each of the form {0,1}^k_i (variable layer) or {1,…,k_i} (choice layer) for some i, or {0,1} (control layer). Intuitively, variable layers will hold MSO variables assignments, and choice and control layers are used only for first-order variables as a control mechanism. Sets S_l are precisely defined as follows:


  * S_1 = {0,1}^k_1 and if 1∈ then S_2=S_1×{1,…,k_1} and S_3=S_2×{0,1},

  * for 1≤ i<n, S_(i)+1=S_(i)×{0,1}^k_i+1 and if i+1∈ then S_(i)+2=S_(i)+1×{1,…,k_i+1} and S_(i)+3=S_(i)+2×{0,1}.


 If j=(i) ≤ l with i∉ or j=(i)-2≤ l with i∈ then the j-th layer of S_l is a variable layer, denoted as V_i(S_l), and intuitively represents an assignment for the tuple of variables x_i^1,…, x_i^k_i. For 1≤ j≤ k_i, we denote by V_i^j(S_l) the j-th binary component of V_i(S_l) which intuitively represents an assignment for variable x_i^j. For i∈ and j=(i)-1≤ l, the jth layer of S_l is a choice layer, denoted χ_i(S_l). Other layers, precisely j-th layers with j=(i) with i∈, are control layers and denoted K_i(S_l). Choice layer χ_i together with control layer K_i are used to ensure that the corresponding variable layer V_i correctly encodes a k_i-tuple of assignments of first-order variables, i.e. is a k_i-tuple of binary configurations each having exactly one position in state 1. 

 We denote by π the natural projection from S_l onto S_l-1 (for any 2≤ l≤(n)) which removes the last (l-th) layer of elements of S_l.

A well-formed configuration where all vertices are in a state from S_(n) intuitively contains an assignment for all variables involved in formula Ψ (provided the control mechanism for first-order variables to be detailed below has been successful). We need to implement a distributed check of the truth  of quantifier-free formula R on such an assignment. The key is to ensure that some clause C_j from the disjunctive normal form of R is chosen uniformly on the entire graph and to check everywhere that each terms of C_j is locally correct given the assignment. 
For 1≤ j≤ d, let T_j = S_(n)×{j} (recall that d is the number of clauses in the disjunctive normal form of R(x_1^1,…, x_n^k_n)). We again use notation π to denote the natural projection from T_j onto S_(n), which removes the last component of states. T_j sates will be used to check clause C_j.

We can now define the state set of the CA τ_CA(Ψ) as

    S = {e_0,e_1}∪⋃_1≤ l≤(n) S_l ∪⋃_1≤ j≤ d T_j

where e_1 and e_2 are distinct elements from the rest of S. We say that the type of an element of S is l if it belongs to S_l, error if it is e_0 or e_1 and j-truth-check if it belongs to T_j. We also naturally extend the notation V_i, χ_i  and K_i for any state s∈ T_j by V_i(s) = V_i(π(s)),  χ_i(s)=χ_i(π(s)) and K_i(s)=K_i(π(s)). 

A configuration c∈ S^V is valid if the following conditions hold:


  * states of all pairs of neighboring vertices of G are of the same type, and not of error type;

  * choice layer χ_i of all pairs of neighboring vertices of G are equal;

  * at each vertex v the control layers have zeros where the corresponding variable layers indicated by the choice layers have, precisely: K_i(c_v)≤ V_i^χ_i(c_v)(c_v) for all i such that K_i(c_v) is defined (intuitively, a 1 in a control layer is authorized only if their is a 1 in the 'chosen' component of the corresponding variable layer);


Note that this definition of validity is purely local. For μ a capped multiset (second argument of the local rule of a CA), we write (μ) to express the local validity conditions above on μ: the first two item are checked on each pair of states (s,s') such that μ(s,ϵ)≥ 1 and μ(s',δ)≥ 1 for some δ∈Δ; the third item is checked on state s such that μ(s,ϵ)≥ 1.



    CA local rule.

The behavior of the CA local rule f=τ_CA(Ψ) can intuitively be described as follows:


  * check the local validity of the configuration and if not generate states of error type that alternate with period 2 (between e_0 and e_1),

  * apply projection π on states of type l with l≥ 2 and let states of type 1 unchanged,

  * on states of type j-truth-check, verify that the assignment of variables x_1^1,…, x_n^k_n coded in variable layers V_i^j are such that C_j(x_1^1,…, x_n^k_n) holds, and apply π if it is the case, or generate an error state otherwise.


Of course, the behavior on states of type j-truth-check above has to be understood locally since we are defining a CA. The implementation of this distributed truth check is as follows: each term t(x_a^b,x_p^q) appearing in clause C_j (an atomic formula or its negation), where x_a^b is a first-order variable, is checked only at any vertex having a V_a^b component at 1, otherwise it is considered true by default.

 More precisely, for a pair (σ,μ) made of a vertex label and a capped multiset (arguments of the local rule f), we write (σ,μ) C_j (clause C_j is locally valid) if the local state (unique s such that μ(s,ϵ))  is of type j-truth-check and the neighboring states also, and if all terms of C_j are locally true according to the previous rule.
It turns out that (σ,μ) C_j can be checked by a local rule of CA of radius 1 and using 1-capped multisets (i.e. sets). Precisely, all possible terms of clause C_j are treated as follows (denoting again s the unique state such that μ(s,ϵ)≥ 1):


  * x_a^b  L σ' (resp. its negation) is true if and only if V_a^b(s)=0 or if σ=σ' (resp. σ≠σ'),

  * x_a^b E_δ x_p^q (resp. its negation) is true if and only if V_a^b(s)=0 or if 1∈{V_p^q(q') : μ(q',δ)≥ 1} (resp. 1 does not belong to this set),

  * x_a^b = x_p^q (resp. its negation) is true if and only if V_a^b(s)=0 or V_p^q(s)=1 (resp. V_p^q(s)=0),

  * x_a^b ∈ x_p^q (resp. its negation) is true if and only if V_a^b(s)=0 or V_p^q(s)=1 (resp. V_p^q(s)=0).

For t a term, we write (σ,μ) t if t is locally true according to the above definition.
Recall that x_a^b is a first order variable and the rest of the construction will ensure that, on configurations that matter, there will always exist a node at which V_a^b(s)=1 so these tests will actually check that the assignments of variables encoded in the configuration do satisfy the term as desired.


The CA local rule f is then defined as follows (denoting again s the unique state such that μ(s,ϵ)≥ 1):

    f(σ,μ) =
      
        e_1-i    if s=e_i
    
        e_0     otherwise, and if (μ),
    
        e_0     otherwise, and if s has type j-truth-check and (σ,μ)C_j,
    
        s     otherwise, and if s is of type 1,
    π(s)     otherwise.





















    FO formula.








Most of the task of the FO formula is to check that n configurations are well-positioned in an orbit leading to a fixed-point. However, along this orbit, we also have to make checks to ensure that layers corresponding to first-order variables are well formed. For i∈, the CA behavior already ensures (by generating error states if not) that choice layers χ_i are uniform and that control layers K_i are upper-bounded by the chosen corresponding variable layer V_i^j. In this context, the check is done as follows (intuitively, variable y^i represents a configuration of type (i) at each vertex, for some i∈):

    y^i∀ y, ∀ y', (y^i2 y'∧ y2 y')⇒y=1,


where the formula y=1 expresses that there is exactly 1 configuration other than y with same image as y and can be written explicitly in FO as follows: 
    ∃ y_s,∃ y_+, y_s→ y_+∧ y→ y_+ ∧ y_s≠ y ∧ (∀ y': y'→ y_+ ⇒ (y'=y ∨ y'=y_s)).
 The idea is that a variable layer V_i is good if, for any choice j made in choice layer χ_i, there are only 2 possible ways to correctly complete the control layer K_i, because there is exactly one vertex v at which V_i^j is 1 and therefore at which K_i can be freely chosen to be 0 or 1.


Let us now define formulas to deal with the global structure of the orbit leading to a fixed point:

    1y
        y→ y    if 1∉,
    ∃ y^0, y2 y^0∧ y^0→ y^0∧y    if 1∈,

and for any 2≤ i≤ n 

    iy,y^+
        y^+→ y     if i∉
    
        y^+3 y ∧y^+    if i∈
    .


Then, denote by iy^1,…, y^i for each 1≤ i≤ n the formula:

    iy^1,…, y^i1y^1∧⋀_2≤ k≤ iky^k-1,y^k.


The truth check for R has to make a non-deterministic choice of clause C_j to then use the distributed truth check implemented in the CA, we therefore define the following formula to be used in ϕ: y∃ y'→ y
which make sense when y represents a configuration everywhere of type (n).

As we show later, formula iy^1,…, y^i paired with CA F ensures that the configuration assigned to y^i is a well-formed configuration of type (i) that holds an assignment for variables (x_i^1,…, x_i^k_i) through its variable components V_i^1,…, V_i^k_i. We use these formulas in ϕ to make restricted domain FO quantifications that exactly correspond to well-formed configurations that hold assignments of the corresponding MSO variables. 
  
To make the formula ϕ more readable, we use the following syntactic sugar to express restricted domain quantification. If ϕ_D and ϕ are formulas containing y as free variable, then:


  * ∃ y∈ϕ_D, ϕ stands for ∃ y, ϕ_D∧ϕ,

  * ∀ y∈ϕ_D, ϕ stands for ∀ y, ϕ_D⇒ϕ.


We can finally define FO formula  ϕ=τ_FO(Ψ):


    ϕ_1' y^1∈1y^1, _2' y^2∈2y^1,y^2,…, _n' y^n∈ny^1,…,y^n, y^n


where the FO quantifier _i' is ∃ if the MSO quantifier _i is existential, and ∀ if _i is universal.



    Correctness of the construction.
 First, it can be checked that ϕ only depends on the prefix of Ψ and not on R. Second, the construction of f and ϕ are clearly computable from Ψ. The proof of Theorem <ref> then relies on two lemmas. The first one ensures that i… predicates correctly translate assignments of FO variables quantified in ϕ into assignments of MSO variables quantified in Ψ and conversely. 


  Let G be a (Σ,Δ)-labeled graph which is connected. Consider configurations c^1,…, c^i with 1≤ i≤ n such that F_G,fic^1,…, c^i, then the following holds:
  
  
  * c^k is of type (k) at each vertex, for 1≤ k≤ i;
  
  * for 1≤ l≤ i and 1≤ j≤ k_l, variable component V_l^j(c^k) is the same for all k with l≤ k≤ i, and it is such that exactly one vertex is in state 1 when l∈ ;
  
  * if i<n, for any assignment α of variables (x_i+1^1,…,x_i+1^k_i+1) there exists c^i+1 such that 
    F_G,fi+1c^1,… ,c^i+1
 and V_i+1^j(c^i+1) = α(x_i+1^j) for all 1≤ j≤ k_i+1.
  


  For the first item, we have F_G,f1c^1 so c^1 must be a fixed point if 1∉ and therefore is of type 1=(1) at each vertex because, on any other type of configuration, their is some vertex not in a state of type 1 at which F either applies projection π, or generates an error state. In case 1∈, F^2(c^1) must be a fixed point for the same reason and therefore c^1 is of type (1)=3 at each vertex by definition of F since no transition generating an error state can lead to c^1 and therefore only π can be applied at each vertex.
  More generally, since F_G,fic^1,…, c^i implies F_G,fkc^k-1,c^k for all 2≤ k≤ i, it follows that configuration c^k is of type (k) at each vertex because c^1 lies in its orbit (is reached after precisely (k)-(1) steps) and therefore no error state can appear in this orbit, so only π is applied until reaching c^1.

  For the second item, consider configuration c^l for l∈. Since F_G,flc^l-1,c^l if l≥ 2 or F_G,flc^1 if l=1, we in particular have F_G,fc^l, so for each configuration c such that F^2(c^l)=F^2(c) it holds that c has exactly one sibling configuration. We know that if c' is c or its sibling then it is a valid configuration (because there is no error state in its orbit which reaches the same fixed point as c^l), so we have K_l(c_v')≤ V_l^χ_l(c_v')(c_v') at each node v. We also have that χ_l(c_v') is uniform on the entire graph, because the graph is connected and thus if two vertices hold different values, then there would also be two neighboring vertices holding different values which would contradict validity of the configuration. We deduce that there is exactly one vertex v such that V_l^χ_l(c_v')(c_v')=1 otherwise c would not have exactly one sibling.

  Finally, for the third item, it is enough to complete configuration c^i of type (i) everywhere as shown above to a configuration c^i+1 of type (i+1) everywhere which correctly encode assigned values in its V_i+1 layer (which is completely independent from c^i). It is enough to ensure F_G,fi+1c^i,c^i+1 when i+1∉. In the case where i+1∈, we have to additionally ensure that the choice layer χ_i+1 is uniform and we can choose the control layer to be everywhere 0 so that c^i+1 is indeed valid. Clearly F_G,fc^i+1 with this choices, so we have F_G,fi+1c^i,c^i+1. In both cases we deduce F_G,fi+1c^1,… ,c^i+1, because by hypothesis we already have F_G,fic^1,… ,c^i.



From the above lemma, if F_G,fic^1,…, c^i then c^i codes an assignment for all MSO variables x_l^j for 1≤ l≤ i and 1≤ j≤ k_l through components V_l^j of c^i. Precisely, when l∈ variable x_l^j is assigned to the unique vertex v such that V_l^j(c^i_v)=1, and when l∉ variable x_l^j is assigned to the set of vertices {v : V_l^j(c^i_v)=1}. We denote this assignment by α_c^i.
Moreover, α_c^i is an extension of assignment α_c^j for any 1≤ j<i.


Next lemma ensures that … predicate correctly codes truth of formula R(…) (matrix of Ψ) through the previous assignment translation.


  Under the hypothesis of Lemma <ref>, it holds that  F_G,fc^n if and only if (G,α_c^ n) R(x_1^1,…, x_n^k_n).



  First, by Lemma <ref>, c^n is of type (n) at each vertex and is a valid configuration. If c is a pre-image of c^n, it must be valid (no error state in c^n) and of type j-truth-check for some j for all vertices because the graph is connected (otherwise there would be two neighboring nodes with different types, contradicting local validity). It must also be the case that, at each vertex v, (σ,μ) C_j where σ=L(v) and μ=(c,v,1,1). Now consider any term t of clause C_j with first-order free variable x_a^b and another free variable x_u^v, and let v be the unique vertex such that V_a^b(c_v)=1, which is v=α_c^n(x_a^b). By definition of f, it must be the case that (G,α_c^n) t (straightforward case analysis on atomic formulas). Since this holds for all terms of C_j and since R is a disjunction of clauses C_j, we deduce (G,α_c^ n) R(x_1^1,…, x_n^k_n).

  Conversely, if (G,α_c^ n) R(x_1^1,…, x_n^k_n), then by definition there must some j such that (G,α_c^ n) C_j(x_1^1,…, x_n^k_n). Let c be the configuration of type j-truth-check everywhere such that π(c)=c^n (where π is the map applying π at all vertices). We claim that F_G,f(c)=c^n which implies F_G,fc^n. Indeed, considering any term t appearing in C_j and any node v, and denoting σ=L(v) and μ=(c,v,1,1), we have:
  
  
  * (σ,μ) t if v is the assignment of the leftmost free variable appearing in t since (G,α_c^n) t,
  
  * (σ,μ) t by definition otherwise.
  
  We deduce that (σ,μ) C_j and therefore that F_G,f applies projection π at each vertex v on c, proving the claim.



The proof of Theorem <ref> then consists in applying inductively the definition of truth by assignments of variables simultaneously in Ψ and ϕ, use Lemma <ref> as base case and Lemma <ref> for the induction step to translate assignments between MSO variables and FO variables.


  Consider any (Σ,Δ)-labeled graph which is connected. For 1≤ i≤ n+1, denote by ϕ_i the subformula of ϕ starting from the ith quantifier (and without quantifier if i=n+1):
  
    ϕ_i_i'y^i∈iy^1,…, y^i,…, _n'y^n∈ny^1,…,y^n:y^n

  and by Ψ_i the subformula of Ψ starting from the ith alternation of quantifiers:
  
    Ψ_i_i x_i^1,…, _i^k_ix_i^k_i,…,_n x_n^1,…, _n x_n^n : R(x_1^1,…, x_n^k_n).

  ϕ_1=ϕ and Ψ_1=Ψ and for i>1  the free variables of ϕ_i are y^1,…, y^i-1 and those of Ψ_i are x_1^1,…, x_i-1^k_i-1.

  Suppose first that F_G,fϕ. We show by induction from i=n+1 downto 1 that the following holds (H_i): 
  

    .9 for all configurations c^1,…, c^i-1, if F_G,fi-1c^1,…, c^i-1 and F_G,fϕ_i(c^1,…, c^i-1) then (G,α_c^i-1)Ψ_i
    
  

  (to be understood without configuration and without assignment when i=1). Recall that assignment α_c^i-1 is well-defined thanks to Lemma <ref>. This implies GΨ since ϕ_1=ϕ and Ψ_1=Ψ.
  
  
  * the base case directly follows from Lemma <ref> since ϕ_n+1 is exactly y^n and Ψ_n+1 is exactly R(x_1^1,…, x_n^k_n);
  
  * for the induction step, suppose that the hypothesis (H_i) holds and consider c^1,…, c^i-2 such that F_G,fi-2c^1,…, c^i-2 and F_G,fϕ_i-1(c^1,…, c^i-2).
    
    
  * if '_i-1 = ∀, then F_G,fϕ_i-1(c^1,…, c^i-2) means that for all configuration c^i-1 such that F_G,fi-1c^1,…, c^i-1 it holds that F_G,fϕ_i(c^1,…, c^i-1), and then by (H_i) it also holds that (G,α_c^i-1)Ψ_i. By item 3 of Lemma <ref>, this implies (G,α)Ψ_i for any assignment α extending α_c^i-2 to variables (x_i-1^1,…, x_i-1^k_i-1). Now since _i-1 is a universal quantifier, this precisely means (G,α_c^i-2)Ψ_i-1.
    
  * if '_i-1 = ∃, then F_G,fϕ_i-1(c^1,…, c^i-2) means that there exists a configuration c^i-1 such that F_G,fi-1c^1,…, c^i-1 and F_G,fϕ_i(c^1,…, c^i-1), and then by (H_i) it also holds that (G,α_c^i-1)Ψ_i. But α_c^i-1 is some extension of assignment α_c^i-2 to variables (x_i-1^1,…, x_i-1^k_i-1). Thus, since _i-1 is an existential quantifier, we actually have (G,α_c^i-2)Ψ_i-1.
    
  

  Suppose now that GΨ. We show by induction from i=n+1 downto 1 that the following holds (H_i'): 
  

    .9 for any assignments α^i-1 of variables x_1^1,…,x_i-1^k_i-1, (G,α^i-1)Ψ_i implies that for all configurations (c^1,…, c^i-1) such that F_G,fi-1c^1,…, c^i-1 and α_c^i-1=α^i-1, it holds that F_G,fϕ_i(c^1,…,c^i-1)
    
  

  (to be understood without free variable and without assignment when i=1). This implies (G F)ϕ since ϕ_1=ϕ and Ψ_1=Ψ.
  
  
  * the base case directly follows from Lemma <ref> since ϕ_n+1 is exactly y^n and Ψ_n+1 is exactly R(x_1^1,…, x_n^k_n).
  
  * for the induction step, suppose that the hypothesis (H_i') holds and consider an assignment α^i-2 of variables x_1^1,…,x_i-1^k_i-1 such that (G,α^i-2)Ψ_i-1
    
    
  * if _i-1 = ∀, then F_G,fϕ_i-1(c^1,…, c^i-2) means that for all assignments α^i-1 extending α^i-2 to variables x_i-1^1,…, x_i-1^k_i-1 we have (G,α^i-1)Ψ_i. So by hypothesis (H_i') we also have F_G,fϕ_i(c^1,…,c^i-1) for all configurations (c^1,…, c^i-1) such that F_G,fi-1c^1,…, c^i-1 and α_c^i-1=α^i-1. Since _i' is universal with domain restriction by i-1…, and because F_G,fi-1c^1,…, c^i-1 implies F_G,fi-2c^1,…, c^i-2, this actually means that, for all configurations (c^1,…, c^i-2) such that F_G,fi-2c^1,…, c^i-2 and α_c^i-1=α^i-1, it holds that  F_G,fϕ_i-2(c^1,…, c^i-2). We thus have proven (H_i-1').
    
  * if _i-1 = ∃, then F_G,fϕ_i-1(c^1,…, c^i-2) means that there is an assignment α^i-1 extending α^i-2 to variables x_i-1^1,…, x_i-1^k_i-1 with (G,α^i-1)Ψ_i. So, by hypothesis (H_i'), we also have F_G,fϕ_i(c^1,…,c^i-1) for all configurations (c^1,…, c^i-1) such that F_G,fi-1c^1,…, c^i-1 and α_c^i-1=α^i-1. But for any configurations (c^1,…, c^i-2) such that F_G,fi-1c^1,…, c^i-2 there is a configuration c^i-1 such that F_G,fϕ_i(c^1,…,c^i-1) and α_c^i-1=α^i-1 by item 3 of Lemma <ref>. Since _i-1' is existential with domain restriction by i-1… this actually means that for all configurations (c^1,…, c^i-2) such that F_G,fi-1c^1,…, c^i-2 it holds that F_G,fϕ_i-1(c^1,…,c^i-2). We have thus proven (H_i-2').
    
  





    Generalizing to arbitrary graphs.

In the previous construction, we use the fact that considered graphs are connected in two places: to ensure uniformity of choice layers χ_i and to ensure a uniform choice of j for testing clause C_j with states of type j-truth-check. When generalized to possibly disconnected graphs, such uniformity conditions cannot be checked by the CA alone, simply because the CA has no possibility to communicate between connected components. We can compensate this impossibility by slightly changing the behavior of F and adding new FO constraints in the definition of ϕ. The price to pay is that the new definition of ϕ will depend on all parts of Ψ, not only its prefix signature.

First, the case of choice layers χ_i can be solved easily by de-grouping variables x_i^1 to x_i^k_i, i.e. renumbering variables in the prefix of Ψ by  letting k_i=1 and taking ∑_1≤ i≤ nk_i as the new value of n. Then, choice layers become trivial (they contain just one state) and are therefore always uniform by definition.

To solve the case of truth check, we introduce a general pre-image counting trick to ensure that a configuration c is uniform by a FO property. First, each state s of the alphabet S used by c is associated to a distinct prime number p_s, and there is a probing mechanism that selects a set of vertices and allows exactly p_s predecessors at selected vertices which are in state s, and only 1 at vertices which are not selected. The trick to check that c is s-uniform then consists in counting the number of pre-images up to max_s'∈ S p_s': whatever the set of selected vertices, it should always be a power of p_s.



  There are two recursive transformations τ_FO from MSO formulas to FO formulas and τ_CA from MSO formulas to CA local rules such that for any MSO formula Ψ, and any graph G the following equivalence holds: GΨ if and only if F_G,τ_CA(Ψ)τ_FO(Ψ).


Using notations from the construction of Theorem <ref>, let us now describe precisely the modifications required to generalize to arbitrary graphs.
As explained above, we assume k_i=1 for all 1≤ i≤ n, so choice layers χ_i are always trivial and uniform. States of type l for 1≤ l≤(n) are identical as in the construction of Theorem <ref>.
However, we need additional states to implement the truth check for the matrix R of formula Ψ, and it will spread over 3 time steps of the CA. The key is to ensure that some clause C_j from the disjunctive normal form of R is chosen uniformly on the entire graph and to check everywhere that each terms of C_j is locally correct given the assignment. Let 2=p_1< p_2<⋯ <p_d be the first d prime numbers.
For 1≤ j≤ d, let T_j^0 = S_(n)×{j} and T_j^1 = T_j^0×{0,1} and T_j^2= T_j^1×{1,…,p_j}. T_j^1 is used to mark vertices, while T_j^2 is used to alter the number of preimages depending on j and the mark. We use the notation π to denote at the same time the natural projection from T_j^0 onto S_(n), or from T_j^1 onto T_j^0 or from T_j^2 onto T_j^1, which removes the rightmost component of states. T_j^0 sates will be used to check clause C_j, while states from T_j^1 and T_j^2 will be used to guarantee through a pre-image counting trick that the same choice of j is made on the entire graph, thus ensuring correctness of the truth check of formula R.

We can now define the state set of the CA local rule τ_CA(Ψ) as

    S = {e_0,e_1}∪⋃_1≤ l≤(n) S_l ∪⋃_1≤ j≤ d T_j^0∪ T_j^1∪ T_j^2.

We say that the type of an element of S is l if it belongs to S_l, error if it is e_0 or e_1 and (j,m)-truth-check if it belongs to T_j^m for 1≤ j≤ d and m=0,1 or 2. 

A configuration c∈ S^V is valid if the following conditions hold:


  * states of all pairs of neighboring vertices of G are of the same type, and not of error type;

  * at each vertex v the control layers have zeros where the corresponding variable layers indicated by the choice layers have, precisely: K_i(c_v)≤ V_i^χ_i(c_v)(c_v) for all i such that K_i(c_v) is defined (intuitively, a 1 in a control layer is authorized only if their is a 1 in the 'chosen' component of the corresponding variable layer);


  * for a state (s,m,w)∈ T_j^2 where s∈ T_j^0, m∈{0,1} and w∈{1,…,p_j}, it must be the case that w=1 whenever m=0 (this condition expresses intuitively, that only marked vertices can generate preimages and it will allow through a preimage counting trick in the FO formula to ensure that the choice to check truth of clause j is coherent on the entire graph).
 
We write (μ) when the capped multiset μ represents a locally valid neighborhood according to the above conditions.







The modified CA local rule f is almost identical as the one from Theorem <ref> and defined as follows (denoting again s the unique state such that μ(s,ϵ)≥ 1):

    f(σ,μ) =
      
        e_1-i    if s=e_i
    
        e_0     otherwise, and if (μ),
    
        e_0     otherwise, and if s has type (j,0)-truth-check and (σ,μ)C_j,
    
        s     otherwise, and if s is of type 1,
    π(s)     otherwise.



The key aspect of this new construction is that the correctness of the distributed truth check implemented in the CA above by states of type (j,m)-truth check rely on a modification of the considered FO formula. Let jy be a FO formula expressing that the number of pre-images of y is either >p_d or a multiple of p_j. We use the following  modified definition of formula y:

    y⋁_1≤ j≤ d∃ y^j : y^j→ y ∧(∀ y': y'→ y^j ⇒jy')

which intuitively makes sense when y represents a configuration everywhere of type (n), so y^j represents of configuration of type (j,0)-truth check everywhere. We this new definition of y, we introduce a strong dependence of the FO-formula on the matrix part of Ψ (by the presence of d for instance), which was not the case in Theorem <ref>.

The final FO formula ϕ is defined exactly as in Theorem <ref> but using this modified version of y:


    ϕ_1' y^1∈1y^1, _2' y^2∈2y^1,y^2,…, _n' y^n∈ny^1,…,y^n : y^n


where the FO quantifier _i' is ∃ if the MSO quantifier _i is existential, and ∀ if _i is universal.


The proof of Theorem <ref> is based on two lemmas adapted from Lemma <ref> and <ref>, and can be copied word for word from the proof of Theorem <ref>, but simply removing the connectedness hypothesis.


  Let G be a (Σ,Δ)-labeled graph. Consider configurations c^1,…, c^i with 1≤ i≤ n such that F_G,fic^1,…, c^i, then the following holds:
  
  
  * c^k is of type (k) at each vertex, for 1≤ k≤ i;
  
  * for 1≤ l≤ i and 1≤ j≤ k_l, variable component V_l^j(c^k) is the same for for all k with l≤ k≤ i, and it is such that exactly one vertex is in state 1 when l∈ ;
  
  * if i<n, for any assignment α of variables (x_i+1^1,…,x_i+1^k_i+1) there exists c^i+1 such that 
    F_G,fi+1c^1,… ,c^i+1
 and V_i+1^j(c^i+1) = α(x_i+1^j) for all 1≤ j≤ k_i+1.
  


  Straightforward adaptation from the proof of Lemma <ref>, where χ_i components are by definition uniform since k_i=1 so that we don't use the hypothesis of connectivity on the graph.









  Under the hypothesis of Lemma <ref>, it holds that  F_G,fc^n if and only if (G,α_c^ n) R(x_1^1,…, x_n^k_n).


  First, by Lemma <ref>, the hypothesis implies that c^n is of type (n) at each vertex and is a valid configuration. If c is a pre-image of c^n, it must be valid (because no error state appears in c^n), as well as any of its preimage, and any preimage of its preimage.


Suppose now that F_G,fc^n.
We claim that any pre-image c of c^n must be of type (j,0)-truth-check at every vertex for some j (i.e. of uniform type on the entire graph). Indeed, if it were not the case, there would exist two vertices v and v' such that c is of type (j,0)-truth-check at v and of type (j',0)-truth-check at v' with j≠ j'. Thus c would have a preimage c' where only v is marked which would have exactly p_j preimages, and another c” where only v' is marked which would have exactly p_j' preimages, thus contradicting F_G,fc^n.

It must also be the case that, at each vertex v, (σ,μ) C_j where σ=L(v) and μ=(c,v,1,1), because F_G,f applied on c checks this condition and c^n contains no error. Now consider any term t of clause C_j with first-order free variable x_a^b and another free variable x_u^v, and let v be the unique vertex such that V_a^b(c_v)=1, which is v=α_c^n(x_a^b). By definition of f, it must be the case that (G,α_c^n) t (straightforward case analysis on atomic formulas). Since this holds for all terms of C_j and since R is a disjunction of clauses C_j, we deduce (G,α_c^ n) R(x_1^1,…, x_n^k_n).


  Conversely, if (G,α_c^ n) R(x_1^1,…, x_n^k_n), then by definition there must some j such that (G,α_c^ n) C_j(x_1^1,…, x_n^k_n). Let c be the configuration of type (j,0)-truth-check everywhere such that π(c)=c^n (where π is the map applying π at all vertices). We claim that F_G,f(c)=c^n which implies F_G,fc^n (because clearly all preimages of c have a number of preimages which is a power of p_j by construction). Indeed, considering any term t appearing in C_j and any node v, and denoting σ=L(v) and μ=(c,v,1,1), we have:
  
  
  * (σ,μ) t if v is the assignment of the leftmost free variable appearing in t since (G,α_c^n) t,
  
  * (σ,μ) t by definition otherwise.
  
  We deduce that (σ,μ) C_j and therefore that F_G,f applies projection π at each vertex v on c, proving the claim.





§ CONSEQUENCES ON FO MODEL CHECKING FOR CA



A set of (Σ,Δ)-labeled graphs, or graph language, is MSO-definable if it is of the form Ψ for some MSO formula Ψ. It is FOCA-definable if it is of the form ϕ,f for some FO formula ϕ and some CA local rule f. From Theorem <ref>, we get the following immediate corollary.


  MSO-definable and FOCA-definable graph languages are the same.


Since the translations given in Section <ref> are effective, we also obtain equivalence of model checking problems. Using <cit.>, this gives a characterization of decidability of FO model checking for CA orbits on f.g. groups.


  On any fixed graph, FO model checking for CA is many-one equivalent to MSO model checking.
  In particular, FO-model checking for CA on a f.g. group Γ is decidable if and only if Γ is virtually free.


We can get a more precise result on graphs of bounded degree, but we need an additional lemma in order to apply Theorem <ref>.
It is well-known that undecidability in MSO can be obtained using the MSO-definability of grids and encoding Turing-computations on it <cit.>. Moreover, MSO on bounded degree graphs actually allows to code quantification on edge sets and not only vertex sets <cit.>, so that we can express the grid minor relation (and not only the fact that a fixed graph is a minor). The following lemma doesn't use any new idea, but it ensures the fact that all this encoding process can be done within a fixed prefix signature. It also gives a variant of the construction for Σ_1^1-hardness (see <cit.>) using infinite grids and the recurring domino problem <cit.>.

  A n× n-grid (or simply a grid when n is not specified), is the directed finite graph with vertices {(i,j) : 1≤ i,j≤ n} and edges the set of pairs ((i,j),(i+1,j)) (the east edges) for 1≤ j≤ n and 1≤ i < n, and pairs ((i,j),(i,j+1)) (the north edges) for 1≤ j< n and 1≤ i ≤ n.
A ∞-grid is the infinite directed graph with vertices × and same north/east adjacency relation.


  Fix some D.  There exists a fixed quantifier prefix signature ρ for MSO such that, for any graph G of degree at most D that contains arbitrarily large grid as minors, deciding whether a given MSO formula in prenex form with prefix signature ρ is satisfied on G is undecidable.
  There also exists a fixed quantifier prefix signature ρ' for MSO such that, for any graph G of degree at most D that contains a ∞-grid as minor, deciding whether a given MSO formula in prenex form with prefix signature ρ' is satisfied on G is Σ_1^1-hard.










  In this proof, label sets Σ and Δ play no role as we will work on the underlying undirected unlabeled graph of G. So to simplify the proof, let's suppose that G is undirected and that Σ and Δ are singletons.
The necessity to have orientation inside grids to encode computation is recovered from the undirected graph G through MSO by introducing adequate colorings. More precisely, an oriented grid is represented by a set of vertices X, a formula (x_1,x_2) substituted for an undirected adjacency relation on X, and a coloring on X, i.e. a tuple of sets .
We then have an MSO formula  such that (X,,) holds if and only if the graph represented by X and  and  is isomorphic to an oriented grid. We also have formulas to test oriented adjacency along the direction  and , for instance (X,,,x_1,x_2) holds if and only if x_2 is at the north of x_1 in the grid graph represented by X,  and . We can also identify each side of the grid with MSO formulas. 

  The minor relation is definable in MSO2, the extension of MSO allowing quantification over vertices, set of vertices but also sets of edges. Indeed, given a set of vertices X and a set of contracted edges Y and a set of suppressed edges Z, we can write the property that two vertices x_1 and x_2 are neighbors in the minor graph induced by vertices X with contraction of edges Y and suppression of edges Z by
expressing that x_i is connected to some x_i' through edges from Y (for i=1,2) and that x'_1 is connected to x'_2 by an edge not in Z nor in Y.
  
  
  
  
  
  
On bounded degree graphs, MSO2 definability can actually be translated into MSO definability <cit.> (see <cit.> for more general results). The intuition is that it is possible to express in MSO that some coloring on vertices has strong enough properties so that an edge can be identified by a vertex and a color. This way a set of edges can be coded as a tuple of set of vertices (the size of the tuple depends on the degree of the graph). We therefore have an MSO formula (X,X_C,X_D,x_1,x_2) expressing that x_1 and x_2 are neighbors in the minor graph of G induced by set of vertices X and with contraction of edges coded via the tuple X_C and deletion of edges coded via the tuple X_D.

Given a finite set S and sets of horizontal and vertical dominos D_𝚎𝚊𝚜𝚝, D_𝚗𝚘𝚛𝚝𝚑⊂ S× S we can express that a coloring of X by S represented through X_S respects the horizontal (resp. vertical) domino constraints on a pair x_1, x_2 of vertices by a simple disjunction of case on D_𝚎𝚊𝚜𝚝 (resp. D_𝚗𝚘𝚛𝚝𝚑) denoted Ψ_h(x_1,x_2,X_S) (resp. Ψ_v(x_1,x_2,X_S)).  We also denote by Ψ_OK(X,X_S) the formula expressing that X_S is a partition of X.
It is well-known that this formalism for the domino problem is equivalent to the Wang tile formalism through higher-block recoding (see proof of Theorem <ref> for details).

With this tools, we can first prove the first part of the lemma.
  Let us define formula Ψ (depending on some given domino constraints) which expresses that any grid minor of G admits a coloring by S respecting the horizontal and vertical domino constraints, precisely:
  
    Ψ   ∀ X, ∀X_C, ∀X_D, ∀,  (X,(X,X_C,X_D,x_1,x_2),) ⇒
       ∃𝐗_𝐒, Ψ_OK(X,𝐗_𝐒)∧∀ x_1,∀ x_2, 
       (X,(X,X_C,X_D,x_1,x_2),,x_1,x_2)⇒Ψ_v(x_1,x_2,𝐗_𝐒)
       ∧(X,(X,X_C,X_D,x_1,x_2),,x_1,x_2)⇒Ψ_h(x_1,x_2,𝐗_𝐒)


  Given a set of domino constraints it is undecidable whether GΨ because it is equivalent to the domino problem <cit.>: G has arbitrarily large grid minors and having correct coloring for arbitrarily large grids as expressed by Ψ is equivalent to having a correct coloring for an infinite grid by compacity.

  Moreover, applying the standard logical transformation for the first implication, it can be verified that Ψ has a prenex normal form starting by ∀ X, ∀X_C, ∀X_D, ∀, ∀X_S followed by a sequence of quantifiers which does not depend on S nor on the domino constraints. This means that we can write the prenex normal form of Ψ with a fixed prefix signature when S and the domino constraints vary.


  Now, for the second part of the lemma, we use a reduction from a variant of the recurring domino problem which gives Σ_1^1-hardness (using the horizontal/vertical domino formulation instead of Wang tiles). Precisely, the following problem is Σ_1^1-hard for a fixed s_0 (problem R2 of <cit.>): deciding whether, for a given set of horizontal/vertical domino constraints with s_0∈ S, there is a coloring of the ∞-grid that satisfy the constraints and contains infinitely many occurrences of s_0 on the leftmost column.

  To encode this problem, we first use an MSO formula Ψ_∞(X,,X_S) expressing that:
  
  
  * the graph G(X,) represented by X and  has a unique vertex of in-degree 0 denoted x_0;
  
  * for any induced (finite) grid in the graph G(X,) with lower-left corner x_0, there is a strictly larger (finite) grid with the same lower-left corner such that:
    
    
  * X_S is a partition and satisfies domino constraints on the larger grid, and
    
  * there is a vertex on the leftmost column of the larger grid, outside the smaller grid, which is colored in s_0 by the coloring X_S.
  
  

  We then consider the formula Ψ (depending on the domino constraints) which express that there exists a minor of G and a coloring of it that satisfies Ψ_∞:
  
    Ψ∃ X, ∃X_C, ∃X_D, ∃X_S : Ψ_∞(X,(X,X_C,X_D,x_1,x_2),X_S).

  First, it should be clear that Ψ has a prenex normal form where the prefix signature doesn't change when S and the domino constraints vary.
  Second, we claim that GΨ if and only if there exists a coloring of the ∞-grid satisfying the domino constraints and containing infinitely many occurrences os s_0 on the first column. Indeed, if there is such a coloring of the ∞-grid and since the ∞-grid occurs as a minor of G, we can chose the corresponding variables quantified existentially to represent exactly this minor and this coloring so that Ψ_∞ will be satisfied. Conversely, if (G,α)Ψ_∞(X,(X,X_C,X_D,x_1,x_2),X_S) for some assignment α of the variables representing both a minor and a coloring, then we can extract a valid coloring of the ∞-grid with infinitely many s_0 on the leftmost column from the validity of Ψ_∞: just consider coloring X_S on the sequence of larger and larger grids which extend each other and add at each step a new occurrence of s_0 on the leftmost column.



This lemma together with Theorem <ref> gives undecidability of model checking for a fixed FO formula expressed in the following corollary. For the first part of the corollary, we use the grid minor theorem <cit.> to translate the statement of the lemma in terms of treewidth <cit.>, and for the second part, it is known that the Cayley graph of a f.g. group which is not virtually free has a thick end (see <cit.>), hence it contains a ∞-grid as a minor by Halin's grid theorem <cit.>. The decidable part of the Corollary comes from <cit.>.


  Fix some D. There is a fixed FO formula ϕ such that for any connected graph G of degree at most D, the set G,ϕ is computable if and only if G has finite treewidth. Moreover,   there is a FO formula ϕ' such that for any Cayley graph G of a f.g. group with at most D generators, the set G,ϕ is:
  
  
  * computable if the group is virtually free,
  
  * Σ_1^1-hard otherwise.
  





In the context of modeling, it makes sense to consider distributed dynamical systems over arbitrary finite graphs. For instance automata networks (which are non-uniform CA on arbitrary finite graphs) are a well-established model for its use in the study of gene regulation networks <cit.>. The theory of automata networks has largely grown around FO properties of orbits (typically fixed points) and their crucial dependence on the graph <cit.>. However, although many results deal with computational complexity in automata networks <cit.>, no natural undecidability result appeared so far to our knowledge. By our translation result from MSO, we can import Trakhtenbrot's theorem <cit.> to obtain an undecidability result for FO properties of CA orbits on finite graphs. It can intuitively be formulated as follows in the context of modeling: it is undecidable to know whether there is some finite interaction graph on which a given local interaction law (CA) induces a given dynamical property (FO).
By the way, this corollary doesn't need Trakhtenbrot's theorem since we have all the expressive power of MSO (not only FO logic on graphs), and we can obtain it for a fixed FO formula. For instance, it follows directly from Theorem <ref> and the techniques of Lemma <ref> (see also <cit.>).


  There exists a FO formula ϕ such that the following problem is undecidable:  given some input CA local rule f, decide whether there exists a finite graph G with F_G,fϕ.



  Finite rectangular n× m-grids are MSO-definable <cit.> and their lower-left and top-right corners are also MSO-identifiable. As in lemma <ref>, they are represented through a coloring  and a set of vertices X. We can also easily express in MSO that some Turing computation starts from the lower-left corner on an empty tape and finishes in an accepting state exactly at the upper-right corner. Formally, a Turing machine computation is a coloring X_S of the grid respecting vertical and horizontal domino constraints. All this conditions being gathered in a formula Ψ_𝚑𝚊𝚕𝚝(X,,X_S), we can define formula Ψ expressing that the entire graph is a grid that can hold a correct halting computation by:
  
    ∃ X,∃, ∃X_S, Ψ_𝚑𝚊𝚕𝚝(X,,X_S)∧∀ x, x∈ X.

  Since no quantification depending on S and the Turing computation appears in Ψ_𝚑𝚊𝚕𝚝, it is clear that Ψ can be written in prenex normal form with a fixed prefix signature when the Turing machine varies. So we can apply Theorem <ref> and effectively obtain a pair ϕ,f such that F_G,fϕ if and only if GΨ and ϕ doesn't depend on the Turing machine considered. ϕ is the formula announced in the corollary, and it is clear  that GΨ for some finite graph G if and only if the Turing machine encoded in Ψ halts starting from the empty tape, and halts exactly at the rightmost ever visited position of its tape. It remains to check that the halting problem with the additional condition of halting at the rightmost visited position of the tape is undecidable, which is straightforward by transforming any machine M (with a tape alphabet using a blank state which can only be erased and never be written) to a new machine working as M but, as soon as M halts, launches a terminal routing that moves the head to the right until reaching the first blank state before stopping.




§ CAYLEY GRAPHS AND DOMINO PROBLEMS





The case of Cayley graphs of f.g. groups is particular for our approach in two relevant ways.
First, we can express in MSO that a set of vertices is infinite.



  For any D≥ 1, there is an MSO formula Ψ(X) such that, on any Cayley graph G of some f.g. group with D generators and any assignment α, it holds that (G,α)Ψ(X) if and only if α(X) is infinite.



  First, for any infinite set of vertices X, there is an oriented walk on the group passing at most 2 times by any vertex and visiting infinitely many elements of X. To see this, consider any spanning tree T of the Cayley graph rooted at an arbitrary vertex v_0. At least one of the subtrees of v_0 contains infinitely many elements from X (finite degree of the Cayley graph): choose one and choose one x∈ X belonging to this subtree. Then let ρ be the path from v_0 to x in T, and let v be the last vertex of this path which possesses a subtree T_v with infinitely many elements from X. Note that v can be v_0 or x or another vertex, but in any case the subtree T_v is disjoint from ρ. We define the start of the walk as follows: ρ from v_0 to x, then back from x to v following the inverse of ρ. We can then iterate this reasoning inside subtree T_v from v to obtain the desired path.

  To define a walk passing at most 2 times by any vertex, it is sufficient to code that each vertex contains 0, 1 or 2 positions (corresponding to steps of the walk) and associate to each position an outgoing direction δ∈Δ and a number 1 or 2 indicating which of the two positions to go to in the vertex pointed by direction δ. Such a walk can be represented by a tuple of second-order variables , and we can express by a formula Ψ_𝙾𝙺() that this tuple actually represents a valid walk: each vertex contains at most 2 positions, each position has a successor, exactly one position has no predecessor and all others have exactly one, and the walk is connected. We can also express by a formula Ψ_𝚛𝚎𝚊𝚌𝚑(x_1,x_2,) that vertex x_2 is reached by the walk  starting from x_1, or x_1 is outside the walk. From this, we have that the following formula Ψ(X) expresses that X is infinite:
  
    Ψ(X)∃,Ψ_𝙾𝙺()∧∀ x_1, ∃ x_2: x_2∈ X ∧Ψ_𝚛𝚎𝚊𝚌𝚑(x_1,x_2,).

It can be check that this formula only depends on Δ, so it works on any Cayley graph of f.g. groups with generators renamed Δ.




From this lemma, it makes sense to extend the signature of FO logic with the addition of new relation  on configurations which is at the heart of the 'Garden of Eden' theorem <cit.>: we write c c' whenever {v:c_v≠ c'_v} is finite. We denote by  the extension of FO signature by adding relation . 
By Lemma <ref>, this extension remains within MSO. Precisely, in any fixed Cayley graph of a f.g. group and
by a straightforward extension of Theorem <ref>, we can compute from any formula in  and CA local rule, an equivalent MSO formula. We deduce that  model checking for CA is decidable on some f.g. group exactly when MSO model checking is, and exactly when FO model checking for CA is.

Besides, if Γ is a f.g. group and G_1 and G_2 two Cayley graphs of Γ with two different sets of generators Δ_1 and Δ_2, then the definable CA global maps F: S^Γ→ S^Γ are the same on G_1 and G_2. More precisely, there is a computable translation τ on CA local maps such that for any local map f for G_1, it holds:
F_G_1,f = F_G_2,τ(f).
This simply comes from the fact that we can translate Δ_1-walks into equivalent Δ_2-walks.

Therefore, if ϕ is a FO formula, we have that the sets ϕ,G_1 and ϕ,G_2 are actually Turing-equivalent. Said differently, by Theorem <ref>, any FO formula (actually any  formula) defines a fragment of MSO logic whose model checking problem's Turing degree is independent of the choice of generators on a f.g. group Γ. It turns out that such fragments naturally capture the domino problem and its classical variants.

Given some finite set S, a domino specification  is a set of pairs D_δ⊆ S^2 for each δ∈Δ. A configuration c∈ S^V is said -valid for some graph if for any v,v'∈ V it holds: (v,v')∈ E_δ implies (c_v,c_v')∈ R_δ. The domino problem on a fixed graph, consists in deciding given  whether there exists a -valid configuration. The seeded domino problem consists in deciding given  and s_0∈ S whether there exists a -valid configuration where s_0 occurs at some vertex. Finally, the recurring domino problem consists in deciding given  and s_0∈ S whether there exists a -valid configuration where s_0 occurs infinitely often. 




  Fix any Cayley graph G of any f.g. group, then:
  
  
  * domino problem   ∃ x, x→ x, 
  
  * seeded domino problem     ∃ x, ∃ y, x→ x∧ y→ x∧ x≠ y, 
  
  * recurring domino problem  ∃ x, ∃ y, x→ x∧ y→ x∧ (x y),
  
  where 'ϕ' means Turing-equivalent to the set ϕ,G (model checking of ϕ for CAs on G).



  In this proof Σ is a singleton and therefore omitted from CA local rules to simplify notations.
  
  For the first item, given some domino specification  it is easy to define a CA local rule f_ whose fixed points are exactly -valid configurations:
  
    f_(μ) =
        
          s     if ∀δ, μ(s',δ)>0⇒ (s,s')∈ D_δ
    
          s'≠ s    otherwise

  where s denotes the unique state such that μ(s,ϵ)>0.

 Conversely, given a local rule f of radius r over state set S , we can define a domino specification  over some state set S' ⊆ S^B(r) where B(r) denotes the ball of radius r in the graph. It is just a matter of applying a higher-block recoding (a well-known technique in symbolic dynamics) and restrict to local patterns of fixed points. Let S' be the set of patterns on which the local rule f doesn't change the state (recall that on Cayley graphs of f.g. groups, μ gives the same information as a pattern from S^B(r)). Then the domino specification is defined by
  
    (p,p')∈ D_δ∀ v,v'∈ B(r), (v,v')∈ E_δ⇒ p_v=p'_v'

  expressing that moving in direction δ can only change the state in a way compatible with translation of local patterns, or said differently, that the S' configuration is the correct higher-block recoding of some S configuration. It is clear that a -valid configuration is just a higher-block recoding of a fixed-point of f.


  For the second and third items, given  over state set S and s_0∈ S, we define f_,s_0  over state set S∪{t,e_0,e_1} (where t,e_0,e_1 are not in S), which duplicates state s_0 in another state t and use error states e_0 and e_1. Precisely:
  
    f_,s_0(μ) = 
        
          e_1-i    if s=e_i
    
          s_0     otherwise and if s=t,
    
          s     otherwise and if ∀δ, μ(s',δ)>0⇒ (ρ(s),ρ(s'))∈ D_δ,
    
          e_0    otherwise.

  where ρ : S∪{t}→ S is the map that sends t to s_0 and is the identity on S.
  Intuitively, this rule checks domino constraints while considering t equal to s_0 and transforms any occurrence of t to s_0. If a domino constraint is violated somewhere it generates an error state e_i which will locally oscillate with period two thus preventing forever the existence of a fixed point.
  One can check that fixed point for f_,s_0 are exactly the -valid configuration: it cannot contain state t, nor any error state, and must follow the D_δ constraints everywhere. Moreover, such a configuration possesses a preimage other than itself if and only if it contains an occurrence of s_0 which is replaced by t in the preimage. Moreover, each vertex at which such a configuration differs from its preimage must be in state s_0 in the configuration and t in the preimage. Thus ,s_0 is a positive instance of the seeded (resp. recurring) domino problem if and only if f_,s_0 satisfies formula of item two (resp. item three). 

  Finally, consider some CA local rule f over state set S and define a new set of domino constraints ^+ over state set S'⊆ S^B(r)× S^B(r) that uses higher-block recoding as above, but this time to represent pairs of configuration (c,c') such that c is a fixed-point and c' is a pre-image of c. Here S' is the set of pairs of patterns over domain B(r) such that the first pattern of the pair induces no change of state at position 0 by local rule f (i.e., locally a fixed point) and the second pattern of the pair is such that its image under f is the state at position 0 of the first (i.e., locally the second configuration is a preimage of the first). Then define S'_0 as the subset of S' where the state at position 0 differs between the first and second pattern. It then holds that ^+-valid configurations are exactly the higher-block recodings of pairs of configurations (c,c') where c is a fixed-point, c' is a pre-image of c and, moreover, c and c' differ at some vertex v if and only if the ^+-valid configuration is in some state from S_0' at v. Therefore, it follows that F_G,f satisfies formula of item two if and only if ^+,s_0 is a positive instance of the seeded domino problem for some element s_0∈ S_0' (hence a Turing reduction). Similarly, F_G,f satisfies formula of item three if and only if ^+,s_0 is a positive instance of the recurring domino problem for some element s_0∈ S_0' (hence a Turing reduction).



The recurring domino problem is Σ_1^1-hard on ^2 <cit.>, as well as the model checking of the corresponding  formula from Theorem <ref>. It is just an existential formula, but it crucially uses relation . We can actually also obtain Σ_1^1-hardness on ^2 with a pure FO formula with just one quantifier alternation, using preimage counting trickery to check finiteness of a set and a reduction from the recurring domino problem.


  The problem ϕ,^2 is Σ_1^1-hard where ϕ is the following formula:
  
    ϕ∃ y,y→ y∧∀ y',∀ y_1, ∀ y_2,∀ y_3, (y'≠ y∧ y'→ y∧⋀_i y_i→ y')⇒⋁_i≠ jy_i=y_j.

















  In plain English, formula ϕ requires the existence of a fixed point such that any of its pre-images (distinct from it) has at most two pre-images.  
  We proceed by reduction from the recurring domino problem (problem R1 of <cit.>). Consider an instance (,s_0) of this problem over states set S and let us describe a CA local rule f over states set S', of radius 1 and using 1-capped multiset. The states from S' are error states or states made of at most three layers, precisely:
  
    S' = S ∪ S× S_□∪ S× S_□×{0,1}∪{e_0,e_1}

  where e_0 and e_1 are error states as usual, and S_□ is used to code a particular set of configurations through domino constraints _□ (detailed below). The type of a state is either error, or its number of layers (e.g. 2 for states from S× S_□). The key property of _□-valid configurations is that they either code a finite square zone with four corners where the interior can be distinguished from the exterior, or they contain at most one corner (possibly corresponding to having an infinite square with an infinite interior). More precisely, we define
  
    S_□ = {N,S,E,W,E_d, W_d,I,I_d,I^d,,,,,,,,,,,,}

  where I and I_d and I^d are the interior states, and ,,, are corner states. _□ is the set of vertical and horizontal dominos appearing in this partial configuration:
  
    N     N    N          
           W     I     I^d     I_d     E_d       
           W     I^d     I_d     I     E       
           W_d     I_d     I     I     E       
              S     S     S

The index d in the above symbols mark a diagonal of the square (since we use only vertical and horizontal domino constraints, we need to mark staircase diagonals). It should be clear that a _□-valid configuration contains at most one occurrence of each corner state type, at most one horizontal segment of N (resp. of S) and at most one vertical segment of W_d/W (resp. E/E_d). Also a valid configuration with four corners contains finitely many occurrences of interior states. Moreover, it can be checked by a simple case analysis that if two corners are present, then actually four are present.
  
 The behavior of f is essentially to let configurations of type 1 unchanged, to project S× S_□×{0,1} onto S× S_□ and S× S_□ onto S. The local rule also verifies the following conditions (and generate an error with period two oscillations between e_0 and e_1 if one condition is violated):


  * two neighboring states must have the same type,

  * a configuration using only states from S must represents a -valid configuration,

  * the S_□ component of a configuration of type 2 or 3 must be a _□-valid configuration,

  * each occurrence of state s_0 in the S component of states, must be at a vertex where the _□ component is in an interior state (I or I_d or I^d),

  * a configuration of type 3 must be such that the {0,1} component at any vertex is 0, except when the S_□ component represents a corner, in which case it can be either 0 or 1 (at this point the reader should see coming a preimage counting trick in order to count the number of corners).

With these conditions, the only possible fixed-points are type 1 configuration representing a -valid configuration ; their pre-images must additionally contain a S_□ component representing a _□-valid configuration ; and the number of possible pre-images of each such pre-image is 2^k where k is the number of corners in the S_□ component.

Therefore, a fixed-point such that each of its pre-image has at most 2 pre-images (like specified in formula ϕ) is a configuration of type 1 such that it is impossible to form a pre-image with two or more corners, i.e. such that it is impossible to form a pre-image with finitely many interior states without generating an error state, and therefore it represents a -valid configuration with infinitely many occurrences of s_0.
Conversely, it is clear that for each -valid configuration with infinitely many occurrences of s_0 we can construct a fixed point with the above properties.





§ PERSPECTIVES


We see several interesting research directions inspired by the approach taken in this work.

First, we believe that the dependence of ϕ on the degree or the number of generators in Corollary <ref> is an artifact that can be removed with more work in the proof of Lemma <ref>.
The same proof techniques should also provide hardness result at any level of the analytical hierarchy.

Then, this corollary should be put into perspective with the Ballier-Stein conjecture <cit.> saying that the domino problem on a f.g. group is decidable if and only if the group is virtually free. On one hand, it seems natural to ask whether the recurring domino problem (or its equivalent FO formula from Theorem <ref>) can play the role of formula ϕ' in Corollary <ref>. 
On the other hand, N. Pytheas Fogg pointed us simple examples of 4-regular graphs having an ∞-grid as subgraph on which the domino problem is decidable. So formula ϕ in Corollary <ref> cannot be the FO formula expressing the existence of a fixed point (Turing-equivalent to the domino problem), and we wonder how simple such formula ϕ can be. Actually, we can ask a similar question for Corollary <ref>.

In general, we believe that the Turing degrees of FO-model checking problems for various concrete formulas is worth being investigated.  As mentioned above, the Turing degree of all such model checking problems for a fixed FO formula is independent of the choice of generators on f.g. groups, and we wonder how they change when changing the group among non virtually free groups. Injectivity of CA is a natural candidate that received little attention to our knowledge since the seminal result on ^2 <cit.>.

Finally, we believe that there exists a fixed CA rule f for which  the FO-model checking problem is undecidable on graph ^2 (the rule is fixed, the formula is given as input). While we see the proof ingredient to obtain this specifically for ^2, we have no idea of whether it is always the case that undecidability of FO model checking for CA orbits can be obtained for a fixed CA rule on any f.g. which is not virtually free.



§ ACKNOWLEDGMENT



We thank anonymous referees for their feedback and their suggestions to improve the presentation. We also warmly thank N. Pytheas Fogg for their hints about domino problems on regular graphs and numerous stimulating discussions that inspired this work.




