Remarks on Primitive Regulation

We prove, and mechanize in Rocq, an obstruction to closure-level Excluded Middle for primitive regulators $C : \mathsf{Form} \to \mathsf{Prop}$ over the closed implication-falsity fragment $A,B ::= \bot \mid A \to B$.

Write $\mathsf{LEM}(C)$ for the demand that $C(A)\lor C(\lnot A)$ hold for every formula $A$.

If $C$ is closed under Modus Ponens, is consistent, and admits a formula $B$ satisfying $B\simeq_C\lnot B$, where $A \simeq_C B$ abbreviates $C(A \to B) \land C(B \to A)$, then $\mathsf{LEM}(C)$ is impossible.

In fact, consistency excludes both $C(B)$ and $C(\lnot B)$, so the global conclusion uses only the excluded-middle instance at $B$.