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 generated $\delta$ -orbit and its arithmetic presentation ${\mathbb{N}}_{\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,+,\cdot \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 $\delta ⇝{\mathbb{N}}_{\delta }$ ↪${\mathbb{Z}}_{\delta }$ ↪${\mathbb{Q}}_{\delta }$ . The metatheoretic systems $\mathbb{N}$ , $\mathbb{Z}$ , and $\mathbb{Q}$ each admit an explicit injection into ${\mathbb{N}}_{\delta }$ . We also classify the recognition quotients of $\left({\mathbb{N}}_{\delta },+,0\right)$ . Under the law of excluded middle, every recognizer is either injective or has kernel congruence ${\equiv }_{i,p}$ for a unique pair $i\ge 0$ , $p\ge 1$ . In the noninjective case, the quotient is the finite monogenic monoid $M\left(i,p\right)$ . 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 $\delta$ -calculus. The main results are formalized in Lean 4.

Keywords

Distinction, -Calculus, Constructive Arithmetic, Choice-Free Number Tower, Recognition Quotients

Share and Cite:

1. Introduction

Let $\delta$ denote the primitive act of distinction. We identify the canonical arithmetic generated by iterated distinction, construct its choice-free number tower through the rationals, and determine the exact metatheoretic logical cost of the recognition quotients of its additive monoid.

The ambient metatheory provides propositions, equality, and collections of elements, which we call carriers. The ambient metatheory is intuitionistic. It provides function types, finite products, inductively generated carriers with their recursion and induction principles, quotients by equivalence relations, and the natural numbers $\mathbb{N}$ , which also index the de Bruijn variables (Section 3). Equality and order on $\mathbb{N}$ are decidable. We work in a fixed universe ${\text{Type}}_u$ . A carrier is a type $K:{\text{Type}}_u$ , and a predicate on $K$ is a map $P:K\to \text{Prop}$ . Equality is the ambient equality, and quotients are formed by equivalence relations on carriers. In Theorem 2.5, induction applies to all such predicates, including the image predicate used for surjectivity. We do not use the law of excluded middle, the limited principle of omniscience, Markov’s principle, or the axiom of choice in the metatheory, except where explicitly assumed, as in Section 7. The ledger (Section 3.1) records principles used inside the $\delta$ -calculus.

The purpose of this construction is not to obtain another copy of the natural numbers, since the metatheory already contains $\mathbb{N}$ . The generated $\delta$ -orbit is instead the canonical object obtained from the empty record by repeated one-step extension. By Theorem 1.6, it is initial among $\delta$ -algebras, and the Peano conditions characterize it up to a unique isomorphism. Thus the resulting arithmetic is unique up to isomorphism.

Each element of the orbit records a finite number of successive distinction steps, and the later stages of the number tower are constructed explicitly from the generated carrier by group completion and fraction construction.

The main question is therefore not what the natural numbers are, but what can be constructed from the generated carrier and at what logical price. For the recognition quotients of $\left({\mathbb{N}}_{\delta },+,0\right)$ , this price is exact: a decidable congruence together with an explicit pair of distinct related elements implies the classification without additional nonconstructive principles; decidability alone requires Markov’s principle; and an arbitrary congruence requires excluded middle.

Definition 1.1. Let $K$ be a carrier. Write

$\text{Dist}\left(K\right):\iff \exists x,y\in K,x\ne y.$

A proof $h:\text{Dist}\left(K\right)$ is called a distinction witness on $K$ .

The predicate $\text{Dist}\left(K\right)$ uses no additional structure on $K$ beyond the equality of the ambient metatheory. A carrier $K$ is called nontrivial if $\text{Dist}\left(K\right)$ holds. $\text{Dist}\left(K\right)$ gives two unequal elements, but it gives no operation which can be iterated. The predicate is not used to generate the $\delta$ -orbit. The symbol $\delta$ is only the name of the one-step extension $r\mapsto Sr$ in Definition 1.2. A distinction witness does not produce 0, $S$ , or induction.

The word distinction has formal and philosophical uses [1] [2]. Spencer-Brown’s Laws of Form [1] develops a calculus from a mark of distinction. Our construction is different. The primitive is not a mark in a plane, but the one-step extension of a finite record. The generated object is the $\delta$ -orbit. The condensation rules of [1] absorb repeated marking, whereas each application of $S$ produces a further stage of the generated record. Successor nonzero, successor injectivity, and induction then give the natural-number object.

A related physical idea appears in Wheeler’s thesis it from bit, where particles, fields, and spacetime receive their physical meaning from elementary yes/no registrations [3]. Since each such registration presupposes two distinguishable alternatives, here we study the prior mathematical step: the finite iteration of distinction. We do not use the calculus of [1], and the scholastic doctrine of formal distinction [2] is not part of the construction.

In constructive algebra, a positive apartness relation is often used in place of negative inequality [4]-[6]. No apartness relation is assumed here. The ambient host is an intuitionistic type theory in the sense of Martin-Löf [7], close to the Calculus of Constructions [8]. We do not introduce a new type theory. Constructive reverse mathematics [9] [10] asks which principles suffice for a theorem, the ledger of Section 3.1 instead records what a given derivation uses.

Definition 1.2. The $\delta$ -orbit $\text{Orb}\left(0,S\right)$ is the collection of finite records generated by two formation rules:

$\frac{}{0\text{is a record}},\frac{r\text{is a record}}{Sr\text{is a record}}.$

here 0 is the empty record, and $Sr$ is the record obtained from $r$ by one further act of distinction.

Proposition 1.3. For all $r,q\in \text{Orb}\left(0,S\right)$ ,

$Sr\ne 0,Sr=Sq\to r=q.$

Moreover, if a predicate $P$ on $\text{Orb}\left(0,S\right)$ satisfies $P\left(0\right)$ and

$P\left(r\right)\to P\left(Sr\right)$ for every $r$ ,

then $P\left(r\right)$ holds for every $r\in \text{Orb}\left(0,S\right)$ .

Proof. The orbit is inductively generated, so it carries the recursion principle: for every carrier $K$ , every $k\in K$ and every $f:\text{Orb}\left(0,S\right)\times K\to K$ there is a map $g:\text{Orb}\left(0,S\right)\to K$ with $g\left(0\right)=k$ and $g\left(Sr\right)=f\left(r,g\left(r\right)\right)$ .

For $Sr\ne 0$ , apply the recursion principle to $K=\mathbb{B}=\left\{0,1\right\}$ , with $k=0$ and $f\left(r,z\right)=1$ . Then $g\left(0\right)=0$ and $g\left(Sr\right)=1$ , so $Sr=0$ would imply $0=1$ .

For injectivity, let us define $\text{pred}:\text{Orb}\left(0,S\right)\to \text{Orb}\left(0,S\right)$ by recursion with $k=0$ and $f\left(r,z\right)=r$ , so that $\text{pred}\left(Sr\right)=r$ for every $r$ . Hence $Sr=Sq$ gives

$r=\text{pred}\left(Sr\right)=\text{pred}\left(Sq\right)=q.$

The last statement is the structural induction principle of the inductively generated orbit. □

The orbit is not defined as the subset $\left\{S^{n}0:n\in \mathbb{N}\right\}$ of a pre-existing carrier, so its definition does not use a prior natural-number object as an index. The notation $S^{n}0$ is used only metatheoretically, for the result of applying $S$ $n$ times to 0. The successor laws and the induction principle for the generated orbit are proved in Proposition 1.3.

The rigidity theorem (Theorem 1.6) reverses the usual direction of explanation. The generated $\delta$ -orbit is not merely another model of the Peano conditions. It is the object those conditions describe. Initiality sends the orbit canonically into every $\delta$ -algebra. When the successor map is injective and the base point is not a successor, this canonical map is an embedding, so every such faithful realization already contains a copy of the orbit. Induction makes the map surjective, and initiality makes the resulting isomorphism unique. The Peano conditions do not create an arithmetic structure by stipulation. They characterize, up to a unique structure-preserving relabeling, the arithmetic generated by repeated distinction. This is a representation-invariance statement within an ambient metatheory supporting inductive generation.

Initiality and Peano categoricity are classical [11]. Here we combine them with distinction-based generation, the choice-free number tower, and the exact metatheoretic logical prices of recognition quotients.

The $\delta$ -calculus is an intuitionistic first-order proof system over the signature $\left\{0,S,+,\cdot \right\}$ , defined in Section 3. The symbol $\delta$ is not part of the formal language. In particular, $\delta$ is not the $\delta$ -rule of the $\lambda$ -calculus [12]. The calculus is called the $\delta$ -calculus because its symbols 0 and $S$ , the distinction axioms, and the induction rule come from the generated $\delta$ -orbit. In the arithmetic projection (Definition 5.1), the empty record is written as 0, and the one-step extension of a record is written by the successor symbol $S$ . At the first-order level, the successor theorems become the distinction axioms

$St\ne 0,St=Ss\to t=s.$

They are validated in the standard model $\mathfrak{N}=\left(\mathbb{N},0,S,+,\cdot \right)$ . The operations + and ∙ are governed by their recursion equations.

Let ${\mathbb{N}}_{\delta }$ denote the arithmetic structure carried by the generated $\delta$ -orbit, with + and ∙ defined by recursion. Its successor laws and induction are given by Proposition 1.3.

We fix the generation grammar consisting of the generation of ${\mathbb{N}}_{\delta }$ from the primitive act $\delta$ , followed by group completion and fraction construction. The stages of the construction are

The first arrow denotes the inductive generation of the $\delta$ -orbit of finite records and the natural-number object presented by it. The next stage is the group completion

${\mathbb{Z}}_{\delta }:=\left({\mathbb{N}}_{\delta }\times {\mathbb{N}}_{\delta }\right)/~,\left(a,b\right)~\left(c,d\right)\iff a+d=c+b.$

The map ${\iota }_{{\mathbb{Z}}_{\delta }}$ is the canonical embedding of ${\mathbb{N}}_{\delta }$ into this quotient, given by $a\mapsto \left[\left(a,0\right)\right]$ .

The next stage is the fraction construction ${\mathbb{Q}}_{\delta }$ , presented by ratio orbits with signed-orbit numerators and nonzero denominators in ${\mathbb{N}}_{\delta }$ , as defined in Section 5. The canonical embedding

${\iota }_{{\mathbb{Q}}_{\delta }}:{\mathbb{Z}}_{\delta }\to {\mathbb{Q}}_{\delta }$

is induced by adjoining denominator 1.

Thus the integer and rational stages are defined by their internal quotient relations. The comparison maps into the standard systems $\mathbb{Z}$ and $\mathbb{Q}$ are constructed after these quotients are formed. The construction is choice-free. In the $\delta$ -calculus, each derivation carries a ledger recording the nonconstructive principles used. The main results are verified in Lean 4 (Section 8).

Definition 1.4. For a carrier $X$ , write

${\text{Enc}}_{\delta }\left(X\right):\iff \text{there exists an injection }X$ ↪${\mathbb{N}}_{\delta }.$

An object satisfying this predicate is called $\delta$ -encodable.

We prove that the metatheoretic number systems $\mathbb{N}$ , $\mathbb{Z}$ , and $\mathbb{Q}$ are $\delta$ -encodable. In this paper, we stop the tower at ${\mathbb{Q}}_{\delta }$ . The real-number stage is not treated in this paper. Its construction gives a further constructive problem, since the Cauchy and Dedekind constructions are not always equivalent.

1.1. Main Results

The paper has three main results. The first is the initiality and rigidity of the generated $\delta$ -orbit. The second is the construction of the number tower from the generated $\delta$ -orbit. The third is the classification of the recognition quotients of $\left({\mathbb{N}}_{\delta },+,0\right)$ , together with their exact metatheoretic logical prices.

The third result contains the new quantitative part of the paper. The classical index-period classification of congruences on a monogenic monoid [13] [14] is refined by assigning exact logical prices to its three forms. The reverse implications of Corollary 7.17 show that the Markov and excluded-middle assumptions cannot be weakened. The three main results are naturally ordered: the first identifies the generated carrier, the second constructs its choice-free number tower, and the third gives the exact metatheoretic logical cost of classifying its recognition quotients.

We use the following standard universal property of the term syntax with de Bruijn variables [15].

Proposition 1.5. For every algebra $A$ of the signature $\left\{0,S,+,\cdot \right\}$ , with carrier $\left|A\right|$ , and every assignment $\rho :\mathbb{N}\to \left|A\right|$ , there exists a unique homomorphism from the term algebra to $A$ extending $\rho$ . Thus the term syntax is the free algebra of this signature on the de Bruijn variables.

Here $\mathbb{N}$ is the metatheoretic index set for the de Bruijn variables. The recursion equations for + and ∙ are validated in the standard model

$\mathfrak{N}=\left(\mathbb{N},0,S,+,\cdot \right),$

with the usual operations. The resulting arithmetic is developed in Section 4.1.

Theorem 1.6. Let $A=\left(\left|A\right|,0_A,S_A\right)$ be a $\delta$ -algebra. There exists a unique homomorphism ${\text{rec}}_A:{\mathbb{N}}_{\delta }\to A$ . If $S_A$ is injective and $0_A\notin \text{im}\left(S_A\right)$ , then ${\text{rec}}_A$ is injective. If, in addition, $A$ satisfies induction for all predicates, then ${\text{rec}}_A$ is bijective and is the unique $\delta$ -algebra isomorphism from ${\mathbb{N}}_{\delta }$ to $A$ .

Theorem 1.6 follows from Theorems 2.2, 2.3, and 2.5, proved in Section 2.

Theorem 1.7. The following hold by choice-free constructions.

(a) The carriers ${\mathbb{N}}_{\delta }$ , ${\mathbb{Z}}_{\delta }$ , and ${\mathbb{Q}}_{\delta }$ are constructed from the generated $\delta$ -orbit. The carrier ${\mathbb{N}}_{\delta }$ is the natural-number object presented by this orbit, ${\mathbb{Z}}_{\delta }$ is the group completion of ${\mathbb{N}}_{\delta }$ , and ${\mathbb{Q}}_{\delta }$ is the field of fractions of ${\mathbb{Z}}_{\delta }$ , presented by ratio orbits with signed-orbit numerators.

(b) The metatheoretic number systems $\mathbb{N}$ , $\mathbb{Z}$ , and $\mathbb{Q}$ are $\delta$ -encodable.

The classification of the recognition quotients of $\left({\mathbb{N}}_{\delta },+,0\right)$ has three forms, depending on the assumptions imposed on the congruence.

Theorem 1.8. Let $c$ be a congruence on $\left({\mathbb{N}}_{\delta },+,0\right)$ . The index-period classification has the following three forms:

(a) if $c$ is decidable and an explicit pair of distinct related elements is given, then $c={\equiv }_{i,p}$ for a unique pair $i\ge 0$ , $p\ge 1$ , without using EM, LPO, or MP.

(b) If $c$ is decidable and is not equality, then the same conclusion is conditional on MP.

(c) For an arbitrary congruence $c$ , it is conditional on EM that $c$ is either equality or $c={\equiv }_{i,p}$ for a unique pair $i\ge 0$ , $p\ge 1$ .

Conversely, the general statements in (b) and (c) imply MP and EM, respectively. Thus these two metatheoretic logical prices cannot be lowered.

The three prices have a simple meaning. If a pair of distinct related elements is given, a bounded search finds the index and the period. No additional principle is used. If we know only that the congruence is not equality, a witness pair is available only under double negation, and Markov’s principle extracts it. If the congruence is arbitrary, even the alternative “equality or not” is missing, so excluded middle is needed. The reverse implications show that the last two steps cannot be dropped. The prices in Theorem 1.8 are metatheoretic, in the sense fixed in Convention 7.1.

1.2. Organization

The paper is organized as follows. Section 2 proves the initiality, faithful embedding, and rigidity of the generated $\delta$ -orbit (Theorem 1.6). Section 3 defines the $\delta$ -calculus and the ledger, and proves the soundness of the forced fragment (Theorem 3.2). Section 4 proves the universal property of the term algebra (Proposition 1.5) and develops the arithmetic validated in the standard model. Section 5 proves Theorem 1.7 by constructing the number tower ${\mathbb{N}}_{\delta }$ ↪${\mathbb{Z}}_{\delta }$ ↪${\mathbb{Q}}_{\delta }$ and giving explicit encodings of $\mathbb{N}$ , $\mathbb{Z}$ , and $\mathbb{Q}$ into ${\mathbb{N}}_{\delta }$ . Section 6 classifies the recognition quotients of the additive monoid $\left({\mathbb{N}}_{\delta },+,0\right)$ (Theorems 6.4 and 6.7). Section 7 prices this classification in the ambient metatheory and proves Theorem 1.8. It gives the three logical forms and proves that the Markov and excluded-middle prices cannot be lowered. Section 8 describes the Lean formalization and its axiom audit, and Section 9 contains concluding remarks.

One limitation of the present carrier is structural, and it also indicates the direction of the sequel. The additive monoid $\left({\mathbb{N}}_{\delta },+,0\right)$ is free on one generator: it records the number of successive distinction steps, but not their order or type. Thus the recognition quotients classified here describe the simplest generated history carrier. In the sequel, ordered histories are represented by monoids of closed walks on a graph, where different loops may lead to noncommutative composition. The exact logical-pricing method of Section 7 then provides the starting point for the corresponding recognition problem.

2. Initiality and Rigidity of the δ-Orbit

We now state the universal property of the generated $\delta$ -orbit. ${\mathbb{N}}_{\delta }$ denotes the $\delta$ -orbit of Definition 1.2, with constructors 0 and $S$ .

Definition 2.1. A $\delta$ -algebra is a triple $A=\left(\left|A\right|,0_A,S_A\right),$ where $\left|A\right|$ is a carrier, $0_A\in \left|A\right|$ , and $S_A:\left|A\right|\to \left|A\right|$ is a unary operation. A homomorphism $f:A\to B$ of $\delta$ -algebras is a map $f:\left|A\right|\to \left|B\right|$ such that

$f\left(0_A\right)=0_B$ and $f\left(S_{A}x\right)=S_{B}f\left(x\right)$

for every $x\in \left|A\right|$ .

The orbit $\left({\mathbb{N}}_{\delta },0,S\right)$ is a $\delta$ -algebra. Proposition 1.5 states the freeness of the term algebra over the signature $\left\{0,S,+,\cdot \right\}$ with variables. Here we study the generated $\delta$ -orbit as an algebra with operations 0 and $S$ .

Theorem 2.2. For every $\delta$ -algebra $A$ , there exists a unique homomorphism ${\text{rec}}_A:{\mathbb{N}}_{\delta }\to A$ . It is determined by

${\text{rec}}_A\left(0\right)=0_A$ and ${\text{rec}}_A\left(Sn\right)=S_A\left({\text{rec}}_A\left(n\right)\right)$ .

Proof. Existence follows from the recursion principle of the inductively generated $\delta$ -orbit.

Let $f:{\mathbb{N}}_{\delta }\to A$ be a homomorphism. We prove $f\left(n\right)={\text{rec}}_A\left(n\right)$ by structural induction on $n$ . For $n=0$ , we have $f\left(0\right)=0_A={\text{rec}}_A\left(0\right)$ . If the equality holds for $n$ , then

$f\left(Sn\right)=S_{A}f\left(n\right)=S_A{\text{rec}}_A\left(n\right)={\text{rec}}_A\left(Sn\right).$

Hence $f={\text{rec}}_A$ . □

Theorem 2.3. Let $A$ be a $\delta$ -algebra. Suppose that $S_A$ is injective and $0_A\notin \text{im}\left(S_A\right)$ . Then the canonical homomorphism ${\text{rec}}_A:{\mathbb{N}}_{\delta }\to A$ is injective.

Proof. We prove

${\text{rec}}_A\left(a\right)={\text{rec}}_A\left(b\right)\Rightarrow a=b$

by structural induction on $a$ .

Let $a=0$ . If $b=0$ , the claim holds. If $b=S{b}^{\prime }$ , then

$0_A={\text{rec}}_A\left(0\right)={\text{rec}}_A\left(S{b}^{\prime }\right)=S_A\left({\text{rec}}_A\left(b^{\prime }\right)\right).$

This contradicts the assumption $0_A\notin im\left(S_A\right)$ .

Let $a=S{a}^{\prime }$ . The element $b$ cannot be 0, since otherwise

$S_A\left({\text{rec}}_A\left(a^{\prime }\right)\right)={\text{rec}}_A\left(S{a}^{\prime }\right)={\text{rec}}_A\left(0\right)=0_A.$

Thus $b=S{b}^{\prime }$ for some $b^{\prime }$ . Then

$S_A\left({\text{rec}}_A\left(a^{\prime }\right)\right)=S_A\left({\text{rec}}_A\left(b^{\prime }\right)\right).$

Since $S_A$ is injective, ${\text{rec}}_A\left(a^{\prime }\right)={\text{rec}}_A\left(b^{\prime }\right)$ . The induction hypothesis gives $a^{\prime }=b^{\prime }$ , and therefore $a=b$ . □

Thus, if $S_A$ is injective and $0_A\notin \text{im}\left(S_A\right)$ , the canonical homomorphism

${\text{rec}}_A:{\mathbb{N}}_{\delta }\to A$

identifies ${\mathbb{N}}_{\delta }$ with the sub-$\delta$ -algebra $\text{im}\left({\text{rec}}_A\right)$ of $A$ .

Definition 2.4. A $\delta$ -algebra $A$ is a Peano realization if

1) $S_A$ is injective;

