peanoSystem
plain-language theorem explainer
The Peano arithmetic foundation is packaged as a minimal formal system whose tokens are natural numbers and whose first distinction is $0\neq 1$. Anyone citing PRC inevitability for named foundations uses this carrier. The definition is a one-line specialization of the two-distinct-primitives constructor, with the inequality discharged by decidability on $\mathbb{N}$.
Claim. Define the arithmetic formal system as the minimal formal system built from $\mathbb{N}$ by taking the two distinct primitives $0$ and $1$: tokens are naturals, distinction is inequality, expressions are finite-trace lengths ordered by $\le$, and the two endpoints map to $0$ and $1$.
background
Primitive Recognition Calculus (PRC) needs a thin interface for an arbitrary formal system: a token type, an expression type, a distinction relation on tokens, an extension order on expressions, and a map from the two abstract endpoints to concrete tokens. That interface is the structure FormalSystem.
Any type with two unequal elements yields such a system via the constructor that sets tokens to the carrier, distinction to inequality, expressions to natural lengths, and extension to the length order, sending the left and right endpoints to the two chosen primitives.
This module collects concrete instances of that construction for standard foundations. The arithmetic case takes the natural-number object and the first Peano distinction $0\neq 1$.
proof idea
One-line definition: apply the two-distinct-primitives constructor to the naturals with witnesses $0$ and $1$, discharging $0\neq 1$ by decide. No further lemmas are needed at the definition site.
why it matters
This instance is the arithmetic leg of the named-foundations package. Downstream, it feeds the theorem that the Peano system admits a PRC embedding of the $\delta$ core, and thence the widened Item-4 claim that four structurally different foundations (two-valued logic, arithmetic $0\neq 1$, set-theoretic empty-vs-singleton, and the type-theoretic bit) each realize $\delta$. It also appears in the dichotomy theorem that those four named foundations are non-degenerate, hence sit on the $\delta$ side rather than the collapse side. The point for Recognition Science is that the primitive distinction is not notation-bound: it appears as soon as two primitives can be told apart, here the first Peano inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.