toposSystem_expressive
plain-language theorem explainer
The topos-of-sets formal system is expressive: its tokens (truth values of Ω) distinguish the two primitive endpoints ⊤ and ⊥. Anyone building a PRC embedding of the δ-core into a categorical FormalSystem cites this. The proof is a one-line reduction to non-degeneracy of the subobject classifier.
Claim. Let $F$ be the formal system whose tokens are global points of the subobject classifier $\Omega=\mathrm{Prop}$, discrimination is inequality of truth values, and the two endpoint tokens are $\top$ and $\bot$. Then $F$ is expressive: it distinguishes $\top$ from $\bot$.
background
In the Primitive Recognition Calculus, a formal system is a token type with a discrimination relation, an expression order, and two distinguished endpoint tokens (left and right). Expressiveness for the first inevitability pass means the system can tell those two endpoints apart: the discrimination relation holds between them.
This module parses ordinary category theory into that interface. The subobject classifier $\Omega$ of the topos of sets is identified with $\mathrm{Prop}$; its two global points are truth and falsity. The parsed system takes tokens to be points of $\Omega$, discrimination to be inequality, and the endpoints to be $\top$ and $\bot$.
Non-degeneracy of the classifier is already on record: $\top\neq\bot$ (a topos with $\top=\bot$ collapses to the terminal category). Expressiveness of the parsed system is exactly that fact restated in the FormalSystem vocabulary.
proof idea
Unfolding Expressive on toposSystem reduces the goal to inequality of the two endpoint tokens, which are True and False as elements of $\Omega$. The proof is a one-line application of the existing non-degeneracy lemma $\top\neq\bot$.
why it matters
This is the expressiveness half of the categorical FormalSystem instance. The immediate parent is the theorem that the categorical foundation contains the δ-core: a nonempty PRC embedding into toposSystem is obtained by feeding this lemma into the generic embedding-target constructor.
In the broader PRC story, the first inevitability pass requires a host system that can host the primitive distinction without collapse. Establishing that ordinary topos logic (sets, $\Omega$, $\top\neq\bot$) meets that bar lets later results treat category theory as a legitimate realization of the δ-core rather than an external metalanguage. Sibling results then close reflexivity, non-degeneracy, and the full category-theory-realizes-δ claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.