PRCFormalSystem_expressive
plain-language theorem explainer
The primitive recognition calculus, viewed as its own minimal formal system, can distinguish the two sides of the primitive distinction. Anyone citing the formal-system certificate or the PRC-as-admissible-foundation package needs this fact. The proof is a one-line appeal to left ≠ right on endpoints.
Claim. The minimal formal system whose tokens are endpoints, expressions are finite traces, and distinction is inequality of tokens, is expressive: it distinguishes the left and right endpoints of the primitive distinction $\delta$.
background
In the Primitive Recognition Calculus, an endpoint is one side of the primitive distinction $\delta$ (K2.3). The two canonical endpoints are left and right; they are definitionally unequal.
A formal system here packages tokens, expressions, a distinction predicate on tokens, and an expression-extension relation, together with maps that send the primitive endpoints and finite traces into that system. Expressiveness for the first inevitability pass means the system distinguishes the images of the two endpoints under its endpoint-token map.
PRC itself is realized as the minimal such system: tokens are endpoints, expressions are traces, distinction is inequality, extension is trace extension, and the endpoint and trace maps are identities. Under that reading, expressiveness collapses to left $\neq$ right.
proof idea
One-line wrapper. Unfolding expressiveness on the PRC formal system yields distinguishes (endpointToken left) (endpointToken right). Both maps are the identity and distinction is inequality, so the goal is exactly Endpoint.left ≠ Endpoint.right, discharged by Endpoint.left_ne_right.
why it matters
This closes the expressiveness half of the formal-system surface for PRC. Downstream, formal_system_certificate packages it with the embedding theorem as the Step 12 certificate that the formal-system surface and embedding are closed. PRCFormalSystem_embedding applies the general embedding-from-expressiveness result to this instance. PRCAdmissibleFoundation records PRC as an admissible foundation by taking this theorem as the expressiveness witness.
In the broader Recognition chain, expressiveness is the minimal logical demand before inevitability arguments can force structure (forcing chain T0–T8, eight-tick octave, $D=3$). Without distinguishing the two sides of $\delta$, no later composition or ladder structure can be stated inside the formal system.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.