Undecidability of satisfiability of expansions of FO [ < ] over words with a FO [ + ] -definable set

Abstract

Two new characterizations of $FO [<, mod]$ -definable sets, i.e. sets of integers definable in first-order logic with the order relation and modular relations, are provided. Those characterizations are used to prove that satisfiability of first-order logic over words with an order relation and a $FO [+]$ -definable set that is not $FO [<, mod]$ -definable is undecidable.

Keywords

Finite model theory first order logic arithmetic undecidability

1. Introduction

A classical result of descriptive complexity theory (see [11]) states that a language of finite words over an alphabet α belongs to the circuit complexity class alternative log-time uniform $A C^{0}$ if and only if it is $FO [+, \times, {(P_{a})}_{a \in α}]$ -definable (where $P_{a} (x)$ holds if and only if the xth letter carries the letter a). One can consider variants where ${+, \times}$ is replaced by weaker arithmetical relations. Two important examples are the fragments $FO [<, {(P_{a})}_{a \in α}]$ and $FO [<, mod, {(P_{a})}_{a \in α}]$ , where mod denotes the set of modular relations. The fragment $FO [<, {(P_{a})}_{a \in α}]$ captures the class of star-free regular languages [13]. The fragment $FO [<, mod, {(P_{a})}_{a \in α}]$ also captures a subclass of the regular languages, which enjoys an (effective) algebraic characterization (see [1, Corollary 10]); moreover $FO [<, mod, {(P_{a})}_{a \in α}]$ is maximal with respect to regular languages, in the sense that every non-trivial extension of the signature ${<, mod}$ with numerical relations allows to define non-regular languages [17]. For more information on this logic, the reader is referred to the book [19].

To our knowledge, there exist only few results on the expressivity of logics which lay between $FO [<, mod, {(P_{a})}_{a \in α}]$ and $FO [+, \times, {(P_{a})}_{a \in α}]$ . The situation contrasts with the extensive literature on definability of fragments of arithmetic over non-negative integers, but is not surprising since many classical (un)definability techniques and results cannot be transferred to finite models. On the one hand, the first-order theory of addition over non-negative integers, $FO [+]$ (i.e. Presburger Arithmetic), is decidable [18], and there exist several characterizations of sets definable in this logic [10,14,16]. On the other hand, the expressive power of $FO [+, {(P_{a})}_{a \in α}]$ over finite words is not completely understood. Recently Choffrut et al. [5] proved several closure properties of $FO [+, {(P_{a})}_{a \in α}]$ -definable languages, and provided a partial characterization.

A natural approach to evaluate the expressive power of these logics is to study the complexity of the satisfiability problem. On the one hand this problem is undecidable for $FO [+, \times]$ , as a direct corollary of Trakhtenbrot’s Theorem [20]. Lange [12, Lemma 6.3] proved that undecidability occurs even for $FO [+, {(P_{a})}_{a \in α}]$ over words. On the other hand satisfiability is decidable for $FO [<, mod, {(P_{a})}_{a \in α}]$ , since this fragment is contained in $MSO [<]$ for which satisfiability is decidable [3,7,21]. In this paper the decidability frontier for logics between $FO [<, mod, {(P_{a})}_{a \in α}]$ and $FO [+, {(P_{a})}_{a \in α}]$ is specified, by proving that for every integer $d ⩾ 1$ and every relation $R \subseteq N^{d}$ , if R is $FO [+]$ -definable but not $FO [<, mod]$ -definable, then satisfiability is undecidable for $FO [<, R, {(P_{a})}_{a \in α}]$ .

One should note that the previous result does not hold anymore when the condition that R is $FO [+]$ -definable is removed. It can be shown for instance that satisfiability is decidable for $FO [<, mod, R, {(P_{a})}_{a \in α}]$ when R denotes the set of factorials or the set of powers of two (this is a direct consequence of Elgot–Rabin’ result that satisfiability of $MSO [<, R]$ is decidable in this case [8]).

In order to obtain our undecidability result, general results about definability in fragments of Presburger Arithmetic are proven. It is known that sets definable in Presburger Arithmetic coincide with semilinear sets [10]. Two characterizations of semilinear sets are given in [14,16] in terms of sets of smaller arity and local properties. Similar results are proven for the logic $FO [<, mod]$ , and also for logics $FO [<, mod m]$ where only modulo m relation is used for some fixed non-negative integer m. Note that the $FO [<, mod]$ -definable sets are sometimes called regular sets because they correspond to languages accepted by synchronous multi-tape automata which read integers in base 1 (e.g. [19]).

The first result, Theorem 4.4, states that for each $d \in N$ , a set $R \subseteq N^{d}$ is $FO [<, mod m]$ -definable if and only if:

Every section of R (i.e. every subset of $N^{d - 1}$ obtained from R by fixing a component) is $FO [<, mod m]$ -definable and

apart from a finite number of sections, R is equal to ${(x_{0} + m, \dots, x_{d - 1} + m) ∣ (x_{0}, \dots, x_{d - 1}) \in R}$ , that is, R translated by m in all directions.

The logics $FO [<, mod m]$ and $FO [<, mod]$ admit another characterization: Theorem 4.18 states that a set R is not $FO [<, mod m]$ -definable if and only if there exists a $FO [<, R]$ -definable set of integers which is not $FO [<, mod m]$ -definable. Similarly Theorem 4.15 states that a $FO [+]$ -definable set R is not $FO [<, mod]$ -definable if and only if there exists a unary $FO [<, R]$ -definable function which is not $FO [<, mod]$ -definable.

It should be noted that $FO [<]$ has the same expressive power as $FO [<, mod 1]$ , hence every result about $FO [<, mod 1]$ holds for $FO [<]$ .

Then in Section 5, Theorem 5.1 states that satisfiability of $FO [<, R, {(P_{a})}_{a \in α}]$ is undecidable over words when R is a $FO [+]$ -definable set which is not $FO [<, mod]$ -definable.

2. Definitions and notations

In this section, useful definitions are recalled and some notations are fixed. To avoid ambiguity, the “=” symbol is used for mathematical equality and definitions, but in logical formulas, the equality relation is denoted by “≐”. Let $N$ denote the set of non-negative integers, let $Z$ denote the set of integers and let $Q$ denote the set of rational numbers. For $S \subseteq Q$ and $c \in Q$ , let $S^{> c}$ (respectively, $S^{⩾ c}$ ) be the set of elements of S which are greater than (respectively, greater or equal to) c.

For a set S, let $# S$ denote its cardinality. For $d \in N^{> 0}$ , let $S^{d}$ denote the set of d-tuples of elements of S. Let $a, b \in N$ , then $[b] = {n \in N ∣ 0 ⩽ n ⩽ b}$ and $[a, b] = {n \in N ∣ a ⩽ n ⩽ b}$ . For $m \in N^{> 0}$ and $k \in [m - 1]$ , let $m N + k$ be the set of non-negative integers congruent to k modulo m. For $d \in N$ , bold letters are used to denote d-tuples of variables, such as $x \in N^{d}$ , which is an abbreviation for $(x_{0}, \dots, x_{d - 1})$ . For $i \in [d - 1]$ , the variable $x_{i}$ is called the ith component of $x$ . Let $({\overline{m, \dots, m}}^{d})$ denote the d-tuple $(m, \dots, m)$ . For $x \in N^{d}$ , let $min (x)$ denote $min {x_{i} ∣ i \in [d - 1]}$ , and let $‖ x ‖$ denote $\sum_{i = 0}^{d - 1} x_{i}$ . Finally, let $x + y$ denote $(x_{0} + y_{0}, \dots, x_{d - 1} + y_{d - 1})$ and let $x - y$ denote $(x_{0} - y_{0}, \dots, x_{d - 1} - y_{d - 1})$ .

2.1. First-order logic over a vocabulary $V$ ( $FO [V]$ )

In this section, the definitions concerning the logical formalisms of this paper are introduced.

Definition 2.1 (Universe).

A universe $U$ is a set. In this paper, $U$ is always equal, either to $N$ or to $[n]$ for $n \in N$ .

Definition 2.2 (Vocabulary).

A vocabulary is a set of the form $\begin{matrix} V = {{(R_{i} / d_{i})}_{i < n}, {(c_{i})}_{i < q}}, \end{matrix}$ where n and q are either integers or ω (the cardinality of the set of integers).

For $i < n$ , the $R_{i}$ ’s are the relation symbols and their arity is $d_{i}$ . For $i < q$ , the $c_{i}$ ’s are the constant symbols.

Definition 2.3 (Structure).

Let $V$ be a vocabulary. A $V$ -structure $S$ over the universe $U$ is a tuple $\begin{matrix} (U, {(R_{i}^{S})}_{i < n}, {(c_{i}^{S})}_{i < q}) \end{matrix}$ where $R_{i}^{S} \subseteq U^{d_{i}}$ for $i < n$ , and $c_{i}^{S} \in U$ for $i < q$ .

For ς a relational symbol with arity d and $ι \subseteq U^{[d - 1]}$ , let $S [ς / ι]$ denote the $V \cup {ς}$ -structure of universe $U$ where $ς^{S [ς / ι]} = ι$ and $τ^{S [ς / ι]} = τ^{S}$ for every symbol $τ \in V ∖ {ς}$ . The same definition is used for a constant symbol ς and $i \in U$ .

Definition 2.4 (Finite structure $S_{| n}$ ).

Let $n \in N$ , let $V$ be a vocabulary and let $S$ be a $V$ -structure of cardinality at least n and such that for each constant symbol $c_{i}$ , $c_{i}^{S} < n$ holds. Then $S_{| n}$ is the $V$ -structure over the universe $[n - 1]$ such that $c_{i}^{S_{| n}} = c_{i}^{S}$ and $R_{i}^{S_{| n}} = R_{i}^{S} \cap {[n - 1]}^{d_{i}}$ .

In this paper, if $V$ contains a symbol with a standard interpretation over $N$ , such as “+” or “<” then the only $V$ -structures $S$ , of universe $U$ , which are considered, are the ones such that each symbol has its standard interpretation. For example, it is always assumed that $+^{S} = {(i, j, k) \in U^{3} ∣ i + j = k}$ . In particular, for a vocabulary $V$ which only contains symbols with a standard interpretation over $N$ , let $N$ denote the structure which associates to each symbol its standard interpretation.

The fragments of first- and second-order logic used in this paper are now defined.

Definition 2.5 ( $V$ -Formulas).

Let $V$ be a vocabulary. The set of quantifier-free $V$ -formulas, denoted by $Σ_{0} [V]$ and $Π_{0} [V]$ , is defined by the grammar: $\begin{array}{rcl} Σ_{0} [V] : : = \neg ϕ_{0} ∣ ϕ_{0} \land ϕ_{1} ∣ ϕ_{0} \lor ϕ_{1} ∣ R_{i} (c_{0}, \dots, c_{d_{i} - 1}) ∣ c_{0} ≐ c_{1} \end{array}$ where the $c_{i}$ ’s are constant symbols of $V$ and the $ϕ_{i}$ ’s are $Σ_{0} [V]$ -formulas.

The sets $Σ_{i} [V]$ , $Π_{i} [V]$ and $D_{i} [V]$ are defined by mutual recursion on i. For $i \in N$ let $D_{i} [V]$ be defined by the grammar: $\begin{array}{rcl} D_{i} [V] : : = \neg ϕ_{0} ∣ ϕ_{0} \land ϕ_{1} ∣ ϕ_{0} \lor ϕ_{1} ∣ ψ \end{array}$ where $ϕ_{i}$ belongs to $D_{i} [V]$ and ψ belongs to $Σ_{i} [V]$ or to $Π_{i} [V]$ .

For $i \in N^{⩾ 0}$ , let $Σ_{i} [V]$ be defined by the grammar: $\begin{array}{rcl} Σ_{i} [V] : : = \exists x . ψ ∣ ϕ_{0} \land ϕ_{1} ∣ ϕ_{0} \lor ϕ_{1} ∣ \neg χ ∣ ξ \end{array}$ where $ψ \in Σ_{i} [V, x]$ , the $ϕ_{i}$ ’s are $Σ_{i} [V]$ -formulas, χ is a $Π_{i} [V]$ -formula and ξ is a $D_{i - 1} [V]$ -formula.

Similarly, let $Π_{i} [V]$ be defined by the grammar: $\begin{array}{rcl} Π_{i} [V] : : = \forall x . ψ ∣ ϕ_{0} \land ϕ_{1} ∣ ϕ_{0} \lor ϕ_{1} ∣ \neg χ ∣ ξ \end{array}$ where $ψ \in Π_{i} [V, x]$ , the $ϕ_{i}$ ’s are $Π_{i} [V]$ -formulas, χ is a $Σ_{i} [V]$ -formula and ξ is a $D_{i - 1} [V]$ -formula.

Let $FO [V]$ be the union of the fragments $Π_{i} [V]$ for $i \in N$ .

For a logical fragment $L [V]$ , let $\exists MSO L [V]$ denote the set of formulas of the form $\exists R_{0}, \dots, R_{n} . ψ$ where ψ is a $L [V, R_{0}, \dots, R_{n}]$ -formula and where the arity of the $R_{i}$ ’s is 1.

Let $ϕ_{0} ⟹ ϕ_{1}$ be an abbreviation for $\neg ϕ_{0} \lor ϕ_{1}$ and let $ϕ_{0} ⟺ ϕ_{1}$ be an abbreviation for $ϕ_{0} ⟹ ϕ_{1} \land ϕ_{1} ⟹ ϕ_{0}$ .

The arity and the curly brackets are omitted in logics’ notations. For instance, $FO [+]$ is written instead of $FO [{+ / 3}]$ .

For a vocabulary $V$ , and a logical fragment $L$ , the $L [V \cup {x_{0}, \dots, x_{d - 1}}]$ -formulas are said to be $L [V]$ -formulas with arity d. The $x_{i}$ ’s for $i \in [d - 1]$ , are called the free variables and do not belong to $V$ . Given some $V$ -structure $S$ , the semantic of a formula is defined recursively as usual.

Definition 2.6 (Definability).

Let $d \in N$ and $ϕ (x_{0}, \dots, x_{d - 1})$ be a formula with d free variables in a logic $L [V]$ . For a $V$ -structure $S$ , the formula ϕ defines in $S$ the d-ary set $ϕ {(x)}^{S} = {x \in U^{d} ∣ S ⊧ ϕ (x)}$ .

A set $R \subseteq U^{d}$ is said to be $L [V]$ -definable in $S$ if there exists $ϕ (x_{0}, \dots, x_{d - 1}) \in L [V]$ such that $R = ϕ {(x_{0}, \dots, x_{d - 1})}^{S}$ . Furthermore, if f is a function from $U^{d}$ to $U$ , then f is $L [V]$ -definable if its graph is $L [V]$ -definable.

In some proofs, it is needed to define a set within another set.

Definition 2.7 (Defining in a set).

Let $F \subseteq N^{d}$ , the formula $ϕ (x)$ defines R in F if, for all $n \in F$ , $S [x / n] ⊧ ϕ (x)$ if and only if $n \in R$ .

In this paper many definability results are given, and they are obtained by explicitly constructing a formula that defines the definable set. Hence for the sake of readability, some notations are introduced. When a formula which defines a set S is constructed, it is sometimes needed to state “If there exists some $(i \in F, x \in N^{d})$ such that $ϕ_{i} (x)$ holds, then we define S by $χ_{i} (x)$ , otherwise we define it by ψ”. In this paper, there is always at most one i and one $x$ for which the property $ϕ_{i} (x)$ holds. Hence the following notation is introduced.

Definition 2.8.
For $i \in F$ , $j \in N$ , let $ϕ_{i} (x), χ_{i} (x) \in Σ_{j} [V]$ and $ψ \in Π_{j} [V]$ be formulas. Let $⟨ ⋁_{i \in F} \exists x . ϕ_{i} (x) ∣ χ_{i} (x) ∣ ψ ⟩$ denote the $D_{j} [V]$ -formula: $\begin{array}{rcl} [\underset{i \in F}{⋁} \exists x . ϕ_{i} (x) \land χ_{i} (x)] \lor [\underset{i \in F}{⋀} \forall x . \neg ϕ_{i} (x) \land ψ] . \end{array}$

Finally, a notation must also be defined to consider functions. Definition 2.9.
Let $ϕ \in FO [<, R]$ be a formula with $x, y$ as free variables. Let $ϕ (x; y)$ denote the fact that for all $x$ , there exists exactly one $y (x)$ such that $ϕ (x, y (x))$ holds. Then ϕ can be seen as a function mapping $x$ to $y (x)$ and $ϕ (x)$ is used to denote $y (x)$ .

Functions

Let us say a word about functions in this paper. Usually in finite model theory, the vocabulary does not contain function symbols, hence the only terms are the constants. Instead, formally, unary functions $f (x)$ are replaced by a binary relation $f (x, y)$ , such that for every $n \in U$ there is at most one $r \in U$ such that $f (n, r)$ holds. For example, the addition of 1 is denoted as the binary relation $+_{1} (x, y)$ interpreted in $[n]$ by ${(x, x + 1) ∣ x < n}$ . The distinction is important because over the universe $[n]$ , the value of $n + 1$ is undefined.

On the other hand, for the sake of clarity, “ $+_{1} (x, y)$ ” is written “ $x + 1 ≐ y$ ”, and more generally if $f (x)$ is a function, then “ $f (x, y)$ ” is written “ $f (x) ≐ y$ ”.

In this paper, the number of alternations of quantifiers of formulas is specified. For the sake of simplicity, we introduce abbreviations such as $f (g (x))$ . The following lemmas explain how to encode formally all of those abbreviations in fragments of the logic.
Lemma 2.10.
Let f be a unary function symbol and x be a constant symbol. Let $V$ be a vocabulary which contains x and f, and let $S$ be a $V$ -structure. Let $ψ (x)$ be a $Σ_{i} [V]$ -formula with $i > 0$ , then $ψ (f (x))$ is equivalent to a $Σ_{i} [V]$ -formula in $S$ .
Proof.
The formula $ψ (f (x))$ is equivalent to the $Σ_{i} [V]$ -formula: $\begin{matrix} \exists y . f (x) ≐ y \land ψ (y) . \end{matrix}$ Clearly, if $f^{S} (x^{S})$ is not defined then this formula does not hold in $S$ , which is the intended behavior as $f (x)$ is not defined either. □

