Remarks on Primitive Regulation
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917552063512576 |
|---|---|
| author | Rosko, Milan |
| author_facet | Rosko, Milan |
| contents | We prove, and mechanize in Rocq, an abstract obstruction theorem for closure predicates $C : \mathsf{Form} \to \mathsf{Prop}$ over the closed implication-falsity fragment $A,B ::= \bot \mid A \to B$. Evaluation completeness, $\mathsf{Eval}(C)$, says that every formula-valued behavior of codes is represented up to closure equivalence, where $A \simeq_C B$ abbreviates $C(A \to B) \land C(B \to A)$. For any $C$ closed under modus ponens and satisfying consistency, this completeness principle is incompatible with the internal excluded-middle schema $\mathsf{LEM}(C)$, namely $\forall A, C(A)\lor C(\neg A)$. Thus $\mathsf{Eval}(C), \mathsf{MP}(C), \mathsf{Cons}(C)$, and $\mathsf{LEM}(C)$ cannot hold jointly. The proof uses evaluation completeness to obtain a formula $B$ such that $B \simeq_C \neg B$. Applying $\mathsf{LEM}(C)$ to this $B$, either alternative gives $C(\bot)$ by detachment, contradicting consistency. Consequently, any Boolean decision procedure for $C$ induces the obstructed excluded-middle schema. Mere refutation behaves differently: its false branch carries no closure condition, and is therefore inhabited by the always-false classifier. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_18924 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Remarks on Primitive Regulation Rosko, Milan Logic 03B20, 68V15, 03F55, 03D10, 18C50, 03B35 F.4.1; F.3.0 We prove, and mechanize in Rocq, an abstract obstruction theorem for closure predicates $C : \mathsf{Form} \to \mathsf{Prop}$ over the closed implication-falsity fragment $A,B ::= \bot \mid A \to B$. Evaluation completeness, $\mathsf{Eval}(C)$, says that every formula-valued behavior of codes is represented up to closure equivalence, where $A \simeq_C B$ abbreviates $C(A \to B) \land C(B \to A)$. For any $C$ closed under modus ponens and satisfying consistency, this completeness principle is incompatible with the internal excluded-middle schema $\mathsf{LEM}(C)$, namely $\forall A, C(A)\lor C(\neg A)$. Thus $\mathsf{Eval}(C), \mathsf{MP}(C), \mathsf{Cons}(C)$, and $\mathsf{LEM}(C)$ cannot hold jointly. The proof uses evaluation completeness to obtain a formula $B$ such that $B \simeq_C \neg B$. Applying $\mathsf{LEM}(C)$ to this $B$, either alternative gives $C(\bot)$ by detachment, contradicting consistency. Consequently, any Boolean decision procedure for $C$ induces the obstructed excluded-middle schema. Mere refutation behaves differently: its false branch carries no closure condition, and is therefore inhabited by the always-false classifier. |
| title | Remarks on Primitive Regulation |
| topic | Logic 03B20, 68V15, 03F55, 03D10, 18C50, 03B35 F.4.1; F.3.0 |
| url | https://arxiv.org/abs/2605.18924 |