2) $S_{A}x\ne 0_A$ for every $x\in \left|A\right|$ ;

3) for every predicate $P$ on $\left|A\right|$ , if

$P\left(0_A\right)$ and $P\left(x\right)\to P\left(S_{A}x\right)$

for every $x\in \left|A\right|$ , then $P\left(x\right)$ holds for every $x\in \left|A\right|$ .

Theorem 2.5. For every Peano realization $A$ , the canonical homomorphism ${\text{rec}}_A:{\mathbb{N}}_{\delta }\to A$ is bijective. It is the unique $\delta$ -algebra isomorphism ${\mathbb{N}}_{\delta }\cong A$ .

Proof. Injectivity follows from Theorem 2.3. For surjectivity, let us consider the predicate

$P\left(x\right):\iff \exists n\in {\mathbb{N}}_{\delta },{\text{rec}}_A\left(n\right)=x.$

The base case holds with witness 0, since ${\text{rec}}_A\left(0\right)=0_A$ . Suppose that $P\left(x\right)$ holds. Let $n\in {\mathbb{N}}_{\delta }$ satisfy

${\text{rec}}_A\left(n\right)=x.$

Then

${\text{rec}}_A\left(Sn\right)=S_A\left({\text{rec}}_A\left(n\right)\right)=S_{A}x.$