The preceding lemma extends easily to the compositions of several function symbols.
2.2. Words

An alphabet α is a finite non-empty set. The set $α^{+}$ stands for the set of finite non-empty sequences of elements of α, which are called words.

It is now explained how to associate a $V$ -structure $S$ to a word w. Unary predicates ${(P_{a})}_{a \in α}$ are introduced in the following definition and are added to $V$ in order to encode w in $S$ . The predicates $P_{a}$ are interpreted by the set of positions of the a’s in the word w.

Definition 2.11.
Let $V$ be a vocabulary and let $S$ be a $V$ -structure of universe $N$ . Let $w = w [0] \dots w [n - 1]$ with $w [i] \in α$ be a word of length n over the alphabet α. Then let $S (w)$ be the $V \cup {{(P_{a})}_{a \in α}}$ -structure $S [{(P_{a} / {i ∣ w [i] = a})}_{a \in α}]$ of universe $[n - 1]$ .

2.3. Relations

The vocabularies $V$ considered in this paper contain relation symbols whose interpretation is fixed. In this section, those symbols are listed, and their interpretation over the universe $N$ is given. For the sake of readability, the infix notation is used when it is more standard than the prefix one.

Let $x, y$ be variables. Let $c \in N$ , $r \in Q^{> 0}$ , $m \in N^{> 0}$ , $N \subseteq N$ and $a \in [m - 1]$ be constants.

For $c \in N$ , the symbol c is also used as a constant symbol of the vocabulary. Then N represents the set of constant symbols belonging to N.

Let $+_{c}$ be the relation ${(n, n + c) ∣ n \in N}$ . Clearly $+_{0}$ is the equality relation and $+_{1}$ is the successor relation. The notation “ $x + c ≐ y$ ” is used instead of “ $+_{c} (x, y)$ ”. Let $+_{N}$ denote the set of relations ${+_{c} ∣ c \in N}$ .

Let “ $\equiv a mod m$ ” denote the set ${x \in N ∣ x \equiv a mod m}$ , and let “ $mod m$ ” be the set containing the m relations $\equiv a mod m$ . For $M \subseteq N^{> 0}$ , let “ $mod M$ ” denote the union of the relations $mod m$ for $m \in M$ , and “mod” denote $mod N^{> 0}$ . Then the notation “ $x \equiv a mod m$ ” is used instead of “ $\equiv a mod m (x)$ ”. Let “ $x + c \equiv y mod m$ ” be an abbreviation for $⋁_{a = 0}^{m - 1} x \equiv a mod m \land y \equiv (a + c) mod m$ .

3. First-order logic

All results concerning the manipulation of formulas and of sets of tuples of integers used in this paper are introduced in this section.

Section 3.1 shows how to adapt formulas about $N$ to formulas about finite structures. Then Section 3.2 introduces the notions of sections, diagonals and subspaces of a set. Then Section 3.3 considers sets of integers and unary functions which are $FO [<, mod]$ -definable, $FO [<, mod m]$ -definable and $FO [+]$ -definable. Finally Section 3.4 shows that the set of $FO [<, mod]$ -formulas admits elimination of quantifiers.

3.1. Logic over $N$ and over finite models

In Section 5, finite models are considered, using results given in this section. Hence, a notion of convergence is needed to state that properties of formulas over $N$ can also be used over finite models.

Definition 3.1 (Set convergence).

Let $V$ be a vocabulary. Let $S$ be a $V$ -structure over $N$ . Let $ϕ (x)$ be a formula with arity d such that its interpretation in $S_{| n}$ (respectively, in $S$ ) is a set $E_{n}$ (respectively, E). Then $ϕ (x)$ is said to be converging to E in $S$ , if for all $c \in N^{d}$ , there exists $N \in N$ such that for all $i ⩾ N$ , $c \in E_{i}$ if and only if $c \in E$ .

For formulas that define functions, this notion is equivalent to pointwise convergence.

Example 3.1.
Let $f_{n}$ be defined on $[n - 1]$ by $f_{n} (c) = c + ⌊ \frac{2 c}{n} ⌋$ . Then for all $c \in N$ , ${(f_{n} (c))}_{n > c}$ is a sequence of integers converging to c, so ${(f_{n})}_{n \in N}$ converges to the identity function.

In fact, in our proofs, the values of $f_{n}$ are only studied on $[c_{n} - 1]$ for some $c_{n} ⩽ n$ and $c_{n}$ increasing to infinity, i.e. the values of $f_{n} (b)$ for $b ⩾ c_{n}$ are not considered.

The following lemma is straightforward from the definition. Lemma 3.2.
Let $f, g : N \to N$ be two converging functions, then $f \circ g$ is a converging function.

3.2. Sections, diagonals and subsets

In this section some notations are introduced to transform sets into sets which are, intuitively, smaller.

Definition 3.3 (Section, diagonal and straight subspace).

Let $d ⩾ 1$ , $R \subseteq N^{d}$ , $i, j$ be distinct elements of $[d - 1]$ , and $c \in N$ . Then we define the section $sec (R; x_{i} = c) \subseteq N^{d - 1}$ as the set obtained from R by fixing the ith component to c: $\begin{matrix} sec (R; x_{i} = c) = {(x_{0}, \dots, x_{i - 1}, x_{i + 1}, \dots, x_{d - 1}) \in N^{d - 1} ∣ (x_{0}, \dots, x_{i - 1}, c, x_{i + 1}, \dots, x_{d - 1}) \in R} . \end{matrix}$ Similarly, the diagonal $diag (R; x_{i} = x_{j} + c) \subseteq N^{d - 1}$ is defined as follows: $\begin{matrix} \begin{array}{l} diag (R; x_{i} = x_{j} + c) \\ = {(x_{0}, \dots, x_{i - 1}, x_{i + 1}, \dots, x_{d - 1}) \in N^{d - 1} ∣ (x_{0}, \dots, x_{i - 1}, x_{j} + c, x_{i + 1}, \dots, x_{d - 1}) \in R} . \end{array} \end{matrix}$

The set of straight subspaces of R of dimension $d^{'} \in [d - 1]$ is defined by induction on $d - d^{'}$ as ${R}$ if $d^{'} = d$ , and as the set of sections and diagonals of straight subspaces of dimension $d^{'} + 1$ otherwise.

Example 3.2.
The sections and diagonals of the addition relation $x_{0} + x_{1} = x_{2}$ are now studied. Let $c \in N$ . One has: $\begin{array}{l} sec (+; x_{0} = c) = sec (+; x_{1} = c) = {(n, n + c) ∣ n \in N}, sec (+; x_{2} = c) = {(n, c - n) ∣ n ⩽ c}, \\ diag (+; x_{0} = x_{1} + c) = diag (+; x_{1} = x_{0} + c) = {(n, 2 n + c) ∣ n \in N}, \\ diag (+; x_{2} = x_{1} + c) = {(c, n) ∣ n \in N}, \\ diag (+; x_{0} = x_{2} + c + 1) = diag (+; x_{1} = x_{2} + c + 1) = \emptyset, diag (+; x_{2} = x_{0} + c) = {(n, c) ∣ n \in N} . \end{array}$

A notation for straight subspaces is now introduced. A pair of d-tuples $(t, c)$ is associated with each straight subspace. The d-tuple $t$ belongs to ${({var, const} \cup {add (i) ∣ i \in [d - 1]})}^{d}$ . Intuitively $t_{i} = const$ means that the ith dimension is fixed, $t_{i} = add (j)$ means that the distance between the jth and the ith dimension is fixed, and $t_{i} = var$ means that the ith dimension is free.

The formal definition is now introduced.
Definition 3.4.
Let $d \in N^{> 0}$ , let $t \in {({var, const} \cup {add (i) ∣ i \in [d - 1]})}^{d}$ and let $c \in N^{d}$ . Let $dim (t)$ be the number of indices i such that $t_{i} = var$ . Then let $sub (R; t, c)$ denote the set $\begin{matrix} {{(x_{i})}_{t_{i} = var} \in N^{dim (t)} ∣ (x_{0}, \dots, x_{d - 1}) \in R, x_{i} = c_{i} if t_{i} = const, x_{i} = x_{j} + c_{i} if t_{i} = add (j)} . \end{matrix}$

The following lemma is an easy consequence of the definition.
Lemma 3.5.
Let $d \in N^{> 0}$ , $R \subseteq N^{d}$ , $d^{'} < d$ and $S \subseteq N^{d^{'}}$ . The two following statements are equivalent:
the set S is a straight subspace of $R \subseteq N^{d}$ ,

