Composition Over the Natural Number Ordering with an Extra Binary Relation

Abstract

The composition method was developed in the 1970’s and 1980’s by Shelah and Gurevich as a powerful tool in the study of monadic second-order theories of labelled orderings and trees. In this paper, we use a variant of the technique for first-order theories of structures $(\mathbb {N}, <, R)$ where R is binary. For the case that R is of “finite valency” (where each element has only finitely many neighbors in the symmetric closure of R), we show results on (non-) definability, on decidability, and on the recursion theoretic complexity of such theories.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The composition method combines two rather diverse features. It opens a way to study theories of labelled orderings (and labelled trees) by considering these structures as sums of substructures, such that from properties of the substrutures and the way they are concatenated one derives properties of the full structure. This is a natural, simple, and intuitively appealing view. On the other hand, the technical details of this attractive idea are somewhat involved, and the landmark papers of Shelah and Gurevich in the 1970’s and 1980’s ([Sh75, Gu79, Gu82, Gu85, GS79, GS83, GS85]) that developed the theory are demanding. Thus – at least in theoretical computer science – not many researchers invested the effort to go deeper into the subject, although it is a key to many decidability results in monadic second-order logic (MSO-logic), complementing and extending results that had earlier been shown by a reduction of MSO-logic to finite automata (Büchi [Bü62], Rabin [Ra69]).

The core idea is best explained for infinite labelled linear orderings, for example structures $\mathcal{A} = (A, <, P)$ with infinite A and unary predicate P. One considers a finite fragment of the MSO-theory of $\mathcal{A}$, in which only sentences of some fixed quantifier-depth m are taken into account, called “m-theory” of $\mathcal{A}$ (sometimes the quantifier alternation rank is used instead), aiming at the decision whether a sentence up to quantifier-depth m belongs to this m-theory. One composes this m-theory from the m-theories of intervals. Invoking a combinatorial argument (e.g., Ramsey’s Theorem [Ra29]) it may turn out that such a decomposition can be guaranteed which is “homogeneous”: For example, for a structure $(\mathbb {N}, <, P)$, this is a decomposition into finite segments where – excepting the first – all have the same m-theory. This can be exploited to infer (non-) definability and decidability results concerning MSO-logic over the given structure.

In the present paper, it is shown how to apply the composition method over the ordering $(\mathbb {N}, <)$ of the natural numbers where the labelling (given by a predicate $P \subseteq \mathbb {N}$) is replaced by a binary relation R. We consider relations that are of “finite valency”, i.e., where for each a there are only finitely many b such that R(a, b) or R(b, a). Also we restrict the logical framework to first-order logic FO. As it turns out, one can then again decompose, for any given quantifier-depth m, the structure $(\mathbb {N}, <, R)$ into a sequence of appropriately defined “segments” where (excepting the first) all segments have the same m-theory. As a consequence, we obtain results on first-order definability in such structures $(\mathbb {N}, <, R)$ – in particular, that addition and multiplication are not FO-definable – and on the recursion theoretic complexity of the FO-theory of such structures. Also examples R are exhibited where the first-order theory of $(\mathbb {N}, <, R)$ is decidable, namely graphs of recursive functions $f: \mathbb {N} \rightarrow \mathbb {N}$ where the distance function $f(n+1) - f(n)$ is strictly increasing.¹

The exposition will not be very formal; for details we refer to [Th80].

2 $(\mathbb {N}, <, P)$ with Monadic P

Let us first recall the composition method for structures $(\mathbb {N}, <, P)$ with monadic P. We identify this labelled ordering with an infinite 0-1-word $\alpha$ such that $\alpha (i) = 1$ iff $i \in P$. Finite segments of the structure are then finite words over $\{0,1\}$ (denoted by $u, v, w, \ldots$). We restrict here to first-order logic FO although the results of the present section can as well be obtained for monadic second-order logic MSO.

The quantifier-depth of a formula $\varphi$ is the depth of nesting of quantifiers in $\varphi$. Two labelled orderings u and v are called m-equivalent (written $u \equiv _m v$) if for all FO-sentences $\varphi$ of quantifier-depth m we have $u \models \varphi$ iff $v \models \varphi$. It is well-known that a convenient method to verify $\equiv _m$-equivalence is the Ehrenfeucht-Fraïssé game. We extend the relation also to infinite words. Then, for example, $1 \equiv _1 1111\ldots$ but $1 \not \equiv _2 1111\ldots$; in the latter case, the sentence $\forall x \exists y \ x < y$ shows the $\equiv _2$-inequivalence.