Thus $Sn$ witnesses $P\left(S_{A}x\right)$ . Induction in $A$ gives $P\left(x\right)$ for every $x\in \left|A\right|$ . Hence ${\text{rec}}_A$ is surjective.

The uniqueness of the isomorphism follows from Theorem 2.2. □

The predicate $P$ used in the previous theorem is an ambient predicate. The third condition of Definition 2.4 applies to every such predicate, including the image predicate used for surjectivity.

Remark 2.6. Theorem 2.5 is relative to an ambient metatheory supporting inductive generation. It shows that every Peano realization is uniquely isomorphic to ${\mathbb{N}}_{\delta }$ (cf. [11]). For the standard Peano algebra

$A=\left(\mathbb{N},0,n\mapsto n+1\right),$

the canonical map ${\text{rec}}_A$ is the counting map $D$ of Section 5. Hence Lemma 5.3 is the standard-model instance of Theorem 2.5.

Theorems 2.2, 2.3, and 2.5 together prove Theorem 1.6.

3. The δ-Calculus

We now define the $\delta$ -calculus, a natural-deduction system for an intuitionistic first-order arithmetic with equality over the signature $\left\{0,S,+,\cdot \right\}$ . Each derivation has a ledger recording the use of the law of excluded middle (EM), the limited principle of omniscience (LPO), Markov’s principle (MP), and induction on formulas containing a quantifier. The ledger is defined in Section 3.1.

