The δ-Calculus: From Distinction to Arithmetic

Let $\delta$ denote the primitive act of distinction, formally realized as the one-step extension $r？Sr$ of a finite record. We study the generated $\delta$ -orbit and its arithmetic presentation ${？}_{\delta }$ . 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 corresponding $\delta$ -calculus is an intuitionistic first-order proof system over the signature $\left\{0,S,+,？\right\}$ . The name is independent of $\delta$ -reduction in the $\lambda$ -calculus: here $\delta$ generates the arithmetic carrier, and is not a term rewriting rule. 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. The last entry does not affect whether a derivation is forced. Every closed formula derivable in the forced fragment is true in the standard model. Starting from $\delta$ , we construct the choice-free number tower