induction
plain-language theorem explainer
The induction principle for LogicNat states that any property holding at the identity element and preserved under successor holds for every element in the orbit generated by the Law of Logic. Researchers deriving arithmetic and recursion from the functional equation would cite this result to justify inductive arguments over the constructed naturals. The proof applies Lean's induction tactic to the two-constructor inductive type, dispatching the identity case to the base hypothesis and the step case to the successor hypothesis.
Claim. Let $P$ be any predicate on the natural numbers constructed as the orbit under the generator from the Law of Logic. If $P$ holds at the identity element and $P(n)$ implies $P$ at the successor of $n$ for every $n$, then $P$ holds for all such natural numbers.
background
LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity in the orbit) and step (one further iteration of the generator). Its structure encodes the smallest subset of positive reals closed under multiplication by the generator and containing 1, as forced by the Law of Logic. Zero is identified with identity and successor with the step constructor. The module ArithmeticFromLogic derives the Peano axioms as theorems from this inductive structure rather than positing them, following the import of LogicAsFunctionalEquation.
proof idea
The proof introduces the arbitrary element and applies Lean's induction tactic to the inductive definition of LogicNat. The identity constructor is discharged exactly by the base hypothesis. The step constructor applies the successor hypothesis to the predecessor together with the induction hypothesis from the recursive call.
why it matters
This result derives Peano induction (P3) as a theorem from the Law of Logic, enabling the subsequent recursive definitions of addition and multiplication in the same module. It supplies the inductive foundation needed for arithmetic built on the functional equation and the J-cost orbit. In the Recognition framework it closes one step in constructing the natural numbers that later support the phi-ladder and mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.