REVIEW 1 major objections 3 minor 3 references
On the first-order theory of the remainder
T0 review · 1 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash
Pith's one-line read Remainder arithmetic has no decision algorithm.
desk verdict The undecidability result for (N, mod) is likely true and new, but the printed proof has a real gap at the successor definition that must be fixed before the argument goes through. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The key mechanism is a reduction lemma for a general binary operation #. The lemma says that if # satisfies three identities — zero is definable by y#y = 0, order is definable by x<y iff (x=0 and y≠0) or x#y=x, and divisibility is definable by x=0 or x#y=0 — then the first-order theory of (N,#) is undecidable. The proof interprets (N+, <, |) inside (N, #), first defining the successor function from the order and then invoking classical definability results that recover multiplication from successor and divisibility. The remainder operation mod satisfies all three identities by the elementary properties of division, so the main corollary follows.
What would settle it
Evaluate the paper's displayed successor definition: for x > y, every z > x already satisfies z > y, so the universal condition holds automatically and the formula is equivalent to x > y. That concrete failure shows the printed proof does not supply the required successor definition; the central claim would need a corrected definition to be sustained.
Extended reading notes
Core claim
The central discovery is that modulo is not a tame operation: in first-order logic, the structure (N, mod) can interpret the positive naturals with order and divisibility. The interpretation is direct — the positive integers are the nonzero elements, a < b is defined by a mod b = a, and b divides a is defined by a mod b = 0. Because the first-order theory of the positive naturals with order and divisibility is undecidable, and because interpretation preserves undecidability, the theory of (N, mod) is undecidable as well.
Load-bearing premise
The proof depends on being able to define the successor function in the positive naturals with the usual order, because that definition is what allows the classical theorems to recover multiplication from order and divisibility; the paper's displayed formula for successor is false, so this premise is not established by the printed text.
Editorial extensions
If this is right
- There is no decision algorithm for first-order sentences about remainders on the natural numbers, even when quantifiers are unrestricted.
- Any structure that can define the modulo operation will also have an undecidable theory.
- The proof gives explicit first-order formulas for order and divisibility in terms of mod, showing that one binary function can replace the infinite family of congruence relations.
- The undecidability holds for the full structure including zero, so the artificial totalization of mod at 0 is not what drives the result.
Reading between the lines
- The printed proof contains a gap: the displayed definition of the successor function in (N+, <) is not valid, because for x>y the quantifier condition is vacuous and the formula reduces to x>y. That step is the bridge to the classical definability of multiplication, so the proof as written is incomplete.
- The gap looks repairable: the successor relation can be defined in (N+, <) by x>y together with the absence of any z strictly between y and x, which would restore the classical definability theorem.
- The reduction pattern may generalize: any binary operation that encodes order and divisibility through simple algebraic identities is a candidate for undecidability, including remainder-like operations on the integers or on rings of residues.
- The sharp contrast with addition-only arithmetic suggests that the decidability of congruence predicates comes from using infinitely many predicates rather than from the arithmetic content itself.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper claims that the first-order theory of the structure (N, mod), where mod is the total remainder operation with the convention n mod 0 = n, is undecidable. The proof proceeds by proving Lemma 1: any operation # on N satisfying three conditions (definability of zero, of the strict order on positive integers, and of divisibility) has an undecidable first-order theory, because the resulting structure interprets (N+, <, |), whose theory is undecidable by classical results of Tarski, Mostowski, and Robinson. The corollary then asserts that mod satisfies the three conditions. The argument is concise and depends on external classical theorems rather than on any self-referential or circular reasoning.
Significance. If the proof is repaired, the result is a clean and natural undecidability statement: a single binary operation, the remainder operation, suffices to make the first-order theory of the natural numbers undecidable, in sharp contrast to Presburger arithmetic. The interpretation strategy is standard, the verification of the three conditions for mod is correct, and the dependence on Julia Robinson's definability theorems and on Tarski–Mostowski–Robinson is legitimate and clearly attributed. The paper contains no fitted parameters or invented axioms. The main weakness is a single but load-bearing false formula in the proof of Lemma 1; because that formula is the only step that defines successor in (N+, <), the printed proof is incomplete as it stands. The gap appears to be easily fixable with a standard corrected definition of successor.
major comments (1)
- [Lemma 1, proof] The displayed definition of successor is false: the paper states that x = S(y) iff x > y ∧ ∀z (z > x → (z = y ∨ z > y)). For every x > y, every z > x already satisfies z > y, so the parenthetical disjunction is automatically true and the formula is logically equivalent to x > y. For example, with y = 0 and x = 2 the formula holds, although 2 is not the successor of 0. Since this is the only step that defines successor in (N+, <), the subsequent application of Robinson's Theorem 1.2 to obtain multiplication from successor and divisibility rests on a false premise. The paper should replace the formula with a correct definition, for instance y < x ∧ ∀z (y < z → (z = x ∨ x < z)), and then re-derive the definability of addition and multiplication in (N+, <, |).
minor comments (3)
- [Introduction] The convention n mod 0 := n is artificial but clearly stated; the paper could note explicitly that this convention does not affect the interpretation of the positive part of the structure, where the divisor is always positive.
- [References] The reference to Presburger's paper contains malformed text ('¨Uber' and 'Comptes rendus du I Congres des Pays Slaves'); the same applies to 'T arski' in the third reference. These should be corrected in the final version.
- [Global] The paper writes the structure variously as ( N, mod) and (N, #); the spacing and notation should be made uniform.
Circularity Check
No circularity: the undecidability of (N, mod) is derived from independent classical results by Robinson and by Tarski, Mostowski, and Robinson, plus a direct interpretation argument.
full rationale
The paper's derivation chain is: (1) Lemma 1 states sufficient conditions on an operation # under which (N, #) has undecidable first-order theory; (2) the lemma is proved by citing Julia Robinson's theorems that addition and multiplication are definable from successor and divisibility, and by citing Tarski-Mostowski-Robinson undecidability of (N+, <, |); (3) the structure (N+, <, |) is interpreted into (N, #) using the three assumed properties of #; (4) Corollary 1 checks that the actual remainder operation mod satisfies those three properties directly from the definition of mod. The externally cited theorems are independent published results, not results of this paper and not self-citations. The interpretation step is a standard syntactic reduction and does not assume the undecidability of (N, mod). The final check that mod satisfies the lemma's conditions is a direct verification from the definition of remainder, not a use of the target result. The reader's note about a false successor formula is a genuine correctness gap in the printed proof, but it is not circularity: it concerns the validity of a cited definability route, not a reduction of the conclusion to the hypothesis. Because no load-bearing step is equivalent by construction to its inputs and no fitted parameter or self-citation chain is present, the circularity score is 0.
Assumptions & free parameters
assumptions (6)
- standard math Robinson's Theorem 1.1: on N+, addition is first-order definable from multiplication and successor, and from multiplication and less-than.
- standard math Robinson's Theorem 1.2: on N+, multiplication is first-order definable from successor and divisibility.
- standard math Tarski-Mostowski-Robinson: the first-order theory of (N+, +, ·) is undecidable.
- standard math Interpretation theorem: if an undecidable theory interprets in a structure, that structure's theory is undecidable.
- standard math Successor is first-order definable from strict order on N+.
- domain assumption The operation mod is extended to a total operation by setting n mod 0 = n for all n, including 0 mod 0 = 0.
Cite this review
Pith. "Pith review of On the first-order theory of the remainder." pith.science (2026). https://pith.science/paper/7NZT6M2X
@misc{pith2026250603204,
author = {Pith},
title = {Pith review of: On the first-order theory of the remainder},
year = {2026},
howpublished = {\url{https://pith.science/paper/7NZT6M2X}},
note = {Machine review of arXiv:2506.03204}
}
read the original abstract
It is proved that the first-order theory of the structure (N,mod) is undecidable. Here mod denotes the operation of computing the remainder for any division between positive integers; i.e. x mod y is the remainder obtained by the division x : y.
Reference graph
Works this paper leans on
-
[1]
Presburger ¨Uber die Vollst¨ andigkeit eines gewissen Systems der Arithmetik
M. Presburger ¨Uber die Vollst¨ andigkeit eines gewissen Systems der Arithmetik. Comptes rendus du I Congres des Pays Slaves, Warsaw 1929
work page 1929
-
[2]
Robinson Definability and Decision Problems in Arithmetic
J. Robinson Definability and Decision Problems in Arithmetic. The Journal of Symbolic Logic, Vol. 14, No. 2, pp. 98–114, 1949
work page 1949
-
[3]
Alfred T arski, Andrzej Mostowski, Raphael M. RobinsonUndecidable Theories. North-Holland publishing Company, Amsterdam, 1953. 2
work page 1953
Reviewed August 7, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.