Linear Orders in Presburger Arithmetic

Alexander Zapryagaev; Fedor Pakhomov

arxiv: 2209.11598 · v2 · submitted 2022-09-23 · 🧮 math.LO

Linear Orders in Presburger Arithmetic

Fedor Pakhomov , Alexander Zapryagaev This is my paper

Pith reviewed 2026-05-24 10:48 UTC · model grok-4.3

classification 🧮 math.LO

keywords Presburger arithmeticlinear ordersfirst-order definabilitylexicographic orderdefinable embeddings

0 comments

The pith

Linear orders first-order definable in (Z;<,+) are exactly those definably embeddable into lexicographic order on Z^n for some n.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that the linear orders definable by first-order formulas in the integers with addition and order are precisely the orders that admit a definable embedding into the lexicographic ordering of n-tuples of integers for some finite n. This equivalence classifies every possible definable linear order in Presburger arithmetic by reducing it to a concrete embedding construction. A sympathetic reader would care because the result supplies an explicit structural form for all such orders rather than leaving definability as an open-ended question.

Core claim

The central claim is that a linear order is first-order definable in the structure (Z;<,+) if and only if there exists some n such that the order is (Z;<,+)-definably embeddable into the lexicographic ordering on Z^n.

What carries the argument

Definable embeddability into the lexicographic ordering on Z^n, which serves as the canonical representative that captures every first-order definable linear order.

If this is right

Every first-order definable linear order arises via a definable embedding into some finite-dimensional lexicographic product.
No linear order outside this embedding class can be defined first-order in the Presburger structure.
The definable orders inherit the piecewise-linear character of the lexicographic orders on Z^n.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The characterization supplies a uniform way to represent all definable orders by a single embedding dimension n.
It opens the possibility of deciding order-theoretic properties such as density or successor relations by inspecting the embedding rather than the original formula.

Load-bearing premise

The structure is the standard integers with the usual addition and strict order, and definability is restricted to first-order formulas in that language.

What would settle it

Exhibit a linear order on a definable subset of Z that is first-order definable using < and + yet admits no definable embedding into any lexicographic Z^n, or exhibit an order that embeds definably into some lex Z^n yet is not first-order definable in (Z;<,+).

read the original abstract

We prove the linear orders first-order definable in the standard model $(\ZZ;<,+)$ of Presburger arithmetic are exactly those that are $(\ZZ;<,+)$-definably embeddable into the lexicographic ordering on $\ZZ^n$ for some $n$.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a clean if unsurprising characterization of definable linear orders in Presburger arithmetic as those embeddable into lex order on some Z^n.

read the letter

The central claim is that the FO-definable linear orders in (Z; <, +) are exactly the ones that admit a (Z; <, +)-definable embedding into the lexicographic order on Z^n for some n. The converse is immediate once you note that lex order itself is quantifier-free definable, so the real work is the forward direction. That direction rests on the standard semilinear description of definable sets and functions in Presburger arithmetic after adding divisibility predicates. If the proof simply assembles those facts into an explicit embedding construction, the result is useful but not revolutionary; it organizes what was already implicit in the quantifier-elimination literature rather than introducing new machinery. The paper does well by stating the equivalence precisely and avoiding extra parameters or ad-hoc constructions. No circularity appears in the statement, and the claim aligns with the known model theory of the structure. A minor soft spot is that the abstract gives no indication of effectivity or bounds on n, which might matter for applications in verification even if it is not required for the pure characterization. Readers working on definability in Presburger arithmetic or on o-minimal expansions will find this worth citing when they need a reference for what linear orders can appear. It is not broad enough to interest people outside that niche. The work is coherent on its own terms and rests on established facts rather than fitting or invented notions, so it deserves a serious referee even if the proof turns out to be mostly a careful assembly of prior results.

Referee Report

0 major / 0 minor

Summary. The paper proves that the linear orders first-order definable in the standard model (Z;<,+) of Presburger arithmetic are exactly those that are (Z;<,+)-definably embeddable into the lexicographic ordering on Z^n for some n.

