boolLogicSystem_expressive
plain-language theorem explainer
Classical two-valued Boolean logic is expressive for the primitive recognition calculus: its carrier distinguishes the two endpoints of the primitive distinction. Anyone assembling the PRC inevitability witnesses for the Law of Logic cites this fact. The argument is a one-line specialization of the general two-distinct-primitives lemma, with false ≠ true discharged by decide.
Claim. The formal system whose carrier is the Boolean pair $\{\mathrm{false},\mathrm{true}\}$ is expressive: it distinguishes the left and right endpoint tokens of the primitive distinction.
background
In the Primitive Recognition Calculus, a formal system is expressive for the first inevitability pass precisely when it can distinguish the two endpoints of the primitive distinction. That predicate is the gate condition for a PRC embedding into the system.
The Boolean logic system is the concrete formal system built from the two unequal values false and true. Its doc-comment calls it the Law of Logic's own two-valued carrier. Endpoint tokens are mapped to those two values, so expressiveness reduces to false ≠ true.
Upstream, any system assembled from two distinct primitives is automatically expressive: the general lemma unfolds the Expressive predicate and the of-two-distinct constructor and returns the supplied inequality.
proof idea
One-line term proof. Apply the general lemma that every of-two-distinct system is expressive, instantiate the two primitives at false and true, and discharge the inequality hypothesis by decide. No further unfolding is required at the call site.
why it matters
This is the concrete Item 4 witness in the PRC inevitability instances. It is the sole hypothesis fed to the parent result that Boolean logic admits a nonempty PRC embedding of the δ core: distinguishing true from false is the primitive distinction, so the Law of Logic's carrier carries a PRC embedding.
That embedding anchors the logical foundation inside the recognition calculus before the forcing chain (T0–T8) is invoked. Sibling witnesses (Peano, set foundation, type theory) play the same role for other carriers; this one is the pure Boolean case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.