Terms are generated by de Bruijn variables, zero, successor, addition, and multiplication:

$t::=x_n\left|0\right|St|t+t|t\cdot t.$

Under the arithmetic projection (Definition 5.1), the symbol 0 represents the empty record and $S$ represents one further extension of a record.

Formulas are generated by the grammar of first-order logic with equality [16]:

$\phi ::=t=t|\perp |\phi \wedge \phi |\phi \vee \phi |\phi \to \phi |\forall \phi |\exists \phi ,$

where $\neg \phi :=\phi \to \perp$ .

The nonlogical vocabulary of the calculus is exactly $0,S,+,\cdot$ . Lifting and substitution are defined by the standard structural recursions for de Bruijn syntax. For every metatheoretic natural number $n$ , the expression $S^{n}0$ is a closed term, called the numeral for $n$ .

3.1. The Ledger

Let

$L=\left\{\text{EM},\text{LPO},\text{MP},\text{QInd}\right\}.$

A ledger Λ is a subset of $L$ . For each rule instance $r$ , define a label $\ell \left(r\right)\subseteq L$ as follows: EM, LPO, and MP contribute their corresponding singleton. Induction on a formula containing a quantifier contributes {QInd}. For every other rule instance $r$ , we set $\ell \left(r\right)=\varnothing$ .

The ledger of a derivation $d$ is

$\text{Λ}\left(d\right)={\displaystyle \underset{r\text{in}d}{\cup }\ell }\left(r\right).$

A derivation has empty ledger if $\Lambda \left(d\right)=\varnothing$ . Let

${\Lambda }_{\text{pos}}\left(d\right)=\Lambda \left(d\right)\cap \left\{\text{EM},\text{LPO},\text{MP}\right\}.$

A derivation $d$ is forced if ${\Lambda }_{\text{pos}}\left(d\right)=\varnothing$ , and conditional on $O$ , for $O\subseteq \left\{\text{EM},\text{LPO},\text{MP}\right\}$ , if ${\Lambda }_{\text{pos}}\left(d\right)=O$ . The entry QInd does not affect whether $d$ is forced.

The definition of the ledger is close in spirit to constructive reverse mathematics, which classifies theorems by the principles they require [9] [17]. Constructive reverse mathematics studies the relation of theorems to principles over a fixed base theory. Its standard families also include principles such as the weak limited principle of omniscience (WLPO) and the lesser limited principle of omniscience (LLPO), whose relations with LPO and MP are not linear. Our ledger is instead a syntactic annotation carried by each derivation of the $\delta$ -calculus. The two are complementary: the ledger records what a given derivation uses, while reverse mathematics studies which principles are sufficient or necessary for a theorem. We record EM, LPO, and MP, since these are the principles used by the present derivations. The principles WLPO and LLPO are not needed here and are not part of the ledger.

3.2. Derivations

The $\delta$ -calculus is presented as a natural deduction system with the following rules:

• the assumption rule, with formulas in the context accessed by de Bruijn indices;

• the standard rules for equality, including reflexivity and Leibniz substitution;

• the first-order distinction axioms

$St\ne 0,St=Ss\to t=s;$

• the recursion equations

$t+0=t,t+Ss=S\left(t+s\right),$

$t\cdot 0=0,t\cdot Ss=t\cdot s+t;$

• the induction rule;

• the intuitionistic rules for propositional connectives and quantifiers;

• the additional schemas corresponding to EM, LPO, and MP.

The induction rule is

$\frac{\Gamma ⊢\phi \left[0\right]\Gamma ⊢\forall \left(\phi \to \phi \left[S{x}_0\right]\right)}{\Gamma ⊢\forall \phi }\left(\text{Ind}\right),$

where $\phi \left[t\right]$ denotes substitution of the term $t$ for the free variable $x_0$ , with the usual lifting of the remaining de Bruijn variables. The rule contributes QInd when $\phi$ contains a quantifier.

A context Γ is a finite list of formulas, and the derivability judgment is $\Gamma ⊢\phi$ . The assumption rule selects a formula of Γ by its de Bruijn index.

Lifting and substitution are defined by the standard capture-avoiding structural recursion for de Bruijn syntax [15]. Under a binder, the substitution is lifted so that the newly bound variable is fixed. Equality uses reflexivity, symmetry, transitivity, Leibniz substitution, and congruence. The usual intuitionistic introduction and elimination rules are used for connectives and quantifiers.

The schemas EM, LPO, and MP can be applied in any well-formed context. Each application contributes the corresponding entry to the ledger. For LPO and MP, the matrix $\theta$ must be decidable in the forced fragment. Lemma 3.1 gives this for the quantifier-free case used below.

Let $\phi$ be a formula, and let $\theta \left(x,\overrightarrow{y}\right)$ be a decidable formula, in the sense that

$\forall x \left(\theta \left(x,\overrightarrow{y}\right)\vee \neg \theta \left(x,\overrightarrow{y}\right)\right)$

is derivable in the forced fragment. Lemma 3.1 below shows that every quantifier-free formula is decidable in this sense.

The additional schemas are

$\phi \vee \neg \phi \left(\text{EM}\right),$

$\exists x\theta \left(x,\overrightarrow{y}\right)\vee \forall x\neg \theta \left(x,\overrightarrow{y}\right)\left(\text{LPO}\right).$

This is the arithmetic form of LPO, with decidable predicates on $\mathbb{N}$ in place of binary sequences [9] [17].

$\neg \neg \exists x\theta \left(x,\overrightarrow{y}\right)\to \exists x\theta \left(x,\overrightarrow{y}\right)\left(\text{MP}\right).$

In the $\delta$ -calculus, the following implications hold

