2026/07/04 by Fabio F. G. Buono · 1 voice
Computer Science · #cs.LO
This paper does not address the mathematical truth of P versus NP. Instead, it identifies a structural limitation of uniform proof-generation methods in the standard Turing model. The observation is model-theoretic: it concerns the interaction between semantic invariants and syntactic verification, not the provability of complexity statements. We formalise an admissible method as a generator-verifier pair that produces, for each program, a finite certificate establishing a semantic property. Admissibility forces the generator-verifier composition to behave uniformly with respect to the invariant being certified. In the standard model, such uniform semantic certification implicitly induces a decision procedure for the property. Rice's theorem shows that this implicit behaviour cannot be realised for non-trivial semantic invariants, revealing a structural constraint on formal certification. Understanding this requires a meta-computational perspective: the obstruction arises from the computational behaviour induced by certification, not from the complexity-theoretic status of the property. We apply this framework to two semantic invariants naturally associated with formal certification of P vs. NP and with cryptographic hardness assumptions (in particular, one-way functions). Both fall under the same limitation: no uniform admissible method can certify them in the standard model. A complete Coq formalisation is provided, capturing the extensional structure of admissible methods and the semantic-syntactic interaction underlying the result.