Let us list some basic facts (see. e.g., [EF95]).

Lemma 1

 

• 1. $\equiv _m$ is an equivalence relation of finite index. (The equivalence classes are called m-types.)

• 2. An m-type $\tau$ is definable by a sentence $\varphi _\tau$ of quantifier-depth m.

• 3. Each sentence of quantifier-depth m is equivalent to a disjunction of sentences $\varphi _\tau$. (If $\varphi _\tau$ implies $\varphi$, we say that $\tau$ induces $\varphi$.)

“Composition” refers to the fact that the m-types of two words u, v determine the m-type of their concatenation uv.

Lemma 2

 

• 1. From the m-types of u and v one can compute the m-type of uv, and from the m-types of a segment u and an infinite word $\alpha$ one can compute the m-type of $u \alpha$.

• 2. Given a word $\alpha = v_1 v_2 v_3 \ldots$ where all $v_i$ have the same m-type $\tau$, the m-type $\varrho$ of $\alpha$ is computable from $\tau$.

Given the types $\sigma$ and $\tau$ of u, v (or $\alpha$), respectively, we write $\sigma + \tau$ for the m-type of uv (or $u \alpha$), similarly for a word $\alpha = v_1 v_2 v_3 \ldots$ where all $v_i$ have m-type $\tau$, we write $\sum _\omega \tau$ for the m-type of $\alpha$.

Over a model $\alpha = (\mathbb {N}, <, P)$ the m-types induce a finite coloring on pairs (i, j) of natural numbers; we define the color of (i, j) (for $i < j$) to be the m-type of the substructure over the interval [i, j). Invoking Ramsey’s Theorem (for infinite sets), one obtains an infinite “homogeneous set” $H = \{h_0 < h_1 < h_2 \ldots \}$ such that all the colors of intervals $[h_k, h_{k+1})$ and even of all intervals $[h_k, h_\ell )$ with $\ell < k$ coincide.

Thus, taking m-types as colors, for arbitrary $\alpha$ a decomposition of $\alpha$ in the form $u v_1 v_2 v_3 \ldots$ exists such that all $v_i$ share the same m-type $\tau$, and – writing $\sigma$ for the m-type of u – the m-type of $\alpha$ is obtained as $\sigma + \sum _\omega \tau$. In this sense, truth of a sentence $\varphi$ of quantifier-depth m in a model $\alpha$ can be reduced to the question whether $\alpha$ is decomposable in this way such that $\sigma + \sum _\omega \tau$ induces $\varphi$. So a sentence $\varphi$ of quantifier-depth m is equivalent to a finite disjunction of MSO-statements $\chi _{\sigma , \tau }$ saying that there is a homogeneous set for the colors $\sigma$ and $\tau$, taken for all $\sigma , \tau$ such that $\sigma + \sum _\omega \tau$ induces $\varphi$. More precisely, $\chi _{\sigma , \tau }$ expresses that a homogeneous set $H = \{h_0 < h_1 < h_2 \ldots \}$ exists where the m-type of the interval $[0, h_0)$ is $\sigma$ and for all $i < j$, the m-ype of the interval $[h_i, h_j)$ is $\tau$.

Our next aim is to derive from this ultimately periodic structure of an infinite model $\alpha$ a normal form of FO-sentences. Here we follow [Th81]. Assume we have a coloring C of pairs (i, j) with $i < j$ by colors in a finite set Col, and that this coloring is additive, i.e. that the colors $c_1$ of (i, j) and $c_2$ of (j, k) determine the color d of (i, k). (So an example is given by associating with (i, j) the m-type of the interval [i, j).) As mentioned, the statement that a decomposition according to Ramsey’s Theorem with the two colors c, d exists is an MSO-formula (here in the signature with the binary relations $x<y$ and $C(x,y) = c$ for $c \in \mathrm{Col}$):

$(*)$ there is an infinite set $H = \{h_0 < h_1 < h_2 \ldots \}$ such that $(0, h_0)$ has color c and for all $i < j$, $(h_i, h_j)$ has color d.

