Expressive
plain-language theorem explainer
A formal system is expressive precisely when it separates the two endpoints of the primitive distinction δ. Inevitability and embedding certificates cite this predicate as the minimal visibility condition before any PRC embedding can exist. The body is a one-line definition: the system's distinguishes relation holds on the left and right endpoint tokens.
Claim. A formal system $F$ is expressive when $F$ distinguishes the token of the left endpoint from the token of the right endpoint of the primitive distinction $\delta$.
background
The Primitive Recognition Calculus (PRC) treats the primitive distinction $\delta$ as having two endpoints (left and right). A formal system, in the sense used here, is a minimal verifier-side interface: carriers for tokens and expressions, a binary distinguishes relation on tokens, an expression-extension relation, a map from endpoints to tokens, and a map from finite traces to expressions that respects trace extension.
Expressive is the first filter on that interface. It asks only whether the two endpoint tokens are separated by distinguishes. Nothing about traces, embeddings, or external foundations is required at this layer.
The surrounding module builds the formal-system surface for the PRC inevitability theorem: once a system is expressive, one can ask for a PRC embedding that preserves endpoint distinction and finite trace extension.
proof idea
Definition, not a theorem. The predicate unfolds in one line to the formal system's distinguishes relation applied to the images of Endpoint.left and Endpoint.right under endpointToken. No lemmas are invoked; downstream theorems (for example the native PRC system being expressive) discharge this by proving the two endpoint tokens are distinct under the concrete distinguishes instance.
why it matters
This is the gate condition for the first inevitability pass. AdmissibleFoundation packages a formal system together with this predicate. FormalSystemEmbeddingTarget states that every expressive system admits a nonempty PRC embedding. FormalSystemCertificate closes Build Order step 12 by requiring the native PRC system to be expressive and embeddable, and by recording the embedding-target implication from expressiveness.
Downstream, ExternalFoundationParsingTarget requires every external foundation in a corpus to parse to some expressive formal system before inevitability applies. The predicate therefore sits between the bare FormalSystem interface and the embedding/inevitability layer: without endpoint separation, δ is not visible inside the system, so no PRC embedding can preserve the primitive distinction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.