Remarks on Primitive Regulation

Abstract

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::=\perp \mid A\to B$. Write $\mathsf{LEM}(C)$ for the demand that $C(A)\vee C(\neg A)$ hold for every formula $A$. If $C$ is closed under Modus Ponens, is consistent, and admits a formula $B$ satisfying $B{\simeq }_C\neg B$, where $A{\simeq }_{C}B$ abbreviates $C(A\to B)\wedge C(B\to A)$, then $\mathsf{LEM}(C)$ is impossible. In fact, consistency excludes both $C(B)$ and $C(\neg B)$, so the global conclusion uses only the excluded-middle instance at $B$.

14 pages. No consistent regulator can combine Modus Ponens, a closure-equivalence negation fixed point, and closure-level Excluded Middle. Version 3 aligns the exposition with the streamlined Rocq developments: collapse holds for any target formula, each branch uses only the required implication and detachment steps, and consistency excludes both sides at the fixed point