Introduction↩︎

Skolem arithmetic (denoted by \(Sk\)) is the first order theory of the structure of natural numbers with multiplication, i.e., \(\langle \mathbb{N}; \cdot, = \rangle\). The decidability of this theory was first claimed by Skolem [1], but the first complete proof was published by Mostowski [2]. A few years later Feferman and Vaught published a generalization of Mostowski’s result [3]. Subsequently, the decidability of Skolem arithmetic was also proven using quantifier elimination in some extended language [4]. There are also some other proofs [5]–[7].

Mostowski’s method proceeds by characterizing sets definable in strong and weak powers of first-order theories; in particular, Skolem arithmetic can be regarded as a weak power of Presburger arithmetic [8]. In that framework the principal technical challenge is the elimination of quantifiers.

In this note we restrict attention to Skolem arithmetic itself. However, the presented characterization of definable sets could be also extended to general weak powers. While the high-level idea is reminiscent of Mostowski’s, the characterization and several proof steps differ: in our setting quantifier elimination is routine, and the main difficulty is handling negations (complements).

Preliminaries↩︎

Vectors

Let \(\mathbb{P}\) be the set of prime numbers. Fix \(d \in \mathbb{N}\). We use the following notational convention: for vectors \(\mathbf{u}, \mathbf{v} \in \mathbb{N}^d\) by \(\mathbf{u} \mathbf{v}\) we denote their pointwise product, i.e., \[\begin{pmatrix} u_1 \\ \vdots \\ u_d \end{pmatrix} \begin{pmatrix} v_1 \\ \vdots \\ v_d \end{pmatrix} = \begin{pmatrix} u_1v_1 \\ \vdots \\ u_d v_d \end{pmatrix}.\] Furthermore, for \(p \in \mathbb{P}\) and \(\mathbf{v} = (v_1, \ldots, v_d)^T \in \mathbb{N}^d\) let \(p^{\mathbf{v}} = \begin{pmatrix} p^{v_1}, \ldots, p^{v_d} \end{pmatrix}^T\). For \(N \in \mathbb{N}\) and \(p \in \mathbb{P}\) we denote by \(V_{p}(N)\) the greatest \(n \in \mathbb{N}\) such that \(p^n | N\). For a vector \(\mathbf{v} = (v_1, \ldots, v_d)^T \in \mathbb{N}^d\) we denote \(V_{p}(\mathbf{v}) = (V_{p}(v_1), \ldots, V_{p}(v_d))^T\). Observe that \(\prod_{p \in \mathbb{P}} p^{V_{p}(\mathbf{v})} = \mathbf{v}\).

Let \([d] = \{1, \ldots, d\}\). For \(\mathbf{v} \in \mathbb{N}^d\) and a coordinate \(x \in [d]\) we denote by \(\pi_{x}(\mathbf{v})\) the vector obtain from \(\mathbf{v}\) by projecting away the coordinate \(x\). Moreover, for \(S \subseteq \mathbb{N}^d\) let \(\pi_{x}(S) = \left\{\pi_{x}(\mathbf{v}) \ | \ \mathbf{v} \in S \right\} \subseteq \mathbb{N}^{d-1}\). We use a convention that \(\mathbb{N}^0 = \{\varepsilon\}\), where \(\varepsilon\) is the unique empty tuple, and we denote \(\top = \{\varepsilon\}\). For \(S \subseteq \mathbb{N}\) and a coordinate \(x=1\) let \(\pi_{x}(S) = \top\) if \(S \ne \emptyset\) and \(\pi_{x}(S) = \emptyset\) otherwise.

Let \(i,j \in [d]\). We denote by \(\mathbf{e}_i, \mathbf{e}_{ij} \in \mathbb{N}^d\) the vectors defined as follows: \[\mathbf{e}_{ij}(k) = \begin{cases} 1, \text{ if } k = i \text{ or } k = j \\ 0, \text{ if } k \ne i,j \end{cases} \qquad \mathbf{e}_{i}(k) = \begin{cases} 1, \text{ if } k = i \\ 0, \text{ if } k \ne i \end{cases} .\] We assume a convection that \(\mathbf{e}_{ij} = \mathbf{e}_i\) if \(i = j\).