An analysis of Ramsey’s Theorem (see [Th81]) shows that $(*)$ can be written as a first-order formula in the mentioned signature:

Theorem 1

Over $(\mathbb {N}, <, C)$ with additive finite coloring C of the number pairs (i, j) with $i < j$, the condition $(*)$ can be expressed by a finite disjunction of first-order formulas of the form

$$\begin{aligned} \forall x \exists y > x \ \psi (y) \ \ \wedge \ \ \exists x \forall y > x \ \psi '(y) \end{aligned}$$

where $\psi (y), \psi '(y)$ are bounded in y, i.e. all quantifiers $\exists z, \forall z$ are relativized to $z \le y$.

This result also holds for MSO-logic, with the same proof strategy. It is then a logical version of McNaughton’s Theorem on the determinization of Büchi automata. In that context, one starts with a condition $(*)$ where the $\equiv _m$-relation is replaced by an automata theoretic equivalence between finite words. In the logical context, one obtains the remarkable consequence that over $\omega$-words MSO has the same expressive power as weak MSO (where set quantification is restricted to finite sets). As stated, Theorem 1 amounts to a first-order version of McNaughton’s Theorem.

3 $(\mathbb {N}, <, R)$ with Binary R of Finite Valency

Now we consider structures $(\mathbb {N}, <, R)$ with binary R. Then a problem arises in the attempt to compose the m-type of an interval [i, k) from the m-types of subintervals [i, j) and [j, k): There may be elements $a \in [i,j), b\in [j,k)$ with R(a, b); this connection is present in the full interval [i, k) but not detectable from the (m-types of the) two subintervals. Moreover, there may be elements $a < i, b \ge k$ with R(a, b); also in this case the “R-link” between a and b is not visible in the interval [i, j) which lies in between.

On the other hand, one knows from first-order model theory, in particular from a result of Hanf [Ha65], that a formula of quantifier-depth m can only establish a connection between a and b via R if they are not too far in terms of their “R-distance” – more precisely, if b belongs to the $2 ^m$-sphere around a (which contains all elements connected to a via a path of length $2 ^m$ of edges of the symmetric closure of R). This motivates to work with long enough segments in a decomposition (for given quantifier-depth m), where we try to ensure that R-connections between elements a, b can be established by formulas of quantifier-depth m only if a, b belong to the same or two successive segments of the decomposition. More concretely, one can try to reach a situation where we use a segment [i, j) with [h, i) in front and [j, k) afterwards if the $2^m$-spheres of elements in [i, j) do not extend below h, say only down to $i^* \ge h$, and that the $2^m$-spheres of elements in $[j,\infty )$ do not extend below i, say only down to $j^* \ge i$. It will turn out that for relations R of finite valency, this approach will work. It leads to decompositions where the participating segments overlap (namely, rather than [i, j) we shall consider $[i^*, j)$). With these overlappings a composition result on appropriately defined m-types still holds. This will allow us to obtain results in good analogy to the above mentioned case of structures $(\mathbb {N}, <, P)$ with monadic P. Since we are dealing with overlapping intervals, we refer to intervals [i, j] rather than [i, j).

Recall that a binary relation $R \subseteq M \times M$ is of finite valency if for any $a \in M$ there are only finitely many $b \in M$ such that R(a, b) or R(b, a). Call [a, b] an R-segment if R(a, b) or R(b, a).

We begin by noting a key property of relations of finite valency when the underlying ordering is $(\mathbb {N}, <)$: For any b there are only finitely many elements $d>b$ such that d is R-connected to some element $\le b$.

So, given any [a, b], two elements $c \le a$ and $d \ge b$ can be found such that no R-connection exists between elements $< c$ and $> d$. We iterate this process of separation, following the idea of building “spheres” as mentioned above. Our eventual aim is to work with intervals [a, b] such that R-connections from above b will only reach elements downward to some element $b^* > a$.

Definition 1

Define for each b a sequence $b(0) \ge b(1) \ge \ldots$ as follows:

• $b(0) = b$

• $b(i+1)$ = maximal c which is below all R-segments $[k, \ell ]$ intersecting $[b(i), \infty )$, if such c exists, otherwise 0

We call the segment [a, b] m-admissible if $b({2^m}) > a$, and we write $b^*$ for $b(2^m)$ if m is clear.