Significance. If the result holds, it supplies a concrete geometric characterization of definable linear orders in Presburger arithmetic by reducing them to definable embeddings into lex orders on finite-dimensional integer lattices. The converse direction is immediate from the quantifier-free definability of lexicographic order and closure under definable maps; the forward direction rests on the known semilinear structure of definable sets after quantifier elimination in the expanded language with divisibility predicates. This strengthens the model-theoretic understanding of (Z;<,+) and may facilitate further work on definable orders and relations in this structure.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their careful reading and positive recommendation to accept the paper. The report accurately summarizes the main result and its significance.

Circularity Check

0 steps flagged

No significant circularity; standard model-theoretic characterization

full rationale

The paper establishes a two-directional characterization: FO-definable linear orders on Z in the language {<, +} are precisely the definably embeddable ones into lex(Z^n) for some n. The converse holds immediately because lex order on Z^n is quantifier-free definable in (Z; <, +) and definable sets are closed under definable embeddings. The forward direction invokes the standard quantifier elimination for Presburger arithmetic in the expanded language with divisibility predicates, yielding the known semilinear structure of definable sets and functions; this is an external, independently established fact about the structure and is not derived from or reduced to any input of the present paper. No self-citations, fitted parameters, self-definitional steps, or uniqueness theorems imported from the authors appear in the claim or its justification. The result is therefore self-contained against external model-theoretic benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Only the abstract is available, so the ledger is necessarily incomplete; no free parameters, invented entities, or non-standard axioms are mentioned.

axioms (2)

standard math First-order logic over the structure (Z; <, +) is the definability language.
Invoked by the abstract's use of 'first-order definable'.
domain assumption The standard model of Presburger arithmetic is the usual integers with usual operations.
Stated explicitly in the abstract.

pith-pipeline@v0.9.0 · 5547 in / 1219 out tokens · 21392 ms · 2026-05-24T10:48:34.899589+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

14 extracted references · 14 canonical work pages

[1]

A.: Linear orders in the pushdown hier archy

Braud, L., Carayol. A.: Linear orders in the pushdown hier archy. Automata, Lan- guages and Programming: 37th International Colloquium, IC ALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II. Springer (2010)

work page 2010
[2]

R.: Combinatorial remarks on partitions of a m ultipartite number

Blakley, G. R.: Combinatorial remarks on partitions of a m ultipartite number. Duke Math. J. 31.2, 335-340 (1964)

work page 1964
[3]

Cluckers, R.: Presburger sets and p-minimal ﬁelds. J. Sym bolic Logic, 68(1), 153- 162 (2003)

work page 2003
[4]

Paciﬁc J

Ginsburg, S., Spanier, E.: Semigroups, Presburger formu las, and languages. Paciﬁc J. Math. 16.2, 285-296 (1966)

work page 1966
[5]

Ito, R.: Every semilinear set is a ﬁnite union of disjoint l inear sets. J. Comput. System Sci. 3.2, 221-231 (1969)

work page 1969
[6]

ACM Trans

Khoussainov, B., Rubin, S., Stephan, F.: Automatic linea r orders and trees. ACM Trans. Comput. Log. 6.4, 675-700 (2005)

work page 2005
[7]

Journal of Mathematical Logic 9.2, 201-239 (2009)

Alf O., Steinhorn, C.: On linearly ordered structures of ﬁ nite rank. Journal of Mathematical Logic 9.2, 201-239 (2009)

work page 2009
[8]

Pakhomov, F., Zapryagaev, A.: Multi-dimensional interp retations of Presburger arithmetic in itself. J. Log. Comput., 30.8, 1681-1693 (202 0)

work page
[9]

Comptes Rendus du I congr` es de Math´ ematiciens des Pays Slaves , 92–101 (1929) – English translation in [13]

Presburger, M.: ¨Uber die Vollst¨ andigkeit eines gewissen Systems der Arith metik ganzer Zahlen, in welchem die Addition als einzige Operatio n hervortritt. Comptes Rendus du I congr` es de Math´ ematiciens des Pays Slaves , 92–101 (1929) – English translation in [13]

work page 1929
[10]

Ramakrishnan, J.: Deﬁnable linear orders deﬁnably embe d into lexicographic or- ders in o-minimal structures. Proc. Am. Math. Soc. 141.5, 18 09-1819 (2013)

work page 2013
[11]