$\text{EM}\Rightarrow \text{LPO}\Rightarrow \text{MP}.$

Applying EM to $\exists x \theta \left(x,\overrightarrow{y}\right)$ gives LPO. Under LPO, the alternative $\forall x \neg \theta \left(x,\overrightarrow{y}\right)$ contradicts $\neg \neg \exists x \theta \left(x,\overrightarrow{y}\right)$ , and therefore gives MP.

Lemma 3.1. Every quantifier-free formula is decidable without using EM, LPO, or MP. More precisely, if $\theta \left(\overrightarrow{x}\right)$ is quantifier-free, then

$\forall \overrightarrow{x} \left(\theta \left(\overrightarrow{x}\right)\vee \neg \theta \left(\overrightarrow{x}\right)\right)$

has a derivation whose ledger contains none of EM, LPO, or MP.

Proof. We first prove decidability of equality:

$\forall x\forall y \left(x=y\vee x\ne y\right).$

We use induction on $x$ , with a subsidiary induction on $y$ . The base and successor cases follow from

$St\ne 0$ and $St=Ss\to t=s$ .

The subsidiary induction formulas are quantifier-free. The outer induction formula contains the quantifier over $y$ , and therefore contributes QInd, but no instance of EM, LPO, or MP.

The general statement follows by structural induction on $\theta$ . Atomic equalities are decidable by the preceding argument, and $\perp$ is decidable intuitionistically. If $\phi$ and $\psi$ are decidable, then so are

$\phi \wedge \psi ,\phi \vee \psi ,\phi \to \psi ,\neg \phi ,$

by case analysis on the corresponding decision disjunctions. Hence every quantifier-free formula is decidable without using any schema from $\left\{\text{EM},\text{LPO},\text{MP}\right\}$ . □

Terms are interpreted in the standard arithmetic structure $\mathfrak{N}=\left(\mathbb{N},0,S,+,\cdot \right)$ , where the operations are the usual operations on the metatheoretic natural numbers. Formulas are evaluated by the corresponding Tarski semantics.

Theorem 3.2. If a forced derivation in the empty context proves a closed formula $\phi$ , then

$\mathfrak{N}\models \phi .$

Proof. We prove by induction that, for every context Γ, valuation $\rho$ , and forced derivation of $\Gamma ⊢\phi$ , satisfaction of Γ under $\rho$ implies satisfaction of $\phi$ under $\rho$ .

A valuation $\rho :\mathbb{N}\to \mathbb{N}$ interprets the de Bruijn variable $x_n$ as $\rho \left(n\right)$ . Under a quantifier it is extended by

$\left(a::\rho \right)\left(0\right)=a,\left(a::\rho \right)\left(n+1\right)=\rho \left(n\right).$

A context is satisfied if all its formulas are satisfied under the given valuation. The equality and logical rules follow from the corresponding Tarski semantics, while the distinction axioms and the recursion equations are valid in $\mathfrak{N}$ . The quantifier cases use the standard lifting and substitution lemmas for de Bruijn syntax [15]. The induction-rule case follows from induction in $\mathbb{N}$ .

Since $d$ is forced, the cases for EM, LPO, and MP do not occur. The proof uses none of these principles and no axiom of choice. □

4. The Universal Property and Arithmetic

This section proves the universal property stated in Proposition 1.5. It also develops the arithmetic validated in the standard model.

Every term is generated by the constructors

$x_n,0,S,+,\cdot ,$

and every term has a unique such constructor form. At this stage the term algebra is not quotiented by the recursion equations.

Let $A$ be an algebra of the signature $\left\{0,S,+,\cdot \right\}$ , with carrier $\left|A\right|$ : a constant $0_A\in \left|A\right|$ , a unary operation

$S_A:\left|A\right|\to \left|A\right|,$

and binary operations

${+}_A,{\cdot }_A:\left|A\right|\times \left|A\right|\to \left|A\right|.$

Let

$\rho :\mathbb{N}\to \left|A\right|$

be an assignment of the de Bruijn variables. No equations are assumed in $A$ .

Proof of Proposition 1.5. Define the map $h$ on terms by structural recursion:

$h\left(x_n\right)=\rho \left(n\right),h\left(0\right)=0_A,h\left(St\right)=S_{A}h\left(t\right),$

$h\left(t+s\right)=h\left(t\right){+}_{A}h\left(s\right),h\left(t\cdot s\right)=h\left(t\right){\cdot }_{A}h\left(s\right).$

These equations define a homomorphism from the term algebra to $A$ . By construction it preserves $0,S,+,\cdot$ and extends $\rho$ , which gives existence.

For uniqueness, let $h^{\prime }$ be any homomorphism from the term algebra to $A$ such that $h^{\prime }\left(x_n\right)=\rho \left(n\right)$ for all $n$ . A structural induction on $t$ shows that $h^{\prime }\left(t\right)=h\left(t\right)$ for every term $t$ . Hence $h^{\prime }=h$ . □

4.1. Arithmetic and Derived Objects

In the standard model $\mathfrak{N}$ , the closed numeral $S^{n}0$ is interpreted as $n$ .

The recursion equations for + and ∙ are validated in $\mathfrak{N}$ . They do not follow from the universal property, since an arbitrary algebra of the signature is not assumed to satisfy any equations. The identities for + and ∙, including associativity, commutativity, and distributivity, are derived with empty ledger. Indeed, each of them is proved by induction on a formula which is quantifier-free in the induction variable, the remaining variables being free, so no instance of the induction rule contributes QInd. The universal closures are then obtained by $\forall$ -introduction, which contributes nothing.

The forced fragment (Section 3.1) is an intuitionistic first-order arithmetic over the signature $\left\{0,S,+,\cdot \right\}$ , with equality, the distinction axioms, the recursion equations, and full induction. Empty-ledger derivations also exclude QInd. Hence induction in that fragment is restricted to quantifier-free formulas.

5. The Number Tower

This section proves Theorem 1.7(a). The construction proceeds from the orbit carrier ${\mathbb{N}}_{\delta }$ to its group completion ${\mathbb{Z}}_{\delta }$ , and then to the fraction construction ${\mathbb{Q}}_{\delta }$ . All constructions in this section are choice-free.

The natural-number object ${\mathbb{N}}_{\delta }$ is presented by the generated $\delta$ -orbit of Definition 1.2, with constructors 0 and $S$ . Its elements are the finite records generated by these constructors. For each metatheoretic natural number $n$ , we write $S^{n}0$ for the element of ${\mathbb{N}}_{\delta }$ obtained by applying $S$ $n$ times to 0.

Let Num denote the inductively generated collection of closed terms determined by the rules

$0\in \text{Num},t\in \text{Num}\Rightarrow St\in \text{Num}.$

Definition 5.1. The arithmetic projection is the map

${\pi }_{\text{ar}}:{\mathbb{N}}_{\delta }\to \text{Num}$

defined by structural recursion:

${\pi }_{\text{ar}}\left(0\right)=0,{\pi }_{\text{ar}}\left(Sr\right)=S{\pi }_{\text{ar}}\left(r\right).$

Thus the empty record is represented by the closed term 0, and each one-step extension of a record is represented by one application of the successor symbol $S$ .

Definition 5.2. Addition and multiplication on ${\mathbb{N}}_{\delta }$ are defined by structural recursion:

$x+0=x,x+Sy=S\left(x+y\right),$

and

$x\cdot 0=0,x\cdot Sy=x\cdot y+x.$

We write

$1:=S0.$