there exists $(t, c)$ such that $S = sub (R; (t, c))$ and there are $d^{'}$ integers i such that $t_{i} = var$ .

A formula which defines $sub (R; t, c)$ is now introduced.
Definition 3.6.
Let $L$ be a fragment of logic and let $V$ be a vocabulary. Let $χ (x)$ be an $L [V]$ -formula. Let $t, c$ be as in Notation 3.4.

Then let $sub (χ, t, c) (x)$ denote the $L [V, N, +_{N}]$ -formula $χ (y)$ defined as the conjunction of the following formulas, for each $i \in [d - 1]$ :
$y_{i} = x_{h}$ , if $t_{i} = var$ , and h is the ith value such that $t_{h} = var$ ,

$y_{i} = c_{i}$ if $t_{i} = const$ and

$y_{i} = x_{h} + c_{i}$ if $t_{i} = add (j)$ , and h is the jth value such that $t_{h} = var$ .
In particular, $sub (R, t, c)$ is a $Σ_{0} [N, +_{N}, R]$ -formula.

The following lemma is a straightforward application of the definitions.
Lemma 3.7.
Let $d \in N$ , let $V$ be a vocabulary and let $S$ be a $V$ -structure. Let $L$ be a logical fragment.

Let $χ (x)$ be an $L [V]$ -formula, then $sub (χ (x), t, c) {(x)}^{S}$ equals $sub (χ {(x)}^{S}; t, c)$ .
Definition 3.8 (Fixed order).

Let $P_{d}$ be the set of permutations of $[d - 1]$ . For every permutation σ of $P_{d}$ , let $N_{σ}^{d}$ be the subset of $N^{d}$ where for each $i \in [d - 2]$ , the relation $x_{σ (i)} ⩽ x_{σ (i + 1)}$ holds. It is defined by the $Σ_{0} [<]$ -formula $⋀_{i = 0}^{d - 2} x_{σ (i)} ⩽ x_{σ (i + 1)}$ .

It should be noted that $N^{d}$ is the union of the $N_{σ}^{d}$ ’s. Therefore, for every vocabulary $V$ which contains <, for every logical fragment $L$ , a set $R \subseteq N^{d}$ is $L [V]$ -definable if and only if for each $σ \in P_{d}$ , the set R is $L [V]$ -definable in $N_{σ}^{d}$ .

3.3. $FO [+]$ -, $FO [<, mod]$ - and $FO [<, mod m]$ -definable sets

Some well-known facts about $FO [+]$ -, $FO [<, mod]$ - and $FO [<, mod m]$ -definable sets are now stated. The first lemma concerns unary sets which are $FO [+]$ or $FO [<, mod]$ -definable. Before giving this lemma, the following definition is needed.

Definition 3.9 (Ultimately (m-)periodic).

A set $R \subseteq N$ , is ultimately m-periodic if there exists an integer $τ \in N$ (which is called the threshold) such that for all $n ⩾ τ$ , $n \in R$ if and only if $n + m \in R$ . In particular the ultimately 1-periodic unary sets are the finite or co-finite sets. The set R is ultimately periodic if it is ultimately m-periodic for some $m \in N^{> 0}$ .

For R an ultimately periodic set of integers, let ${thres}_{m} (R) \in N$ denote the minimal integer such that for all $n ⩾ {thres}_{m} (R)$ , $n \in R$ is equivalent to $n + m \in R$ .

Let ${mod}_{m} (R) \subseteq [m - 1]$ denote the subset of $[m - 1]$ such that, for all $n ⩾ {thres}_{m} (R)$ , $n \in R$ if and only if $n \equiv p mod m$ for some $p \in {mod}_{m} (R)$ .

Intuitively, ${mod}_{m} (R)$ is the set of congruence classes modulo m which ultimately belong to R, and $[m - 1] ∖ {mod}_{m} (R)$ is the set of congruence classes modulo m which are ultimately disjoint from R.

Lemma 3.10 ([18]).

Let R be a subset of $N$ .

The set R is $FO [<, mod m]$ -definable if and only if it is ultimately m-periodic.

The set R is $FO [+]$ -definable if and only if it is ultimately periodic.

The set R is $FO [<, mod]$ -definable if and only if it is ultimately periodic.

The second lemma concerns unary functions over integers which are $FO [+]$ -definable or $FO [<, mod m]$ -definable.

Lemma 3.11 ([9]).

A unary function $f : N \to N$ is $FO [+]$ -definable if and only if there exist $m, τ \in N$ , $r_{0}, \dots, r_{m - 1} \in Q^{⩾ 0}$ and $s_{0}, \dots, s_{m - 1} \in Q$ such that $f (n) = r_{j} n + s_{j}$ for all $n ⩾ τ$ such that $n \equiv j mod m$ .

Furthermore, f is $FO [<, mod]$ -definable if and only if $r_{k} \in {0, 1}$ for every $k \in [m - 1]$ .

It should be noted that if f is a unary $FO [+]$ -definable function which is not $FO [<, mod]$ -definable, then one of the $r_{i}$ is different from 0 and 1.

In particular, several proofs of this paper involve $FO [+]$ -definable functions which are increasing. They are now characterized.

Lemma 3.12.
A unary increasing function $f : N \to N$ is $FO [+]$ -definable if and only if there exist $m \in N^{> 0}$ , $τ \in N$ , $r \in Q^{⩾ 0}$ and $s_{0}, \dots, s_{m - 1} \in Q$ such that $f (n) = r n + s_{j}$ for all $n ⩾ τ$ such that $n \equiv j mod m$ .

The value of r is called the slope of f.
Proof of Lemma 3.12.
By Lemma 3.11, there exist $m \in N^{> 0}$ , $τ \in N$ , $r_{0}, \dots, r_{m - 1} \in Q^{⩾ 0}$ and $s_{0}, \dots, s_{m - 1} \in Q$ such that $f (n) = r_{j} n + s_{j}$ for all $n ⩾ τ$ such that $n \equiv j mod m$ . It suffices to prove that $r_{i} = r_{j}$ for all $i, j \in [m - 1]$ .

For the sake of contradiction, let us assume that there exist $i, j \in [m - 1]$ such that $r_{i} > r_{j}$ . Without loss of generality, let us assume that $j > i$ . Since $j > i$ and f is increasing, $f (n + j) ⩾ f (n + i)$ .

Let $n \in N$ be such that $n \equiv 0 mod m$ and $n > max (\frac{r_{j} (j - i) + s_{j} - s_{i}}{r_{i} - r_{j}}, τ)$ . Then: $\begin{array}{l} n > \frac{r_{j} j - r_{i} i + s_{j} - s_{i}}{r_{i} - r_{j}} & ⟺ (r_{i} - r_{j}) n > r_{j} j - r_{i} i + s_{j} - s_{i}, \\ ⟺ r_{i} (n + i) + s_{i} > r_{j} (n + j - i) + s_{j}, \\ ⟺ f (n + i) > f (n + j) . \end{array}$ which is a contradiction. □

Some proofs of this paper consider increasing $FO [+]$ -definable functions whose slope is strictly greater than 1. It is now proven that such a function allows to define a function whose slope is as great as needed. Lemma 3.13.
Let f be a unary function symbol and let $S$ be a ${f, <}$ -structure such that $f^{S}$ is an increasing $FO [+]$ -definable function with slope $c > 1$ . Let $c^{'}, e \in N^{> 0}$ . There exists a converging $Σ_{1} [N, <, +_{N}, f]$ -formula $μ_{f^{S}} (x; y)$ which defines a function $g : N \to N$ in $S$ such that for all $n \in N$ , $g (n) ⩾ c^{'} n + e$ .
Proof.
The proof consists in two parts: defining a function $h : N \to N$ with slope at least $c^{'}$ , and then defining the function g.

By an easy induction on i, the ith iterate $f^{i}$ of f, is increasing, $FO [+]$ -definable, and its slope is $c^{i}$ . Let $k = max (1, ⌈ {log}_{c} (c^{'}) ⌉)$ . It suffices to set h equal to $f^{k}$ .

Let us assume that h is increasing, $FO [+]$ -definable, with slope at least c. Then there exists τ, m and $s_{0}, \dots, s_{m - 1}$ as in Lemma 3.11. Then it suffices to take $g (n)$ to be:
$c^{'} n + e$ for $n < τ$ , and

$h (n) + ⌈ e - min ({s_{i} ∣ i \in [d - 1]} \cup {e}) ⌉$ for $n ⩾ τ$
It should be noted that $min ({s_{i} ∣ i \in [d - 1]} \cup {e}) ⩽ e$ , hence $e - min ({s_{i} ∣ i \in [d - 1]} \cup {e}) ⩾ 0$ .

The formula $μ_{f^{S}} (x; y)$ is then: $\begin{matrix} y ≐ f^{k} (x) + e - min ({s_{i} ∣ i \in [d - 1]} \cup {e}) . \end{matrix}$ By Lemma 3.2, the set of converging functions is closed by composition, hence $f^{k}$ is converging. □

3.4. Quantifier elimination for $FO [<, mod]$ and $FO [<, mod m]$

Cooper’s algorithm [6] transforms a $FO [+]$ -formula into an equivalent $Σ_{0} [N, +, <, mod m]$ -formula for some $m \in N$ .

Let $M \subseteq N$ be closed under the least common multiple operation. In this paper, M is always equal, either to a singleton or to $N$ . Cooper’s algorithm is now given for the vocabulary ${N, <, +_{N}, mod M}$ . The algorithm Cooper:

takes as input a $FO [N, <, +_{N}, mod M]$ -formula $ϕ (x)$ and

returns a boolean combination of atomic formulas of the form $x_{i} + c \sim x_{j}$ , $x_{i} \sim c$ , and $x_{i} \equiv k mod m$ with ∼ belonging to ${<, ≐, >}$ , $c \in N$ , $m \in M$ and $k \in [m - 1]$ .

Definition 3.14 (Cooper).

Let $ϕ (x)$ be a $FO [N, <, +_{N}, mod M]$ -formula. Then, let $Cooper (ϕ) (x)$ be the $Σ_{0} [N, <, +_{N}, mod M]$ -formula defined by induction on ϕ as follows:

If $ϕ (x)$ is an atomic formula then $Cooper (ϕ) (x) = ϕ (x)$ .

If $ϕ (x)$ is of the form $\neg ψ (x)$ , then $Cooper (ϕ) (x) = \neg Cooper (ϕ) (x)$ .

If $ϕ (x)$ is of the form $ψ_{0} (x) \lor ψ_{1} (x)$ , then $Cooper (ϕ) (x) = Cooper (ψ_{0}) (x) \lor Cooper (ψ_{1}) (x)$ .

If $ϕ (x)$ is of the form $ψ_{0} (x) \land ψ_{1} (x)$ , then $Cooper (ϕ) (x) = Cooper (ψ_{0}) (x) \land Cooper (ψ_{1}) (x)$ .

If ϕ is of the form $\exists y . ψ (y, x)$ : let $ψ^{'} (y, x) = Cooper (ψ) (y, x)$ . By induction, $ψ^{'} (y, x)$ is a boolean combination of atomic formulas of the form:

$y < t_{i}$ or $y = t_{i}$ or $y > t_{i}$ , where $t_{i}$ is either a non-negative integer or a term of the form $x_{i} + c$ with $c \in Z$ , or

$y \equiv c_{i} mod m_{i}$ , where $m_{i}$ belongs to M and $c_{i} \in [m_{i} - 1]$ .

Let m be the least common multiple of the

m_{i}

, it belongs to M. Let

T (ψ^{'} (y, x))

be the set containing the integer 0 and the terms

t_{i}

. Then let

ψ^{″}

\begin{matrix} \underset{t_{i} \in T (ψ^{'} (y, x))}{⋁} \underset{j \in [m]}{⋁} ψ^{'} (t_{i} + j, x) . \end{matrix}

It should be noted that

t_{i} + j

is of the form

x_{i} + c + j

with

c \in Z

, hence

c + j

may be negative. In this case

ψ^{″} (x)

does not belong to

Σ_{0} [N, <, +_{N}, mod M]

. It remains to modify the formula to restrict additions to positive integers.

Let $Cooper (ϕ) (x)$ be the formula $ψ^{″} (x)$ where:

each atomic formula of the form $x_{i} + c \sim x_{i} + c^{'}$ , with ∼ being <, ≐ or >, is replaced by true if $c \sim c^{'}$ , and is replaced by false otherwise,

each atomic formula of the form $x_{i} + c \sim x_{j} + c^{'}$ with $i \neq j$ , $c ⩽ c^{'}$ and ∼ belonging to ${<, ≐, >}$ , is replaced by $x_{i} \sim x_{j} + (c^{'} - c)$ ,

each atomic formula of the form $x_{i} + c \sim c^{'}$ with $c ⩽ c^{'}$ and ∼ belonging to ${<, ≐, >}$ , is replaced by $x_{i} \sim (c^{'} - c)$ ,

each atomic formula of the form $x_{i} + c \sim c^{'}$ with $c > c^{'}$ and ∼ being <, ≐ or >, is replaced by the formula false, false and true respectively, and,

each atomic formula of the form $x_{i} + c \equiv c^{'} mod m$ is replaced by $x_{i} \equiv c^{'} - c mod m$ .

Finally, if $ϕ (x)$ is of the form $\forall y . ψ (y, x)$ , then $Cooper (ϕ) (x) = \neg Cooper (\exists y . \neg ψ) (y, x)$ .

Example 3.3.
Let ϕ be the formula $\exists x . (x ≐ y \land x ≐ 0) \lor (x + 4 ⩽ y \land x \equiv 0 mod 2)$ . Then $T (ϕ) = {y, y - 4, 0}$ and $m = 2$ . Then $ψ^{'}$ is equal to: $\begin{array}{l} ⋁_{i = 0}^{2} {(i ≐ y \land i ≐ 0) \lor (i + 4 ⩽ y \land i \equiv 0 mod 2)} \\ \lor ⋁_{i = - 4}^{- 2} {(y + i ≐ y \land y + i ≐ 0) \lor (y + i + 4 ⩽ y \land y + i \equiv 0 mod 2)} \\ \lor ⋁_{i = 0}^{2} {(y + i ≐ y \land y + i ≐ 0) \lor (y + i + 4 ⩽ y \land y + i \equiv 0 mod 2)}, \end{array}$ hence $Cooper (ϕ)$ is equal to $\begin{array}{l} ⋁_{i = 0}^{2} {(i ≐ y \land i ≐ 0) \lor (i + 4 ⩽ y \land i \equiv 0 mod 2)} \\ \lor ⋁_{i = - 3}^{- 2} {(false \land y ≐ - i) \lor (false \land y \equiv i mod 2)} \\ \lor {(false \land y ≐ 4) \lor (true \land y \equiv 0 mod 2)} \\ \lor ⋁_{i = 1}^{2} {(false \land false) \lor (false \land y \equiv i mod 2)} \\ \lor {(true \land y ≐ 0) \lor (false \land y \equiv 0 mod 2)} . \end{array}$

Let us prove that the algorithm Cooper behaves as expected.
Proposition 3.15.
Let $ϕ (x) \in FO [N, <, +_{N}, mod M]$ , then $Cooper (ϕ) (x)$ belongs to $Σ_{0} [N, <, +_{N}, mod M]$ .

For all $n \in N^{d}$ , let $N^{'} = N [x / n]$ . Then $N^{'} ⊧ ϕ (x)$ is equivalent to $N^{'} ⊧ Cooper (ϕ) (x)$ .

The proof of this proposition follows closely the proof of [6]. Proof of Proposition 3.15.
It is trivial to check by induction on $ϕ (x)$ that $Cooper (ϕ) (x)$ belongs to $Σ_{0} [N, <, +_{N}, mod M, x]$ . Let $n \in N^{d}$ and let $N^{'} = N [x / n]$ . Let us prove that $N^{'} ⊧ ϕ (x)$ is equivalent to $N^{'} ⊧ Cooper (ϕ) (x)$ . The proof goes by induction on ϕ. The only non-trivial case is when $ϕ (x)$ is of the form $\exists x . ψ (y, x)$ .

Let $ψ^{'} (y, x)$ , $T (ψ^{'})$ and m be as in Definition 3.14. By the induction hypothesis $ψ (y, x)$ is equivalent to $ψ^{'} (y, x)$ . Furthermore, $N^{'} ⊧ ψ^{″} (x)$ is easily equivalent to $N^{'} ⊧ Cooper (ϕ) (x)$ . Hence, it remains to prove that $N^{'} ⊧ \exists y . ψ^{'} (y, x)$ is equivalent to $N^{'} ⊧ ψ^{″} (x)$ .

Let us first assume that $N^{'} ⊧ ψ^{″} (x)$ , and let us prove that $N^{'} ⊧ \exists y . ψ^{'} (y, x)$ . Since $N^{'} ⊧ ψ^{″} (x)$ , there exists $t \in T (ψ^{'})$ and $j \in [m]$ such that $N^{'} ⊧ ψ^{'} (t_{i} + j, x)$ , hence $N^{'} [y / t_{i}^{' N^{'}} + j] ⊧ ψ^{'} (y, x)$ and then $N^{'} ⊧ \exists y . ψ^{'} (y, x)$ .

Let us now assume that $N^{'} ⊧ \exists y . ψ^{'} (y, x)$ , and let us prove that $N^{'} ⊧ ψ^{″} (x)$ . Let $n \in N$ be the least integer such that $N^{'} [y / n] ⊧ ψ^{'} (y, x)$ . Let us prove that n is of the form $t + j$ with $t \in T (ϕ^{'})$ and $j \in [m]$ , which implies that $N^{'} ⊧ ψ^{″} (x)$ . For the sake of contradiction, let us assume that n is not of the form $t + j$ with $t \in T (ϕ^{'})$ . Hence $n > m$ . Then, by an easy induction on the subterms ξ of $ϕ^{'}$ , $N^{'} [y / n] ⊧ ξ$ is equivalent to $N^{'} [y / n - m] ⊧ ξ$ , which contradicts the minimal hypothesis about n. □

4. Characterization of $FO [<, mod]$ - and of $FO [<, mod m]$ -definable sets

In this section, two characterizations of $FO [<, mod m]$ -definable sets and one characterization of $FO [<, mod]$ -definable sets are given.

In Section 4.1, a first characterization of $FO [<, mod m]$ -definable sets is given, in term of local properties and recursive properties. In Section 4.2, it is proven that, from a $FO [+]$ -definable set which is not $FO [<, mod]$ -definable, a unary functions which is not $FO [<, mod]$ -definable can be defined. Finally, in Section 4.3, it is proven that, from a set of tuples of integers which is not $FO [<, mod m]$ -definable, a set of integers which is not $FO [<, mod m]$ -definable can be defined.

4.1. Local and recursive characterization of $FO [<, mod m]$ -definable sets

In this section, a characterization of $FO [<, mod m] -definable$ -sets is given. Then some easy consequences of this characterization are given. This characterization is similar to Muchnik’s characterization of $FO [N, +]$ , which is first recalled. For this, two notions are first introduced.

The notion of cube is now introduced.

Definition 4.1.
Let $d \in N$ , $R \subseteq N^{d}$ , $x \in N^{d}$ and let $k \in N$ . Then let $C (x, k)$ denote the cube with size k and whose minimal element is $x$ . Formally, it is defined as: $\begin{matrix} C (x, k) = {x + c ∣ c \in {[k - 1]}^{d}} \end{matrix}$

The notion of P-periodicity for a set P of tuples is now introduced.
Definition 4.2 (p-periodicity in F).

Let $S, F \subseteq N^{d}$ , and $p \in N^{d}$ . Then S is $p$ -periodic in F if for all $x \in F$ such that $x + p \in F$ , $x \in S$ is equivalent to $x + p \in S$ .

For $m \in N$ , S is said to be m-periodic in F if it is $({\overline{m, \dots, m}}^{d})$ -periodic in F.

For $P \subseteq Z^{d}$ , a set of possible periodicities, the set S is said to be P-periodic in F if S is p-periodic for some $p \in P$ .

Muchnik’s theorem [2,16] which characterizes $FO [+]$ can now be stated.

Theorem 4.3 ([16, Theorem 1]).

Let $d \in N^{> 0}$ and $R \subseteq N^{d}$ . The following properties are equivalent;

The set R is $FO [+]$ -definable.

All sections of R are $FO [+]$ -definable and

there exists a finite set $P \subseteq Z^{d} ∖ {({\overline{0, \dots, 0}}^{d})}$ such that for every $k \in N$ , there exists $t \in N$ such that for all $x \in N^{d}$ with $‖ x ‖ > t$ , R is P-periodic in $C (x, k)$ .

Moreover the latter property only has to be verified for

k = \sum_{p \in P} ‖ p ‖

Intuitively the set P is the set of possible periods, k is the size of the cube and t is the “threshold” for the periodicity.

A similar theorem for $FO [<, mod m]$ -definable sets is now given.

Theorem 4.4.
Let $d \in N^{> 0}$ , $R \subseteq N^{d}$ , and $m \in N$ . The following three statements are equivalent:
The set R is $FO [<, mod m]$ -definable.

There exists $t \in N$ such that R is m-periodic in ${(N^{⩾ t})}^{d}$ and

if $d > 1$ , then all sections and diagonals of R are $FO [<, mod m]$ -definable.

For every straight subspace S of dimension $d^{'} ⩾ 1$ of R, there exists $t \in N$ such that S is $({\overline{m, \dots, m}}^{d^{'}})$ -periodic in ${(N^{⩾ t})}^{d^{'}}$ .

The notation ${thres}_{m} (R)$ is introduced in Definition 3.9 for $R \subseteq N$ . It is now generalized to any dimension $d \in N^{> 0}$ .
Definition 4.5.
Let $d \in N^{> 0}$ , $R \subseteq N^{d}$ , and $m \in N$ . If R satisfies Condition 2b of Theorem 4.4, let ${thres}_{m} (R)$ denote the least integer t which satisfies this condition.

An example of application of Theorem 4.4 is given first.
Example 4.1.
As seen in Example 3.2, all strict straight subspaces of + are $FO [<, mod]$ -definable sets. So + satisfies the criterion (2b) of Theorem 4.4. For each $l \in N$ , one has $(l, l, 2 l) \in +$ . For every $m \in N$ , the 3-tuple $(l + m, l + m, 2 l + m)$ does not belong to the relation +, so + does not satisfy the criterion (2a).

Let us consider another example. Let $R = {(0, n^{2}) ∣ n \in N}$ . The set R is 1-periodic in ${(N^{⩾ 1})}^{2}$ , so it satisfies the criterion (2a). But clearly $R^{x_{0} = 0} = {n^{2} ∣ n \in N}$ is not $FO [<, mod]$ -definable, so it does not satisfy the criterion (2b).

Theorem 4.4 is now proven.
Proof of Theorem 4.4.
Let us show by induction on $d \in N$ that properties (1), (2) and (3) are equivalent for every $R \subseteq N^{d}$ .

Let us first assume that $d = 1$ . Lemma 3.10 proves the equivalence of (1) and of (2). Since R is the only straight subspace of R of dimension at least 1, (3) and (2a) are equivalent. Moreover, (2b) holds since $d = 1$ . Hence (2) and (3) are equivalent.

Let us now assume that $d > 1$ and that the property holds for $d - 1$ . Proof of (1) $⟹$ (3).
Assume that R is $FO [<, mod m]$ -definable and let us prove that for every integer $d^{'} ⩽ d$ , and every straight subspace S of R of dimension $d^{'}$ , there exists ${thres}_{m} (S)$ such that S is $({\overline{m, \dots, m}}^{d^{'}})$ -periodic in ${(N^{⩾ {thres}_{m} (S)})}^{d^{'}}$ .

By Property 3.15, there exists a quantifier-free $Σ_{0} [N, <, +_{N}, mod M]$ -formula $χ (x)$ which defines R. Let S be a straight subspace of R, then by Lemma 3.7, there exists a $Σ_{0} [N, <, +_{N}, mod M]$ -formula $χ_{S} (x)$ which defines S. Let ${thres}_{m} (S) = max {c \in N ∣ x_{i} \sim c appears in χ_{S} (x), \sim being <, = or >} + 1$ .

Let us prove by induction on the subformulas $ξ (x)$ of $χ_{S} (x)$ that $ξ {(x)}^{N}$ is $({\overline{m, \dots, m}}^{d})$ -periodic in ${(N^{⩾ {thres}_{m} (S)})}^{d^{'}}$ . Let $n \in N^{d^{'}}$ with $min (n) > {thres}_{m} (S)$ , it must be proven that $ξ (n)$ is equivalent to $ξ (n + ({\overline{m, \dots, m}}^{d}))$ . The induction case is trivial. Let us consider the base case:
if $ξ (x)$ is of the form $x_{i} \equiv a mod m$ , then $n_{i} \equiv a mod m$ is equivalent to $n_{i} + m \equiv a mod m$ ,

if $ξ (x)$ is of the form $x_{i} - x_{j} \sim c$ for ∼ being < or ≐, then $n_{i} - n_{j} \sim c$ is equivalent to $(n_{i} + m) - (n_{j} + m) \sim c$ ,

if $ξ (x)$ is of the form $x_{i} < c$ or $x_{i} ≐ c$ , then by hypothesis $c < {thres}_{m} (S)$ , hence neither $ξ (n)$ nor $ξ (n + ({\overline{m, \dots, m}}^{d}))$ hold,

if $ξ (x)$ is of the form $x_{i} > c$ then by hypothesis $c < {thres}_{m} (S)$ , hence $ξ (n)$ and $ξ (n + ({\overline{m, \dots, m}}^{d}))$ hold.

Proof of (3) $⟹$ (2).
The set R is a straight subspace of R hence by hypothesis, there exists ${thres}_{m} (R) \in N$ such that R is $({\overline{m, \dots, m}}^{d})$ -periodic in ${(N^{⩾ {thres}_{m} (R)})}^{d}$ .
Proof of (2) $⟹$ (1).
Let R be such that all sections $sec (R; x_{i} = c)$ and diagonals $diag (R; x_{i} = x_{j} + c)$ are $FO [<, mod m]$ -definable. Then, for all distinct elements $i, j \in [d - 1]$ and for all $c \in N$ , let $ψ_{sec (R; x_{i} = j)} (x_{0}, \dots, x_{d - 2})$ and $ψ_{diag (R; x_{i} = x_{j} + c)} (x_{0}, \dots, x_{d - 2})$ be $FO [N, <, +_{N}, mod M]$ -formulas which define $sec (R; x_{i} = c)$ , and $diag (R; x_{i} = x_{j} + c)$ , respectively. Those formulas exist by hypothesis.

Figure 1 serves as example for the proof. It represents the set R defined by the formula $ϕ (x_{0}, x_{1})$ equal to $\begin{matrix} (1) & {(x_{0} + 2 ⩾ x_{1} \land x_{0} + 4 ≐̸ x_{1}) \lor x_{1} ≐ 1} \land x_{0} \equiv 1 mod 2 . \end{matrix}$ In this example, $m = 2$ and ${thres}_{m} (R) = 2$ .

Figure 1.
${(x_{0} + 2 ⩾ x_{1} \land x_{0} + 4 ≐̸ x_{1}) \lor x_{1} ≐ 1} \land x_{0} \equiv 1 mod 2$ .

A ⊆-decreasing sequence $F_{0}, F_{1}, F_{2, σ}, F_{3}, F_{4}$ of subsets of $N^{d}$ , with $F_{0} = N^{d}$ , is introduced. The proof consists in reducing the problem of defining R in $F_{i}$ to the problem of defining R in $F_{i + 1}$ . A formula $ϕ_{i} (x)$ is then given, such that $ϕ_{i} {(x)}^{N}$ defines R in $F_{i}$ . The formula $ϕ_{i}$ uses a formula which defines R in $F_{i + 1}$ , a formula which defines R in $F_{i} ∖ F_{i + 1}$ and the formula $ϕ_{i + 1}$ .

It is proven that $ϕ_{i} (n)$ defines R in $F_{i}$ .
The set $F_{0}$ .
Let $τ = {thres}_{m} (R)$ and let $F_{1} = {(N^{⩾ τ})}^{d}$ . The set $F_{1}$ is considered, because, by definition of τ, the set R is m-periodic in $F_{1}$ .

The formula $ϕ_{0}$ is constructed using a formula which defines R in $F_{0} ∖ F_{1}$ , a formula which defines R in $F_{1}$ and a formula which defines $F_{1}$ . It should be noted that $F_{0} ∖ F_{1}$ is included in a finite union of sections of R, and hypothesis (2a) can be used on each of those sections. Let us assume that $ϕ_{1} (x)$ defines R in $F_{1}$ . Then let $ϕ_{0}$ be: $\begin{matrix} ϕ_{0} (x) = ⟨ ⋁_{i = 0}^{d - 1} ⋁_{j = 0}^{l - 1} x_{i} ≐ j ∣ ψ_{sec (R; x_{i} = j)} (x_{0}, \dots, x_{i - 1}, x_{i + 1}, \dots, x_{d - 2}) ∣ ϕ_{1} (x) ⟩ . \end{matrix}$ In the example of Fig. 1, let $n_{0} = (9, 1)$ , $n_{1} = (11, 11)$ and $n_{2} = (11, 17)$ , then $n_{0} \notin F_{1}$ and $n_{1}, n_{2} \in F_{1}$ . The vertical and horizontal dotted line represent the boundary of $F_{1}$ .

Let us prove that $n \in R$ if and only if $N^{'} ⊧ ϕ_{0} (x)$ holds, where $N^{'} = N [x / n]$ . Let us first assume that $n \in R$ and let us prove that $N^{'} ⊧ ϕ_{0} (x)$ . Two cases must be considered, depending on whether $min (n) < τ$ or not.
Let us assume that $min (n) < τ$ , then there exist $i \in [d - 1]$ and $j \in [τ - 1]$ such that $n_{i} = j$ . Hence $N^{'} ⊧ x_{i} ≐ j$ . Let $n^{'}$ be $n$ without its ith component. By definition of section, $n \in R$ is equivalent to $n^{'} \in sec (R; x_{i} = j)$ , and by definition of $ψ_{sec (R; x_{i} = j)} (x)$ , it implies that $N^{'} ⊧ ψ_{sec (R; x_{i} = j)} (n^{'})$ . Hence $N^{'} ⊧ ϕ_{0} (x)$ .

Let us now assume that $min (n) ⩾ τ$ , then, $N^{'} ⊧ \neg (⋁_{i = 0}^{d - 1} ⋁_{j = 0}^{l - 1} x_{i} ≐ j)$ and by hypothesis about $ϕ_{1} (x)$ , $n \in R$ is equivalent to $N^{'} ⊧ ϕ_{1} (x)$ . Hence $N^{'} ⊧ ϕ_{0} (x)$ .
Finally, in both cases, $N^{'} ⊧ ϕ_{0} (x)$ .

Let us now assume that $N^{'} ⊧ ϕ_{0} (x)$ and let us prove that $n \in R$ . Again, two cases must be considered. Since $ϕ_{0}$ is a disjunction, one of the two subformulas holds over $N^{'}$ . Either $N^{'} ⊧ ⋁_{i = 0}^{d - 1} ⋁_{j = 0}^{l - 1} x_{i} ≐ j \land ψ_{sec (R; x_{i} = j)} (x_{0}, \dots, x_{i - 1}, x_{i + 1}, \dots, x_{d - 2})$ or $N^{'} ⊧ \neg (⋁_{i = 0}^{d - 1} ⋁_{j = 0}^{l - 1} x_{i} ≐ j) \land ϕ_{1} (x)$ . In the first case, there exists $i \in [d - 1]$ such that $n_{i} < τ$ and for $n^{'}$ defined as above, $n^{'}$ belongs to $sec (R; x_{i} = n_{i})$ , hence $n \in R$ . Otherwise, by hypothesis, $n \in R$ .
The set $F_{1}$ .
Let us now consider the set $F_{1}$ .

For all $σ \in P_{d}$ , let $F_{2, σ} = F_{1} \cap N_{σ}^{d}$ . The sets $F_{2, σ}$ are considered because, for each $n \in F_{2, σ}$ , $n_{σ (0)}$ is the smallest of the $n_{i}$ ’s. The set $R \cap F_{1}$ is equal to the union of the sets $R \cap F_{2, σ}$ for $σ \in P_{d}$ . Using this idea, the formula $ϕ_{1}$ is constructed as the disjunction of the $d!$ formulas which state that $x \in N_{σ}^{d}$ and that $ϕ_{2, σ} (x)$ holds (for each $σ \in P_{d}$ ).

Let us assume that $ϕ_{2, σ} (x)$ defines the set $R \cap N_{σ}^{d}$ in $F_{2, σ}$ , then let $ϕ_{1} (x)$ be: $\begin{matrix} \underset{σ \in P_{d}}{⋁} (⋀_{i = 0}^{d - 2} x_{σ (i)} ⩽ x_{σ (i + 1)}) \land ϕ_{2, σ} (x) . \end{matrix}$ In the example of Fig. 1, $n_{1}$ and $n_{2}$ belongs to $F_{2, (1, 0)}$ while $n_{0}$ belongs to $F_{2, (0, 1)}$ . The dashed diagonal line represents the boundary between those two sets.

Let us prove that $n \in R$ if and only if $N^{'} ⊧ ϕ_{0} (x)$ holds. Let us assume that $n \in R$ and let us prove that $N^{'} ⊧ ϕ_{0} (x)$ . Let σ be a permutation such that $n \in F_{2, σ}$ , then by hypothesis about $ϕ_{2, σ} (x)$ , $N^{'} ⊧ ϕ_{2, σ} (x)$ , and furthermore $N^{'} ⊧ ⋀_{i = 0}^{d - 2} x_{σ (i)} ⩽ x_{σ (i + 1)}$ , hence $N^{'} ⊧ ϕ_{0}$ .

Let us assume that $N^{'} ⊧ ϕ_{0} (x)$ and let us prove that $n \in F_{2, σ}$ . Let $σ \in P_{d}$ be such that $N^{'} ⊧ (⋀_{i = 0}^{d - 2} x_{σ (i)} ⩽ x_{σ (i + 1)} \land ϕ_{2, σ} (x))$ . Then $n \in N_{σ}^{d}$ , and by hypothesis about $ϕ_{2, σ} (x)$ , it implies that $n \in R$ .
The sets $F_{2, σ}$ .
For the sake of simplicity, let us consider the permutation $σ = (0, \dots, d - 1)$ and let $F_{2} = F_{2, (0, \dots, d - 1)}$ . For all $n \in F_{2}$ , for all $i \in [d - 2]$ , $n_{i} ⩽ n_{i + 1}$ .

It follows from hypothesis (2a) that, for all $p \in N$ , the section $sec (R; x_{0} = p)$ is $FO [<, mod m]$ -definable. By the induction hypothesis there exists $t_{p}^{'} = {thres}_{m} (sec (R; x_{0} = p)) \in N$ such that $sec (R; x_{0} = p)$ is m-periodic in ${(N^{⩾ t_{p}^{'}})}^{d - 1}$ . Let $t^{'} = max {t_{p}^{'} ∣ p \in [τ, τ + m - 1]}$ .

In the example of Fig. 1, ${thres}_{m} (sec (R; x_{0} = 2)) = 0$ and ${thres}_{m} (sec (R; x_{0} = 3)) = 8$ . Hence $t^{'} = 8$ . The line $x_{1} = 8$ is represented by the horizontal dashed line. It should be noted that the sections $sec (R; x_{0} = 2)$ and $sec (R; x_{0} = 3)$ are 2-periodic on the right side of this line.

Let $F_{3} = {x \in F_{2} ∣ x_{0} + t^{'} ⩽ x_{1}}$ . The set $F_{3}$ is considered for two reasons:
for $p \in [τ, τ + m - 1]$ , $sec (R; x_{0} = p)$ is m-periodic in $sec (F_{3}; x_{0} = p)$ , and

it is proven below that, for $p ⩾ τ + m$ , the study of sections $sec (R; x_{0} = p)$ can be reduced to the study of the m sections $sec (R; x_{0} = p^{'})$ for $p^{'} \in [τ, τ + m - 1]$ .

As for $F_{1}$ , the formula $ϕ_{2} (x)$ which defines R in $F_{2}$ is constructed, using the formula $ϕ_{3} (x)$ which defines R in $F_{3}$ , a formula which defines R in $F_{2} ∖ F_{3}$ , and a formula which defines $F_{3}$ in $F_{2}$ . By the induction hypothesis, for each $i \in N$ , there exists a formula $ψ_{diag (R; x_{1} = x_{0} + i)} (x_{0}, \dots, x_{d - 2})$ which defines the diagonal $diag (R; x_{1} = x_{0} + i)$ in $N^{d}$ , hence in $F_{2}$ . Let us assume that $ϕ_{3} (x)$ is a formula which defines R in $F_{3}$ . Then R is defined in $F_{2}$ by the formula $ϕ_{2} (x)$ : $\begin{matrix} ⟨ ⋁_{i = 0}^{t^{'} - 1} x_{0} + i ≐ x_{1} ∣ ψ_{diag (R; x_{1} = x_{0} + i)} (x_{0}, x_{2}, \dots, x_{d - 1}) ∣ ϕ_{3} (x) ⟩ . \end{matrix}$ In the example of Fig. 1, $n_{1}$ belongs to $F_{3}$ and $n_{2}$ does not belong to $F_{3}$ . The diagonal dashed line represents the boundary of $F_{3}$ .

The proof that $n \in R$ is equivalent to $N^{'} ⊧ ϕ_{3}$ is similar to the proof for $F_{1}$ , apart that diagonals are considered instead of sections.
The set $F_{3}$ .
Let us now consider the set $F_{3}$ . Note that $n_{0} + t^{'} ⩽ n_{1}$ for all $n \in F_{3}$ .

For all $n \in F_{3}$ , let $n_{0}^{″}$ the be least integer greater than τ equivalent to $n_{0}$ modulo m. Equivalently, $n_{0}^{″}$ is the only element of $[τ, τ + m - 1]$ equivalent to $n_{0}$ modulo m.

In the example of Fig. 1, the vertical dashed line represents $x_{0} = 4 = τ + m$ .

Then, let $n^{″} \in N^{d}$ be the d-tuple such that $n_{i}^{″} = n_{i}$ for each $i > 0$ .

For Fig. 1 when $n = n_{2}$ , then $n^{″}$ is equal to $(3, 17)$ , which is denoted as $n_{2}^{″}$ in the figure.

Let us claim that for all $n \in F_{3}$ , $n \in R$ is equivalent to $n^{″} \in R$ . In this case, R is defined in $F_{3}$ by the formula $ϕ_{3} (x)$ : $\begin{matrix} ⋁_{k = τ}^{τ + m - 1} x_{0} \equiv k mod m \land ψ_{sec (R; x_{0} = k)} (x_{1}, \dots, x_{d - 1}) . \end{matrix}$

It remains to prove that $n \in R$ is equivalent to $n^{″} \in R$ . Let $k = \frac{n_{0} - n_{0}^{″}}{m}$ and let $n^{'} \in N^{d} = n - k ({\overline{m, \dots, m}}^{d})$ . It suffices to prove that $n \in R$ is equivalent to $n^{'} \in R$ and that $n^{'} \in R$ is equivalent to $n^{″} \in R$ . For Fig. 1 with $n = n_{2}$ , the value $n^{'}$ is $n_{2}^{'}$ in the figure.

Let us first prove that $n \in R$ is equivalent to $n^{'} \in R$ . By induction on $i \in N$ , $n \in R$ is equivalent to $n - i ({\overline{m, \dots, m}}^{d}) \in R$ when $n_{0} - i m ⩾ τ$ . And since $n^{'} = n - k ({\overline{m, \dots, m}}^{d})$ and $n_{0}^{'} = n_{0}^{″} ⩾ τ$ by construction, $n \in R$ is equivalent to $n^{'} \in R$ .

Let us now prove that $n^{'} \in R$ is equivalent to $n^{″} \in R$ . Let $N^{'}$ and $N^{″}$ be $n^{'}$ and $n^{″}$ without their first component, respectively. Since $n_{0}^{'} = n_{0}^{″}$ , it suffices to prove that $N^{'} \in sec (R; x_{0} = n_{0}^{'})$ is equivalent to $N^{″} \in sec (R; x_{0} = n_{0}^{'})$ .

It should be noted that $n_{0} ⩾ 0$ and $n_{1} - n_{0} ⩾ t^{'}$ , hence $n_{1} ⩾ t^{'}$ . And by definition of $t^{'}$ , $sec (R; x_{0} = n_{0}^{'})$ is m-periodic in ${(N^{⩾ t^{'}})}^{d - 1}$ . Hence, by induction on $i \in N$ , $N^{'} \in sec (R; x_{0} = n_{0}^{'})$ is equivalent to $N^{'} + i ({\overline{m, \dots, m}}^{d - 1}) \in sec (R; x_{0} = n_{0}^{'})$ . In particular, $N^{″} = N^{'} + k ({\overline{m, \dots, m}}^{d - 1})$ , hence $N^{'} \in sec (R; x_{0} = n_{0}^{'})$ is equivalent to $N^{″} \in sec (R; x_{0} = n_{0}^{'})$ .
□

The above-mentioned Theorem 4.3 of [16] admits the following corollary.
Theorem 4.6 ([16, Theorem 2]).

There exists a $FO [+, R]$ -formula $μ_{d}$ such that $S ⊧ μ_{d}$ if and only if $R^{S}$ is $FO [+]$ -definable.

Since the characterization given in Theorem 4.4 is $FO [<]$ -expressible, Theorem 4.4 admits the following similar corollary.

Corollary 4.7.
Let $d, m \in N^{> 0}$ , and R be a relation symbol of arity d. There exists a $Π_{3} [<, +, R]$ -formula $μ_{d, m}$ which holds over ${R}$ -structures $S$ such that $R^{S}$ is $FO [<, mod m]$ -definable.
Proof.
The proof mostly uses the formula $sub (R, t, c)$ introduced in Notation 3.6. $\begin{matrix} \begin{matrix} μ_{d, m} & = \underset{t \in {({var, const} \cup {add (i) ∣ i \in [d - 1]})}^{d}}{⋀} \forall c . \exists N . \forall {(n_{i} > N)}_{t_{i} = var} sub (R, t, c) (n) \\ ⟺ sub (R, t, c) (n + ({\overline{m, \dots, m)}}^{dim (t)}) . \end{matrix} \end{matrix}$ □

The formula which defines the value of ${thres}_{m} (R)$ is now given.
Lemma 4.8.
Let $d \in N^{> 0}$ , let $m \in N$ . Let R be a relation symbol with arity d.

There exists a $Π_{1} [+_{m}, <, R]$ -formula $θ_{d, m} (x)$ such that if $R^{S}$ is $FO [<, mod m]$ -definable then:
$θ_{d, m} {(x)}^{S} = {{thres}_{m} (R^{S})}$ and

$θ_{d, m} {(x)}^{S_{| n}} = {{thres}_{m} (R^{S})}$ for all $n > {thres}_{m} (R^{S}) + m$ .

It should be noted that the interpretation of $θ_{d, m} {(x)}^{S_{| n}}$ for $n < {thres}_{m} (R^{S}) + m$ is undefined.
Proof of Lemma 4.8.
The $Π_{1} [<, +_{N}, R]$ -formula $θ_{d, m} (x)$ is the conjunction of two subformulas. The first one, $ϕ_{⩾} (x)$ states that the threshold is at most x. It is: $\begin{matrix} \forall n_{0}, \dots, n_{d - 1} (⋀_{i = 0}^{d - 1} n_{i} ⩾ x) ⟹ [R (n_{0}, \dots, n_{d - 1}) ⟺ R (n_{0} + m, \dots, n_{d - 1} + m)] . \end{matrix}$ The second formula, $ϕ_{> - 1} (x)$ , states that the threshold is strictly greater than $x - 1$ . That is, either $x = 0$ , or there exists $n \in N^{d}$ with $min (n) = x - 1$ and $n \in R$ is not equivalent to $n + ({\overline{m, \dots, m}}^{d}) \in R$ . It is: $\begin{matrix} x ≐ 0 \lor \exists y . (⋁_{i = 0}^{d - 1} y_{i} + 1 ≐ x \land ⋀_{i = 0}^{d - 1} y_{i} ⩾ x - 1 \land (R (y) ⟺ \neg R (y + ({\overline{m, \dots, m}}^{d})))) . \end{matrix}$ Then, let $θ_{d, m} (x)$ be $ϕ_{⩾} (x) \lor ϕ_{> - 1} (x)$ .

For any universe of cardinality greater than ${thres}_{d, m} (R^{S}) + m$ , the integer ${thres}_{d, m} (R^{S})$ is the only value which satisfies the formula. Hence $θ_{d, m} (x)$ converges. □

In the two following sections, proofs consider the evolution of thresholds of sections.
Definition 4.9.
Let $d \in N^{> 1}$ , and let $R \subseteq N^{d}$ . Then let $τ_{R, m} (n)$ be the function which maps $n \in N$ to the greatest threshold of section $sec (R; x_{0} = i)$ for $i ⩽ n$ . Formally: $\begin{matrix} τ_{R, m} (n) = max {{thres}_{m} (sec (R; x_{0} = r)) ∣ r ⩽ n} . \end{matrix}$
Lemma 4.10.
Let $d \in N^{> 1}$ , let R be a relation symbol with arity d and let $S$ be a ${<, +_{N}, R}$ -structure. There exists a $Π_{2} [<, +_{N}, R]$ -formula $τ_{d, m} (N; x)$ which defines the function $τ_{R^{S}, m}$ .

The naive method would be to universally quantify the value $n ⩽ N$ and use the formula ${thres}_{m} [R] (x_{1}, \dots, x_{d - 1})$ on the sections $sec (R; x_{0} = n)$ . But such a formula does not belong to $Π_{2} [<, +_{N}, R]$ .
Proof of Lemma 4.10.
The formula $τ_{R^{S}, m}$ is now constructed. It is similar to the formula of Lemma 4.8.

The formula $τ_{d, m} (N; x)$ is the conjunction of two formulas. The first formula $ϕ_{⩾} (N, x)$ , states that the threshold of every sections $sec (R; x_{0} = n)$ is less than x for all $n ⩽ N$ . Let $ϕ_{⩾} (N, x)$ be the $Π_{2} [<, +_{N}, R]$ -formula: $\begin{matrix} \forall n < N . (\forall z_{1} ⩾ x, \dots, z_{d - 1} ⩾ x .) ⟹ (R (n, z_{1}, \dots, z_{d - 1}) ⟺ R (z, z_{1} + m, \dots, z_{d - 1} + m)) . \end{matrix}$

The second formula, $ϕ_{> - 1} (N, x)$ , states that there exists some $n ⩽ N$ such that the threshold of the sections $sec (R; x_{0} = n)$ is strictly greater than $x - 1$ . It is possible either if $x = 0$ , or if there exists $n \in N^{d}$ with $n_{0} ⩽ N$ and $min {n_{1}, \dots, n_{d - 1}} = x - 1$ such that $n \in R$ is not equivalent to $n + (0, {\overline{m, \dots, m}}^{d - 1}) \in R$ . Let $ϕ_{> - 1} (N, x)$ be the $Π_{2} [<, +_{N}, R]$ -formula: $\begin{matrix} x ≐ 0 \lor \exists n . [n_{0} ⩽ N \land ⋁_{i = 1}^{d - 1} n_{i} ≐ x - 1 \land (R (n) ⟺ \neg R (n + ({\overline{m, \dots, m}}^{d})))] . \end{matrix}$

Then let $τ_{d, m} (N; x)$ be $ϕ_{⩾} (N, x) \land ϕ_{> - 1} (N, x)$ . □

Theorem 4.6 of [16] admits the following easy corollary:
Theorem 4.11 ([16, Theorem 3]).

Let M be a finite automaton whose input is a d-tuple of natural numbers written in positional system (all numbers have the same base and are aligned). One can decide whether the set recognized by M is definable in Presburger Arithmetic.

Similarly, Corollary 4.7 admits the following corollary:

Corollary 4.12.
Let M be a finite automaton as in Theorem 4.11 . It is decidable whether the set recognized by M is $FO [<, mod m]$ -definable (respectively, $FO [<, mod]$ -definable).

The proof follows closely the proof of [16, Theorem 3].
Proof of Corollary 4.12.
The addition and order relation are recognizable by finite automata. The family of recognizable sets is closed under logical operations. Therefore, it is possible to construct an automaton which encodes the formula $μ_{d, m}$ (respectively, $\exists m . μ_{d, m}$ ). It recognizes the empty set if $μ_{d, m}$ (respectively, $\exists m . μ_{d, m}$ ) does not hold, hence if the set recognized by M is not $FO [<, mod m]$ -definable (respectively, not $FO [<, mod]$ -definable). □

Corollary 4.7 admits another corollary, similar to Corollary 4.12, considering formulas as inputs instead of automata.
Corollary 4.13.
It is decidable whether a $FO [+]$ -formula $ϕ (x)$ defines a $FO [<, mod]$ -definable set (respectively, a $FO [<, mod m]$ -definable set).

Another algorithm to decide whether $ϕ (x)$ defines a $FO [<, mod]$ -definable set is given in [4, Theorem 10].
Proof of Corollary 4.13.
Since $FO [+]$ is decidable, by [18], it suffices to test whether the formula $\exists m . μ_{d, m}$ (respectively, $μ_{d, m}$ ), where $R (x)$ is replaced by $ϕ (x)$ , holds. □
4.2. Extracting a unary function from a non $FO [<, mod]$ -definable set

In this section, a characterization of $FO [<, mod]$ -definable sets is given. It is similar to the characterization [14, Theorem 5.1] of $FO [+]$ . This characterization is first recalled.

Theorem 4.14 ([14]).

Let $d \in N^{> 0}$ , R be a relation symbol with arity d and $S$ be a ${+, R}$ -structure such that $R^{S}$ is not $FO [+]$ -definable, then there is a $FO [+, R]$ -definable set of integers which is not $FO [+]$ -definable.

Theorem 4.14 does not directly extend to $FO [<, mod]$ . Indeed, the addition relation is not $FO [<, mod]$ -definable but Lemma 3.10 states that every $FO [<, +]$ -definable subset of $N$ is ultimately periodic, hence $FO [<, mod]$ -definable.

Hence, instead of considering sets of integers, the following theorem considers unary function.

Theorem 4.15.
Let $d \in N^{> 0}$ , R be a relation symbol with arity d. Let $S$ be a ${<, R}$ -structure with universe $N$ such that $R^{S}$ is $FO [+]$ -definable and not $FO [<, mod]$ -definable.

There exists a converging formula $ν_{R} (x; y)$ in $Π_{2} [<, +_{N}, R]$ such that $ν_{R} {(x; y)}^{S}$ is the graph of an increasing function with slope greater than 1.

This result can be restated as: the function f is of the form $n : \mapsto r n + g (n)$ with $r > 1$ and $g (n)$ bounded.

By Lemma 3.11, a function is $FO [<, mod]$ -definable if and only if its slope is 0 or 1. Hence the function of Theorem 4.15 is not $FO [<, mod]$ -definable. Hence, Theorem 4.15 implies that a $FO [+]$ -definable set R is $FO [<, mod]$ -definable if and only if every unary $FO [<, R]$ -definable function is $FO [<, mod]$ -definable.

Two lemmas must first be proved. The following lemma states that, when $FO [+]$ -definable sets are considered, one can consider only one periodicity for all straight subspaces of dimension 1.
Lemma 4.16.
Let $d \in N^{> 0}$ and $R \subseteq N^{d}$ be a $FO [+]$ -definable set. Then there exists $m \in N^{> 0}$ such that every straight subspace of R of dimension 1 is $FO [<, mod m]$ -definable.
Proof.
By Proposition 3.15, it can be assumed that R is defined by a quantifier-free formula $ϕ \in FO [+, <, mod]$ . Without loss of generality, it can be assumed that all modular relations are of the form $x_{i} \equiv a mod m$ with only one value m.

Let T be a straight subspace of R of dimension 1. By Lemma 3.5, there exists $t$ such that there is exactly one $i \in [d - 1]$ such that $t_{i} = var$ , and there exists $c \in N^{d}$ such that $T = sub (R; t, c)$ . Then T is defined by the formula $sub (R, t, c) (x)$ given in Notation 3.6.

Since x is the only variable, each occurrence of x in atomic formulas occurring in ψ is of the form $x \equiv k mod m$ or $q \times x > p$ or $q \times x ≐ p$ or $q \times x < p$ with $k \in [m - 1]$ , $q \in N^{> 0}$ , $p \in Z$ . Let $ϕ^{'} (x)$ be the formula obtained from $ϕ (x)$ by replacing the atomic formulas $q \times x > p$ (respectively, $q \times x < p$ , $q \times x ≐ p$ ) are rewritten as $x > ⌊ \frac{p}{q} ⌋$ (respectively, $x < ⌈ \frac{p}{q} ⌉$ , $x ≐ \frac{p}{q}$ if q divides p and false otherwise). The formula $ϕ^{'} (x)$ is equivalent to $ϕ (x)$ and belongs to $FO [<, mod m]$ . □

The following technical lemma states that, given some specific conditions about the evolution of thresholds of sections, it can be claimed that a set is $FO [<, mod m]$ -definable. This lemma is used both for Theorem 4.15 and for Theorem 4.18. Recall that the notation $N_{0, \dots, d - 1}^{d}$ , has been introduced in Definition 3.8.
Lemma 4.17.
Let $d ⩾ 2$ , $m \in N^{> 0}$ and $R \subseteq N_{0, \dots, d - 1}^{d}$ , be such that:
all of its sections and diagonals are $FO [<, mod m]$ -definable, and

the function $τ_{R, m}$ is $FO [+]$ -definable and its slope r is at most 1.
Then R is $FO [<, mod m]$ -definable.

It should be noted that if $τ_{R, m}$ is $FO [<, mod] -definable$ then its slope is 0 or 1. Hence this lemma implies that if $τ_{R, m}$ is $FO [<, mod] -definable$ then R is $FO [<, mod m]$ -definable.

Moreover the function $τ_{R, m}$ is increasing, hence the notion of slope is defined for $τ_{R, m}$ .
Proof of Lemma 4.17.
Since $τ_{R, m}$ is $FO [<, mod]$ -definable, it is $FO [<, mod m^{'}]$ -definable for some $m^{'} \in N$ . The Fig. 2 illustrates the proof, with the function $τ_{R, m}$ represented by unfilled circles.

In the example, $τ_{R, m} (0) = 0$ and $τ_{R, m} (n) = 3 ⌈ \frac{n}{3} ⌉$ for all positive n, thus $τ_{R, m}$ is $FO [<, mod 3]$ definable.
Figure 2.
Example for Lemma 4.17.

The diagonal line of Fig. 2 represents the boundary of $N_{0, 1}^{2}$ . By hypothesis, $R \subseteq N_{0, 1}^{2}$ , hence R belongs to the upper-left half of the figure.

By Lemma 3.11 there exists $θ \in N$ , a rational $r < 1$ and $s_{0}, \dots, s_{m - 1} \in Q$ such that for all $i ⩾ θ$ , $τ_{R, m} (I) = r i + s_{(i mod m^{'})}$ . Let $s = max {s_{i} ∣ i \in [m^{'} - 1]}$ .

For the example of Fig. 2, $r = 1$ , $s_{0} = 0$ , $s_{1} = 2$ and $s_{2} = 1$ and then $s = 2$ .

The $FO [<, mod m]$ -formula $ϕ_{R}$ which defines R is now constructed. The formula which defines $τ_{R, m}$ is not used in $ϕ_{R}$ .

The structure of the proof is similar to the part “(2) $⟹$ (1)” of the proof of Lemma 4.4. A ⊆-decreasing sequence $F_{0}, F_{1}, F_{2}$ of subsets of $N^{d}$ , with $F_{0} = N^{d}$ is introduced. The proof consists in proving that R is definable in $F_{i}$ by proving that it is definable in $F_{i + 1}$ and in $F_{i} ∖ F_{i + 1}$ . The set $F_{0}$ .
Let $F_{1} = {x \in F_{0} ∣ x_{0} + s ⩽ x_{1}}$ . The set $F_{1}$ is considered, because, by definition of θ, for all $i ⩾ θ$ each section $sec (R; x_{0} = i)$ is m-periodic in $sec (F_{1}; x_{0} = i)$ . On Fig. 2, the dashed diagonal represents the boundary of $F_{1}$ .

The set $R ∖ F_{1}$ is equal to $\begin{matrix} ⋃_{i = 0}^{s - 1} {(x_{0}, x_{0} + i, x_{1}, \dots, x_{d - 2}) ∣ (x_{0}, \dots, x_{d - 2}) \in diag (R; x_{1} = x_{0} + i)}, \end{matrix}$ and by hypothesis, each set $diag (R; x_{1} = x_{0} + i)$ is $FO [<, mod m]$ -definable, hence $R ∖ F_{1}$ is $FO [<, mod m]$ -definable. Since $F_{1}$ is also $FO [<, mod m]$ -definable it remains to prove that R is $FO [<, mod m]$ -definable in $F_{1}$ .
The set $F_{1}$ .
Let us now consider $F_{1}$ . Let $t^{'}$ be the maximal threshold of the diagonals $diag (R^{S}; x_{1} = x_{0} + i)$ for $i \in [s, s + m - 1]$ . Let $t^{″} = max {t^{'}, θ}$ . Then let $F_{2} = {x \in F_{1} ∣ x_{0} ⩾ t^{″}}$ . The set $F_{2}$ is considered for two reasons:
all diagonals $diag (R; x_{1} = x_{0} + i)$ are m-periodic for $i \in [s, s + m - 1]$ ,

it is proven below that, for $i ⩾ s$ , the study of diagonals $diag (R; x_{0} = x_{1} + s)$ can be reduced to the study of the m diagonals $diag (R; x_{0} = x_{1} + i^{'})$ for $i^{'} \in [s, s + m - 1]$ .

The dotted vertical line of Fig. 2 represents the boundary of $F_{2}$ .

The set R in $F_{1} ∖ F_{2}$ is the union of the sets $sec (R; x_{0} = i)$ for $i \in [t^{″} - 1]$ . By hypothesis, those sections are $FO [<, mod m]$ -definable hence R is also $FO [<, mod m]$ -definable in $F_{1} ∖ F_{2}$ . Furthermore $F_{2}$ is $FO [<, mod m]$ -definable, hence it remains to prove that R is $FO [<, mod m]$ -definable in $F_{2}$ .
The set $F_{2}$ .
Let us now consider the set $F_{2}$ . Let us prove that R is $FO [<, mod m]$ -definable in $F_{2}$ . By Theorem 4.4 it suffices to prove Property 2 of Theorem 4.4. Property 2b holds by hypothesis. Let us prove Property 2a with the threshold being $t^{″}$ . That is, let $n \in F_{2}$ and let $n^{‴} = n + ({\overline{m, \dots, m}}^{d})$ . It remains to prove that $n \in R$ is equivalent to $n^{‴} \in R$ .

In the example of Fig. 2, let $m = 2$ , $n = (3, 11)$ and $n^{‴} = (5, 12)$ .

The equivalence between $n \in R$ and $n^{‴} \in R$ follows from the following equivalences:
Let $k = ⌊ \frac{n_{1} - (n_{0} + s)}{m} ⌋$ and let $n^{'} = n - k (0, {\overline{m, \dots, m}}^{d - 1})$ , let us prove that $n \in R$ is equivalent to $n^{'} \in R$ .

For the example of Fig. 2, $k = 2$ and $n^{'} = (5, 8)$ .

Let $N$ and $N^{'}$ be $n$ and $n^{'}$ without their first component. It suffices to prove that $N \in sec (R; x_{0} = n_{0})$ is equivalent to $N^{'} \in sec (R; x_{0} = n_{0})$ . By definition of threshold, it suffices for this to prove that $N_{i}^{'} ⩾ {thres}_{m} (sec (R; x_{0} = n_{0}))$ for all $i \in [d - 2]$ . It is a consequence of the following inequalities:
${thres}_{m} (sec (R; x_{0} = n_{0})) ⩽ τ_{R, m} (n_{0})$ by definition of $τ_{R, m}$ ,

since $n \in F_{2}$ by definition of $F_{2}$ and of $t^{″}$ , $n_{0} ⩾ t^{″} ⩾ θ$ . By definition of θ, $τ_{R, m} (n_{0}) = r n_{0} + s_{(n_{0} mod m)}$ ,

since $r ⩽ 1$ , then $r n_{0} + s_{(n_{0} mod m)} = n_{0} + s_{(n_{0} mod m)}$ ,

since $s ⩾ s_{k}$ for all $k \in [m - 1]$ , then $s_{n_{0} mod m} ⩽ n_{0} + s$ ,

by definition of k, $n_{0} + s = n_{1} - (n_{1} - (n_{0} + s)) ⩽ n_{1} - ⌊ \frac{n_{1} - (n_{0} + s)}{m} ⌋ m = n_{1} - k m = n_{1}^{'} = N_{0}^{'}$ and

for all $i \in [d - 3]$ , let us prove that $N_{i}^{'} ⩽ N_{i + 1}^{'}$ :
$N_{i}^{'} = n_{i + 1}^{'}$ by definition of $N^{'}$ ,

$n_{i + 1}^{'} = n_{i + 1} - k m$ by definition of $n^{'}$

$n_{i + 1} - k m ⩽ n_{i + 2} - k m$ since $n \in N_{(0, \dots, d - 1)}^{d}$

$n_{i + 2} - k m = n_{i + 2}^{'}$ by definition of $n^{'}$ ,

$n_{i + 2}^{'} = N_{i + 1}^{'}$ by definition of $N^{'}$ .
Thus $N_{i}^{'} = n_{i + 1}^{'} = n_{i} - k m ⩽ n_{i + 2} - k m = n_{i + 2}^{'} = N_{i + 1}^{'}$ .
Thus, for all $i \in [d - 2]$ , one has: $\begin{matrix} {thres}_{m} (sec (R; x_{0} = n_{0})) ⩽ τ_{R, m} (n_{0}) = r n_{0} + s_{n_{0} mod m} = n_{0} + s_{(n_{0} mod m)} ⩽ n_{0} + s ⩽ N_{0}^{'} ⩽ \dots ⩽ N_{i}^{'} . \end{matrix}$

Let $n^{″} = n^{'} + ({\overline{m, \dots, m}}^{d})$ and let $k^{'} = n_{1}^{'} - n_{0}^{'}$ .

For the example of Fig. 2, $n^{″} = (7, 10)$ and $k^{'} = 3$ . Let us prove that $n^{'} \in R$ if and only if $n^{″} \in R$ . Let $N^{″}$ be $n^{″}$ without its first component. It suffices to prove that $N^{'} \in diag (R; x_{1} = x_{0} + k^{'})$ is equivalent to $N^{″} \in diag (R; x_{1} = x_{0} + k^{'})$ . By definition of threshold, it suffices to prove that for all $i \in [d - 2]$ , $N_{i}^{'} ⩾ {thres}_{m} (diag (R; x_{1} = x_{0} + k^{'}))$ . It follows from the following inequalities:
Let us claim that $k^{'} \in [s, s + m - 1]$ , then ${thres}_{m} (diag (R; x_{1} = x_{0} + k^{'})) ⩽ θ$ by definition of $t^{'}$ ,

by definition of $t^{″}$ , $t^{'} ⩽ t^{″}$ ,

$t^{″} ⩽ n_{0}$ since $n \in F_{2}$ , by definition of $F_{2}$ ,

$n_{0} = n_{0}^{'}$ by definition of $n^{'}$ ,

$n_{0}^{'} < n_{1}^{'} = N_{0}^{'}$ as proven in the previous case,

for all $i \in [d - 2]$ , $N_{i}^{'} ⩽ N_{i + 1}^{'}$ as proven in the previous case.
Thus, for all $i \in [d - 2]$ , one has: $\begin{matrix} {thres}_{m} (diag (R; x_{1} = x_{0} + k^{'})) ⩽ θ ⩽ t^{″} ⩽ n_{0} = n_{0}^{'} < n_{1}^{'} = N_{0}^{'} ⩽ \dots ⩽ N_{i + 1}^{'} . \end{matrix}$

It remains to prove that $k^{'} \in [s, s + m - 1]$ . It follows from the following statements:

$\frac{n_{1} - (n_{0} + s)}{m} - 1 < ⌊ \frac{n_{1} - (n_{0} + s)}{m} ⌋ ⩽ \frac{n_{1} - (n_{0} + s)}{m}$ ,

$\frac{n_{1} - (n_{0} + s)}{m} - 1 < k ⩽ \frac{n_{1} - (n_{0} + s)}{m}$ , by definition of k,

$n_{1} - (n_{0} + s) - m < k m ⩽ n_{1} - (n_{0} + s)$ ,

$- n_{1} + n_{0} + s ⩽ - k m < - n_{1} + n_{0} + s + m$ , by multiplying by $- 1$ ,

$n_{0} + s ⩽ n_{1} - m k < n_{0} + s + m$ , by adding $n_{1}$ ,

$n_{0}^{'} + s ⩽ n_{1}^{'} < n_{0}^{'} + s + m$ , by definition of $n^{'}$ ,

$s ⩽ n_{1}^{'} - n_{0}^{'} < s + m$ .

Finally, the proof that $n^{″} \in R$ if and only if $n^{‴} \in R$ is the same as the proof of equivalence of $n \in R$ and $n^{'} \in R$ . □

Theorem 4.15 can now be proven.
Proof of Theorem 4.15.
The proof goes by induction on d. In the case of $d = 1$ , there is no $FO [+]$ -definable set which is not $FO [<, mod]$ -definable, hence the theorem trivially holds. Let us now assume that $d > 1$ and that it holds for $d - 1$ .

By Lemma 4.16, there exists $m \in N^{> 0}$ such that every straight subspace of dimension 1 of R is $FO [<, mod m]$ -definable.

Two cases must be considered, depending on whether all sections of R are $FO [<, mod m]$ -definable or not. Let us first assume that there is a section $S = sec (R; x_{i} = c)$ for $i \in [d - 1]$ and $c \in N$ such that S is not $FO [<, mod m]$ -definable. Then by the induction hypothesis, there exists a $Π_{2} [<, +_{N}, S]$ -formula $ν_{S} (x; y)$ which defines a non $FO [<, mod m]$ -definable unary function in $N [S / sec (R^{S}; x_{i} = c)]$ . Then let $ν_{m, R} (x)$ be the $Π_{2} [<, +_{N}, R]$ -formula $ν_{S} (x; y)$ where $S (x_{0}, \dots, x_{i - 1}, x_{i + 1}, \dots, x_{d - 1})$ is replaced by $R (x_{0}, \dots, x_{i - 1}, c, x_{i + 1}, \dots, x_{d - 1})$ .

Let us now assume that all sections are $FO [<, mod m]$ -definable. Similarly to the last case, two cases must be considered, depending on whether all diagonals of R are $FO [<, mod m]$ -definable or not. If some diagonal is not $FO [<, mod m]$ -definable, the proof is similar to the case where a section is not $FO [<, mod m]$ -definable.

Let us now assume that all sections and diagonals of $R^{S}$ are $FO [<, mod m]$ -definable. Then there exists a permutation $σ \in P_{d}$ such that $R^{S} \cap N_{σ}^{d}$ is not $FO [<, mod m]$ -definable. For the sake of simplicity, let us assume that $σ = (0, \dots, d - 1)$ and let $R^{'} = R^{S} \cap N_{σ}^{d}$ .

By Lemma 4.8, the function $τ_{R^{'}, m}$ is defined by a $Π_{2} [R^{'}, <, +_{N}]$ -formula $τ_{d, m} (N; x)$ which converges. To define $ν_{R} (x; y)$ , it suffices to replace in $τ_{d, m} (N; x)$ the predicate $R^{'} (x)$ by $R (x) \land ⋀_{i = 0}^{d - 2} x_{i} < x_{i + 1}$ .

Since R is $FO [+]$ -definable $τ_{R^{'}, m}$ is $FO [+]$ -definable. Furthermore $τ_{R^{'}, m}$ is increasing. Let r be its slope. The set $R^{'}$ is not $FO [<, mod]$ -definable, thus $r > 1$ by Lemma 4.17. Hence $ν_{R} (x; y)$ satisfies the conditions of the theorem. □

In the above theorem, R must be $FO [+]$ -definable because the proof of the theorem requires that there exists a positive integer m such that all straight subspaces of dimension 1 are $FO [<, mod m]$ -definable. To the best of our knowledge, it is an open question to know whether a function f which is not $FO [<, mod]$ -definable can be created for any R which is not $FO [+]$ -definable.
4.3. Extracting a unary set from a non $FO [<, mod m]$ -definable set

In this section, a theorem similar to Theorem 4.14 is proved, for the logic $FO [<, mod m]$ .

Theorem 4.18.
Let $d, m \in N^{> 0}$ , and R be a relation symbol with arity d. Let $S$ be a ${<, R}$ -structure with universe $N$ such that $R^{S}$ is not $FO [<, mod m]$ -definable.

There exists a $FO [<, R]$ -formula $ν_{m, R} (x)$ such that $ν_{m, R} {(x)}^{S}$ is not ultimately m-periodic.

In other words, a set R is $FO [<, mod m]$ -definable if and only if every unary $FO [<, R]$ -definable set is ultimately m-periodic.

The following proposition, which considers the simpler case of an increasing function, must be proved first.
Proposition 4.19.
Let $m \in N^{> 0}$ . Let f be a unary function symbol. Let $S$ be a ${<, f}$ -structure with universe $N$ such that $f^{S}$ is increasing, unbounded and not $FO [<, mod m]$ -definable. Then there exists a $FO [<, f]$ -formula $ν_{m, f} (x)$ such that $ν_{m, f} {(x)}^{S}$ is not ultimately m-periodic.

To prove this proposition, the two following lemmas must first be proved. The first lemma is similar to Proposition 4.19. The only difference is that $mod m$ also belongs to the vocabulary. The second lemma lets us encode the modular predicate using only the increasing function f and the order relation.
Lemma 4.20.
Let $m \in N^{> 0}$ . Let f be a unary function symbol. Let $S$ be a ${<, f}$ -structure with universe $N$ such that $f^{S}$ is increasing, unbounded and not $FO [<, mod m]$ -definable. Then there exists a $FO [<, mod m, f]$ -formula $ν_{m, f}^{'} (x)$ such that $ν_{m, f}^{'} {(x)}^{S}$ is not ultimately m-periodic.

The proof of Lemma 4.20 consists in a disjunction between three cases. Let us first give an example of three applications of this lemma, considering each of the three cases.
Example 4.2.
Let $m = 2$ . Some ${<, f}$ -structures $S$ are given, such that $f^{S}$ is not ultimately m-periodic. Then, for each structure, a $FO [<, f]$ -formula ϕ is given such that $ϕ^{S}$ is not ultimately 2-periodic.
Let $f^{S} (n) = 4 n$ . In this case, it suffices to consider the image of f. Let $ϕ (x)$ be $\exists y . f (y) ≐ x$ , then $ϕ {(x)}^{S} = 4 N$ , which is not ultimately 2-periodic.

Let $f^{S} (n) = ⌊ \frac{n}{2} ⌋$ . Its image is $N$ which is ultimately 2-periodic. In this case, it suffices to consider the pre-image of an equivalence class. Let $ϕ (x)$ be $f (x) \equiv 0 mod 2$ , then $ϕ {(x)}^{S} = 4 N \cup (4 N + 1)$ , which is not ultimately 2-periodic.

Let $f^{S} (n) = 2 ⌊ \frac{n}{4} ⌋$ . Its image is $2 N$ , the pre-image of $2 N$ and of $2 N + 1$ are $N$ and ∅, which are ultimately 2-periodic. In this case, it suffices to consider the part of $N$ where f does not increase. Let $ϕ (x)$ be $f (x) ≐ f (x + 2)$ , then $ϕ {(x)}^{S} = 4 N \cup (4 N + 1)$ , which is not ultimately 2-periodic.

Lemma 4.20 is now proved.
Proof of Lemma 4.20.
Since $f^{S}$ is not $FO [<, mod m]$ -definable, according to Lemma 3.11 there exists $k \in [m - 1]$ such that there are no $N, r \in N$ such that $f (n) = n + r$ for every $n > N$ and $n \equiv k mod m$ . From now on, let us consider $f_{∣ m N + k} : m N + k \to N$ , the restriction of $f^{S}$ on the set $m N + k$ , and its image $Im (f_{∣ m N + k})$ .

Two cases must be considered, depending on whether $Im (f_{∣ m N + k})$ is ultimately m-periodic or not. Let us first assume that $Im (f_{∣ m N + k})$ is not ultimately m-periodic. Then, let $ν_{m, f}^{'} (x)$ be $\begin{matrix} \exists y \equiv k mod m . f (y) ≐ x . \end{matrix}$

Let us now assume that the image $Im (f_{∣ m N + k})$ of $f_{∣ m N + k}$ is ultimately m-periodic. Since f is unbounded and increasing, then $Im (f_{∣ m N + k})$ is infinite. Hence, there exists $τ = {thres}_{m} (Im (f_{∣ m N + k})) \in N$ and $P = {mod}_{m} (Im (f_{∣ m N + k})) \subseteq [m - 1]$ as in Definition 3.9. That is, for all $n ⩾ τ$ , $n \in Im (f_{∣ m N + k})$ if and only if $n \equiv p mod m$ for some $p \in N$ . Since $Im (f_{∣ m N + k})$ is infinite, then P is non-empty.

Two cases must be considered depending on whether $# P = 1$ or $# P ⩾ 2$ . Let us first assume that P contains two distinct elements q and $q^{'}$ . Then the inverse of $m N + q$ (respectively of $m N + q^{'}$ ) by $f_{∣ m N + k}$ contains an infinite number of elements. It implies that the inverse of $m N + q^{'}$ by $f_{∣ m N + k}$ is infinite, and its complement in $m N + k$ is also infinite. Hence the inverse of $m N + q^{'}$ by $f_{∣ m N + k}$ is not ultimately m-periodic. Then, let $ν_{m, f}^{'} (x)$ be: $\begin{matrix} f (x) \equiv q mod m . \end{matrix}$

Let us now assume that P is the singleton ${p}$ . Let us claim that the set $\begin{matrix} E = {n \equiv k mod m ∣ f_{∣ m N + k} (n) = f_{∣ m N + k} (n + m)} \end{matrix}$ is not ultimately m-periodic. In this case, let $ν_{m, f}^{'} (x)$ be: $\begin{matrix} f (x) ≐ f (x + m) . \end{matrix}$

Let us now prove that E is not ultimately m-periodic. It suffices to prove that E is infinite and $(m N + k) ∖ E$ is infinite.

Let us first prove that $(m N + k) ∖ E$ is infinite. Let $N \equiv k mod m$ and let us prove that there exists $n > N$ such that $n \notin E$ , that is, such that $f (n) \neq f (n + m)$ . Since $f_{∣ m N + k}$ is unbounded, there exists $n^{'} \equiv k mod m$ such that $f (n^{'}) > f (N + m)$ , and since f is increasing, $n^{'} > N + m$ . Let us assume that $n^{'}$ is chosen minimal. Let us prove that $n = n^{'} - m$ is such that $f (n) \neq f (n + m)$ .

By the minimality of $n^{'}$ , $f (n^{'} - m) ⩽ f (N + m)$ . Finally, $f (n) = f (n^{'} - m) ⩽ f (N + m) < f (n^{'}) = f (n + m)$ .

Let us now prove that E is infinite. Let $N > max (τ, 2 m)$ be such that $N \equiv k mod m$ and let us prove that there exists $n ⩾ N$ belonging to E. Let $r = f_{∣ m N + k} (N - m) - (N - m)$ . Let n be the minimal integer such that $n ⩾ N + m$ , $n \equiv k mod m$ and $f_{∣ m N + k} (n) \neq n + r$ , by hypothesis about k it exists. Let us prove that $n - m \in E$ , note that $n - m ⩾ N$ . By definition of E, it suffices to prove that $f_{∣ m N + k} (n) = f_{∣ m N + k} (n - m)$ . Since n is minimal, either $n = N + m$ or $f_{∣ m N + k} (n - m) = n - m + r$ . Note that $f (N - m) = N - m + r$ hence $n \neq N - m$ . The two preceding statements implies that $f_{∣ m N + k} (n - m) = n - m + r$ .

For the sake of contradiction, let us now assume that $f_{∣ m N + k} (n) \neq f_{∣ m N + k} (n - m)$ . Let us claim that $f_{∣ m N + k} (n) ⩾ n + r + m$ . Since $n + r \equiv p mod m$ and $n + r ⩾ τ$ , by definition of τ, there exists $s \in m N + k$ such that $f_{∣ m N + k} (s) = n + r$ . Since $n + r - m < n + r < n + r + m ⩽ f_{∣ m N + k} (n)$ , $n + r - m = f_{∣ m N + k} (n - m)$ , $n + r = f_{∣ m N + k} (s)$ and $f_{∣ m N + k}$ is increasing, $n - m < s < n$ . Since $s \equiv p$ and $p \equiv n mod m$ then $s \equiv n mod m$ . Having both $s \equiv n mod m$ and $n - m < s < n$ is a contradiction.

Let us now prove that $f_{∣ m N + k} (n) ⩾ n + r + m$ . It follows from the following (in)equalities:
Since $f_{∣ m N + k}$ is increasing, $f_{∣ m N + k} (n) ⩾ f_{∣ m N + k} (n - m)$ .

Since $f_{∣ m N + k} (n) \neq f_{∣ m N + k} (n - m)$ , $f_{∣ m N + k} (n) > f_{∣ m N + k} (n - m)$ .

By minimality of n, $f_{∣ m N + k} (n - m) = n - m + r$ , hence $f_{∣ m N + k} (n) > f_{∣ m N + k} (n - m) = n - m + r$ .

Since $n ⩾ τ$ , $f_{∣ m N + k} (n) \equiv p mod m$ . Let us claim that $n + r \equiv p mod m$ then $f_{∣ m N + k} (n) ⩾ n + r$ . Let us now prove that $n + r \equiv p mod m$ . Since $n - m > τ$ , $n + r \equiv n + r - m = f_{∣ m N + k} (n - m) \equiv p mod m$ .

By $f_{∣ m N + k} (n) ⩾ n + r$ and by definition of n, $f_{∣ m N + k} (n) \neq n + r$ , hence $f_{∣ m N + k} (n) > n + r$ .

Having $f_{∣ m N + k} (n) \equiv p mod m$ , $n + r \equiv p mod m$ and $f_{∣ m N + k} (n) > n + r$ imply $f_{∣ m N + k} (n) ⩾ n + r + m$ . □

The following lemma states how to define a modular relation using an ultimately periodic set of integers.
Lemma 4.21.
Let R be a monadic relation symbol. Let $S$ be an ${<, R}$ -structure such that $R^{S}$ is ultimately periodic. Let $m \in N^{> 0}$ be the least period of $R^{S}$ . Then $m N$ is $FO [<, R]$ -definable in $S$ .
Proof.
Since $R^{S}$ is ultimately m-periodic, there exist $τ \in N$ and ${mod}_{m} (R^{S}) \subseteq [m - 1]$ as in Definition 3.9. That is, for all $n ⩾ τ$ , $n \in Im (f_{∣ m N + k})$ if and only if $n \equiv p mod m$ for some $p \in {mod}_{m} (R^{S})$ .

Let us assume that $ϕ_{⩾ τ} (x)$ defines $m N$ in $N^{⩾ τ}$ . Then $m N$ is defined by $\begin{matrix} ϕ (x) = ⟨ i < τ ∣ ⋁_{i = 0}^{\frac{τ}{m}} x = i m ∣ ϕ_{⩾ τ} (x) ⟩ . \end{matrix}$

Let us now define $ϕ_{⩾ τ} (x)$ which defines $m N$ in $N^{⩾ τ}$ . Let us assume that for all $n \equiv 0 mod m$ for all $n ⩾ τ$ if and only if $n + p \in R^{S}$ for all $p \in {mod}_{m} (R^{S})$ , and $n + p \notin R^{S}$ for all $p \in [m - 1] ∖ {mod}_{m} (R^{S})$ . Then let $ϕ_{⩾ τ} (x)$ be: $\begin{matrix} \underset{p \in {mod}_{m} (R^{S})}{⋀} R (x + p) \land \underset{p \in [m - 1] ∖ {mod}_{m} (R^{S})}{⋀} \neg R (x + p) . \end{matrix}$

Let us prove that for all $n ⩾ τ$ , the two following statements are equivalent:
$n \equiv 0 mod m$ and

for all $p \in {mod}_{m} (R^{S})$ , $n + p \in R^{S}$ and for all $p \in [m - 1] ∖ {mod}_{m} (R^{S})$ , $n + p \notin R^{S}$ .
The fact that (1) implies (2) follows directly from the definition of τ and ${mod}_{m} (R^{S})$ . Let us prove that (2) implies (1).

For the sake of contradiction, let us assume that there exists $k \in [m - 1] ∖ {0}$ such that $n \equiv k mod m$ . It implies that for all $p \in [m - 1]$ , $p \in {mod}_{m} (R^{S})$ is equivalent to $p + k \in {mod}_{m} (R^{S})$ if $p + k < m$ , and to $p + k - m \in {mod}_{m} (R^{S})$ otherwise.

Let us prove that $R^{S}$ is ultimately k-periodic, which contradicts the minimal hypothesis about m. It suffices to prove that for all $n ⩾ τ$ , $n \in R^{S}$ if and only if $n + k \in R^{S}$ .

Let $n ⩾ τ$ . The following statements are equivalent:
$n \in R^{S}$ ,

by definition of ${mod}_{m} (R^{S})$ : $n mod m \in {mod}_{m} (R^{S})$ ,

by hypothesis about k: $n + k mod m \in {mod}_{m} (R^{S})$ ,

by definition of ${mod}_{m} (R^{S})$ : $n + k \in R^{S}$ . □

Proposition 4.19 is now proved.
Proof of Proposition 4.19.
The proof consists in exhibiting a $FO [<, f]$ -formula which defines a set which is not ultimately m-periodic.

Let $m_{f} \in N^{> 0}$ be the greatest integer which divides m and is such that $m_{f} N$ is $FO [<, f]$ -definable in $S$ . Note that 1 divides m and $1 N$ is $FO [<, f]$ -definable in $S$ , hence $m_{f}$ is correctly defined. Let $ϕ_{m_{f}}$ be the $FO [<, f]$ -formula which defines $m_{f} N$ in $S$ .

Since f is not $FO [<, mod m]$ -definable and $m_{f}$ divides m, f is not $FO [<, mod m_{f}]$ -definable. By Lemma 4.20 there exists a $FO [<, f, mod m_{f}]$ -formula $ξ_{E}^{'}$ which defines a set $E \subseteq N$ which is not ultimately $m_{f}$ -periodic. Let $ξ_{E}$ be the $FO [<, f]$ -formula $ξ_{E}^{'}$ where each occurrence of $x \equiv a mod m_{f}$ is replaced by $ϕ_{m_{f}} (x - a + m_{f})$ , it also defines E.

Let $m_{E}$ be the least integer such that E is ultimately $m_{E}$ -periodic. By Lemma 4.21, there exists a $FO [<, E]$ -formula $ψ_{m_{E}}$ which defines $m_{E} N$ in $S$ . Let $ϕ_{m_{E}}$ be the $FO [<, f]$ -formula $ψ_{m_{E}}$ where $E (x)$ is replaced by $ξ_{E}$ ; it defines $m_{E} N$ in $S$ . Note that E is ultimately n-periodic if and only if $m_{E}$ divides n, for all $n \in N^{> 0}$ . Two cases must be considered, depending on whether $m_{E}$ divides m or not. If $m_{E}$ does not divide m, then E is not ultimately m-periodic, hence the result is proved. Let us now assume that $m_{E}$ divides m. Since E is not ultimately $m_{f}$ -periodic, $m_{E}$ does not divide $m_{f}$ .

Let $m_{lcm} = lcm (m_{f}, m_{E})$ . Since $m_{E}$ does not divide $m_{f}$ , $m_{lcm} > m_{f}$ . Since $m_{f}$ and $m_{E}$ divides m, $m_{lcm}$ divides m. The set $m_{lcm} N$ is $FO [<, f]$ -defined by $ϕ_{m_{f}} \land ϕ_{m_{E}}$ . Since $m_{lcm} N$ is $FO [<, f]$ -definable and $m_{lcm}$ divides m, by maximality hypothesis about $m_{f}$ , $m_{lcm} ⩽ m_{f}$ . Having $m_{lcm} > m_{f} ⩾ m_{lcm}$ is a contradiction. □

Let us now prove Theorem 4.18.
Proof of Theorem 4.18.
The proof is by induction on d. If $d = 1$ then let $ν_{m, R^{S}} (x)$ be the formula $R (x)$ . It is now assumed that $d > 1$ and that the theorem holds for $d - 1$ .

Two cases must be considered, depending on whether there exists a section E of $R^{S}$ which is $FO [<, mod m]$ -definable or not. Let us first assume that there is a section $E = sec (R^{S}; x_{i} = c)$ for $i \in [d - 1]$ and $c \in N$ such that E is not $FO [<, mod m]$ -definable. Then by the induction hypothesis, there exists a formula $ν_{m, S} (x)$ such that $ν_{m, S} (x)$ defines E in $S$ . Then let $ν_{m, R^{S}} (x)$ be the formula $ν_{m, S} (x)$ where $E (x_{0}, \dots, x_{i - 1}, x_{i + 1}, \dots, x_{d - 1})$ is replaced by $R (x_{0}, \dots, x_{i - 1}, c, x_{i + 1}, \dots, x_{d - 1})$ .

Let us now assume that all sections of $R^{S}$ are $FO [<, mod m]$ -definable. Similarly, two cases must be considered, depending on whether there exists a diagonal E of $R^{S}$ which is not $FO [<, mod m]$ -definable. If there exists such a diagonal, the proof is similar to the preceding case. Let us now assume that all diagonals of $R^{S}$ are $FO [<, mod m]$ -definable.

The problem is reduced to the study of a set included in $N_{σ}^{d}$ which is not $FO [<, mod m]$ -definable for some permutation σ.

The set $R^{S}$ is the union of the $d!$ sets $R^{S} \cap N_{σ}^{d}$ for $σ \in P_{d - 1}$ . Since $R^{S}$ is not $FO [<, mod m]$ -definable, there exists $σ \in P_{d - 1}$ such that $R^{S} \cap N_{σ}^{d}$ is not $FO [<, mod m]$ -definable. For the sake of simplicity, let us assume that σ is the identity permutation, that it $(0, \dots, d - 1)$ .

Let $R^{'} = R^{S} \cap N_{(0, \dots, d - 1)}^{d}$ and let $S^{'}$ be $S [R / R^{'}]$ . Let us assume that there exists a $FO [<, R^{'}]$ -formula $ϕ_{R^{'}}$ which defines in $S^{'}$ a set $E \subseteq N$ which is not $FO [<, mod m]$ -definable. Then it suffices to set $ν_{m, R} (x)$ as the formula obtained from $ϕ_{R^{'}}$ by replacing every atomic formula $R^{'} (x)$ by $R (x) \land ⋀_{i = 0}^{d - 2} x_{i} ⩽ x_{i + 1}$ .

By Lemma 4.17, the function $τ_{m, R^{'}}$ is not $FO [<, mod]$ -definable. Then, by Proposition 4.19, there exists a set $E \subseteq N$ which is $FO [<, R]$ -definable and which is not ultimately m-periodic. Since $τ_{R^{S}, m}$ is $FO [<, R]$ -definable in $S$ , E is $FO [<, R]$ -definable. □

Let us give an example of application of Theorem 4.18. Some $FO [<, mod m]$ -definable sets R are considered. From them, some subsets of $N$ which can be defined from R are considered. Example 4.3.
Let $m = 1$ and $R = {x ∣ x_{1} + x_{2} = x_{3} x_{0}}$ . Fixing $x_{0}$ to 1 gives the addition relation, which is not $FO [<]$ -definable. So a $FO [R, <]$ -definable set which is not $FO [<]$ -definable can be obtained by exhibiting a $FO [+, <]$ -definable set which is not $FO [<]$ -definable.

Every section of + is $FO [<, mod m]$ -definable, so induction can not be used anymore. Let $σ = (0, 1, 2)$ , then $S = + \cap N_{(0, 1, 2)}^{3} = {x ∣ x_{0} ⩽ x_{1}, x_{1} + x_{0} = x_{2}}$ . Let $T_{n} = sec (S; x_{0} = n) = {(x, x + n) ∣ x ⩽ n}$ . Then $(n, 2 n) \in T_{n}$ and $(n + 1, 2 n + 1) \notin T_{n}$ , so ${thres}_{1} (n) > 2 n$ . Having $y, z > n$ , $(y, z) \notin T_{n}$ and $(y + 1, z + 1) \notin T_{n}$ imply ${thres}_{1} (n) = 2 n + 1$ , and so $τ_{R, m} (n) = 2 n + 1$ .

The image of $τ_{R^{S}, m}$ is the set of odd integers, which is not $FO [<] - d e f i n a b l e$ . Note that this set is $FO [<, mod 2] -definable$ .

5. About (finite) satisfiability of some class of existential-monadic formulas

This section considers the (finite) satisfiability problem for a logic with a $FO [+]$ -definable predicate which is not $FO [<, mod]$ -definable.

Let α be an alphabet and ϕ be a $FO [V, {(P_{a})}_{a \in α}]$ -formula without free variable. The formula Φ is said to be (finitely) satisfiable over a $V$ -structure $S$ if there exists a (finite) word w such that $S_{w} ⊧ ϕ$ .

The (finite) satisfiability problem of $FO [V, {(P_{a})}_{a \in α}]$ is said to be decidable if there exists an algorithm which takes as input a formula, and accepts if and only if ϕ is (finitely) satisfiable.

The main theorem of this section is now stated.

Theorem 5.1.
Let $d \in N^{> 0}$ and let R be a relation symbol with arity d. Let $S$ be a ${N, <, +_{N}, R}$ -structure such that $R^{S}$ is $FO [+]$ -definable and not $FO [<, mod]$ -definable. The finite satisfiability of $Π_{3} [N, <, +_{N}, R, P_{a}, P_{b}]$ , as well as the satisfiability of $Π_{3} [N, <, +_{N}, R, P_{a}, P_{b}]$ over $N$ , are undecidable in $S$ .

Note that our theorem considers a binary alphabet. It easily extends to any alphabet of cardinality at least 2.
5.1. 2-counter automata

Our undecidability result is obtained by a reduction from the halting problem for 2-counter automata which is undecidable [15]. Let us briefly recall the definition of a 2-counter automaton.

Definition 5.2 (2-counter automaton).

A 2-counter automaton A consists of a list of instructions. Let $# A$ denote the number of instruction of A. The instructions are “ $incr (h)$ ”, “ $decr (h)$ ”, “ $jmp (j)$ ”, “ $jz (h, j)$ ” with $h \in {a, b}$ , $j \in [# A - 1]$ and “Halt”. The jth instruction is written $A_{j}$ . Without loss of generality, it is assumed that only one Halt instruction appears in the list and that it appears as the last instruction.

Then it is explained how those automata compute.

Definition 5.3 (Configuration and simulation).

Let A be a 2-counter automaton. A configuration of A is a 3-tuple of natural numbers $(q, n_{0}, n_{1})$ where q is the next instruction of the automaton and $n_{j}$ is the value of the jth counter.

The simulation of A is a 3-tuple of sequences ${(κ [i], c_{0} [i], c_{1} [i])}_{i \in I}$ (where I is an initial segment of $N$ ) that satisfies the following properties:

The first configuration, which is denoted by $(κ [1], c_{0} [1], c_{1} [1])$ , equals $(0, 0, 0)$ .

For every $l \in N$ such that the lth configuration is $(κ [l], c_{0} [l], c_{1} [l])$ and $A_{κ [l - 1]} \neq Halt$ (that is $κ [l - 1] < # A - 1$ ), then the lth configuration, denoted by $(κ [l + 1], c_{0} [l + 1], c_{1} [l + 1])$ is defined as follows:

if $A_{κ [l]} = incr (i)$ then $c_{i} [l + 1] = c_{i} [l] + 1$ , $c_{1 - i} [l + 1] = c_{1 - i} [l]$ , and $κ [l + 1] = κ [l] + 1$ ,

if $A_{κ [l]} = decr (i)$ then $c_{i} [l + 1] = c_{i} [l] - 1$ , $c_{1 - i} [l + 1] = c_{1 - i} [l]$ , and $κ [l + 1] = κ [l] + 1$ ,

if $A_{κ [l]} = jmp (m)$ then $\forall i . c_{i} [l + 1] = c_{i} [l]$ , and $κ [l + 1] = m$ ,

if $A_{κ [l]} = jz (i, m)$ then $\forall i . c_{i} [l + 1] = c_{i} [l]$ , if $c_{i} [l] = 0$ then $κ [l + 1] = m$ and otherwise $κ [l + 1] = κ [l] + 1$ .

The last configuration, if it exists, satisfies $κ [last] = # A - 1$ .

It should be noted that those automata do not have any input. Hence an automaton admits at most one computation.

It is now explained how to transform a sequence of configuration ${(κ [i], c_{0} [i], c_{1} [i])}_{i \in I}$ into a language $L (κ, c_{0}, c_{1})$ . This transformation is such that two distinct sequences correspond to disjoint languages.

A language $L (q, n_{0}, n_{1})$ is first associated to each configuration $(q, n_{0}, n_{1})$ .

Definition 5.4.
The definition of $L (q, n_{0}, n_{1})$ uses another language $L^{'} (n_{0}, n_{1})$ , which is defined by induction on $n_{0}$ and $n_{1}$ as follows: $\begin{matrix} L^{'} (n_{0}, n_{1}) = \{\begin{matrix} ϵ, & if n_{0} = n_{1} = 0, \\ b a b^{} L^{'} (n_{0} - 1, n_{1}) & if n_{0} > 0, \\ b a a b^{} L^{'} (n_{0}, n_{1} - 1) & if n_{1} > 0 . \end{matrix} \end{matrix}$ Let $q \in N$ . The language $L (q, n_{0}, n_{1})$ is defined by the rational expression: $\begin{matrix} b a^{q + 3} b^{*} L^{'} (n_{0}, n_{1}) \end{matrix}$

Finally, for a finite or infinite sequence ${(κ [i], c_{0} [i], c_{1} [i])}_{i \in I}$ , let $L (κ, c_{0}, c_{1})$ be the concatenation of the languages $L (κ [i], c_{0} [i], c_{1} [i])$ for $i \in [n - 1]$ .

Intuitively, in $L (q, n_{0}, n_{1})$ , the letter b serves as separator and the number of successive a contains all the information.

Let ${(κ [i], c_{0} [i], c_{1} [i])}_{i \in I}$ be a sequence of configurations. Let w be a word of $L (κ, c_{0}, c_{1})$ . Let ${(s_{i})}_{i \in [n - 1]}$ be the successive positions in w such that $w [s_{i}] w [s_{i} + 1] w [s_{i} + 2] w [s_{i} 3] = b a a a$ . Then let $[s_{i}, s_{i + 1} - 1]$ be called the ith segment, denoted by $S_{i}$ .

The values of $κ [i]$ , $c_{0} [i]$ and of $c_{1} [i]$ can be read in $S_{i}$ since:

$κ [i]$ is the length of the first sequence of a, minus 2,

$c_{0} [i]$ is the number of factors $b a b$ in $S_{i}$ , and

$c_{1} [i]$ is the number of factors $b a a b$ in $S_{i}$ .

An example of word encoding the two first configurations of some automaton is now given. Example 5.1.
Let A be a 2-counter automaton with 2 instructions: $incr (0)$ and $jmp (0)$ . Let $(κ, c_{0}, c_{1})$ be a simulation of this automaton. Equation (2) represents a word of $L (κ [0], c_{0} [0], c_{1} [0]) L (κ [1], c_{0} [1], c_{1} [1])$ .

The $| |$ ’s represent the beginning of each sequence, and the |’s represent the beginning of each part which corresponds to a counter. The $\dots$ ’s corresponds to sequences of b’s.

5.2. Undecidability

Theorem 5.1 is now proved.

Proof of Theorem 5.1.
The proof goes by reduction from the halting problem for 2 counter automaton. Let A be a 2 counter automaton with $# A$ states.

The first part of the proof consists in defining in $Π_{2} [N, <, +_{N}, R, P_{a}, P_{b}]$ an increasing function g in $S$ such that, for all $n \in N$ , $g (n) ⩾ 2 n + # A + 5$ . The second part consists in creating an $Π_{3} [N, <, +_{N}, R, P_{a}, P_{b}]$ -formula which holds in $S$ if and only if A halts. The formula of the second part uses the function g. Defining g .
By Theorem 4.15, there exists a converging formula $ν_{R} (x; y)$ in $Π_{2} [N, <, +_{N}, R]$ such that $ν_{R} {(x; y)}^{S}$ is the graph of an increasing function f with slope l greater than 1.

By Lemma 3.13, there exists a $Σ_{1} [N, <, +_{N}, f]$ -definable function $g : N \to N$ such that for all n, $g (n) ⩾ 4 n + # A + 1$ . Hence g is $Π_{3} [N, <, +_{N}, R]$ -definable in $S$ .
Reduction from a 2-counter automata.
The simulation of a 2-counter automaton A is encoded by a formula $ϕ_{A}$ in $Π_{3} [N, <, +_{N}, R, P_{a}, P_{b}]$ such that there exists a word $w \in {a, b}^{+}$ such that $S (w) ⊧ ϕ_{A}$ if and only if A halts.

More precisely, the formula $ϕ_{A}$ states that the word w belongs to $L (κ, c_{0}, c_{1})$ where $(κ, c_{0}, c_{1})$ is a simulation of A.

Some notations are now introduced:
for $q \in [# A - 1]$ , let $Q_{q}$ be the set of positions p such that the factor of length $q + 5$ of w beginning at position p is $b a^{q + 3} b$ ,

for $i \in {0, 1}$ , let $C_{i}$ be the set of positions p such that the factor of length $i + 3$ of w beginning at position p, is $b a^{i + 1} b$ .

let S be the union of the sets $Q_{q}$ for $q \in [# A - 1]$ ,
The set $Q_{q}$ (respectively, $C_{i}$ ) is defined by the $Σ_{1} [+_{N}, P_{a}, P_{b}]$ -formula $ς_{q + 3} (x)$ (respectively, $ς_{i + 1} (x)$ ), where $ς_{n} (x)$ states that the factor of w of length $n + 2$ beginning at position x is $b a^{n} b$ . The formula $ς_{n} (x)$ is $\begin{matrix} P_{b} (x) \land ⋀_{j = 1}^{n} P_{a} (x + j) \land P_{b} (x + n + 1) . \end{matrix}$ The set S is defined by $⋁_{q = 0}^{# A - 1} Q_{q} (x)$ .
Defining S .
Let us assume that the simulation halts after n steps. Then the finite structure is partitioned into n consecutive segments of the form $S_{i} = [s_{i}, s_{i + 1} - 1]$ for $i \in [n]$ , with $s_{0} = 0$ and $s_{i + 1} = g^{S} (s_{i})$ for all $i \in [n]$ . The ith segment, denoted by $S_{i}$ , encodes the ith step of the simulation.

In Example 5.1 corresponds to the case $g (n) = 2 n + 7$ (with $# A = 2$ ).

By an easy induction on i, $S_{i}$ has length at least $4^{i} (# A + 5)$ .

For the sake of readability, the notation $g^{- 1} (n)$ is used for any n belonging to the image of g. For any formula $ψ (x)$ , let $ψ (g^{- 1} (n))$ be an abbreviation for the $Σ_{3} [n, S, g]$ formula: $\begin{matrix} \exists n^{'} . g (n^{'}) ≐ n \land S (n^{'}) \land ψ (n^{'}) . \end{matrix}$

A $Π_{4} [N, <, +_{N}, R, S]$ -formula $ϕ_{S}$ which asserts that S is the image of 0 by a sequence of iterations of g is now given. An integer n belongs to S if and only if $n = s_{0} = 0$ , or there exists $n^{'} < n$ such that $g^{S} (n^{'}) = n$ and $S (n^{'})$ holds. Let $ϕ_{S}$ be: $\begin{matrix} \forall n . {S (n) ⟺ [n ≐ 0 \lor S (g^{- 1} (n))]} . \end{matrix}$
Simulation.
Let us now consider a run of A. Let us first consider the states. For $i \in [n]$ , for $q \in [# A - 1]$ , the formula $ϕ_{q}$ requires that $Q_{q} (s_{i})$ holds if and only if $κ (i) = q$ .

Let us now consider the counters. For $i \in [n]$ , the formula $ϕ_{q}$ requires that $# (C_{j} \cap S_{i}) = c_{j} [i]$ .

The main issue with this encoding is that in order to ensure that two successive segments encode two successive configurations, it is needed to compare the cardinality of two sets, which does not seem possible in our logic. To overcome this, the properties of the function $g^{S}$ are used. For example if the ith step is a $jump$ , then $c_{j} [i] = c_{j} [i + 1]$ , and in this case $C_{j}$ can be chosen in $S_{i + 1}$ to be the image by $g^{S}$ of $C_{j}$ in $S_{i}$ . If the ith step is $incr (j)$ then it is enough to add a single position to $C_{j}$ in $S_{i + 1}$ . Note that the properties of the function $g^{S}$ ensure that such a position exists.

Formally, the formula $ϕ_{q}$ states the following requirements:
The initial state is 0, which is defined by: $\begin{matrix} Q_{0} (0) . \end{matrix}$

The last state is $# A$ , which is defined by: $\begin{matrix} \exists x . \neg \exists y . g (x) ≐ y \land Q_{# A - 1} (x) . \end{matrix}$ In this formula, x represents the beginning of the last segment of the universe.

Let s be an integer of the form $s_{n}$ , then let $s^{'} = s_{n + 1}$ and $s^{″} = s_{n + 2}$ . Let q be the ith step of the computation. Let us now give formulas $ϕ_{q}$ which assert that two successive segments $[s, s^{'} - 1]$ and $[s^{'}, s^{″} - 1]$ encode a step of the computation

If the ith step is $jmp (q^{'})$ , that is $Q_{q} (s_{i})$ with $A_{κ (q)} = jmp (q^{'})$ , then:
$Q_{q^{'}} (s_{i + 1})$ ,

for $p \in [s_{i + 1}, s_{i + 2} - 1]$ , for $j \in {0, 1}$ , $C_{j} (p)$ holds if and only if there exists $p^{'}$ with $g^{S} (p^{'}) = p$ and $C_{j} (p^{'})$ holds. This can be expressed by the $Π_{4} [N, <, +_{N}, R, P_{a}, P_{b}]$ -formula $ϕ_{copy j}$ : $\begin{array}{rcl} \forall p \in [s^{'}, s^{″} - 1] . (C_{j} (p) ⟺ C_{j} (g^{- 1} (p^{'}))) . \end{array}$
This can be expressed by the $Π_{4} [N, <, +_{N}, R, P_{a}, P_{b}]$ -formula $ϕ_{q}$ equal to $\begin{matrix} Q_{q^{'}} (s_{i + 1}) \land ϕ_{copy 0} \land ϕ_{copy 1} \end{matrix}$

If the ith step is $jz (z, q^{'})$ , that is $Q_{q} (s_{i})$ with $A_{κ (q)} = jz (z, q^{'})$ , then:
For $p \in [s_{i + 1}, s_{i + 2} - 1]$ , for $j^{'} \in {0, 1}$ , $C_{j^{'}} (p)$ holds if and only if there exists $p^{'}$ with $g^{S} (p^{'}) = p$ and $C_{j^{'}} (p^{'})$ holds.

If there exists a position $p \in [s_{i}, s_{i + 1} - 1]$ such that $C_{z} (p)$ then $Q_{q + 1} (s_{i + 1})$ , and $Q_{q^{'}} (s_{i + 1})$ otherwise. This can be expressed by the $Σ_{1} [N, <, +_{N}, R, s, s^{'}, s^{″}, P_{a}, P_{b}]$ -formula $ϕ_{jz}$ : $\begin{matrix} ⟨ \exists p \in [s, s^{'} - 1] . C_{j} (p) ∣ Q_{q^{'}} (s^{'}) ∣ Q_{q + 1} (s^{'}) ⟩ \end{matrix}$
Then $ϕ_{q}$ is the $D_{1} [N, <, +_{N}, R, s, s^{'}, s^{″}, P_{a}, P_{b}]$ -formula: $\begin{array}{rcl} ϕ_{jz} \land ϕ_{copy 0} \land ϕ_{copy 1} \end{array}$

If the ith step is $decr (j)$ , that is $Q_{q} (s_{i})$ with $κ (q) = decr (j)$ , then
$Q_{q + 1} (s_{i + 1})$ ,

there exists exactly one integer $p \in [s_{i}, s_{i + 1} - 1]$ such that $C_{j} (p)$ holds and $C_{j} (g (p))$ does not hold .

Formally, it is expressed as the conjunction of two formulas, a $Σ_{3} [<, +_{1}, s, s^{'}, C_{j}, Q_{q + 1}]$ -formula $ϕ_{q, \exists}$ which states the existence of such a p: $\begin{matrix} \exists p \in [s, s^{'} - 1] . C_{j} (p) \land \neg C_{j} (g (p)), \end{matrix}$ and a $Π_{4} [<, +_{1}, s^{'}, s^{″}, C_{j}, g]$ -formula $ϕ_{q,!}$ which states that there are no two such p: $\begin{matrix} (\forall p_{0}, p_{1} \in [s, s^{'} - 1] . C_{j} (p_{0}) \land \neg C_{j} (g (p_{0})) \land C_{j} (p_{1}) \land \neg C_{j} (g (p_{1}))) p_{0} ≐ p_{1} . \end{matrix}$

for all $q \in [s_{i + 1}, s_{i + 2} - 1]$ , if ${(g^{S})}^{- 1} (q)$ is not defined or $C_{j} ({(g^{S})}^{- 1} (q))$ does not hold, then $C_{j} (q)$ does not hold. This can be expressed by the $Π_{4} [N, <, +_{N}, R, s^{'}, s^{″}, P_{a}, P_{b}]$ -formula $ϕ_{j}$ : $\begin{matrix} \forall p \in [s^{'}, s^{″} - 1] (\neg C_{j} (g^{- 1} (p)) ⟹ \neg C_{j} (p)) . \end{matrix}$

for all $q \in [s_{i + 1}, s_{i + 2} - 1]$ , $C_{1 - j} (q)$ holds if and only if there exists $q^{'}$ with $g^{S} (q^{'}) = q$ and $C_{1 - j} (q^{'})$ holds.
This can be expressed by the $Π_{4} [<, +_{1}, s^{'}, s^{″}, C_{0}, C_{2}, g]$ -formula $ϕ_{q}$ : $\begin{array}{rcl} Q_{q + 1} (s^{'}) \land ϕ_{q, \exists} \land ϕ_{q,!} \land ϕ_{j} \land ϕ_{copy 1 - j} \end{array}$

If the ith step is $incr (j)$ , that is $Q_{q} (s_{i})$ with $κ (q) = incr (j)$ , then
$Q_{q + 1} (s_{i + 1})$ ,

there exists exactly one $p \in [s_{i + 1}, s_{i + 2} - 1]$ such that $C_{j} (p)$ holds and there is no $p^{'}$ such that $g (p^{'}) = p$ and $C_{j} (p^{'})$ hold.

Formally, it is expressed by two formulas, a $Σ_{3} [<, +_{1}, s, s^{'}, C_{j}, Q_{q + 1}]$ -formula which states the existence of such a p, $ϕ_{q, \exists}$ : $\begin{matrix} \exists p \in [s^{'}, s^{″} - 1] . C_{j} (p) \land \neg C_{j} (g^{- 1} (p)), \end{matrix}$ and a $Π_{4} [<, +_{1}, s^{'}, s^{″}, C_{j}, g]$ -formula $ϕ_{q,!}$ which states that there are no two such p, $\begin{matrix} (\forall p_{0}, p_{1} \in [s^{'}, s^{″} - 1] . C_{j} (p_{0}) \land \neg C_{j} (g^{- 1} (p_{0})) \land C_{j} (p_{1}) \land \neg C_{j} (g^{- 1} (p_{1}))) p_{0} ≐ p_{1} . \end{matrix}$

for all $q \in [s_{i + 1}, s_{i + 2} - 1]$ , if $C_{j} ({(g^{S})}^{- 1} (q))$ holds, then $C_{j} (q)$ holds. This can be expressed by the $Π_{4} [N, <, +_{N}, R, s^{'}, s^{″}, P_{a}, P_{b}]$ -formula $ϕ_{j}$ : $\begin{matrix} \forall p \in [s^{'}, s^{″} - 1] (C_{j} (g^{- 1} (p)) ⟹ C_{j} (p)) . \end{matrix}$

for all $q \in [s_{i + 1}, s_{i + 2} - 1]$ , $C_{1 - j} (q)$ holds if and only if there exists $q^{'}$ with $g^{S} (q^{'}) = q$ and $C_{1 - j} (q^{'})$ holds.
This can be expressed by the $Π_{4} [<, +_{1}, s^{'}, s^{″}, C_{0}, C_{2}, g]$ -formula $ϕ_{q}$ : $\begin{array}{rcl} Q_{q + 1} (s^{'}) \land ϕ_{q, \exists} \land ϕ_{q,!} \land ϕ_{j} \land ϕ_{copy 1 - j} \end{array}$

finally if the ith step is $Halt$ , that is $Q_{q} (s_{i})$ with $A_{κ (q)} = Halt$ , then $ϕ_{q}$ is true.
The above-mentioned formula $ϕ_{A}$ which accepts encoding of simulations of A is now given. Let $ϕ_{A}$ be the $Π_{4} [N, <, +_{N}, R, P_{a}, P_{b}]$ -formula: $\begin{array}{l} ϕ_{S} \land Q_{0} (0) \land \exists x . Q_{# A - 1} (x) \\ \land (\forall s, s^{'}, s^{″} . S (s) \land g (s) = s^{'} \land g (s^{'}) = s^{″}) ⟹ ⋀_{q = 0}^{# A - 1} (Q_{q} (s) \land ϕ_{q}) . \end{array}$
Universe $N$ .
Let us now consider the satisfiability problem over $N$ . The proof is the same as finite case excepts that it must be asserted that the word ends by an infinite sequence of b’s and only the letters up to the last a are considered.

Formally, one quantifies existentially over a variable m which represents the last occurrence of a. Then all quantifications of $ϕ_{A}$ are restricted to integers less than or equal to m.
□

6. Conclusion

It is proven in this paper that a set R is $FO [<, mod]$ -definable if and only if every unary $FO [<, R]$ -definable set of integers is ultimately periodic. It is also proven that the class of $FO [<, mod m]$ -definable sets also admits a Muchnik-like property in terms of local and recursive properties.

It has also been proved that finite satisfiability of $FO [<, R, {(P_{a})}_{a \in α}]$ is undecidable for every set R which is $FO [+]$ -definable and not $FO [<, mod]$ -definable.

We see many directions for further research. We may want to minimize the number of alternations of quantifiers needed to get undecidability, and conversely to find an algorithm to decide those logics with one or two alternations.

Let us note that a construction similar to the proof of Theorem 5.1 can be used to prove undecidability of some other related logics:

$FO [R, + 1, {(P_{a})}_{a \in α}]$ when R is $FO [+]$ -definable and not $FO [<, mod]$ -definable,

$FO [+ 1, g]$ as soon as g is not interpreted, and

$FO [<, g, {(P_{a})}_{a \in α}]$ when g is ultimately greater than any function $+ c$ for $c \in N$ .

Another direction for further research is to extend Corollary 4.12 in order to obtain a polynomial-time algorithm.

Footnotes

Acknowledgements

We thank the anonymous referees of the first version of this paper for their remarks and suggestion to improve the paper. We thank Alexis Bès for his help during the preparation of this paper. We thank the organizers of Computatibility in Europe 2013 conference, where this result was first publicly presented.

References

D.A.M.

Barrington,

Compton,

Straubing and

Thérien, Regular languages in

N C^{1}

, Journal of Computer and System Sciences 44(3) (1992), 478–499. doi:10.1016/0022-0000(92)90014-A.

Bruyère,

Hansel,

Michaux and

Villemaire, Logic and p-recognizable sets of integers, Bull. Belg. Math. Soc 1 (1994), 191–238.

J.R.

Büchi, Weak second-order arithmetic and finite automata, Zeitschrift für Mathematische Logik und Grudlagen der Mathematik 6 (1960), 66–92. doi:10.1002/malq.19600060105.

Choffrut, Deciding whether a relation defined in Presburger logic can be defined in weaker logics, RAIRO ITA 42(1) (2008), 121–135.

Choffrut,

Malcher,

Mereghetti and

Palano, On the expressive power of FO[+], in: LATA,

A.H.

Dediu,

Fernau and

Martín-Vide, eds, Lecture Notes in Computer Science, Vol. 6031, Springer, 2010, pp. 190–201.

D.C.

Cooper, Theorem proving in arithmetic without multiplication, Machine Intelligence 7 (1972), 91–99.

C.C.

Elgot, Decision problems of finite automata design and related arithmetics, Trans. Amer. Math. Soc. 98 (1961), 21–52. doi:10.1090/S0002-9947-1961-0139530-9.

C.C.

Elgot and

M.O.

Rabin, Decidability and undecidability of extensions of second (first) order theory of (generalized) successor, J. Symb. Log. 31(2) (1966), 169–181. doi:10.2307/2269808.

Finkel and

Leroux, Presburger functions are piecewise linear, Research Report LSV-08-08, Laboratoire Spécification et Vérification, ENS Cachan, France, 2008, 9 pp.

10.

Ginsburg and

E.H.

Spanier, Presburger formulas, and languages, Semigroups, Pacific Journal of Mathematics 16 (1966), 285–296. doi:10.2140/pjm.1966.16.285.

11.

Immerman, Descriptive Complexity, Springer, 1999.

12.

K.-J.

Lange, Some results on majority quantifiers over words, in: IEEE Conference on Computational Complexity, IEEE Computer Society, 2004, pp. 123–129.

13.

McNaughton and

Papert, Counter-Free Automata, M.I.T. Press, Cambridge, Mass, 1971.

14.

Michaux and

Villemaire, Presburger arithmetic and recognizability of sets of natural numbers by automata: New proofs of Cobham’s and Semenov’s theorems, Ann. Pure Appl. Logic 77(3) (1996), 251–277. doi:10.1016/0168-0072(95)00022-4.

15.

M.L.

Minsky, Recursive unsolvability of post’s problem of “tag”: And other topics in theory of turing machines, Group report, Massachusetts Institute of Technology, Lincoln Laboratory, 1960.

16.

A.A.

Muchnik, The definable criterion for definability in Presburger arithmetic and its applications, Theor. Comput. Sci. 290(3) (2003), 1433–1444. doi:10.1016/S0304-3975(02)00047-6.

17.

Péladeau, Formulas, regular languages and Boolean circuits, Theor. Comput. Sci. 101(1) (1992), 133–141. doi:10.1016/0304-3975(92)90152-6.

18.

Presburger, Über die vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen, die addition als einzige operation hervortritt, in: Comptes Rendus du Premier Congrès des Mathématicienes des Pays Slaves, Warsaw, 1927, pp. 92–101, 395.

19.

Straubing, Finite Automata, Formal Logic, and Circuit Complexity, Birkhäuser, 1994.

20.

B.A.

Trakhtenbrot, Impossibility of an algorithm for the decision problem in finite classes, Doklady Akademii Nauk SSSR 70 (1950), 569–572 (in Russian).

21.