Graph matchings

In this paragraph we present a graph theoretic lemma that we will use. Recall that \(G = (L \cup R, E)\) is a bipartite graph if \(E \subseteq L \times R\). A matching of a set \(S \subseteq L \cup R\) of nodes is a set \(M \subseteq E\) of pairwise non-adjacent edges that covers all nodes in \(S\).

Definable sets↩︎

We assume that the reader is familiar with Presburger arithmetic and semilinear sets [8], [10]. We say that a set \(S \subseteq \mathbb{N}^d\) is skolemian if there exist semilinear sets \(\alpha_1, \ldots, \alpha_n, \alpha \subseteq \mathbb{N}^d\) with \(\mathbf{0} \in \alpha\) and \(\mathbf{0} \not\in \alpha_i\) for \(i \in [n]\) such that \[S = \left\{ p_1^{\mathbf{v}_1} \ldots p_n^{\mathbf{v}_n} q_1^{\mathbf{u}_1} \ldots q_k^{\mathbf{u}_k} \ | \k \in \mathbb{N}, \; \mathbf{v}_i \in \alpha_i, \; \mathbf{u}_j \in \alpha \text{ for } i \in [n], j \in [k] \right\},\] where \(p_1, \ldots, p_n, q_1, \ldots, q_n\) range over pairwise distinct prime numbers. In other words, \(\mathbf{w} \in S\) if and only if there exist pairwise distinct primes \(p_1, \ldots, p_n\) such that \(V_{p_i}(\mathbf{w}) \in \alpha_i\) for \(i \in [n]\) and \(V_{q}(\mathbf{w}) \in \alpha\) for all other \(q \in \mathbb{P}\) with \(V_{q}(\mathbf{w}) \neq \mathbf{0}\). We say that formulas \(\alpha_1, \ldots, \alpha_n, \alpha\) define the skolemian set \(S\), and we write \(S = \textrm{Def}(\alpha_1, \ldots, \alpha_n; \alpha)\). In particular, if \(n=0\) then we write \(S = \textrm{Def}(\alpha)\).

A set \(S\) is semiskolemian if there are skolemian sets \(S_1, \ldots, S_m\) such that \(S = \bigcup_{i=1}^m S_m\).

Now we are ready to formulate the main theorem of this note.

We will omit the proof of the easier implication: every semiskolemian set is definable in Skolem arithmetic. Now we focus on the reverse implication. The proof is by induction. If suffices to show that atomic formulas define semiskolemian sets, and if sets defined by formulas \(\Phi\), \(\Psi\) are semiskolemian then also sets defined by \(\Phi \wedge \Psi\), \(\neg \Phi\) and \(\exists_X \Phi\) are so, assuming that \(X\) is a free variable of \(\Phi\). The three properties are equivalent to the following closure properties of semiskolemian sets: closure under intersection, complement and projecting away a coordinate.

Note that we could prove that semiskolemian sets are closed under union instead of intersection. The closure under union follows directly from the definition of semiskolemian sets. However, we prove the closure under intersection anyway, as the proof of closure under complement will use this fact.

Closure properties↩︎

This section is devoted to the proofs of closure properties of semiskolemian sets. We start with proving that atomic formulas of Skolem arithmetic define semiskolemian sets.

• Equality

  Suppose that \(S \subseteq \mathbb{N}^d\) is defined by a formula \(x_i=x_j\), where \(x_i, x_j\) are variables corresponding to coordinates \(i,j \in [d]\), respectively. Let \(\alpha\) be a semilinear set defined by a Presburger formula \(x_i = x_j\). Roughly speaking, two nonnegative integers are equal if and only if each prime appears with the same exponent in the factorization of both. Hence, \[S = \textrm{Def}(\alpha).\]

