01

Natural numbers from zero and successor¶

Represent every natural number as either zero or the successor of a natural number, then read equality and addition directly from those cases.

Definition

Axioms and recursive definitions¶

We use these Peano ideas:

• zero is a natural number;
• every natural number n has a successor S(n);
• zero is not a successor;
• S(n) = S(m) implies n = m;
• induction is the proof principle for properties of all natural numbers.

Addition is then specified separately by recursive equations:

The first equation stops recursion. The second makes the right operand one successor smaller. These equations are definitions of addition, not additional Peano axioms.

Representation

One field stores the predecessor chain¶

@dataclass(frozen=True, slots=True, eq=False, repr=False)
class NaturalNumber:
    pre: NaturalNumber | None = None

NaturalNumber() has pre=None and represents zero. NaturalNumber(n) represents S(n). Thus natural_number(2) stores the chain S(S(0)); it does not store the Python integer 2 as its value.

structural_str() follows this chain and renders only 0 and S:

def structural_str(self) -> str:
    depth = 0
    current = self
    while current.pre is not None:
        depth += 1
        current = current.pre
    return f"{'S(' * depth}0{')' * depth}"

Implementation

Equality exposes the zero and successor cases¶

@log(log_level=1)
def __eq__(self, other: object) -> tuple[bool, LogMessage]:
    if not isinstance(other, NaturalNumber):
        return cast(bool, NotImplemented), lambda: "NotImplemented"
    left_predecessor = self.pre
    right_predecessor = other.pre
    if left_predecessor is None or right_predecessor is None:
        result = left_predecessor is None and right_predecessor is None
        return result, lambda: (
            f"{translate('equality.zero')} "
            f"eq({self.structural_str()}, {other.structural_str()}) -> {result}"
        )
    return left_predecessor == right_predecessor, lambda: (
        f"{translate('equality.successor')} "
        f"eq({self.structural_str()}, {other.structural_str()}) -> "
        f"eq({left_predecessor.structural_str()}, "
        f"{right_predecessor.structural_str()})"
    )

If exactly one predecessor is None, zero is being compared with a successor and the answer is false. If both values are successors, comparison moves to their predecessors. This is the code-level correspondence to the two axioms.

Addition mirrors its two equations¶

@log(log_level=4)
def __add__(self, other: object) -> tuple[NaturalNumber, LogMessage]:
    if not isinstance(other, NaturalNumber):
        return cast(NaturalNumber, NotImplemented), lambda: "NotImplemented"
    predecessor = other.pre
    if predecessor is None:
        return self, lambda: (
            f"{translate('addition.base')} "
            f"add({self.structural_str()}, 0) -> {self.structural_str()}"
        )
    return successor(self + predecessor), lambda: (
        f"{translate('addition.recursive')} "
        f"add({self.structural_str()}, {other.structural_str()}) -> "
        f"S(add({self.structural_str()}, {predecessor.structural_str()}))"
    )

predecessor is None implements n + 0 = n. successor(self + predecessor) implements n + S(m) = S(n + m).

Trace

Run after writing your prediction.

Test

The tests name the intended claims: zero is not a successor, successor is injective, and the two recursive equations hold for selected values. They detect implementation regressions. Induction, not enumeration by a test suite, is what turns compatible base and successor arguments into a theorem for all natural numbers.

Boundary

Unary predecessor chains make the structure visible and arithmetic slow. Large numbers are intentionally outside the useful range. Python's built-in int appears only at input and display boundaries.

Next: construct integers from pairs of natural numbers →