One-Way Permutations and the Conditional Unprovability of Exact Semantic Carrier Separation in PV

Abstract

The Exact Semantic Carrier condition EC1b requires a distinguishing admitted query whenever two carrier codes differ. We study this requirement in a fixed conservative definitional extension of Cook's universal theory \(\mathbf{PV}\). A width \(n\) is represented by a supplied marker \(M=2^n\), so admitted state and query codes are bounded by the \(\mathcal{L}_{\mathbf{PV}}\)-term \(M\); no exponentiation from a binary-coded security parameter occurs. For a uniformly polynomial-time, length-preserving permutation family, a named evaluation function induces the preimage-membership response map, and the identity carrier is full-response exact in the standard model. We give a normalized separation sentence whose matrix is open after expansion of its bounded existential. Relative Herbrand witnessing for the fixed universal presentation \(\mathbf{PV}_f\) yields finitely many terms; a fixed first-success selector combines them into a deterministic \(\mathbf{FP}\) separator whose output is provably within the admitted width. Calling that separator on both orders of an independent challenge--comparison pair gives a probabilistic inverter with success probability at least \(1/2+2^{-n-1}\). Hence a one-way permutation family makes the true normalized separation sentence unprovable in the fixed universal presentation \(\mathbf{PV}_f\). The conclusion is conditional and construction-specific; no transfer to another response model is claimed without an explicit reduction.