These are metatheoretic operations on ${\mathbb{N}}_{\delta }$ . Lemmas 5.4 and 5.5 show that under the map $D$ , they correspond to the interpretations of the function symbols + and ∙ in the standard model $\mathfrak{N}$ .

Let us define

$D:{\mathbb{N}}_{\delta }\to \mathbb{N},D\left(0\right)=0,D\left(St\right)=D\left(t\right)+1,$

and

$\nu :\mathbb{N}\to {\mathbb{N}}_{\delta },\nu \left(n\right)=S^{n}0.$

The map $D$ assigns to each finite record the number of its successive extensions, while $\nu$ assigns to each $n\in \mathbb{N}$ the record obtained by applying $S$ $n$ times to 0.

For $n\in \mathbb{N}$ , let $\overline{n}\in \text{Num}$ denote the closed numeral $S^{n}0$ . Then

${\pi }_{\text{ar}}\left(\nu \left(n\right)\right)=\overline{n}.$

Lemma 5.3. The maps $D$ and $\nu$ are mutually inverse:

$D\circ \nu ={\text{id}}_{\mathbb{N}},\nu \circ D={\text{id}}_{{\mathbb{N}}_{\delta }}.$

Proof. The identity $D\left(\nu \left(n\right)\right)=n$ follows by induction on the metatheoretic natural number $n$ . The identity $\nu \left(D\left(x\right)\right)=x$ follows by structural induction on $x\in {\mathbb{N}}_{\delta }$ . □

By Remark 2.6, this lemma is an instance of Theorem 2.5 at the standard model.

Lemma 5.4. For all $x,y\in {\mathbb{N}}_{\delta }$ ,

$D\left(x+y\right)=D\left(x\right)+D\left(y\right).$

Consequently, $D:\left({\mathbb{N}}_{\delta },+,0\right)\to \left(\mathbb{N},+,0\right)$ is a monoid isomorphism.

Proof. The identity follows by structural induction on $y$ , using

$x+0=x,x+Sy=S\left(x+y\right),D\left(Sz\right)=D\left(z\right)+1.$

Thus $D$ preserves addition and zero. Since $D$ is bijective by Lemma 5.3, it is a monoid isomorphism. □

Lemma 5.5. For all $x,y\in {\mathbb{N}}_{\delta }$ , it holds

$D\left(x\cdot y\right)=D\left(x\right)D\left(y\right).$

Proof. We use structural induction on $y$ . The case $y=0$ is immediate. For the successor case, we have

$\begin{array}{c}D\left(x\cdot Sy\right)=D\left(x\cdot y+x\right)\\ =D\left(x\cdot y\right)+D\left(x\right)\\ =D\left(x\right)D\left(y\right)+D\left(x\right)\\ =D\left(x\right)D\left(Sy\right).\end{array}$

□

Proposition 5.6. The structure $\left({\mathbb{N}}_{\delta },+,\cdot ,0,1\right)$ is a commutative semiring. Moreover,

$x+z=y+z\to x=y,$

$x\cdot y=0\to x=0\vee y=0,$

and

$x\cdot z=y\cdot z,z\ne 0\to x=y.$

Proof. By Lemmas 5.3, 5.4, and 5.5, the map $D:{\mathbb{N}}_{\delta }\to \mathbb{N}$ is a bijection preserving 0, 1, addition, and multiplication. The proof follows from the corresponding properties of $\mathbb{N}$ . □

Definition 5.7. A signed orbit is a pair $\left(p,n\right)\in {\mathbb{N}}_{\delta }\times {\mathbb{N}}_{\delta }$ , where $p$ and $n$ are its positive and negative parts. Two signed orbits are balanced, written

$\left(p,n\right)~\left(p^{\prime },n^{\prime }\right),$

if $p+n^{\prime }=p^{\prime }+n$ .

Lemma 5.8. The balance relation is a decidable equivalence relation.

Proof. Reflexivity and symmetry are immediate. For transitivity, suppose

$\left(p,n\right)~\left(p^{\prime },n^{\prime }\right)$ and $\left(p^{\prime },n^{\prime }\right)~\left(p^{″},n^{″}\right)$ .

Then

$p+n^{\prime }=p^{\prime }+n,p^{\prime }+n^{″}=p^{″}+n^{\prime }.$

Adding $n^{″}$ to the first relation and using the second, we obtain

$\left(p+n^{″}\right)+n^{\prime }=\left(p^{″}+n\right)+n^{\prime },$

and additive cancellation (Proposition 5.6) gives $p+n^{″}=p^{″}+n$ , so $\left(p,n\right)~\left(p^{″},n^{″}\right)$ .

The relation is decidable because addition and equality on ${\mathbb{N}}_{\delta }$ are decidable. Lemma 5.3 implies that $D$ is injective. Hence, for all $x,y\in {\mathbb{N}}_{\delta }$ , we get

$x=y\iff D\left(x\right)=D\left(y\right).$

Since equality on $\mathbb{N}$ is decidable, then equality on ${\mathbb{N}}_{\delta }$ is decidable. □

Lemma5.9. The operations on signed orbits defined by

$\left(p,n\right)+\left(p^{\prime },n^{\prime }\right)=\left(p+p^{\prime },n+n^{\prime }\right)$

and

$\left(p,n\right)\cdot \left(p^{\prime },n^{\prime }\right)=\left(p\cdot p^{\prime }+n\cdot n^{\prime },p\cdot n^{\prime }+n\cdot p^{\prime }\right)$

are compatible with the balance relation in each argument.

Proof. Suppose

$\left(p,n\right)~\left(q,m\right),p+m=q+n,$

and let $\left(r,s\right)$ be a signed orbit.

For addition, we have

$\begin{array}{c}\left(p+r\right)+\left(m+s\right)=\left(p+m\right)+\left(r+s\right)\\ =\left(q+n\right)+\left(r+s\right)\\ =\left(q+r\right)+\left(n+s\right).\end{array}$

Finally, we have $\left(p+r,n+s\right)~\left(q+r,m+s\right)$ .

For multiplication, we obtain

$\begin{array}{c}\left(p\cdot r+n\cdot s\right)+\left(q\cdot s+m\cdot r\right)=r\cdot \left(p+m\right)+s\cdot \left(n+q\right)\\ =r\cdot \left(q+n\right)+s\cdot \left(m+p\right)\\ =\left(q\cdot r+m\cdot s\right)+\left(p\cdot s+n\cdot r\right).\end{array}$

Thus multiplication is compatible with balance in the first argument. Compatibility in the second argument follows from commutativity. □

Definition 5.10. The integer object is the quotient ${\mathbb{Z}}_{\delta }:=\left({\mathbb{N}}_{\delta }\times {\mathbb{N}}_{\delta }\right)/~$ . Its addition and multiplication are defined by

$\left[\left(p,n\right)\right]+\left[\left(p^{\prime },n^{\prime }\right)\right]=\left[\left(p+p^{\prime },n+n^{\prime }\right)\right]$

and

$\left[\left(p,n\right)\right]\cdot \left[\left(p^{\prime },n^{\prime }\right)\right]=\left[\left(p\cdot p^{\prime }+n\cdot n^{\prime },p\cdot n^{\prime }+n\cdot p^{\prime }\right)\right].$

These operations are well-defined by Lemma 5.9.

For a signed orbit $u=\left(p,n\right)$ , define

$-u:=\left(n,p\right).$

On ${\mathbb{Z}}_{\delta }$ , define

$-\left[\left(p,n\right)\right]:=\left[\left(n,p\right)\right],0_{{\mathbb{Z}}_{\delta }}:=\left[\left(0,0\right)\right],1_{{\mathbb{Z}}_{\delta }}:=\left[\left(1,0\right)\right].$

