Remarks on Primitive Regulation
Source: arXiv:2605.18924 · Published 2026-05-18 · By Milan Rosko
TL;DR
This paper addresses an abstract obstruction theorem concerning primitive closure predicates defined on a minimal propositional language of falsity and implication within a constructive metatheory. The setting captures structural limitations underlying classical logical limitative results like Gödel’s incompleteness and Tarski’s undefinability. The author defines two distinct completeness principles for such closure predicates: evaluation completeness (Eval(C)), a generative property asserting that every formula-valued behavior of codes is represented by a code up to closure equivalence; and excluded-middle completeness (LEM(C)), a decisional property stating every formula or its negation is accepted by the closure predicate. The main contribution is showing that the conjunction of Eval(C) and LEM(C), combined with modus ponens closure and consistency, leads to a diagonal fixed-point formula B equivalent under closure to its own negation, which forces acceptance of falsity and thus contradiction. This gives a precise obstruction against simultaneously having evaluation completeness and full excluded middle classification. Notably, a weaker negative-only refutation principle is not obstructed. All results are mechanized in the Coq-like proof environment Rocq, formalizing the structural assumptions, fixed-point constructions, and diagonal collapse.
Key findings
- Eval(C) ensures every formula-valued behavior of codes has a representing code up to closure equivalence (Def 2.3.1, Eq. 4).
- LEM(C) demands a global classification: every formula A satisfies C(A) ∨ C(¬A) (Def 2.2.5, Eq. 16).
- Eval(C) applied to the diagonal behavior produces a formula B with B ≃C ¬B, a negation fixed-point (Theorem 3.1.8).
- With modus ponens MP(C), the fixed-point forces C(B) → C(⊥) and C(¬B) → C(⊥), collapsing acceptance into falsity (Lemma 3.2.1).
- Combining Eval(C), MP(C), Cons(C), and LEM(C) yields a contradiction ⊥, blocking Boolean classification with the closure structures (Theorem 3.2.4).
- Decision principles Dec(C) imply LEM(C) and are thus obstructed similarly (Theorem 3.3.2).
- Refutation principles Ref(C), consisting only of negative decisions without coverage requirements, are inhabited vacuously and not obstructed (Theorem 3.3.5).
- The mechanization L001 in Rocq discharges assumptions without extra classical or modal axioms ensuring proof-theoretic robustness.
Threat model
The work considers an abstract logical setting rather than an adversarial system, focusing on the capabilities and limits of primitive regulator predicates C that internalize their own evaluation and classification. The assumptions limit C to closure under modus ponens, consistency against falsity, generative evaluation completeness, and a completeness principle asserting excluded middle over formulas. The adversary is effectively the diagonal construction enabled by Eval(C), which forces contradictory acceptance under LEM(C). There are no external attackers or information leaks; the 'threat' is the incompatibility of these principles simultaneously.
Methodology — deep read
Threat Model & Assumptions: The adversary is theoretical—no direct attacker but an abstract logical setting with a primitive regulator closure predicate C: Form → Prop on formulas over a minimal syntax of falsity and implication. The paper analyzes the possibility space for closure predicates with four core structural properties: modus ponens (MP(C)) closure, consistency (Cons(C)) rejecting falsity acceptance, evaluation completeness Eval(C), and excluded-middle completeness LEM(C). No meta-classical principles are assumed, working constructively.
Data & Syntax: The object syntax (Form) consists only of ⊥ and →, with negation defined as A → ⊥. There are no propositional variables or atoms, emphasizing the minimal fragment. Formulas are finite trees.
Architecture / Algorithm: The notion of closure equivalence ≃C is defined as mutual acceptance of implications in C. The evaluation frame provides an evaluation operation eval: Code × Code → Form, and a completeness property states every Code → Form behavior is represented by some code up to ≃C equivalence. The critical fixed-point B satisfying B ≃C ¬B is constructed by applying Eval(C) to the diagonal behavior f(x) = ¬eval(x,x), making use of closure equivalence rather than syntactic equality. The fixed-point lemma is central.
Training Regime: N/A as this is a formal theoretical proof framework. Instead, formal proofs proceed via constructive reasoning within the logical framework, ensuring no uses of classical excluded middle or choice. All proofs are mechanized in the Rocq proof assistant, with explicit interface data encoding evaluation frames.
Evaluation Protocol: The core evaluation is a logical consistency check: assuming all four properties simultaneously, produce a formula B with B ≃C ¬B that forces acceptance of falsity C(⊥). Modus ponens propagates acceptance from B or ¬B to ⊥, which conflicts with Cons(C). Theorem 3.2.4 formally derives contradiction under these assumptions. Alternative weaker principles like refutation are tested and shown to avoid the obstruction.
Reproducibility: The entire development is mechanized in Gallina (Coq-like language) within the Rocq framework. Complete mechanization is available in the public repositories "M001" for the substrate and "L001" for the obstruction theorems. The mechanization avoids classical or modal axioms, exporting only a verified assumption report with no admitted or axiom dependencies.
Example: To instantiate the diagonal fixed-point, take the behavior f(x) := ¬eval(x,x). Eval(C) provides a code c such that for any x, eval(c,x) ≃C f(x). Evaluating at x = c produces B := eval(c,c) with B ≃C ¬B. Then by LEM(C), either C(B) or C(¬B) holds. By MP(C) applying acceptance along the arrows of ≃C, either case yields C(⊥), contradicting Cons(C). This contradiction establishes the obstruction.
Technical innovations
- Isolating the diagonal obstruction underlying classical limitative theorems as an abstract interplay of evaluation completeness (Eval(C)) and excluded-middle completeness (LEM(C)) in a minimal propositional primitive regulator framework.
- Introducing closure equivalence ≃C to relax syntactic fixed-point equalities into acceptance equivalences within closure predicates, enabling fixed-point constructions without syntactic self-reference.
- Mechanizing the entire obstruction theorem in Rocq, a constructive proof assistant, without classical axioms or choice, ensuring highly reliable, assumption-free verification.
- Distinguishing decisional (two-sided) and refutational (negative-only) completeness principles to precisely identify excluded-middle completeness as the obstruction boundary.
Limitations
- The setting is restricted to a minimal propositional fragment with only falsity and implication; results may not immediately generalize to richer logics with atoms, quantifiers, or modalities.
- The admission of arbitrary type Code and evaluation operation eval abstracts away from concrete computational realizations, which may limit direct computational interpretations.
- The mechanization relies on closure equivalence ≃C, which is weaker than syntactic equality and may not preserve all intuitive semantic properties of formulas.
- No adversarial or empirical evaluation is performed since the work is foundational and purely theoretical.
- Assumptions like Detachment (MP(C)) and Consistency (Cons(C)) are taken as basic but their applicability to all logical systems or closure predicates is not explored in depth.
Open questions / follow-ons
- How does the obstruction extend to richer logical languages with atoms, disjunction, or quantifiers beyond the minimal falsity-implication fragment?
- Can the obstruction be characterized or circumvented by relaxing or modifying closure equivalence ≃C or the form of completeness principles?
- What classes of regulator reductions preserve the obstruction and which transform the boundary between decidability and refutation principles?
- Are there operational or computational interpretations of the evaluation frame and closure predicates that link the abstract fixed-point obstruction to concrete computability or complexity theory?
Why it matters for bot defense
This paper provides a rigorous foundational insight into limits of representing and classifying logical behaviors within an internalized evaluation framework, highlighting an intrinsic obstruction formed by combining generative completeness and full classical-like classification principles. For bot-defense and CAPTCHA practitioners, while the paper does not directly address security or ML models, the conceptual understanding of fixed-point obstructions and diagonalization effects can inform the limits of constructing perfect classifiers that self-reference or certify completeness internally. The dichotomy between decision principles that are obstructed versus refutation principles that survive may suggest design patterns: enforcing partial coverage or asymmetric classification rather than total Boolean decisions might avoid fundamental obstructions. Moreover, the method of mechanizing subtle logical obstructions offers an example for formally verifying the soundness and limits of complex bot-detection logics or heuristics.
Cite
@article{arxiv2605_18924,
title={ Remarks on Primitive Regulation },
author={ Milan Rosko },
journal={arXiv preprint arXiv:2605.18924},
year={ 2026 },
url={https://arxiv.org/abs/2605.18924}
}