TITLE:
The δ-Calculus: From Distinction to Arithmetic
AUTHORS:
Jonathan Washburn, Milan Lj. Zlatanović
KEYWORDS:
Distinction, -Calculus, Constructive Arithmetic, Choice-Free Number Tower, Recognition Quotients
JOURNAL NAME:
Advances in Pure Mathematics,
Vol.16 No.9,
September
21,
2026
ABSTRACT: Let
δ
denote the primitive act of distinction, formally realized as the one-step extension
r↦Sr
of a finite record. We study the generated
δ
-orbit and its arithmetic presentation
ℕ
δ
. 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 corresponding
δ
-calculus is an intuitionistic first-order proof system over the signature
{
0,S,+,⋅ }
. The name is independent of
δ
-reduction in the
λ
-calculus: here
δ
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
δ
, we construct the choice-free number tower
δ⇝
ℕ
δ
↪
ℤ
δ
↪
ℚ
δ
. The metatheoretic systems
ℕ
,
ℤ
, and
ℚ
each admit an explicit injection into
ℕ
δ
. We also classify the recognition quotients of
(
ℕ
δ
,+,0
)
. Under the law of excluded middle, every recognizer is either injective or has kernel congruence
≡
i,p
for a unique pair
i≥0
,
p≥1
. In the noninjective case, the quotient is the finite monogenic monoid
M(
i,p
)
. We determine the exact metatheoretic logical price of this classification. 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. These prices are computed in the ambient metatheory. They are distinct from the syntactic ledger of derivations in the
δ
-calculus. The main results are formalized in Lean 4.