If $\left(p,n\right)~\left(p^{\prime },n^{\prime }\right)$ , then $p+n^{\prime }=p^{\prime }+n$ . By commutativity, $n+p^{\prime }=n^{\prime }+p$ , that is $\left(n,p\right)~\left(n^{\prime },p^{\prime }\right)$ . Hence negation is well-defined on ${\mathbb{Z}}_{\delta }$ .

Lemma 5.11. The map

${\iota }_{{\mathbb{Z}}_{\delta }}:{\mathbb{N}}_{\delta }\to {\mathbb{Z}}_{\delta },{\iota }_{{\mathbb{Z}}_{\delta }}\left(a\right)=\left[\left(a,0\right)\right],$

is an injective map preserving addition and multiplication.

Proof. Both identities

$\left[\left(a+b,0\right)\right]=\left[\left(a,0\right)\right]+\left[\left(b,0\right)\right],\left[\left(a\cdot b,0\right)\right]=\left[\left(a,0\right)\right]\cdot \left[\left(b,0\right)\right]$

hold by Definition 5.10. If ${\iota }_{{\mathbb{Z}}_{\delta }}\left(a\right)={\iota }_{{\mathbb{Z}}_{\delta }}\left(b\right)$ , then $\left(a,0\right)~\left(b,0\right)$ , that is $a=b$ . □

Lemma 5.12. The map

$D_{\mathbb{Z}}:{\mathbb{Z}}_{\delta }\to \mathbb{Z},D_{\mathbb{Z}}\left(\left[\left(p,n\right)\right]\right)=D\left(p\right)-D\left(n\right),$

is a bijection satisfying

$D_{\mathbb{Z}}\left(0_{{\mathbb{Z}}_{\delta }}\right)=0,D_{\mathbb{Z}}\left(1_{{\mathbb{Z}}_{\delta }}\right)=1,$

and preserving addition, multiplication, and negation.

Proof. By Lemmas 5.4 and 5.5, we obtain

$D\left(a+b\right)=D\left(a\right)+D\left(b\right),D\left(a\cdot b\right)=D\left(a\right)D\left(b\right)$

for all $a,b\in {\mathbb{N}}_{\delta }$ .

Suppose $\left(p,n\right)~\left(p^{\prime },n^{\prime }\right)$ . Then $p+n^{\prime }=p^{\prime }+n$ , hence $D\left(p\right)+D\left(n^{\prime }\right)=D\left(p^{\prime }\right)+D\left(n\right)$ , and therefore

$D\left(p\right)-D\left(n\right)=D\left(p^{\prime }\right)-D\left(n^{\prime }\right).$

Thus $D_{\mathbb{Z}}$ is well-defined. Since $D\left(1\right)=D\left(S0\right)=D\left(0\right)+1=1$ , we have

$D_{\mathbb{Z}}\left(0_{{\mathbb{Z}}_{\delta }}\right)=D\left(0\right)-D\left(0\right)=0,D_{\mathbb{Z}}\left(1_{{\mathbb{Z}}_{\delta }}\right)=D\left(1\right)-D\left(0\right)=1,$

and

$D_{\mathbb{Z}}\left(-\left[\left(p,n\right)\right]\right)=D_{\mathbb{Z}}\left(\left[\left(n,p\right)\right]\right)=D\left(n\right)-D\left(p\right)=-D_{\mathbb{Z}}\left(\left[\left(p,n\right)\right]\right).$

For addition, we have

$\begin{array}{c}{D}_{\mathbb{Z}}\left(\left[\left(p,n\right)\right]+\left[\left(p^{\prime },n^{\prime }\right)\right]\right)=D\left(p+p^{\prime }\right)-D\left(n+n^{\prime }\right)\\ =\left(D\left(p\right)-D\left(n\right)\right)+\left(D\left(p^{\prime }\right)-D\left(n^{\prime }\right)\right)\\ =D_{\mathbb{Z}}\left(\left[\left(p,n\right)\right]\right)+D_{\mathbb{Z}}\left(\left[\left(p^{\prime },n^{\prime }\right)\right]\right).\end{array}$

For multiplication, we have

$\begin{array}{l}{D}_{\mathbb{Z}}\left(\left[\left(p,n\right)\right]\cdot \left[\left(p^{\prime },n^{\prime }\right)\right]\right)\\ =D\left(p\cdot p^{\prime }+n\cdot n^{\prime }\right)-D\left(p\cdot n^{\prime }+n\cdot p^{\prime }\right)\\ =\left(D\left(p\right)D\left(p^{\prime }\right)+D\left(n\right)D\left(n^{\prime }\right)\right)-\left(D\left(p\right)D\left(n^{\prime }\right)+D\left(n\right)D\left(p^{\prime }\right)\right)\\ =\left(D\left(p\right)-D\left(n\right)\right)\left(D\left(p^{\prime }\right)-D\left(n^{\prime }\right)\right)\\ =D_{\mathbb{Z}}\left(\left[\left(p,n\right)\right]\right)D_{\mathbb{Z}}\left(\left[\left(p^{\prime },n^{\prime }\right)\right]\right).\end{array}$

If $D_{\mathbb{Z}}\left(\left[\left(p,n\right)\right]\right)=D_{\mathbb{Z}}\left(\left[\left(p^{\prime },n^{\prime }\right)\right]\right)$ , then

$D\left(p\right)+D\left(n^{\prime }\right)=D\left(p^{\prime }\right)+D\left(n\right),$

so $D\left(p+n^{\prime }\right)=D\left(p^{\prime }+n\right)$ . Since $D$ is injective by Lemma 5.3, we get $p+n^{\prime }=p^{\prime }+n$ , hence $\left(p,n\right)~\left(p^{\prime },n^{\prime }\right)$ and $\left[\left(p,n\right)\right]=\left[\left(p^{\prime },n^{\prime }\right)\right]$ . Thus $D_{\mathbb{Z}}$ is injective.

If $z\ge 0$ , then $D_{\mathbb{Z}}\left(\left[\left(\nu \left(z\right),0\right)\right]\right)=z$ , and if $z<0$ , then $D_{\mathbb{Z}}\left(\left[\left(0,\nu \left(-z\right)\right)\right]\right)=z$ . Thus $D_{\mathbb{Z}}$ is surjective. □

Corollary 5.13. The structure $\left({\mathbb{Z}}_{\delta },+,\cdot ,-,0_{{\mathbb{Z}}_{\delta }},1_{{\mathbb{Z}}_{\delta }}\right)$ is a commutative ring, and $D_{\mathbb{Z}}$ is a ring isomorphism.

Proof. By Lemma 5.12, $D_{\mathbb{Z}}$ is a bijection preserving 0, 1, addition, multiplication, and negation. Hence the commutative ring structure of $\mathbb{Z}$ transfers to ${\mathbb{Z}}_{\delta }$ , and $D_{\mathbb{Z}}$ is a ring isomorphism. □

We now construct the fraction object over ${\mathbb{Z}}_{\delta }$ , using signed-orbit representatives as numerators and nonzero elements of ${\mathbb{N}}_{\delta }$ as denominators.

Definition 5.14. A ratio orbit is a pair $\left(u,d\right)$ , where $u$ is a signed orbit and $d\in {\mathbb{N}}_{\delta }$ is nonzero. We identify $d\in {\mathbb{N}}_{\delta }$ with the signed orbit $\left(d,0\right)$ .

