logicNatLift
The definition constructs the canonical homomorphism from the Peano algebra carried by LogicNat into an arbitrary Peano algebra B via the primitive recursive fold. Algebraists working on initial objects in the category of Peano algebras cite it when establishing uniqueness up to unique isomorphism for the arithmetic extracted from a logic realization. The construction sets the carrier map to the fold and confirms the homomorphism axioms by reflexivity on the base and step clauses.
claimFor any Peano algebra $B$, the map $f$ from the carrier of the logic-natural Peano algebra to the carrier of $B$ defined by $f(0)=0_B$ and $f(s(n))=s_B(f(n))$ is a homomorphism of Peano algebras.
background
A Peano algebra is a carrier type equipped with a zero element and a successor map. A homomorphism between two Peano algebras is a function that sends zero to zero and commutes with successor. The logic-natural Peano algebra has carrier LogicNat together with its zero and successor. The fold into a target algebra B sends the identity element to B's zero and recurses by applying B's successor at each step.
proof idea
This is a direct definition that installs logicNatFold as the underlying function. Zero preservation holds by reflexivity on the base case. Successor preservation holds by reflexivity on the inductive clause of the fold.
why it matters in Recognition Science
The definition supplies the lift required to prove that the logic-natural Peano algebra is initial. It is invoked directly in the statement that LogicNat is initial among Peano algebras and in the subsequent realization fold and lift constructions. This realizes the initiality mechanism that extracts arithmetic from any law-of-logic realization, the step that underpins universal forcing in the Recognition framework.
scope and limits
- Does not prove uniqueness of the homomorphism.
- Does not construct the Peano algebra on LogicNat.
- Applies only to single-zero single-successor algebras.
- Does not address termination or complexity of the recursion.
formal statement (Lean)
95def logicNatLift (B : PeanoObject) : PeanoObject.Hom logicNatPeano B where
96 toFun := logicNatFold B
proof body
Definition body.
97 map_zero := rfl
98 map_step := by
99 intro x
100 rfl
101