• Multiplication

  This case is similar to the previous one. Suppose that \(S \subseteq \mathbb{N}^d\) is defined by a formula \(x_i \cdot x_j = x_k\), where \(x_i, x_j, x_k\) are variables corresponding to coordinates \(i,j,k \in [d]\), respectively. Note that \(i,j,k\) are not necessarily pairwise different. Let \(\alpha\) be a semilinear set defined by a Presburger formula \(x_i + x_j = x_k\). We observe that \[S = \textrm{Def}(\alpha).\]

• Intersection

  Observe that \(\left(\bigcup_{i \in I} S_i\right) \cap \left(\bigcup_{j \in J} S_j'\right) = \bigcup_{i \in I, j \in J} S_i \cap S_j'\). Hence, it suffices to prove that intersection of two skolemian sets is semiskolemian.

  Let \(S = \textrm{Def}(\alpha_1, \ldots, \alpha_{n}; \alpha)\) and \(S' = \textrm{Def}(\beta_1, \ldots, \beta_{m}; \beta)\) for semilinear sets \(\alpha_1, \ldots, \alpha_{n}, \alpha\) and \(\beta_1, \ldots, \beta_{m}, \beta\). We call a subset \(P\) of \((\{0\} \cup [n]) \times (\{0\}\cup [m])\) correct if the following condition is satisfied: for every \(i \in [n]\) there exists exactly one \(j \in \{0\} \cup [m]\) such that \((i, j) \in P\) and for every \(j \in [m]\) there exists exactly one \(i \in \{0\} \cup [n]\) such that \((i, j) \in P\). Denote by \(\mathcal{P}\) the family of all correct sets. Then the set \(S \cap S'\) is represented as semiskolemian set as follows \[S \cap S' = \bigcup_{P \in \mathcal{P}} \textrm{Def}\left(\left(\alpha_i \cap \beta_j\right)_{(i,j) \in P}; \alpha \cap \beta \right).\] Indeed, if \(P\) is correct then any element of \(\textrm{Def}\left(\left(\alpha_i \cap \beta_j\right)_{(i,j) \in P}; \alpha \cap \beta \right)\) belongs to both \(S\) and \(S'\). On the other hand, for every \(\mathbf{w} \in S \cap S'\) there exists \(P \in \mathcal{P}\) which witness that \(\mathbf{w}\) belongs to the above semiskolemian set.

• Complement

  For a set \(A \subseteq \mathbb{N}^d\) let \(A^c = \mathbb{N}^d \setminus A\). Observe that \((\bigcup_{i = 1}^{m} S_i)^c = \bigcap_{i=1}^m S_i^c\). As we already proved that semiskolemian sets are closed under intersection, it suffices to show that a complement of a skolemian set is semiskolemian.

  Let \(\mathbf{w} \in \mathbb{N}^d\) and \(S = \textrm{Def}(\alpha_1, \ldots, \alpha_n; \alpha)\). Let \(P\) be the set of primes \(p\) satisfying \(V_{p}(\mathbf{w}) \neq \mathbf{0}\) and \(P_0 \subseteq P\) be its subset that consists of primes \(p\) such that \(V_{p}(\mathbf{w}) \not\in \alpha\). Consider a bipartite graph \(G = (P \cup [n], E)\), where \((p, i) \in E\) if and only if \(V_{p}(\mathbf{w}) \in \alpha_i\). We will use the following fact.

  Claim 2. \(\mathbf{w} \in S\) if and only if the following conditions are satisfied:

  1. there is a matching of \(P_0\) in \(G\);

  2. there is a matching of \([n]\) in \(G\).

  Proof. Observe that if \(\mathbf{w} \in S\) then conditions (a),(b) are satisfied. Let us focus on the opposite direction.

  From Lemma 1 we conclude that there exists a matching \(M\) of \(P_0 \cup [n]\) in \(G\). Let \(p_i \in P\) be the prime such that \((p_i, i) \in M\) for \(i \in [n]\). Observe that \(V_{q}(\mathbf{w}) \in \alpha\) for every \(q \in P \setminus P_0\). Therefore, \[\mathbf{w} = \prod_{i \in [n]} p_i^{V_{p_i}(\mathbf{w})} \prod_{q \in P \setminus \{p_1, \ldots, p_n\}} q^{V_{q}(\mathbf{w})} \in S.\] Indeed, \(V_{p_i}(\mathbf{w}) \in \alpha_{i}\) for \(i \in [n]\) and \(V_{q}(\mathbf{w}) \in \alpha\) for \(q \in P \setminus \{p_1, \ldots, p_n\}\). ◻

  We continue the proof that a complement of a skolemian set is semiskolemian. Let \(S = \textrm{Def}(\alpha_1, \ldots, \alpha_n; \alpha)\). Then \(\mathbf{w} \not\in S\) if and only if one of conditions (a),(b) from Claim 2 is not satisfied. Let \(S_a, S_b \subseteq \mathbb{N}^d\) be the sets of vectors that does not satisfy conditions (a), (b) respectively. As \(S^c = S_a \cup S_b\), it suffices to show that sets \(S_a, S_b\) are semiskolemian.

  • (a) fails

    There may be two reasons why (a) does not hold. The first one is that \(|P_0| > n\). We define the set of vectors \(\mathbf{w}\) such that \(V_{p}(\mathbf{w}) \not\in \alpha\) for at least \(n+1\) primes \(p\): \[\textrm{Def}(\underbrace{\alpha^c, \ldots, \alpha^c}_{n+1}; \mathbb{N}^d).\] In the second case we assume that there is no matching of \(P_0\) in \(G\) but \(|P_0| \leq n\). From the Hall’s theorem we conclude that there exists \(P_0' \subseteq P_0\) with \(|P_0'| = n' \leq n\) such that for less than \(n'\) indexes \(i \in [n]\) the condition \(p \in \alpha_i\) is satisfied for some \(p \in P_0'\). Equivalently, there is \(n-n'+1\) sets out of \(\{\alpha_1, \ldots, \alpha_n\}\) and \(n'\) primes \(p \in P\) such that \(V_{p}(\mathbf{w})\) neither belongs to any of these sets nor to \(\alpha\). For \(I \subseteq [n]\) let \(\beta_I := \alpha^c \cap \bigcap_{i \in I} \alpha_i^c\). Then we define the set of vectors \(\mathbf{w}\) satisfying this condition as follows: \[\bigcup_{n' \leq n} \; \bigcup_{\substack{I \subseteq [n] \\ |I| = n-n'+1}} \textrm{Def}(\underbrace{\beta_I, \ldots, \beta_I}_{n'}; \mathbb{N}^d).\]

  • (b) fails

    Again we use the Hall’s theorem to conclude that there exists \(I \subseteq [n]\) with the property that there is less than \(|I|\) primes \(p \in P\) such that \(V_{p}(\mathbf{w})\) belongs to some set from the family \(\left\{\alpha_i \ | \ i \in I \right\}\). Let \(\gamma_I = \bigcup_{i \in I} \alpha_i\). Then \[S_b = \bigcup_{I \subseteq [n]} \;\bigcup_{n' < |I|} \textrm{Def}(\underbrace{\gamma_I, \ldots, \gamma_I}_{n'}; \gamma_I^c).\]

• Projecting away a coordinate

  It suffices to prove that a set obtained by projecting away a coordinate from a skolemian set is skolemian. Suppose that \(S = \textrm{Def}(\alpha_1, \ldots, \alpha_n ; \alpha)\) and \(x \in [d]\) is a coordinate. Then \[\pi_{x}(S) = \textrm{Def}(\pi_{x}(\alpha_1), \ldots, \pi_{x}(\alpha_n) ; \pi_{x}(\alpha)).\]

Conclusion↩︎

Theorem 1 implies the following decidability result.

References↩︎