← All papers
First page of The $δ$-calculus: from distinction to arithmetic

The $δ$-calculus: from distinction to arithmetic

Jonathan Washburn, Milan Zlatanović

math.LO Jul 31, 2026 · v2
Main results, including soundness of the forced fragment, the number tower and the ledger-priced congruence classification, are formalized in Lean 4 over Mathlib, with axiom audits.
Let $δ$ denote the primitive act of distinction, formally realized as the one-step extension $r\mapsto Sr$ of a finite record. We prove that the $δ$-orbit is initial among $δ$-algebras: every $δ$-algebra admits a unique structure-preserving map from the orbit. The map is injective when the successor operation is injective and the base point is not a successor. If the $δ$-algebra also satisfies induction for all predicates, the map is bijective and gives the unique isomorphism with the generated $δ$-orbit. The $δ$-calculus is an intuitionistic first-order proof system over the signature $\{0,S,+,\cdot\}$. Each 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. Every closed formula derivable in the forced fragment is true in the standard model. Starting from $δ$, we construct the choice-free number tower $δ\leadsto \mathbb{N}_δ\hookrightarrow \mathbb{Z}_δ\hookrightarrow \mathbb{Q}_δ$. The metatheoretic systems $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{Q}$ each admit an explicit injection into $\mathbb{N}_δ$. Under the law of excluded middle, every recognizer is either injective or has kernel congruence $\equiv_{i,p}$ for a unique pair $i\geq0$, $p\geq1$. In the noninjective case, the quotient is a finite monogenic monoid $M(i,p)$. A decidable congruence together with an explicit pair of distinct related elements implies the classification without additional nonconstructive principles. For a decidable congruence 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 are exact. They are distinct from the syntactic ledger of derivations in the $δ$-calculus.

The paper asks how natural-number structure arises from a primitive one-step extension (the δ-orbit). It also asks which constructive principles (EM, LPO, MP, quantified induction) are needed for derivations and for the classification of recognition quotients of the additive monoid.

The authors define the δ-calculus, an intuitionistic first-order arithmetic over {0,S,+,·} in which each derivation carries a ledger of nonconstructive principles used. They prove initiality of the δ-orbit and soundness of the forced fragment, and build a choice-free tower N_δ → Z_δ → Q_δ. Congruences on (N_δ,+,0) are classified into equality or index-period congruences, and the exact logical price of each form is determined. The results are formalized in Lean 4 over Mathlib, with #print axioms audits.

For a decidable congruence with an explicit pair of distinct related elements, the classification needs no nonconstructive principle. For a decidable congruence other than equality it is equivalent to Markov's principle, and for an arbitrary congruence it is equivalent to excluded middle. Most Lean declarations depend only on propext and Quot.sound. Lean's axiom audit cannot distinguish the MP and EM prices, so the formalization states the required principle as an explicit hypothesis.

ResultLean declaration
Proposition 1.5bootstrap_initiality
Theorem 2.1sound_forced
Theorem 6.12nat_catalogue_markov, orbit_catalogue_markov
Corollary 6.17catalogue_markov_iff_mp, catalogue_classical_iff_em
Selected main results and their Lean 4 declarations