toposSystem
plain-language theorem explainer
The topos of sets is packaged as a formal system whose tokens are truth values (global points of the subobject classifier Ω ≅ Prop), distinguished by inequality, with endpoints ⊤ and ⊥ and expression order by derivation length on ℕ. Anyone citing the categorical parse of the δ-core or the three-foundations non-degeneracy theorems uses this carrier. Construction is a direct field-by-field instance of the FormalSystem interface, with length monotonicity from an existing lemma.
Claim. Define a formal system with token type the subobject classifier $\Omega = \mathrm{Prop}$, expression type $\mathbb{N}$, discrimination relation $a \neq b$ on truth values, expression extension order $m \le n$, and endpoint map sending the left (resp. right) side of a primitive distinction to $\top$ (resp. $\bot$), using trace length as the expression assignment.
background
The Primitive Recognition Calculus inevitability theorem is stated against a minimal FormalSystem interface: a token type, an expression type, a discrimination relation on tokens, an extension relation on expressions, a map from the two sides of a primitive distinction to endpoint tokens, and a trace-to-expression assignment with monotonicity. The point is to make the forced two-sided distinction (the δ-core) visible inside an arbitrary foundation.
Here the foundation is the elementary topos of sets. The subobject classifier Ω is taken as Prop; its two global points are truth and falsity. As the sibling note records, subobjects of the terminal object (predicates on Unit) are in bijection with global points of Ω via characteristic truth values. Traces are finite sequences of distinction acts (empty or one-step extension), and length is the obvious Nat-valued measure.
This module only parses that categorical data into the FormalSystem shape so the same embedding and non-degeneracy lemmas apply uniformly to set theory, type theory, and category theory.
proof idea
Not a proof: a structure instance. Token is Ω (= Prop). Expr is ℕ. Discrimination is propositional inequality. Extension is ≤ on naturals. The endpoint map matches on Side: left ↦ True, right ↦ False. Trace-to-expression is Trace.length. The required monotonicity obligation (length respects trace extension) is discharged in one line by length_le_of_extends from the inevitability instances module.
why it matters
This carrier is the categorical leg of the three-foundations parse. Downstream, expressiveness collapses to True ≠ False; the embedding theorem shows a nonempty PRC embedding into this system; non-degeneracy places it on the δ side of the distinction dichotomy; and the packaged theorem category_theory_realizes_delta conjoins subobject classification of ⊤/⊥, distinctness of the two truth values, and that embedding.
At the multi-foundation level, three_foundations_not_degenerate and three_foundations_realize_delta cite it beside the set-theoretic and type-theoretic parses. In Recognition Science terms, that supports the claim that any sufficiently expressive classical foundation already contains the primitive distinction forced by the recognition calculus, before the forcing chain (T5 J-uniqueness, T6 φ, T7 eight-tick, T8 D = 3) is run. No physical constant or mass-ladder claim is settled here; the work is foundation-level only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.