ofTwoDistinct_expressive
plain-language theorem explainer
Any type with two unequal elements yields an expressive formal system under the two-primitive construction: the left and right endpoints of δ are sent to those elements and are therefore distinguished. Cited by the generic Item-4 embedding that any such foundation realizes the δ core, and by the Boolean logic instance. The proof unfolds expressiveness and the construction, then returns the given inequality.
Claim. For any type $\alpha$ and elements $a_0, a_1 \in \alpha$ with $a_0 \neq a_1$, the formal system built from those two primitives is expressive: it distinguishes the tokens assigned to the left and right endpoints of the primitive distinction $\delta$.
background
Primitive Recognition Calculus treats $\delta$ as the minimal distinction, with two endpoints (left and right sides). A formal system, in the sense used here, is a thin interface: token and expression carriers, a distinguishability relation on tokens, an extension order on expressions, and a map sending each endpoint to a token.
Expressiveness is the first inevitability gate: the system must distinguish the tokens of the two endpoints. The two-primitive construction builds such a system from any type $\alpha$ and two named elements $a_0, a_1$: tokens are elements of $\alpha$, distinguishability is inequality, expressions are natural numbers ordered by length, and the endpoint map sends left to $a_0$ and right to $a_1$.
This module supplies concrete instances for the PRC inevitability theorem: whenever a foundation exposes two distinguishable primitives, the $\delta$ core is visible inside it.
proof idea
Term-mode tactic proof, essentially definitional. Unfold expressiveness and the two-primitive construction. After simplifying the endpoint map on left and right, expressiveness reduces exactly to $a_0 \neq a_1$, which is the given hypothesis. No external lemmas beyond the definitions of Expressive, ofTwoDistinct, and the two endpoint constants.
why it matters
Closes the expressiveness half of Item 4 (generic): any foundation with two distinguishable primitives realizes the $\delta$ core. Downstream, two_distinct_realizes_delta feeds this fact into the embedding-target lemma to obtain a nonempty PRC embedding into the two-primitive system. The Boolean instance boolLogicSystem_expressive is the one-line specialization to false and true, which then supports the concrete claim that the Law of Logic's two-valued carrier admits a PRC embedding.
In the Recognition forcing picture this is foundational plumbing rather than a T5–T8 step: it shows that the primitive distinction is not an extra axiom piled on logic or set theory, but is already present as soon as two distinct tokens exist. That is the entry point for arguing that every sufficiently expressive foundation carries the $\delta$ core used later in the inevitability chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.