boolLogicSystem
plain-language theorem explainer
Classical two-valued logic is packaged as a minimal formal system for the PRC inevitability argument: tokens are Booleans, distinction is inequality, and the endpoints are false and true. Anyone citing the Law of Logic as a δ-realizing foundation uses this witness. The definition is a one-line application of the two-distinct-primitives constructor with a decidable inequality proof.
Claim. The formal system of classical two-valued logic: tokens are the Booleans, expressions are natural numbers (finite-trace lengths) ordered by $\le$, distinction is token inequality, and the two endpoints are mapped to $\mathrm{false}$ and $\mathrm{true}$. Equivalently, it is the two-distinct-primitives construction on $\{\mathrm{false},\mathrm{true}\}$.
background
Primitive Recognition Calculus (PRC) inevitability needs a thin interface for arbitrary foundations. A formal system supplies a token type, an expression type, a distinction relation on tokens, an extension order on expressions, and a map from the two abstract endpoints into tokens. That interface is exactly what makes the primitive distinction δ visible inside a foundation.
The two-distinct-primitives constructor builds such a system from any type with two unequal elements: tokens are the carrier, expressions are natural numbers (trace lengths), distinction is inequality, extension is the length order $\le$, and the endpoints land on the two chosen primitives.
This definition specializes that constructor to Boolean logic, the Law of Logic's own two-valued carrier.
proof idea
One-line definitional wrapper. Apply the two-distinct-primitives constructor to $\mathrm{false}$ and $\mathrm{true}$, discharging the inequality hypothesis by decide (Boolean inequality is decidable). No further proof content.
why it matters
This is the concrete logical witness for Item 4 of the PRC inevitability package: distinguishing true from false is the primitive distinction, so the Law of Logic's carrier admits a PRC embedding. Downstream, expressiveness and the nonempty embedding into this system are proved from the generic two-distinct lemmas; those facts feed the widened claim that four named foundations (logic, Peano arithmetic, set theory, type theory) each realize the δ core, and the dichotomy theorem that none of them is degenerate.
In the Recognition framework this anchors the claim that δ is not an artifact of one notation: wherever two primitives can be told apart, the same core appears. It sits on the foundation side of the forcing story rather than on T5–T8 constants, but it is the logical instance those later steps presuppose when foundations are required to be non-degenerate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.