{"id":"arxiv/2605.18924","url":"https://arxiv.org/abs/2605.18924","tags":["math.LO"],"score":0,"title":"Remarks on Primitive Regulation","domain":"math.LO","source":"arxiv","authors":["Milan Rosko"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-05-18","reactions":{}}