The $\delta$-calculus: from distinction to arithmetic

Abstract

Let $\delta$ denote the primitive act of distinction, formally realized as the one-step extension $r\mapsto Sr$ of a finite record. We prove that the $\delta$-orbit is initial among $\delta$-algebras: every $\delta$-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 $\delta$-algebra also satisfies induction for all predicates, the map is bijective and gives the unique isomorphism with the generated $\delta$-orbit. The $\delta$-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 $\delta$, we construct the choice-free number tower $\delta \leadsto \mathbb{N}_\delta \hookrightarrow \mathbb{Z}_\delta \hookrightarrow \mathbb{Q}_\delta$. The metatheoretic systems $\mathbb{N}$, $\mathbb{Z}$, and $\mathbb{Q}$ each admit an explicit injection into $\mathbb{N}_\delta$. 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 $\delta$-calculus.