Rosenstein, J.: Linear orderings. Vol. 98. Academic press (1982)

work page 1982
[12]

ACM Trans

Schweikardt, N.: Arithmetic, ﬁrst-order logic, and cou nting quantiﬁers. ACM Trans. Comput. Log. 6.3, 634-671 (2005)

work page 2005
[13]

Cornell University (1984)

Stansifer, R.: Presburger’s Article on Integer Arithme tic: Remarks and Translation (Technical Report). Cornell University (1984)

work page 1984
[14]

In Kr acht M., de Rijke M., Wans- ing H., Zakharyaschev M., ed., Advances in Modal Logic

Visser, A.: An overview of interpretability logic. In Kr acht M., de Rijke M., Wans- ing H., Zakharyaschev M., ed., Advances in Modal Logic. CSLI Lecture Notes 1.87, 307-359 (1998)

work page 1998

[1] [1]

A.: Linear orders in the pushdown hier archy

Braud, L., Carayol. A.: Linear orders in the pushdown hier archy. Automata, Lan- guages and Programming: 37th International Colloquium, IC ALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II. Springer (2010)

work page 2010

[2] [2]

R.: Combinatorial remarks on partitions of a m ultipartite number

Blakley, G. R.: Combinatorial remarks on partitions of a m ultipartite number. Duke Math. J. 31.2, 335-340 (1964)

work page 1964

[3] [3]

Cluckers, R.: Presburger sets and p-minimal ﬁelds. J. Sym bolic Logic, 68(1), 153- 162 (2003)

work page 2003

[4] [4]

Paciﬁc J

Ginsburg, S., Spanier, E.: Semigroups, Presburger formu las, and languages. Paciﬁc J. Math. 16.2, 285-296 (1966)

work page 1966

[5] [5]

Ito, R.: Every semilinear set is a ﬁnite union of disjoint l inear sets. J. Comput. System Sci. 3.2, 221-231 (1969)

work page 1969

[6] [6]

ACM Trans

Khoussainov, B., Rubin, S., Stephan, F.: Automatic linea r orders and trees. ACM Trans. Comput. Log. 6.4, 675-700 (2005)

work page 2005

[7] [7]

Journal of Mathematical Logic 9.2, 201-239 (2009)

Alf O., Steinhorn, C.: On linearly ordered structures of ﬁ nite rank. Journal of Mathematical Logic 9.2, 201-239 (2009)

work page 2009

[8] [8]

Pakhomov, F., Zapryagaev, A.: Multi-dimensional interp retations of Presburger arithmetic in itself. J. Log. Comput., 30.8, 1681-1693 (202 0)

work page

[9] [9]

Comptes Rendus du I congr` es de Math´ ematiciens des Pays Slaves , 92–101 (1929) – English translation in [13]

Presburger, M.: ¨Uber die Vollst¨ andigkeit eines gewissen Systems der Arith metik ganzer Zahlen, in welchem die Addition als einzige Operatio n hervortritt. Comptes Rendus du I congr` es de Math´ ematiciens des Pays Slaves , 92–101 (1929) – English translation in [13]

work page 1929

[10] [10]

Ramakrishnan, J.: Deﬁnable linear orders deﬁnably embe d into lexicographic or- ders in o-minimal structures. Proc. Am. Math. Soc. 141.5, 18 09-1819 (2013)

work page 2013

[11] [11]

Rosenstein, J.: Linear orderings. Vol. 98. Academic press (1982)

work page 1982

[12] [12]

ACM Trans

Schweikardt, N.: Arithmetic, ﬁrst-order logic, and cou nting quantiﬁers. ACM Trans. Comput. Log. 6.3, 634-671 (2005)

work page 2005

[13] [13]

Cornell University (1984)

Stansifer, R.: Presburger’s Article on Integer Arithme tic: Remarks and Translation (Technical Report). Cornell University (1984)

work page 1984

[14] [14]

In Kr acht M., de Rijke M., Wans- ing H., Zakharyaschev M., ed., Advances in Modal Logic

Visser, A.: An overview of interpretability logic. In Kr acht M., de Rijke M., Wans- ing H., Zakharyaschev M., ed., Advances in Modal Logic. CSLI Lecture Notes 1.87, 307-359 (1998)

work page 1998