Two ratio orbits $\left(u,d\right)$ and $\left(u^{\prime },d^{\prime }\right)$ are cross-equal, written $\left(u,d\right)\approx \left(u^{\prime },d^{\prime }\right)$ , if the signed orbits $u\cdot d^{\prime }$ and $u^{\prime }\cdot d$ are balanced.

Lemma 5.15. Let $u,v$ be signed orbits and let $d\in {\mathbb{N}}_{\delta }$ be nonzero. If

$u\cdot d~v\cdot d,$

then $u~v$ .

Proof. Let $u=\left(p,n\right)$ and $v=\left(q,m\right)$ . We have

$p\cdot d+m\cdot d=q\cdot d+n\cdot d,$

and therefore

$\left(p+m\right)\cdot d=\left(q+n\right)\cdot d.$

Since $d\ne 0$ , using cancellation from Proposition 5.6, we have

$p+m=q+n.$

Hence $u~v$ . □

Lemma 5.16. Cross-equality is a decidable equivalence relation on ratio orbits.

Proof. Reflexivity and symmetry follow from reflexivity and symmetry of the balance relation. For transitivity, suppose

$\left(u,d\right)\approx \left(u^{\prime },d^{\prime }\right)$ and $\left(u^{\prime },d^{\prime }\right)\approx \left(u^{″},d^{″}\right)$ .

Then

$u\cdot d^{\prime }~u^{\prime }\cdot d,u^{\prime }\cdot d^{″}~u^{″}\cdot d^{\prime }.$

By Lemma 5.9, multiplying the first relation by $d^{″}$ and the second by $d$ , and using associativity and commutativity of multiplication, we have

$\left(u\cdot d^{″}\right)\cdot d^{\prime }~\left(u^{″}\cdot d\right)\cdot d^{\prime }.$

We use cancellation with respect to balance. Since $d^{\prime }\ne 0$ , cancellation gives

$u\cdot d^{″}~u^{″}\cdot d.$

Therefore $\left(u,d\right)\approx \left(u^{″},d^{″}\right)$ , so cross-equality is transitive.

Finally, cross-equality is decidable because multiplication of signed orbits is recursively defined and balance is decidable. □

Lemma 5.17. Addition and multiplication are well-defined on cross-equality classes.

Proof. By Proposition 5.6, the semiring ${\mathbb{N}}_{\delta }$ has no zero divisors, so the product of two nonzero denominators is nonzero. Suppose

$\left(u,d\right)\approx \left(v,e\right),u\cdot e~v\cdot d.$

For any ratio orbit $\left(w,f\right)$ , the products $w\cdot d\cdot e\cdot f$ and $w\cdot e\cdot d\cdot f$ coincide by Proposition 5.6, and Lemma 5.9 applied to $u\cdot e~v\cdot d$ gives

$\left(u\cdot f+w\cdot d\right)\cdot \left(e\cdot f\right)~\left(v\cdot f+w\cdot e\right)\cdot \left(d\cdot f\right),$

so addition is compatible with cross-equality. Also, we have

$\left(u\cdot w\right)\cdot \left(e\cdot f\right)~\left(v\cdot w\right)\cdot \left(d\cdot f\right),$

so multiplication is compatible with cross-equality. The same argument applies to the second variable. □

Definition 5.18. The rational object is the quotient

${\mathbb{Q}}_{\delta }:=\left\{\left(u,d\right):u\text{is}\text{a}\text{signed}\text{orbit},d\in {\mathbb{N}}_{\delta },d\ne 0\right\}/\approx .$

Addition and multiplication are induced by

$\left(u,d\right)+\left(u^{\prime },d^{\prime }\right)=\left(u\cdot d^{\prime }+u^{\prime }\cdot d,d\cdot d^{\prime }\right)$

and

$\left(u,d\right)\cdot \left(u^{\prime },d^{\prime }\right)=\left(u\cdot u^{\prime },d\cdot d^{\prime }\right).$

The zero and unit of ${\mathbb{Q}}_{\delta }$ are represented by

$0_{{\mathbb{Q}}_{\delta }}=\left[\left(\left(0,0\right),1\right)\right],1_{{\mathbb{Q}}_{\delta }}=\left[\left(\left(1,0\right),1\right)\right].$

By Lemma 5.17, these formulas induce well-defined operations on ${\mathbb{Q}}_{\delta }$ . For a signed orbit $u=\left(p,n\right)$ , let $-u=\left(n,p\right)$ . The formula

$-\left[\left(u,d\right)\right]:=\left[\left(-u,d\right)\right]$

defines a negation on ${\mathbb{Q}}_{\delta }$ . If $\left(u,d\right)\approx \left(v,e\right)$ , then

$u\cdot e~v\cdot d$

implies

$\left(-u\right)\cdot e~\left(-v\right)\cdot d.$

Hence negation is well-defined.

Lemma 5.19. The map

${\iota }_{{\mathbb{Q}}_{\delta }}:{\mathbb{Z}}_{\delta }\to {\mathbb{Q}}_{\delta },{\iota }_{{\mathbb{Q}}_{\delta }}\left(\left[\left(p,n\right)\right]\right)=\left[\left(\left(p,n\right),1\right)\right],$

is injective and preserves addition and multiplication.

Proof. If $\left(p,n\right)~\left(p^{\prime },n^{\prime }\right)$ , then $\left(\left(p,n\right),1\right)\approx \left(\left(p^{\prime },n^{\prime }\right),1\right)$ , so the map is well-defined. The two operation formulas of Definition 5.18. reduce to the operations of Definition 5.10. when both denominators equal 1, so ${\iota }_{{\mathbb{Q}}_{\delta }}$ preserves addition and multiplication. Finally, $\left[\left(\left(p,n\right),1\right)\right]=\left[\left(\left(p^{\prime },n^{\prime }\right),1\right)\right]$ gives $\left(p,n\right)\cdot 1~\left(p^{\prime },n^{\prime }\right)\cdot 1$ , hence $\left(p,n\right)~\left(p^{\prime },n^{\prime }\right)$ . □

Proposition 5.20. The map

$D_{\mathbb{Q}}:{\mathbb{Q}}_{\delta }\to \mathbb{Q},D_{\mathbb{Q}}\left(\left[\left(u,d\right)\right]\right)=\frac{D_{\mathbb{Z}}\left(\left[u\right]\right)}{D\left(d\right)},$

is a bijection preserving 0, 1, addition, multiplication, and negation.

Proof. Since $d\ne 0$ , we have $D\left(d\right)>0$ . Suppose $\left(u,d\right)\approx \left(v,e\right)$ . Then $u\cdot e~v\cdot d$ , and therefore

$D_{\mathbb{Z}}\left(\left[u\right]\right)D\left(e\right)=D_{\mathbb{Z}}\left(\left[v\right]\right)D\left(d\right).$

Hence $D_{\mathbb{Q}}$ is well-defined.

By Lemmas 5.12 and 5.5,

$D_{\mathbb{Z}}\left(\left[u\cdot e\right]\right)=D_{\mathbb{Z}}\left(\left[u\right]\right)D\left(e\right),D\left(d\cdot e\right)=D\left(d\right)D\left(e\right),$

where $e\in {\mathbb{N}}_{\delta }$ is identified with the signed orbit $\left(e,0\right)$ .

Conversely, if

$D_{\mathbb{Q}}\left(\left[\left(u,d\right)\right]\right)=D_{\mathbb{Q}}\left(\left[\left(v,e\right)\right]\right),$

then

$D_{\mathbb{Z}}\left(\left[u\right]\right)D\left(e\right)=D_{\mathbb{Z}}\left(\left[v\right]\right)D\left(d\right).$