REVIEW 2 major objections 3 minor 17 references
The $\delta$-calculus: from distinction to arithmetic
T0 review · 2 major / 3 minor · reviewed 2026-08-03 · deepseek-v4-flash
Pith's one-line read The paper establishes that the primitive act of distinction — one-step extension of a finite record — generates a natural-number object whose arithmetic is classified by index-period congruences, and that the classification's logical cost i
desk verdict Standard monogenic-monoid classification with an exact constructive price tag; math is sound, but the advertised Lean formalization cannot be audited from the text. 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 load-bearing object is the δ-orbit: the inductive carrier generated from the empty record 0 by the unary successor operation S, equipped with structural recursion and induction. It is presented first-orderly by the δ-calculus over {0,S,+,·}, and the map D:Nδ→N (with inverse ν) is a monoid isomorphism that carries congruences back and forth. The classification uses the index-period relation ≡_{i,p}, which identifies x and y when x=y or both sit at or after index i and differ by a multiple of p; its quotient is the finite monogenic monoid M(i,p). The 'ledger' annotates each derivation with the nonconstructive principles it uses, separating the forced fragment from derivations conditional o
What would settle it
Apply the proof of Theorem 6.11 to the decidable congruence generated by 0∼2 on (N,+,0): the theorem predicts it is exactly ≡_{0,2} — that is, the parity relation. Checking directly that the congruence relates all even numbers to each other and all odd numbers to each other, but never relates an even to an odd, either confirms the forced classification or produces the smallest counterexample. For the price statements, a metatheory where Markov's principle fails yet MarkovForm holds would refute Proposition 6.15.
Extended reading notes
Core claim
The core is the δ-orbit: the inductive collection generated from 0 by the one-step extension S, which yields successor nonzero, injectivity, and induction, making Nδ a natural-number object with decidable equality. The map D:Nδ→N counting extensions is a monoid isomorphism, so the classical congruence classification on (N,+,0) transfers to Nδ: every congruence is equality or a unique ≡_{i,p}. The new content is the exact pricing: with a decidable congruence and an explicit distinct pair, the classification is forced; with a decidable congruence not equality, it needs Markov's principle; with an arbitrary congruence, it needs excluded middle. The reverse implications prove both prices are exa
Load-bearing premise
The entire construction depends on the intuitionistic metatheory providing inductively generated carriers with recursion and induction — so the δ-orbit is genuinely an inductive type — and on the metatheoretic natural numbers N having decidable equality and order; without those, the isomorphism D between Nδ and N, and therefore the transferred congruence classification, has no footing.
Editorial extensions
If this is right
- Every recognizer r:(Nδ,+,0)→(V,∗,e) is uniquely determined by the image of S0; it is either injective (image isomorphic to Nδ) or its image is a finite monogenic monoid M(i,p) with exactly i+p elements.
- The forced fragment of the δ-calculus is sound in the standard model: a closed formula derivable without EM, LPO, or MP is true in N.
- The number tower δ⇝Nδ↪Zδ↪Qδ is built without the axiom of choice, and each of the metatheoretic N, Z, Q admits an explicit injection into Nδ.
- The classification prices are exact: MarkovForm is equivalent to Markov's principle, and ClassicalForm is equivalent to excluded middle, so neither principle can be weakened.
- The decidability assumption on the congruence is classically redundant but constructively separates the Markov-price form from the excluded-middle-price form — a distinction invisible to a classical axiom audit.
Reading between the lines
- Inference: Because the classification transfers from N via the monoid isomorphism D, the exact prices are really a fact about the congruence theory of (N,+,0); the same three-tier pricing should reappear for any structure presented as a natural-number object with recursive addition.
- Inference: The paper separates a bare 'distinction witness' (two unequal elements with no iterable operation) from the δ-orbit (where successor can be iterated); this suggests a hierarchy of distinctness notions, and a testable extension is to ask whether any signature with an iterable successor necessarily yields a unique natural-number object.
- Inference: Since no separate LPO-level price appears, a natural experiment would be to add LPO to the forced fragment and ask whether the set of provable closed formulas changes; the soundness theorem suggests truth in the standard model would be unchanged.
- Inference: The construction stops at Qδ; the authors flag that the real-number stage is a further ledger problem because Cauchy and Dedekind constructions are not constructively equivalent. A concrete next step would be to price the construction of the Cauchy reals over Qδ with the same ledger.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper develops an intuitionistic arithmetic Nδ generated from a primitive one-step distinction, constructs a choice-free number tower Nδ → Zδ → Qδ, and gives explicit injections of the metatheoretic N, Z, Q into Nδ. Its central result is the classification of additive congruences on (Nδ,+,0), equivalently of recognition quotients of its additive monoid: Theorem 1.7 proves that, with an explicit distinct related pair, the congruence is forced to be a unique index-period congruence ≡_{i,p}; for a decidable non-equality congruence the classification is conditional on Markov's principle; for an arbitrary congruence it is conditional on excluded middle. Propositions 6.15 and 6.16 establish the reverse implications, so the prices are exact. A Lean 4 formalization of the main results is reported in Section 7.
Significance. If the results stand, the paper gives a clean and genuinely informative constructive analysis of a classical algebraic classification: it separates the logically forced case from the Markov-principle case and from the excluded-middle case, and proves the prices cannot be lowered. The proofs of Sections 4–6 are coherent and appear correct: the construction of Nδ, Zδ, and Qδ is carried out by explicit quotients, the encodings are explicit and choice-free, and the congruence classification is proved from scratch with bounded, decidable searches in the forced case. The reverse implications in Propositions 6.15 and 6.16 are particularly convincing and show that the prices are not merely artifacts of the proof strategy. The paper is explicit about its metatheoretic assumptions in Section 1, which is a strength. The main weakness is the formalization claim: as presented, the Lean artifact and its axiom audit cannot be independently checked.
major comments (2)
- [Section 7, Table 1] The paper claims that the main results are formalized in Lean 4 and reports an axiom audit, but it supplies only a repository URL and module names. There is no commit hash, no build instructions, and no code listing, so a reader cannot reproduce the #print axioms output or verify that the declarations in Table 1 correspond to the theorems stated. Since the abstract and Section 7 make the formalization a substantive part of the evidence, this is not merely a presentation issue. Please provide a frozen artifact (commit hash or archive), a build environment, and a script or command that emits the axiom sets listed in Table 1.
- [Section 7 / Section 1] Table 1 states that all forced declarations have axiom sets contained in {propext, Quot.sound}. Section 1 lists the assumed intuitionistic metatheory: inductive carriers, quotients by equivalence relations, and decidable equality and order on N. Propositional extensionality is not listed there. In intensional type theory propext is an additional axiom, and its status in the paper's informal metatheory is unclear. Please clarify whether propext and Quot.sound are part of the intended ambient metatheory, and if so, state this in Section 1 and explain why they do not affect the ledger prices. Without this, the formalized theorems may be proved in a stronger base theory than the one described in the text.
minor comments (3)
- [Definition 1.1] The symbol ':⇐ ⇒' appears to be a typographical corruption of a bi-implication; it should read '\Leftrightarrow' (and similarly in a few later displays).
- [§2.1, §6] The word 'ledger' is used both for the annotation on object-calculus derivations (Section 2.1) and for the metatheoretic pricing of classification statements (Convention 6.1). Convention 6.1 is helpful, but an early forward-reference in Section 2 would prevent the reader from conflating the two uses.
- [Section 7] The footnote gives a GitHub URL but no revision identifier. Even after the requested artifact is supplied, the paper should cite a stable archive (e.g., Zenodo DOI or a specific commit hash) so the formalization is immutable.
Circularity Check
No significant circularity: the congruence classification is proved from scratch, prices derived by reverse implications, and self-citations are not load-bearing.
full rationale
The paper's central classification (Theorem 1.7 / Corollary 6.17) does not reduce to its inputs. The index-period classification of additive congruences on (N,+,0) is developed in Section 6 from explicit definitions of periods (Definition 6.2) and proved by bounded, decidable searches (Theorem 6.11), with uniqueness via Lemma 6.10. The transfer to (Nδ,+,0) is via the explicit monoid isomorphism D (Lemma 4.4 and Section 6.1), not by assuming the target. The Markov and classical forms are shown sufficient (Theorems 6.12, 6.14) and then necessary: Proposition 6.15 derives Markov's principle from MarkovForm and Proposition 6.16 derives excluded middle from ClassicalForm, so the 'prices' are not assumed—they are proved exact. The reference to 'Recognition Geometry' [15] supplies only the word 'recognizer' and the paper redefines the notion fully in Section 5 (homomorphism r, kernel congruence, quotient), including the caveat in Remark 5.8 that arbitrary functions yield every equivalence relation; thus the citation is not load-bearing. The Lean formalization's lack of a concrete audited commit hash is a verification artifact, not a circularity. No fitted parameter is renamed as a prediction, and no equation is defined in terms of the result it is used to prove. The paper is self-contained against the stated constructive metatheory.
Assumptions & free parameters
assumptions (4)
- domain assumption The ambient metatheory is an intuitionistic type theory providing inductively generated carriers with recursion/induction, natural numbers N with decidable equality and order, and quotients by equivalence relations.
- standard math The standard arithmetic structure N=(N,0,S,+,·) is a Tarski model validating the distinction axioms, recursion equations, and induction.
- domain assumption Convention 6.1: MP and EM are treated as hypotheses on the ambient metatheory (rather than being derivable), and the reverse implications are proved by constructing explicit congruences from arbitrary propositions/predicates.
- standard math The classical classification of congruences on the free monogenic monoid (N,+) is background (Birkhoff 1935; Clifford-Preston 1961).
Cite this review
Pith. "Pith review of The $\delta$-calculus: from distinction to arithmetic." pith.science (2026). https://pith.science/paper/TJ2FMA62
@misc{pith2026260729349,
author = {Pith},
title = {Pith review of: The $\delta$-calculus: from distinction to arithmetic},
year = {2026},
howpublished = {\url{https://pith.science/paper/TJ2FMA62}},
note = {Machine review of arXiv:2607.29349}
}
abstract
Let $\delta$ denote the primitive act of distinction, formally realized as the one-step extension $r \mapsto Sr$ of a finite record. We study the inductively generated $\delta$-orbit and its first-order arithmetic presentation $\mathbb{N}_\delta$. The corresponding $\delta$-calculus is an intuitionistic first-order proof system over the signature $\{0,S,+,\cdot\}$. Every derivation carries a ledger recording the use of the law of excluded middle, the limited principle of omniscience, Markov's principle, and induction on quantified formulas. The last entry does not affect whether a derivation is forced. If a closed formula is derivable in the forced fragment, then it is true in the standard model. Starting from $\delta$, we construct a choice-free number tower $\delta \leadsto \mathbb{N}_\delta \hookrightarrow \mathbb{Z}_\delta \hookrightarrow \mathbb{Q}_\delta$. The metatheoretic number systems $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{Q}$ each admit an explicit injection into $\mathbb{N}_\delta$. We also classify the recognition quotients of the additive monoid $(\mathbb{N}_\delta,+,0)$. Assuming the law of excluded middle, every recognizer is either injective or has a kernel congruence $\equiv_{i,p}$, with index $i$ and period $p$, for a unique pair $i\ge 0$, $p\ge 1$. In the noninjective case the quotient is isomorphic to the finite monogenic monoid $M(i,p)$. We price this classification with the ledger, determining which nonconstructive principles each form requires. If the congruence is decidable and an explicit pair of distinct related elements is given, the classification is forced. If the congruence is decidable and different from equality, Markov's principle is needed. For an arbitrary congruence, the dichotomy requires the law of excluded middle. The reverse implications show that the last two prices cannot be lowered. The main results are formalized in Lean 4.
Reference graph
Works this paper leans on
-
[1]
Birkhoff,On the structure of abstract algebras, Mathematical Proceedings of the Cambridge Philosophical Society,31(1935), 433–454
G. Birkhoff,On the structure of abstract algebras, Mathematical Proceedings of the Cambridge Philosophical Society,31(1935), 433–454
1935
-
[2]
Bishop,Foundations of Constructive Analysis, New York, McGraw-Hill, 1967
E. Bishop,Foundations of Constructive Analysis, New York, McGraw-Hill, 1967. THEδ-CALCULUS: FROM DISTINCTION TO ARITHMETIC 25
1967
-
[3]
Bishop and D
E. Bishop and D. Bridges,Constructive Analysis, Grundlehren der mathematischen Wissenschaften, vol. 279, Springer-Verlag, Berlin, 1985
1985
-
[4]
A. H. Clifford and G. B. Preston,The Algebraic Theory of Semigroups, Vol. I, Mathematical Surveys and Monographs Vol. 7, 1961
1961
-
[5]
Crvenković, M
S. Crvenković, M. Mitrović, and D. A. Romano,Semigroups with apartness, Math. Log. Quart.59(2013), 407–414
2013
-
[6]
Crvenković, M
S. Crvenković, M. Mitrović, and D. A. Romano,Basic notions of (constructive) semigroups with apartness, Semigroup Forum92(2016), 659–674
2016
-
[7]
N.G.deBruijn,Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem,Nederl. Akad. Wetensch. Proc. Ser. A 75, Indag. Math, 34 (1972), pp. 381-392
1972
-
[8]
de Moura and S
L. de Moura and S. Ullrich,The Lean 4 theorem prover and programming language, in: Automated Deduction, CADE 28, LNCS 12699, Springer, 2021, 625–635
2021
Show all 17 references
-
[9]
Ishihara,Reverse mathematics in Bishop’s constructive mathematics, Philosophia Scientiae, Cahier spécial 6 (2006), 43–59
H. Ishihara,Reverse mathematics in Bishop’s constructive mathematics, Philosophia Scientiae, Cahier spécial 6 (2006), 43–59
2006
-
[10]
F. W. Lawvere,An elementary theory of the category of sets, Proc. Nat. Acad. Sci. USA52(1964), 1506–1511
1964
-
[11]
The mathlib Community,The Lean mathematical library, in: CPP 2020, ACM, 2020, 367–381
2020
-
[12]
Mitrović, M
M. Mitrović, M. N. Hounkonnou, and M. A. Baroni,Theory of constructive semigroups with apartness- foundations, development and practice, Fund. Inform.184(2021), 233–271
2021
-
[13]
Spencer-Brown,Laws of Form, George Allen and Unwin, 1969
G. Spencer-Brown,Laws of Form, George Allen and Unwin, 1969
1969
-
[14]
van Dalen,Logic and Structure, 5th ed., Universitext, Springer London, 2013
D. van Dalen,Logic and Structure, 5th ed., Universitext, Springer London, 2013
2013
-
[15]
Washburn, M
J. Washburn, M. Zlatanović, and E. Allahyarov,Recognition geometry, Axioms15(2026), 90
2026
-
[16]
R. G. Wengert,The development of the doctrine of the formal distinction in the Lectura Prima of John Duns Scotus, The Monist49(1965), 571–587
1965
-
[17]
J. A. Wheeler,Recent Thinking about the Nature of the Physical World: It from Bit,Ann. N. Y. Acad. Sci. (1992), 655, 349–364. Recognition Physics Institute, Austin, Texas, USA Email address:jon@recognitionphysics.org Department of Mathematics, F aculty of Science and Mathemati...
1992
Reviewed August 3, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.