Let us denote by $\widetilde{b}$ the sequence $(b(0), \ldots , b(2^m))$. Invoking the remark above we see that for any k there exist admissible segments [a, b] above k.

We now define generalized m-types of intervals [a, b] in which an element $b^*$ is designated as explained above. In order to allow inductive proofs, we define the m-types for expansions of intervals by additional elements $a_0, \ldots , a_{r-1} \in [a,b]$.

Definition 2

Let [a, b] be an m-admissible interval in $(\mathbb {N}, <, R)$, $a_0, \ldots , a_{r-1} \in [a,b]$.

• $T^m_R[a,b](a_0, \ldots , a_{r-1})$ is the m-type of the restriction of $(\mathbb {N}, <, R)$ to [a, b].

• $D^m_R[a,b](a_0, \ldots , a_{r-1})$ is the m-type $T^m_R[a^*,b](\widetilde{a}, \widetilde{b}, a_0, \ldots , a_{r-1})$

So $D^m_R[a,b]$ refers also to elements $< a$, namely those down to $a^*$; note that the parameter a occurs in $\widetilde{a}$ and thus is not lost.

Lemma 3

(Composition Lemma).

• 1. Given m-admissible segments [a, b] and [b, c] of $(\mathbb {N}, <, R)$ with R of finite valency, $D^m_R[a,b]$ and $D^m_R[b, c]$ determine effectively the type $D^m_R[a,c]$.

• 2. Given a sequence $a_0, a_1, \ldots$ such that $[a_i, a_{i+1}]$ is m-admissible and such that $D^m_R[a_i, a_{i+1}] = \tau$ for some m-type $\tau$, $D^m_R[a_0, \infty )$ is determined effectively from $\tau$.

Remark 1

In the inductive proof of the Composition Lemma, segment types $D^m_R[a,b](\overline{a})$ with parameters $\overline{a}$ have to be considered. It is then relevant whether an element $a_i$ occurs below or above the element $b^* \in [a,b]$. This distinction is not needed in a situation where a composition of m-admissible segments $[k_0, k_1], [k_1, k_2], [k_2, k_3]$ is treated such that no parameters occur in the middle segment $[k_1,k_2]$. For example, if $a_0 \in [k_0, k_1]$ and $b,c \in [k_2, k_3]$, then the m-type $D^m_R[k_0,k_3](a,b,c)$ is determined as a sum

$$\begin{aligned} D^m_R[k_0, k_1](a) + D^m_R[k_1, k_2] + D^m_R[k_2, k_3](b,c). \end{aligned}$$

Now we proceed in analogy to the case of structures $(\mathbb {N}, < , P)$ with unary P. For any structure $(\mathbb {N}, <, R)$ with R of finite valency and for given m we can pick a sequence $\{n_0, n_1, n_2, \ldots \}$ forming an infinite set N such that each $[n_i, n_j]$ is m-admissible. Over N we obtain an additive coloring and can apply Ramsey’s Theorem. We get a homogeneous subset H of N, $H = \{ h_0 < h_1 < h_2 \ldots \}$, whence the m-type of $(\mathbb {N}, <, R)$ can be obtained as a sum $\sigma + \sum _\omega \tau$ where $\sigma = D^m_R[0, h_0]$ and $\tau = D^m_R[h_0, h_1] (= D^m_R[h_i, h_j]$ for all $i < j$). Applying further Theorem 1, we conclude:

Theorem 2

(Normal Form Theorem). Over a structure $(\mathbb {N}, <, R)$ with R of finite valency, a sentence of quantifier-depth m can (effectively) be written as a disjunction of sentences

$$\begin{aligned} \forall x \exists y > x \ \psi (y) \ \ \wedge \ \ \exists x \forall y > x \ \psi '(y) \end{aligned}$$

where $\psi (y), \psi '(y)$ are bounded in y, with atomic formulas of the form $x < y$ and $D^m_R[x,y] = \tau$.

4 Applications

Theorem 3

In a structure $(\mathbb {N}, <, R)$ with R of finite valency, neither addition nor multiplication is FO-definable.

We derive this result from the following:

Proposition 1

Let $f : \mathbb {N}^2 \rightarrow \mathbb {N}$ be FO-definable in $(\mathbb {N}, <, R)$ where R is of finite valency. Then one of the following two sets is finite:

