July 06, 2026
We study sets and functions definable in the three additive theories \(\mathrm{FO}(\mathbb{Z},+,\leq)\), \(\mathrm{FO}(\mathbb{R},+,\leq)\), and \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\).
The Ginsburg–Spanier theorem [1] characterizes \(\mathrm{FO}(\mathbb{Z},+,\leq)\)-definable sets as exactly the semi-linear sets. We extend this characterization in two directions.
First, we show that \(\mathrm{FO}(\mathbb{Z},+,\leq)\)-definable functions are exactly the piecewise linear functions (Theorem [thm:integer]), and that \(\mathrm{FO}(\mathbb{R},+,\leq)\)-definable functions are also exactly the piecewise linear functions (Theorem [thm:real]). The proofs are direct algebraic arguments using only a stability lemma and the Ginsburg–Spanier theorem.
Second, we introduce semi-polinear sets as the \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\) analogue of semi-linear sets, and prove that the class of mixed-linear sets and the class of semi-polinear sets coincide (Theorem [thm:mixed-sets]). We further show that \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\)-definable functions are exactly the piecewise-simple functions (Theorem [thm:mixed-functions]), a new class of functions that are linear in the integer part and in the fractional part of the argument, but with potentially different linear coefficients for each.
These algebraic characterizations unify the three theories in a single framework, and the proofs are purely algebraic, without reference to automata or machines.
Presburger arithmetic \(\mathrm{FO}(\mathbb{Z},+,\leq)\) [2] is the decidable first-order theory of the integers with addition and order. The Ginsburg–Spanier theorem [1] characterizes its definable sets as exactly the semi-linear sets, i.e., finite unions of linear sets. The real additive theory \(\mathrm{FO}(\mathbb{R},+,\leq)\) is decidable via Fourier–Motzkin elimination, with definable sets being exactly the finite unions of polyhedral convex sets [3]. The mixed additive theory \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\) was shown decidable by Weispfenning [4] via quantifier elimination, and later by Boigelot, Jodogne and Wolper [5] via an alternative approach using weak Büchi automata.
Concerning Presburger functions, prior work studied computability by flat (without nested loops) counter automata [6]–[8] or by reversal-bounded counter automata [9], closure under composition [10], and evaluation in linear space and quadratic time [11].
The three additive theories \(\mathrm{FO}(\mathbb{Z},+,\leq)\), \(\mathrm{FO}(\mathbb{R},+,\leq)\), and \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\) are well-studied logics with applications across verification, model checking, and constraint solving. A natural question is: what are the functions definable in these logics, described in purely geometric terms? Prior characterizations of Presburger-definable functions all relied on operational or logical descriptions — flat counter automata [6]–[8] or reversal-bounded counter automata [9], closure under composition [10], or logical normal forms — and the same holds for the mixed theory via quantifier elimination [4] or Büchi automata [5]. Surprisingly, a direct geometric answer was missing from the literature.
| \(\FO(\Z,+,\leq)\) | \(\FO(\R,+,\leq)\) | \(\FO(\R,\Z,+,\leq)\) | |
|---|---|---|---|
| Decidability | [2], 2-EXPSPACE [12], [13] | via Fourier–Motzkin QE | [4], [5] |
| Logic / QE | Cooper; singly-exp. [14] | Fourier–Motzkin | extended logic [4] |
| Automata | counter automata [6], [7], [9] | — | weak Büchi aut. [5] |
| Sets | semi-linear [1] | polyhedral convex [3] | semi-polinear |
| Functions | piecewise linear | piecewise linear | piecewise-simple |
The Ginsburg–Spanier theorem [1] is the starting point. Weispfenning [4] describes mixed-linear sets but with an error corrected here (Remark 11). The piecewise linear characterization of \(\mathrm{FO}(\mathbb{Z},+,\leq)\)-definable functions is implicitly present in the literature (applying [1] to \(G_f\)) but was never stated explicitly as a theorem with a direct algebraic proof.
(1) Presburger functions are piecewise linear. A function is definable in \(\mathrm{FO}(\mathbb{Z},+,\leq)\) if and only if it is piecewise linear on a Presburger partition of its domain (Theorem 5). The proof uses only a stability argument and the Ginsburg–Spanier theorem.
(2) Extension of the Ginsburg–Spanier theorem to the mixed theory. We introduce semi-polinear sets as the \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\) analogue of semi-linear sets (Theorem 10), and show that functions definable in \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\) are exactly the piecewise-simple functions (Theorem 14). We correct an error in Weispfenning [4] regarding the structure of mixed-linear sets of \(\mathbb{R}\) (Remark 11).
The proofs rely on standard techniques from linear algebra and the Ginsburg–Spanier theorem, and may appear elementary. We argue that the results are nonetheless of real interest. First, they are new: despite the maturity of the field, no paper had stated the piecewise-linear or piecewise-simple characterizations as explicit theorems with direct algebraic proofs. Second, the proofs are self-contained and short, making the results easy to verify and teach. Third, they unify three theories in a single geometric framework, as Table 1 illustrates: the algebraic row was the only one missing. Fourth, we correct an error in the only prior work on mixed-linear sets [4]. Fifth, the notions of piecewise-linear and piecewise-simple functions are defined without reference to logic or automata, making them useful independently in verification, synthesis, and constraint solving.
Section 2 introduces notations and the three logics of interest. Section 3 characterizes definable functions in the real additive theory. Section 4 characterizes definable functions in the integer additive theory, recalling the Ginsburg–Spanier theorem. Section 5 introduces semi-polinear sets and proves the extension of the Ginsburg–Spanier theorem to the mixed case, then characterizes mixed definable functions as piecewise-simple functions.
We denote by \(\mathbb{R}\), \(\mathbb{Q}\), \(\mathbb{Q}_{+}\), \(\mathbb{Z}\), \(\mathbb{N}\) the set of real numbers, the set of rational values, the set of non-negative rational values, the set of integers, and the set of non-negative integers. The \(i\)-th component of a vector \(\vec{x}\) is denoted by \(\vec{x}[i]\). The integer-part function \([\cdot] : \mathbb{R}\to \mathbb{Z}\) is defined by \([x] = \max\{k \in \mathbb{Z}\mid k \leq x\}\); for \(\vec{a} \in \mathbb{R}^n\), \([\vec{a}]\) denotes the component-wise integer part. Functions \(f : X \to Y\) are partially defined over definition domains \(\mathrm{dom}(f) \subseteq X\). The graph of \(f\) is the set \(G_f = \{(x,y) \in X \times Y \mid x \in \mathrm{dom}(f) \wedge y = f(x)\}\). The restriction of \(f : X \to Y\) to a subset \(D \subseteq \mathrm{dom}(f)\) is denoted by \(f|_D : X \to Y\).
Lemma 1. Decompositions of \(G_f\) into finite unions \(G_f = G_1 \cup \cdots \cup G_k\) correspond to decompositions of \(\mathrm{dom}(f)\) into finite unions \(\mathrm{dom}(f) = D_1 \cup \cdots \cup D_k\) where \(G_i\) is the graph of \(f_i\) with \(f_i = f|_{D_i}\).
Proof. Given \(G_f = G_1 \cup \cdots \cup G_k\), set \(D_i = \{\vec{x} \mid \exists \vec{y} : (\vec{x},\vec{y}) \in G_i\}\). Since \(G_f\) is a function graph, each \(G_i \subseteq G_f\) is also a function graph (a point \((\vec{x},\vec{y}_1) \in G_i\) and \((\vec{x},\vec{y}_2) \in G_f\) force \(\vec{y}_1 = \vec{y}_2\)), and \(G_i\) is the graph of \(f|_{D_i}\). ◻
The first-order logics \(\mathrm{FO}(\mathbb{Z},+,\leq)\), \(\mathrm{FO}(\mathbb{R},+,\leq)\), and \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\) are respectively called the integer additive theory, the real additive theory, and the mixed additive theory. Let \(\mathcal{L}\) be one of these theories and \(D \subseteq \mathbb{R}^n\). A finite partition \(\Pi = \{X_1,\ldots,X_k\}\) of \(D\) is said definable in \(\mathcal{L}\) if \(X_i\) is definable in \(\mathcal{L}\) for any \(i\).
A function \(f : \mathbb{R}^n \to \mathbb{R}^q\) is said definable in \(\mathcal{L}\) if there exists a formula \(\psi(\vec{x},\vec{y})\) in \(\mathcal{L}\) encoding its graph \(G_f\). Observe that deciding if \(\psi(\vec{x},\vec{y})\) encodes the graph of a function reduces to the non-satisfiability of: \[\psi(\vec{x},\vec{y}_1) \wedge \psi(\vec{x},\vec{y}_2) \wedge \vec{y}_1 \neq \vec{y}_2.\] As the logic \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\) is decidable [4], this property is decidable.
Let \(f : \mathbb{R}^n \to \mathbb{R}^q\). We say that \(f\) is \(\mathbb{Q}\)-linear (or simply linear) if there exist a matrix \(M \in \mathbb{Q}^{q \times n}\) and a vector \(\vec{v} \in \mathbb{Q}^q\) such that \(f(\vec{a}) = M\vec{a} + \vec{v}\) for any \(\vec{a} \in \mathrm{dom}(f)\). We call such functions linear even though they are sometimes called affine in other contexts. We say that \(f\) is piecewise \(\mathbb{Q}\)-linear (or simply piecewise linear) if there exists a finite partition \(\Pi\) of \(\mathrm{dom}(f)\) such that \(f|_X\) is \(\mathbb{Q}\)-linear for any \(X \in \Pi\); if \(\Pi\) is definable in \(\mathcal{L}\), we say that \(f\) is \(\mathcal{L}\)-piecewise linear.
We say that \(f\) is stable by addition (or simply stable) if \(\vec{a}_1 + \vec{a}_2 \in \mathrm{dom}(f)\) and \(f(\vec{a}_1 + \vec{a}_2) = f(\vec{a}_1) + f(\vec{a}_2)\) for any \(\vec{a}_1, \vec{a}_2 \in \mathrm{dom}(f)\).
This section establishes two results: that stable functions with rational graphs are linear (Proposition 1), and that functions definable in \(\mathrm{FO}(\mathbb{R},+,\leq)\) are exactly the piecewise linear ones (Theorem 3).
We first recall some elements of linear algebra. A \(\mathbb{Q}\)-vector space (or simply a vector space) of \(\mathbb{Q}^n\) is a set \(V \subseteq \mathbb{Q}^n\) such that (1) \(\vec{0} \in V\), (2) \(\vec{v}_1 + \vec{v}_2 \in V\) for any \(\vec{v}_1, \vec{v}_2 \in V\), and (3) \(\lambda\vec{v}\) is in \(V\) for any \(\lambda \in \mathbb{Q}\) and any \(\vec{v} \in V\). A basis of a vector space \(V\) is a finite (potentially empty) sequence \((\vec{v}_1,\ldots,\vec{v}_d)\) of \(d\) vectors in \(V\) such that for any \(\vec{v} \in V\) there exists a unique sequence \((\lambda_1,\ldots,\lambda_d)\) of elements in \(\mathbb{Q}\) satisfying \(\vec{v} = \sum_{i=1}^d \lambda_i \vec{v}_i\).
Proposition 1. For any stable function \(f : \mathbb{R}^n \to \mathbb{R}^q\) with \(G_f \subseteq \mathbb{Q}^n \times \mathbb{Q}^q\), there exists a matrix \(M \in \mathbb{Q}^{q \times n}\) such that \(f(\vec{a}) = M\vec{a}\) for any \(\vec{a} \in \mathrm{dom}(f)\).
Proof. As \(G_f \subseteq \mathbb{Q}^n \times \mathbb{Q}^q\), we deduce that \(\mathrm{dom}(f) \subseteq \mathbb{Q}^n\). Let us consider the vector space \(V\) generated by \(\mathrm{dom}(f)\). There exists a basis \((\vec{a}_1,\ldots,\vec{a}_d)\) of \(V\) such that \(\vec{a}_i \in \mathrm{dom}(f)\) for any \(i\). As \(G_f \subseteq \mathbb{Q}^n \times \mathbb{Q}^q\) we deduce that \(f(\vec{a}_i) \in \mathbb{Q}^q\) for any \(i\). As \((\vec{a}_1,\ldots,\vec{a}_d)\) is a basis of \(V\) and \((f(\vec{a}_1),\ldots,f(\vec{a}_d))\) is a sequence of vectors in \(\mathbb{Q}^q\), there exists a matrix \(M \in \mathbb{Q}^{q \times n}\) such that \(M\vec{a}_i = f(\vec{a}_i)\) for any \(i\).
Let us prove that \(f(\vec{a}) = M\vec{a}\) for any \(\vec{a} \in \mathrm{dom}(f)\). Since the case \(d = 0\) is immediate we assume \(d \geq 1\). Let \(\vec{a} \in \mathrm{dom}(f)\). As \(\mathrm{dom}(f) \subseteq V\) and \((\vec{a}_1,\ldots,\vec{a}_d)\) is a basis of \(V\), there exists \((\lambda_1,\ldots,\lambda_d)\) in \(\mathbb{Q}^d\) such that \(\vec{a} = \sum_{i=1}^d \lambda_i \vec{a}_i\). Let \(r \geq 1\) be large enough so that \(r\lambda_i \in \mathbb{Z}\) for any \(i\). There exist \(\mu_i^+, \mu_i^- \in \mathbb{N}\) such that \(r\lambda_i = \mu_i^+ - \mu_i^-\). We deduce: \[r\vec{a} + \sum_{i=1}^d \mu_i^- \vec{a}_i = \sum_{i=1}^d \mu_i^+ \vec{a}_i.\] The image by \(f\) of the two previous vectors can be developed thanks to the stability of \(f\) by addition: \[rf(\vec{a}) + \sum_{i=1}^d \mu_i^- f(\vec{a}_i) = \sum_{i=1}^d \mu_i^+ f(\vec{a}_i).\] By replacing \(\mu_i^+ - \mu_i^-\) by \(r\lambda_i\) in the previous equality, we get \(f(\vec{a}) = M\vec{a}\). ◻
A \(\mathbb{Q}\)-polyhedral convex set of \(\mathbb{R}^n\) (or simply a polyhedral convex set) is a set \(C \subseteq \mathbb{R}^n\) such that there exists a finite (potentially empty) sequence \((\vec{\alpha}_j, \#_j, \beta_j)_{1 \leq j \leq k}\) of tuples in \(\mathbb{Q}^n \times \{<,\leq,=,\geq,>\} \times \mathbb{Q}\) satisfying: \[C = \Bigl\{ \vec{c} \in \mathbb{R}^n \;\Big|\; \forall j\; \sum_{i=1}^n \vec{\alpha}_j[i]\,\vec{c}[i] \;\#_j\; \beta_j \Bigr\}.\] The Fourier–Motzkin elimination shows that the following set \(\exists_i C\) is effectively polyhedral convex for any polyhedral convex set \(C \subseteq \mathbb{R}^n\) and \(1 \leq i \leq n\): \[\exists_i C = \{(c_1,\ldots,c_{i-1},c_{i+1},\ldots,c_n) \in \mathbb{R}^{n-1} \mid \exists c_i \in \mathbb{R}\;(c_1,\ldots,c_n) \in C\}.\] In particular \(\mathrm{FO}(\mathbb{R},+,\leq)\) admits a quantifier elimination algorithm and we deduce that a set is definable in \(\mathrm{FO}(\mathbb{R},+,\leq)\) if and only if it is equal to a finite union of polyhedral convex sets.
Lemma 2. Non-empty polyhedral convex sets of \(\mathbb{R}^n\) contain vectors in \(\mathbb{Q}^n\).
Proof. The proof is by induction over \(n\). For \(n = 1\): a non-empty polyhedral convex set \(C \subseteq \mathbb{R}\) is an interval with bounds in \(\mathbb{Q}\cup \{-\infty,+\infty\}\). If \(C\) contains a unique value then this value is in \(\mathbb{Q}\). Otherwise, \(C\) contains two values \(l < h\), so \(]l,h[ \subseteq C\), and by density of \(\mathbb{Q}\) in \(\mathbb{R}\) there exists \(c \in \mathbb{Q}\) with \(l < c < h\), hence \(c \in C\). For the induction step, given a non-empty polyhedral convex set \(C' \subseteq \mathbb{R}^{n+1}\), let \(I = \exists_{1,\ldots,n} C'\). Fourier–Motzkin shows \(I\) is polyhedral convex and non-empty, so there exists \(c_{n+1} \in I \cap \mathbb{Q}\). The set \(C = \exists_{n+1}\{\vec{x} \in C' \mid \vec{x}[n+1] = c_{n+1}\}\) is polyhedral convex and non-empty, so by induction hypothesis there exists \((c_1,\ldots,c_n) \in C \cap \mathbb{Q}^n\). Then \((c_1,\ldots,c_{n+1}) \in C' \cap \mathbb{Q}^{n+1}\). ◻
Proposition 2. \(C \cap \mathbb{Q}^n\) is dense in \(C\) for any polyhedral convex set \(C\) of \(\mathbb{R}^n\).
Proof. Let \(\vec{c} \in C\). As \(\mathbb{Q}\) is dense in \(\mathbb{R}\), there exist sequences \((\vec{l}_k)_{k \geq 0}\) and \((\vec{h}_k)_{k \geq 0}\) in \(\mathbb{Q}^n\) converging toward \(\vec{c}\) with \(\vec{l}_k[i] \leq \vec{c}[i] \leq \vec{h}_k[i]\) for all \(i\). The set \(C_k = \{\vec{x} \in C \mid \bigwedge_i \vec{l}_k[i] \leq \vec{x}[i] \leq \vec{h}_k[i]\}\) is non-empty since \(\vec{c} \in C_k\). By Lemma 2, there exists \(\vec{c}_k \in C_k \cap \mathbb{Q}^n\), and the limit of \((\vec{c}_k)_{k \geq 0}\) is \(\vec{c}\). ◻
Theorem 3. Definable functions in \(\mathrm{FO}(\mathbb{R},+,\leq)\) are exactly the \(\mathrm{FO}(\mathbb{R},+,\leq)\)-piecewise linear functions.
Proof. Let \(f : \mathbb{R}^n \to \mathbb{R}^q\) with \(G_f\) definable in \(\mathrm{FO}(\mathbb{R},+,\leq)\). We deduce that \(G_f\) can be decomposed into a finite union of polyhedral convex sets. From Lemma 1, we can assume that \(G_f\) is a polyhedral convex set. As \(\mathrm{dom}(f) = \exists_{n+1,\ldots,n+q} G_f\), Fourier–Motzkin elimination shows that \(\mathrm{dom}(f)\) is polyhedral convex, hence definable in \(\mathrm{FO}(\mathbb{R},+,\leq)\). If \(\mathrm{dom}(f)\) is empty the proof is immediate. Otherwise, from Lemma 2 there exists \(\vec{d}_0 \in \mathrm{dom}(f) \cap \mathbb{Q}^n\), and for any \(\vec{d} \in \mathrm{dom}(f) \cap \mathbb{Q}^n\), since \((\vec{d}, f(\vec{d}))\) is the unique vector of \(G_f \cap (\{\vec{d}\} \times \mathbb{R}^q)\), Lemma 2 gives \(f(\vec{d}) \in \mathbb{Q}^q\).
Let \(D = \{(\vec{x},z) \in \mathbb{Q}^n \times (\mathbb{Q}_{+}\setminus \{0\}) \mid \vec{d}_0 + \frac{\vec{x}}{z} \in \mathrm{dom}(f)\}\) and \(h : \mathbb{R}^n \times \mathbb{R}\to \mathbb{R}^q\) defined over \(D\) by \(h(\vec{x},z) = z(f(\vec{d}_0 + \frac{\vec{x}}{z}) - f(\vec{d}_0))\). The convexity of \(G_f\) shows that \(h\) is stable by addition. Since \(D \subseteq \mathbb{Q}^n \times \mathbb{Q}_{+}\) and \(f\) maps \(\mathrm{dom}(f) \cap \mathbb{Q}^n\) into \(\mathbb{Q}^q\) (established above), we have \(G_h \subseteq \mathbb{Q}^{n+1} \times \mathbb{Q}^q\). Proposition 1 then gives a matrix \(N \in \mathbb{Q}^{q \times (n+1)}\) such that \(h(\vec{x},z) = N(\vec{x},z)\) for any \((\vec{x},z) \in \mathrm{dom}(h)\).
For any \(\vec{d} \in \mathrm{dom}(f) \cap \mathbb{Q}^n\), let \(\vec{x} = \vec{d} - \vec{d}_0\) and \(z = 1\). We get \(f(\vec{d}) = f(\vec{d}_0) + N(\vec{d} - \vec{d}_0, 1)\), so there exist \(M \in \mathbb{Q}^{q \times n}\) and \(\vec{v} \in \mathbb{Q}^q\) with \(f(\vec{d}) = M\vec{d} + \vec{v}\) for any \(\vec{d} \in \mathrm{dom}(f) \cap \mathbb{Q}^n\).
Finally, Proposition 2 shows that \(G_f \cap (\mathbb{Q}^n \times \mathbb{Q}^q)\) is dense in \(G_f\). There is a sequence \((\vec{a}_i, f(\vec{a}_i))_{i \geq 0}\) in \(G_f \cap (\mathbb{Q}^n \times \mathbb{Q}^q)\) converging to \((\vec{c}, f(\vec{c}))\). Since \(\vec{x} \mapsto M\vec{x} + \vec{v}\) is linear, it is continuous. Therefore \(f(\vec{a}_i) = M\vec{a}_i + \vec{v} \to M\vec{c} + \vec{v}\), and thus \(f(\vec{c}) = M\vec{c} + \vec{v}\). ◻
A set \(L \subseteq \mathbb{Z}^n\) is said linear [1] if there exist a vector \(\vec{b} \in \mathbb{Z}^n\) and a finite set \(P \subseteq \mathbb{Z}^n\) such that \(L = \vec{b} + P^*\) where \(P^*\) is the submonoid of \((\mathbb{Z}^n,+)\) generated by \(P\). Recall [1] that sets definable in \(\mathrm{FO}(\mathbb{Z},+,\leq)\) are exactly the finite unions of linear sets (also called semi-linear sets).
Theorem 4 ([1]). The sets definable in \(\mathrm{FO}(\mathbb{Z},+,\leq)\) are exactly the semi-linear sets.
This characterization shows that the Presburger sets are exactly the rational sets of \((\mathbb{Z}^n,+)\).
Theorem 5. Definable functions in \(\mathrm{FO}(\mathbb{Z},+,\leq)\) are exactly the \(\mathrm{FO}(\mathbb{Z},+,\leq)\)-piecewise linear functions.
Proof. Let \(f : \mathbb{Z}^n \to \mathbb{Z}^q\) such that \(G_f\) is definable in \(\mathrm{FO}(\mathbb{Z},+,\leq)\). Since \(G_f\) is definable in \(\mathrm{FO}(\mathbb{Z},+,\leq)\), Theorem 4 gives a decomposition of \(G_f\) into a finite union of linear sets. From Lemma 1, we can assume that \(G_f\) is a linear set. Since \(\mathrm{dom}(f) = \exists_{n+1,\ldots,n+q} G_f\) we deduce that \(\mathrm{dom}(f)\) is definable in \(\mathrm{FO}(\mathbb{Z},+,\leq)\). As \(G_f\) is a linear set, there exists \((\vec{x}_0,\vec{y}_0) \in \mathbb{Z}^n \times \mathbb{Z}^q\) and a finite set \(P \subseteq \mathbb{Z}^n \times \mathbb{Z}^q\) such that \(G_f = (\vec{x}_0,\vec{y}_0) + P^*\). We consider the function \(h\) defined over \(\mathrm{dom}(h) = \mathrm{dom}(f) - \vec{x}_0\) by \(h(\vec{d}) = f(\vec{x}_0 + \vec{d}) - \vec{y}_0\) for any \(\vec{d} \in \mathrm{dom}(h)\). By definition of \(h\), we have \(G_h = G_f - (\vec{x}_0,\vec{y}_0) = P^*\), so \(h\) is stable by addition and \(G_h \subseteq \mathbb{Q}^n \times \mathbb{Q}^q\). Proposition 1 proves that there exists \(M \in \mathbb{Q}^{q \times n}\) such that \(h(\vec{d}) = M\vec{d}\) for any \(\vec{d} \in \mathrm{dom}(h)\). Now let \(\vec{x} \in \mathrm{dom}(f)\) and \(\vec{d} = \vec{x} - \vec{x}_0\). From \(h(\vec{d}) = M\vec{d}\) and \(h(\vec{d}) = f(\vec{x}_0 + \vec{d}) - \vec{y}_0\) we deduce \(f(\vec{x}) = M\vec{x} + \vec{v}\) where \(\vec{v} = \vec{y}_0 - M\vec{x}_0\). Therefore \(f\) is linear. ◻
Remark 6. In contrast to the operational characterizations of Presburger functions via counter automata [6], [7], [9] and the composition-closure results of [10], Theorem 5 provides a direct algebraic normal form using only linear algebra and the Ginsburg–Spanier theorem.
Remark 7. The piecewise linear characterization is implicitly present in the literature: applying [1] to the graph \(G_f \subseteq \mathbb{Z}^n \times \mathbb{Z}^q\) yields a semilinear decomposition from which linearity on each piece follows by the above argument. However, this consequence was never stated explicitly as a theorem with a direct proof.
We fix a countable set \(\mathcal{X}\) of variables. Valuations are totally-defined functions \(v : \mathcal{X} \to \mathbb{R}\) and we write \(v \models \phi\) if \(v\) satisfies a formula \(\phi\). When \(\phi\) is a formula of the mixed linear arithmetic, the denoted set \(S \subseteq \mathbb{R}^n\) is said to be mixed-linear.
In [4], Weispfenning showed that the mixed-linear arithmetic is decidable via a quantifier elimination algorithm for an effectively equivalent extended logic. The description of mixed-linear sets in [4] is incomplete; Theorem 10 below provides the correct characterization via semi-polinear sets (see Remark 11).
Let us recall that a finitely generated monoid is a subset \(M \subseteq \mathbb{Z}^n\) such that there exists a finite set \(P \subseteq \mathbb{Z}^n\) satisfying \(M = P^*\) where \(P^* := \{\vec{0}\} \cup \{p_1 + \cdots + p_k \mid k \geq 1,\, p_i \in P\}\).
Definition 1. A polinear set* is a subset \(L \subseteq \mathbb{R}^n\) of the form \[L := C + b + M \;=\; \{c + z \mid c \in C,\; z \in b + M\},\] where \(b \in \mathbb{Z}^n\), \(M \subseteq \mathbb{Z}^n\) is a finitely generated monoid, and \(C \subseteq [0,1)^n\) is a non-empty polyhedral convex set. A semi-polinear set is a finite union of polinear sets.*
Remark 8. The term polinear* combines polyhedral (for the convex part \(C\)) and linear (for the integer part \(b + M\)).*
Since every vector in \(\mathbb{R}^n\) decomposes uniquely as \(c + z\) with \(c \in [0,1)^n\) and \(z \in \mathbb{Z}^n\), each element of \(L\) has fractional part in \(C\) and integer part in \(b + M\). When \(C = \{\vec{0}\}\), the polinear set reduces to the linear set \(b + M \subseteq \mathbb{Z}^n\). The linear sets of Definition 1 coincide with those of [1], and semi-linear sets are a special case of semi-polinear sets.
We denote by \(e_i \in \mathbb{Z}^n\) the \(i\)-th standard basis vector, and by \(\exists_i S = \{\vec{s} \in \mathbb{R}^{n-1} \mid \exists s_i\in\mathbb{R}:\, (s_1,\ldots,s_n) \in S\}\) the \(i\)-th component removal.
Proposition 9. The class of semi-polinear sets is stable by finite union, finite intersection, complement, and component removal.
Proof. The unique decomposition \(s = c + z\) with \(c \in [0,1)^n\) and \(z \in \mathbb{Z}^n\) is the key: every set operation acts independently on the polyhedral part (in \([0,1)^n\)) and on the semilinear part (in \(\mathbb{Z}^n\)). It suffices to treat a single polinear set \(L = C + b + M\) (the general case follows by distributing over finite unions). Let also \(L' = C' + b' + M'\) be a second polinear set.
Intersection. Since the fractional/integer split is unique: \[L \cap L' = (C \cap C') + \bigl((b + M) \cap (b' + M')\bigr).\] \(C \cap C'\) is polyhedral convex (intersection of two polyhedral convex sets in \([0,1)^n\)); \((b+M) \cap (b'+M')\) is semilinear by Theorem 4. If either part is empty, so is \(L \cap L'\).
Complement. For \(s = c + z \in \mathbb{R}^n\): \(s \notin C + b + M\) iff \(c \notin C\) or \(z \notin b + M\). Hence: \[\mathbb{R}^n \setminus L \;=\; \bigl(([0,1)^n \setminus C) + \mathbb{Z}^n\bigr) \;\cup\; \bigl(C + (\mathbb{Z}^n \setminus (b + M))\bigr).\] Both terms are semi-polinear: \([0,1)^n \setminus C\) is a finite union of polyhedral convex sets in \([0,1)^n\) (Boolean closure of polyhedral sets), and \(\mathbb{Z}^n = \{\pm e_1,\ldots,\pm e_n\}^*\) is finitely generated, so the first term is semi-polinear; \(\mathbb{Z}^n \setminus (b+M)\) is semilinear by Theorem 4, so the second term is semi-polinear.
Component removal. Let \(\bar{b} = (b_1,\ldots,b_{i-1},b_{i+1},\ldots,b_n)\) and \(\bar{M} = \{(m_1,\ldots,m_{i-1},m_{i+1},\ldots,m_n) \mid \vec{m} \in M\}\). Then: \[\exists_i L = (\exists_i C) + \bar{b} + \bar{M}.\] \(\exists_i C\) is polyhedral convex in \([0,1)^{n-1}\) by Fourier–Motzkin elimination; \(\bar{M}\) is a finitely generated monoid (image of \(M\) under coordinate projection). So \(\exists_i L\) is semi-polinear. ◻
We introduce the addition relation \(G_+ := \{(\alpha,\beta,\gamma) \in \mathbb{R}^3 \mid \alpha + \beta = \gamma\}\) and the first-order logic \(\mathrm{FO}(\mathbb{R},\mathbb{Z},\mathbb{R}_{\geq 0},G_+)\), which is effectively equivalent to the mixed-linear arithmetic.
Theorem 10. The class of semi-polinear sets and the class of mixed-linear sets are equal.
Proof. It is clear that every semi-polinear set is mixed-linear. For the converse, let \(\mathcal{F}\) be the set of formulas \(\phi\) of \(\mathrm{FO}(\mathbb{R},\mathbb{Z},\mathbb{R}_{\geq 0},G_+)\) such that, for any tuple of free variables \((x_1,\ldots,x_n)\) of \(\phi\), the set \(\{(s_1,\ldots,s_n) \in \mathbb{R}^n \mid \phi[x_i \mapsto s_i]\}\) is semi-polinear. We prove that \(\mathcal{F}\) contains all formulas by structural induction.
The key case is the predicate \(G_+(x_i,x_j,x_k)\). The corresponding set \(S_+\) is semi-polinear via the decomposition \[S_+ = \bigcup_{\delta \in \{0,1\}} \bigl\{c \in [0,1)^n \;\big|\; c_i + c_j = c_k + \delta\bigr\} + \delta e_k + M,\] where \(M := \{z \in \mathbb{Z}^n \mid z_i + z_j = z_k\}\) is a finitely generated monoid (it is a free abelian group of rank \(n-1\), generated as a monoid by \(n-1\) basis vectors and their negatives). Indeed, decomposing \(s \in \mathbb{R}^n\) as \(s = c + z\) with \(c \in [0,1)^n\) and \(z \in \mathbb{Z}^n\), \(s \in S_+\) iff \((c_i + z_i) + (c_j + z_j) = (c_k + z_k)\), i.e.\(z_k - z_i - z_j = c_i + c_j - c_k\). Since the left-hand side is an integer and the right-hand side belongs to \((-1,2)\), there exists \(\delta \in \{0,1\}\) such that \(z_k - z_i - z_j = \delta\) and \(c_i + c_j - c_k = \delta\).
The remaining base cases are: \(\{s \mid s_i \in \mathbb{Z}\} = \{c \in [0,1)^n \mid c_i = 0\} + \mathbb{Z}^n\) (polinear, since \(\mathbb{Z}^n\) is generated by \(\{\pm e_1,\ldots,\pm e_n\}\)); and \(\{s \mid s_i \geq 0\} = [0,1)^n + \{z \in \mathbb{Z}^n \mid z_i \geq 0\}\) (polinear, since \(\{z \in \mathbb{Z}^n \mid z_i \geq 0\}\) is generated by \(\{e_i\} \cup \{\pm e_j \mid j \neq i\}\)). The stability properties of Proposition 9 then handle the Boolean connectives (\(\neg\), \(\wedge\), \(\vee\)) and existential quantification (\(\exists r\)) by induction. ◻
Remark 11. Weispfenning [4] claims that mixed-linear sets of \(\mathbb{R}\) are finite unions of sets of the form \(J + p\mathbb{Z}\) where \(J\) is an interval with rational bounds and \(p \in \mathbb{Z}\). This is incorrect: \(\mathbb{N}\) is a mixed-linear set but is not a finite union of sets of this form (any \(J + p\mathbb{Z}\) with \(p \neq 0\) contains arbitrarily negative integers, and \(p = 0\) gives a bounded interval). The error stems from describing the periodic component as a subgroup* (\(p\mathbb{Z}\)) rather than a submonoid (\(p\mathbb{N}\)). The correct form is \(I + p\mathbb{N}\): when the monoid \(M \subseteq \mathbb{N}\) has only non-negative generators, by Theorem 10 the semi-polinear sets of \(\mathbb{R}\) with such monoids are exactly finite unions of sets \(I + p\mathbb{N}\) where \(I \subseteq [0,1)\) is a rational interval and \(p \geq 0\) (by the Frobenius lemma [15]: every finitely generated submonoid of \(\mathbb{N}\) is \(\{0\}\) or of the form \(B + d\mathbb{N}\) with \(B \subseteq \mathbb{N}\) finite and \(d \geq 1\)). More generally, monoids with mixed-sign generators (e.g.\(M = \mathbb{Z}\), generated by \(\{1,-1\}\)) yield sets such as \(I + \mathbb{Z}\) that are not of this form but are still semi-polinear.*
**Relation to Weispfenning’s ultimately periodically simple sets. Weispfenning works with the extended logic \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq,[\cdot])\), which adds the integer-part function \([\cdot]\) to achieve quantifier elimination, and characterizes its definable sets as the ultimately periodically simple sets [4]. Since \([x]\) is already definable in \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\) (via \([x] \leq x < [x]+1\) with \([x] \in \mathbb{Z}\)), both logics define the same sets. With the submonoid correction above (replacing \(p\mathbb{Z}\) by \(p\mathbb{N}\)), the ultimately periodically simple sets of [4] coincide exactly with the semi-polinear sets of Theorem 10.
Remark 12 (Debt to Weispfenning [4]). Although [4] contains an error in the description of mixed-linear sets (Remark 11), it was the source of a key structural intuition: every set definable in \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\) decomposes as a finite union of sets \(Z + D\) with \(Z \subseteq \mathbb{Z}^n\) definable in \(\mathrm{FO}(\mathbb{Z},+,\leq)\) and \(D \subseteq [0,1)^n\) definable in \(\mathrm{FO}(\mathbb{R},+,\leq)\). The present paper makes this decomposition a theorem rather than a lemma from [4]: Theorem 10 establishes it from first principles via the semi-polinear characterization, and the \(Z + D\) structure is then recovered as a consequence (taking \(Z = b + M\) and \(D = C\)).
We call a function \(f : \mathbb{R}^n \to \mathbb{R}^q\) mixed-linear if there exist matrices \(M, N \in \mathbb{Q}^{q \times n}\) and \(\vec{v} \in \mathbb{Q}^q\) such that \(f(\vec{a}) = M\vec{a} + N[\vec{a}] + \vec{v}\) for all \(\vec{a} \in \mathrm{dom}(f)\).
Definition 2. A function \(f : \mathbb{R}^n \to \mathbb{R}\) partially-defined over a semi-polinear set \(D \subseteq \mathbb{R}^n\) is said to be simple* if there exist \(\alpha \in \mathbb{Q}\) and \(a, b \in \mathbb{Q}^n\) such that \[f(c + z) = \alpha + \sum_{i=1}^n a_i c_i + b_i z_i\] for any \(c \in [0,1)^n\), \(z \in \mathbb{Z}^n\) with \(c + z \in D\). A function \(f\) is said piecewise-simple if \(\mathrm{dom}(f)\) admits a finite partition into semi-polinear sets \(D_1,\ldots,D_k\) such that \(f|_{D_j}\) is simple for each \(j\).*
Remark 13. A simple function is linear in the fractional part \(c \in [0,1)^n\) and linear in the integer part \(z \in \mathbb{Z}^n\), but with potentially different slopes. The integer-part function \([\cdot] : \mathbb{R}\to \mathbb{Z}\) is simple (with \(a = 0\), \(b = 1\)), as is the fractional part \(\{\cdot\}\) (with \(a = 1\), \(b = 0\)); neither is piecewise linear. Every simple function is mixed-linear (with \(N = b - a\) in the formula \(f(\vec{a}) = M\vec{a} + N[\vec{a}] + \vec{v}\)), so every piecewise-simple function is definable in \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\).
Theorem 14. A function \(f : \mathbb{R}^n \to \mathbb{R}^q\) is definable in \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\) if and only if it is piecewise-simple.
Proof. If \(f\) is piecewise-simple, then its graph is a finite union of semi-polinear sets: on each piece, the equation defining the output is mixed-linear in the integer and fractional parts. Hence \(f\) is definable by Theorem 10.
For the converse, first assume \(q=1\) and let \(f : \mathbb{R}^n \to \mathbb{R}\) be definable in \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\). By Theorem 10, its graph is semi-polinear. Using Lemma 1, each polinear component is the graph of the restriction of \(f\) to a semi-polinear domain. The finitely many domains can be refined, using Proposition 9, into a semi-polinear partition. It is therefore enough to treat one polinear component of the graph; write it as \(G_f = C + b + M\) where \(C \subseteq [0,1)^{n+1}\) is polyhedral convex, \(b \in \mathbb{Z}^{n+1}\), and \(M = P^*\) for some finite \(P \subseteq \mathbb{Z}^{n+1}\).
Since \(\mathbf{0} \in M\), we have \(C + b \subseteq G_f\); since \(G_f\) is a function graph, \(C\) is the graph of a function \(g : \pi_x(C) \to [0,1)\) (where \(\pi_x : \mathbb{R}^{n+1} \to \mathbb{R}^n\) projects onto the first \(n\) coordinates). Similarly, \(M = P^*\) is the graph of a function \(h : \pi_x(M) \to \mathbb{Z}\). Vectors \(s \in \mathbb{R}^n\) are uniquely decomposed into \(c + z\) with \(c \in [0,1)^n\) and \(z \in \mathbb{Z}^n\), so \(f(c + z) = b_{n+1} + g(c) + h(z - (b_1,\ldots,b_n))\).
The function \(g\). As \(C\) is a polyhedral convex set, it is the set of solutions of a conjunction of equalities and inequalities \(u_1 c_1 + \cdots + u_{n+1} c_{n+1} \mathbin{\#} \alpha\). If one constraint is an equality with \(u_{n+1} \neq 0\), then \(C\) is the graph of a simple function. Otherwise, for each inequality \(I\) of the form \(\beta + a_1 c_1 + \cdots + a_n c_n \mathbin{\#} c_{n+1}\) appearing in the description of \(C\), let \(C_I\) be the set of vectors \(c \in C\) satisfying \(\beta + a_1 c_1 + \cdots + a_n c_n = c_{n+1}\). The restriction of \(g\) to \(\exists_{n+1} C_I\) is simple. Every point in \(\mathrm{dom}(g)\) satisfies at least one such inequality tightly. Indeed, fix \((c_1,\ldots,c_n) \in \mathrm{dom}(g)\): the fiber \(\{c_{n+1} \mid (c_1,\ldots,c_n,c_{n+1}) \in C\}\) is a polyhedral convex subset of \(\mathbb{R}\) that is a singleton (since \(g\) is a function). A singleton polyhedral convex set in \(\mathbb{R}\) is the intersection of its lower and upper bounds, so at least one bounding inequality is tight at \(c_{n+1} = g(c_1,\ldots,c_n)\). Thus \(\mathrm{dom}(g)\) is covered by the finite union of the sets \(\exists_{n+1} C_I\). The covering can again be refined into a finite polyhedral, hence semi-polinear, partition. Hence \(g\) is piecewise-simple.
The function \(h\). We introduce the orthogonal \(S^\perp\) of a set \(S \subseteq \mathbb{Q}^{n+1}\) as the set of vectors \(v \in \mathbb{Q}^{n+1}\) such that \(s_1 v_1 + \cdots + s_{n+1} v_{n+1} = 0\) for any \(s \in S\). We recall from [16] that \((S^\perp)^\perp\) is exactly the \(\mathbb{Q}\)-linear span of \(S\).
Assume by contradiction that \(P^\perp \subseteq \mathbb{Q}^n \times \{0\}\). Every \(v \in P^\perp\) has \(v_{n+1} = 0\), so \(v \cdot e_{n+1} = 0\) for all \(v \in P^\perp\), hence \(e_{n+1} \in (P^\perp)^\perp = \mathrm{span}_\mathbb{Q}(P)\). Write \(e_{n+1} = \sum_j r_j p_j\) with \(r_j \in \mathbb{Q}\). Choose \(d \geq 1\) with \(dr_j \in \mathbb{Z}\) for all \(j\) and write \(dr_j = n_j^+ - n_j^-\) with \(n_j^\pm \in \mathbb{N}\). Set \(p^+ = \sum_j n_j^+ p_j \in P^*\) and \(p^- = \sum_j n_j^- p_j \in P^*\). For \(i = 1,\ldots,n\): \((e_{n+1})[i] = 0\) gives \(\sum_j r_j p_j[i] = 0\), hence \(p^+[i] = \sum_j n_j^+ p_j[i] = \sum_j n_j^- p_j[i] = p^-[i]\). But \(p^+[n+1] - p^-[n+1] = d \cdot (e_{n+1})[n+1] = d \geq 1\). Thus \(p^+\) and \(p^-\) both lie in \(G_h = P^*\) with the same \(\mathbb{Z}^n\)-projection but different \(\mathbb{Z}\)-outputs, contradicting \(h\) being a function.
Hence there exists \(v = (v_1,\ldots,v_n, v_{n+1}) \in P^\perp\) with \(v_{n+1} \neq 0\). For any \(p = (\vec{z}, y) \in P^*\): since \(p\) is a sum of generators from \(P\) and \(v \perp P\), we have \(v \cdot p = 0\), giving \[h(\vec{z}) = y = -\frac{v_1 z_1 + \cdots + v_n z_n}{v_{n+1}} = M_h \vec{z},\] where \(M_h = -v_{n+1}^{-1}(v_1,\ldots,v_n) \in \mathbb{Q}^{1\times n}\). Thus \(h\) is linear on \(\mathrm{dom}(h)\) (simple with \(a_i = 0\) for all \(i\), since the domain is in \(\mathbb{Z}^n\) so fractional parts are zero). Hence \(f(c + z) = b_{n+1} + g(c) + h(z - (b_1,\ldots,b_n))\) is piecewise-simple.
It remains only to record effectivity. Suppose that the graph is given as an explicit finite union of polinear sets \(C+b+P^*\). The refinement of the domains uses the effective Boolean operations on polyhedral convex sets and semilinear sets from Proposition 9. For the real part \(g\), the pieces are obtained by inspecting the finitely many defining constraints of \(C\): equalities with non-zero output coefficient, or active inequalities \(\beta+a_1c_1+\cdots+a_nc_n=c_{n+1}\); their projections are computed by Fourier–Motzkin elimination. For the integer part \(h\), one computes a vector \(v\in P^\perp\) with \(v_{n+1}\neq0\) by Gaussian elimination; this gives the linear expression for \(h\) explicitly. These operations are polynomial in the size of the current polinear component and in the number of pieces actually produced. Thus the conversion from a semi-polinear graph representation to a piecewise-simple representation is effective in output-sensitive time.
For \(q>1\), apply the scalar case to each coordinate function \(f_1,\ldots,f_q\). Each coordinate yields a finite semi-polinear partition on which it is simple. Taking a common refinement of these partitions, using Proposition 9, gives a finite semi-polinear partition on which all coordinates are simple simultaneously. Hence \(f\) is piecewise-simple as a vector-valued function. ◻
Corollary 1. A function is definable in \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\) if and only if it is \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\)-piecewise mixed-linear.
Proof. Every piecewise-simple function is mixed-linear (Remark 13), so the result follows from Theorem 14. ◻
We have established a unified algebraic framework for sets and functions definable in the three additive theories. In \(\mathrm{FO}(\mathbb{Z},+,\leq)\): semi-linear sets (Theorem 4) and piecewise linear functions (Theorem 5). In \(\mathrm{FO}(\mathbb{R},+,\leq)\): polyhedral sets and piecewise linear functions (Theorem 3). In \(\mathrm{FO}(\mathbb{R},\mathbb{Z},+,\leq)\): semi-polinear sets (Theorem 10) and piecewise-simple functions (Theorem 14).
All proofs are purely algebraic, using only linear algebra and the Ginsburg–Spanier theorem; no automata or quantifier elimination procedures are needed. We also correct an error in Weispfenning [4] regarding the structure of mixed-linear sets of \(\mathbb{R}\) (Remark 11).
The algebraic characterization of \(\mathrm{FO}(\mathbb{Z},+,V_p)\)-definable functions (Büchi arithmetic [17]) — the analogue of Theorem 5 for Presburger arithmetic extended with the \(p\)-adic valuation — appears to be open.