logicNatNNO
plain-language theorem explainer
The canonical Lawvere natural-number object is supplied by packaging the Peano algebra LogicNat with its initiality and nontriviality proofs. A researcher building categorical interfaces for arithmetic in the Recognition framework would cite this as the concrete realization. The definition assembles the structure fields directly from the ArithmeticOf and ArithmeticFromLogic modules without additional axioms.
Claim. The Lawvere natural number object is realized by the Peano object induced by the logic-forced natural numbers, equipped with its initiality morphism, the decidable equality on the carrier, and a witness that zero differs from every successor.
background
In the CategoricalLogicRealization module the focus is on providing a Lawvere-style natural-number object using the initial Peano algebra language from ArithmeticOf. The structure LawvereNNO consists of a PeanoObject together with proofs of initiality, decidable equality, and nontriviality. This hooks into the Universal Forcing program by realizing the natural numbers categorically without committing to full Mathlib category theory. Upstream, LogicNat is the inductive type with identity and step constructors, mirroring the orbit under multiplication by the generator. The theorem zero_ne_succ establishes Peano axiom P1 that zero is not a successor.
proof idea
The definition constructs the LawvereNNO by assigning the object field to ArithmeticOf.logicNatPeano. The initial field is filled by the logicNat_initial definition from ArithmeticOf. Decidable equality is obtained from the derived instance on LogicNat. Nontriviality is witnessed by applying succ to zero and using zero_ne_succ to show it differs from zero.
why it matters
This definition provides the concrete NNO that the theorem logicNatNNO_has_category_interface uses to establish the categorical interface. It fills the role of the canonical realization in the foundation for categorical logic, connecting the arithmetic forced by the Law of Logic to the Lawvere NNO structure. In the broader framework it supports the transition from discrete logic realizations to categorical ones, aligning with the initiality properties required for the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.