$$\begin{aligned} X_f := \{x \in \mathbb {N} \mid \lambda y f(x,y) \text{ is } \text{ injective }\}, Y_f := \{y \in \mathbb {N} \mid \lambda x f(x, y) \text{ is } \text{ injective }\} \end{aligned}$$

It is clear that this proposition implies the theorem above since $X_+, Y_+, X_\cdot , Y_\cdot$ are all infinite. For example, $X_+$ contains all x such that the function $y \mapsto x+y$ is injective; hence $X_+ = \mathbb {N}$.

Proof

Assume f is FO-definable by $\varphi (x,y,z)$ of quantifier-depth m. Consider the coloring $D^{m+1}_R$ and a corresponding homogeneous set $H = \{h_0 < h_1 < \ldots \}$.

Assume for contradiction that $X_f, Y_f$ are both infinite. Then we can pick $a_0 \in X_f$, $b_0 \in Y_f$ in two different H-segments beyond $h_0$, say $a_0 \in [h_{i+1}, h_{i+2}]$ and $b_0 \in [h_{j+1}, h_{j+2}]$ such that, moreover, $a_0 < b_0$ and $[h_i, h_{i+4}] \cap [h_j, h_{j+4}] = \emptyset$. Since $D^{m+1}_R[h_{i+1}, h_{i+2}] = D^{m+1}_R[h_{i+2}, h_{h+3}]$, we can choose $a' \in [h_{i+2}, h_{i+3}]$ such that $D^m_R[h_{i+1}, h_{i+2}](a_0) = D^m_R[h_{i+2}, h_{i+3}](a')$, similarly $b' \in [h_{j+2}, h_{j+3}]$ such that $D^m_R[h_{j+1}, h_{j+2}](b_0) = D^m_R[h_{j+2}, h_{j+3}](b')$. Since the m-types $D^m_R[h_k, h_\ell ]$ are for all $k < \ell$ equal to a fixed type $\tau$ (in particular, we have $\tau + \tau = \tau$), we have, by Remark 1,

$$\begin{aligned} D^m_R[h_i, h_{i+4}](a_0) = D^m_R[h_i, h_{i+4}](a'), \ \ D^m_R[h_j, h_{j+4}](b_0) = D^m_R[h_j, h_{j+4}](b'); \end{aligned}$$

note that in all cases the segment with a designated element is preceded and succeeded by a segment of type $\tau$.

Let $c_0 = f(a_0, b_0)$. If $c_0 \not \in [h_i, h_{i+4}]$, say $c_0 > h_{i+4}$, then we apply Remark 1 and obtain

$D^m_R[0, h_i] + D^m_R[h_i, h_{i+4}](a_0) + D^m_R[h_{i+4}, \infty )(b_0, c_0)$

