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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2605.18924
curl -X POST /api/v1/records/arxiv/2605.18924/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2605.18924/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'