Remarks on Primitive Regulation

TL;DR

This paper proves an abstract obstruction theorem for primitive closure predicates in logic, showing how certain completeness principles interact and lead to internal contradictions when combined.

Contribution

It introduces a mechanized proof of an obstruction theorem for primitive closure predicates, analyzing their completeness principles and their logical interactions.

Findings

Evaluation completeness is generative, allowing representation of behaviors by codes.

Excluded-middle completeness is decisional, accepting formulas or their negations.

Their conjunction leads to a fixed-point contradiction and internal collapse.

Abstract

We prove, and mechanize in Rocq, an abstract obstruction theorem for primitive closure predicates, defined as $C : \mathsf{Form} \to \mathsf{Prop}$ over the closed implication-falsity fragment $A,B ::= \bot \mid A \to B$. Two structurally distinct completeness principles for $C$ enter the result. Evaluation completeness $\mathsf{Eval}(C)$ is generative: every formula-valued behavior of codes admits a representing code, up to closure equivalence $A \simeq_C B \triangleq C(A \to B) \land C(B \to A)$. Excluded-middle completeness $\mathsf{LEM}(C)$ is decisional: every formula is accepted, or its object-level negation is accepted. Yet their conjunction is obstructive: $\mathsf{Eval}(C)$ generates a reflective fixed-point $B \simeq_C \lnot B$, which $\mathsf{LEM}(C)$ forces $C$ to classify. Either branch collapses to $C(\bot)$ under modus ponens, and consistency converts the internal collapse into an external contradiction. A Boolean decision strengthens $\mathsf{LEM}(C)$ and is therefore obstructed, whereas refutation imposes no coverage requirement and is inhabited by the always-false classifier.