$\quad \quad \quad \,\,= D^m_R[0, h_i] + D^m_R[h_i, h_{i+4}](a') + D^m_R[h_{i+4}, \infty )(b_0, c_0)$

which implies that the types $T^m_R[0,\infty )(a_0, b_0, c_0)$ and $T^m_R[0, \infty )(a', b_0, c_0)$ coincide. So, by the definition of f using a formula $\varphi (x,y,z)$ of quantifier-depth m, we see that $f(a_0, b_0) = f(a', b_0)$, a contradiction to $b_0 \in Y_f$. If $c_0 \in [h_i, h_{i+1}]$ we have that $c_0 \not \in [h_{j}, h_{j+4}]$ and proceed analogously with the change from $b_0$ to $b'$.

In a next step we analyze Theorem 2 in terms of quantifier complexity.

Proposition 2

Over $(\mathbb {N}, <, R)$ each FO-sentence $\varphi$ is equivalent to a disjunction of sentences

$$\begin{aligned} \forall x \exists y \forall z \ \varphi _i(x,y,z) \wedge \exists x \forall y \exists z \ \psi _i(x,y,z) \end{aligned}$$

where the $\varphi _i, \psi _i$ are bounded in z.

Proof

We analyze the atomic formulas $D^m_R[x,y] = \tau$ in the formula of Theorem 2, in order to reach a sentence in the signature with $<, R$ alone. We can define $D^m_R[x,y] = \tau$ relative to a bound z by a formula $D^m_R[x,y]\upharpoonright z = \tau$ bounded in z. The $D^m_R$-type of [x, y] may change when referring to submodels over domains [0, z] for larger and larger z since more and more R-segments may become visible. However, due to the condition of finite valency, there is a $z_0$ above which no change occurs and where the type $\tau = D^m_R[x,y]$ is reached. This is equivalent to the requirement that $\tau$ occurs for infinitely many z. So we have

$$\begin{aligned} D^m_R[x,y] = \tau \ \Leftrightarrow \ \exists z \forall z' > z \ D^m_R[x,y]\upharpoonright z' = \tau \ \Leftrightarrow \ \forall z \exists z' > z \ D^m_R[x,y]\upharpoonright z' = \tau \end{aligned}$$

Hence we can rewrite the formula of the Normal Form Theorem 2 in the signature with $<, R$, while increasing the alternation of unbounded quantifiers by 1. We arrive at a Boolean combination of $\varSigma _3$-sentences.

From this proposition we can conclude a statement on the recursion theoretic degree of the first-order theory of $(\mathbb {N}, <, R)$ when R is of finite valency and recursive. (We use here and in the sequel basic facts from recursion theory; see, e.g., [Ro67, Od89]).

Theorem 4

If $R \subseteq \mathbb {N}^2$ is recursive and of finite valency, then the first-order theory of $(\mathbb {N}, <, R)$ belongs to level $\varSigma _4 \cap \varPi _4$ of the arithmetical hierarchy.

Proof

It was shown above that each first-order sentence over $(\mathbb {N}, <, R)$, given the assumptions on R, is equivalent to a Boolean combination of $\varSigma _3$-sentences. Thus the first-order theory of $(\mathbb {N}, <, R)$ is Turing-reducible to a complete $\varSigma _3$-set. By the theorem of Kleene and Post on Turing-reducibility this means membership in $\varSigma _4 \cap \varPi _4$.

If R is not recursive, then one can establish a relativized version of the above theorem, obtaining that for a relation R of finite valency, the first-order theory of $(\mathbb {N}, <, R)$ is Turing-reducible to $R'''$, the third jump of R. This gives another perspective on non-definability of addition and multiplication (together): If R is arithmetical, then the FO-theory of $(\mathbb {N}, <, R)$ is arithmetical as well and hence cannot be full first-order arithmetic.

From the results of Sect. 2 we know that for structures $(\mathbb {N}, <, P)$ with unary P, one obtains analogous results but with the levels of recursion theoretic complexity decreased by 1. Let us show that allowing binary R (of finite valency) really leads to a higher complexity.

Theorem 5

There is a $\varPi _3$-complete set that is Turing-reducible to the first-order theory of $(\mathbb {N}, <, R)$ with a suitable recursive relation R of finite valency.

Proof

Consider the following $\varPi _3$-complete set (where $W_n$ is the n-th recursively enumerable set in some effective enumeration):

$$\begin{aligned} V_3 := \{m \mid \forall k \exists \ell > k (\ell \in W_m \wedge W_\ell = \emptyset )\} \end{aligned}$$

So we have $m \in V_3$ iff $W_m$ contains infinitely many indices of the empty set. We build a recursive relation R of finite valency. Let $(\ell _i, m_i)$ the i-th pair in an enumeration of all $(\ell ,m)$ with $\ell \in W_m$.

We construct R in stages: At stage i

• 1. include $(i, i+ m_i +1)$ in R,

• 2. include (i, j) in R for all $j \le i$ with $\ell _j = m_i$, but only if there is no $i'$ with $j < i' < i$ and $(i',j)$ already included in R,

• 3. (i, i) if $\ell _i = m_j$ for some $j \le i$.

The relation R is recursive since for deciding R(a, b) it suffices to run the procedure up to stage $\max (a,b)$. Also R is of finite valency since for any a there are at most three b with R(a, b) or R(b, a). By 1., a pair (i, k) is in R with $i<k$ codes an element of $W_{m_i}$. By 2. and 3., we have a pair $(i', i)$ in R with $i' \ge i$ iff $W_{\ell _i} \not = \emptyset$. Hence $m \in V_3$ iff there are infinitely many $\ell \in W_m$ such that $W_\ell = \emptyset$ iff

$$\begin{aligned} (\mathbb {N}, <, R) \models \forall y \exists x > y \ (R(x, x+m+1) \wedge \forall z \ \lnot R(z,x)) \end{aligned}$$

However, one can sharpen the bound on the level of the arithmetical hierarchy where the FO-theory of $(\mathbb {N}, < , R)$ occurs when working with special relations R: Let us call R effectively of finite valency if the finite sets $N_a = \{b \mid R(a,b)\}$ and $N_b = \{a \mid R(a,b)\}$ are computable from a, b, respectively. It is easy to see that in this case the preceding theorems now hold in precise analogy to the case of unary predicates: The first-order theory of $(\mathbb {N}, <, R)$ is Turing-reducible to a complete $\varSigma _2$-set, and this bound is optimal.

As a last application we mention (without giving the tedious proof) a decidability result. For a monotone function $f: \mathbb {N} \rightarrow \mathbb {N}$ define $\varDelta _f$ by $\varDelta _f(n) = f(n+1) - f(n)$. Call f strongly monotone if $\varDelta _f$ is strictly monotone (in the sense that $x < y$ implies $\varDelta _f(x) < \varDelta _f(y)$). Note that in this case f itself is monotone (and even strictly monotone from the argument 1 onwards). Examples of strongly monotone functions are the natural enumerations of the set of squares, the set of powers of 2, the set of factorial numbers, etc. Each strongly monotone function is injective over the positive natural numbers, hence its graph is of finite valency. A closer analysis (not given here) of Theorem 2 in this context shows the following result:

Theorem 6

If f is strongly monotone and recursive, the first-order theory of ($\mathbb {N}, < , f)$ is decidable.

This result is in an interesting contrast to the case of the MSO-theories of structures $(\mathbb {N}, <, f)$. As Robinson showed in [Ro58], the MSO-theory of $(\mathbb {N}, <, d)$ is undecidable when d is the double function with $d(n) = 2n$. More generally, if we adjoin a unary function f with $f(n) \ge n$ which deviates from the identity in the sense that $\lambda n (f(n) - n)$ is monotone and unbounded, then the MSO-theory of $(\mathbb {N}, <, f)$ is undecidable ([Th75]). So a condition on the growth of unary functions f has opposite effects in FO-logic and MSO-logic.

For the function $f_\mathbb {P}$ given by $f_\mathbb {P}(i) = i$-th prime, $\varDelta _{f_\mathbb {P}}$ is not strictly monotone. Indeed, it is open whether the first-order theory of $(\mathbb {N}, <, f_\mathbb {P})$ is decidable. Note that the twin-prime hypothesis holds iff the sentence

$$\begin{aligned} \forall x \exists y (x < y \wedge f_\mathbb {P}(y) + 2 = f_\mathbb {P}(y+1)) \end{aligned}$$

is true in $(\mathbb {N}, < , f_\mathbb {P})$ (and where successor is defined in terms of $<$).

5 Conclusion

We have outlined a way to approach the first-order theory of a structure $(\mathbb {N}, <, R)$ using the idea of composition when R is of finite valency. It turns out that in the context of first-order logic these structures can be given an “ultimately periodic shape” when considering their m-types only. So, perhaps surprisingly, relations of finite valency show here a similarity to unary predicates.

With more technical work, one obtains analogous results when replacing a single relation R of finite valency by a tuple $(R_1, \ldots , R_n)$ of such relations. On the other hand, it is essential to work with an ordering that is of type $\omega$ or $\omega ^*$. For example, there is a relation R of finite valency over the ordinal $\omega ^2$ such that in the FO-theory of $(\omega ^2, <, R)$ addition and multiplication over the first copy of $\omega$ are definable.

Let us finally mention an open question. As shown in Theorem 5, one can construct recursive relations R of finite valency such that the first-order theory of $(\mathbb {N}, <, R)$ is undecidable. However, these relations are built for the purpose and are based on recursion theoretic concepts. Are there “natural” relations R of finite valency, defined in a way not involving recursion theory, such that the first-order theory of $(\mathbb {N}, <, R)$ is undecidable?

Finally, it should be mentioned that in computer science the study of non-terminating behavior of systems may lead to $\omega$-words equipped with binary relations, induced by connections between separated points of time (e.g. the call and the termination of procedures, or the occurrence of requests and their acknowledgments). It would be interesting to see whether the present work can be applied in such settings.