Extensionality and Positive Introspection without Monotonicity or Conjunctive Closure: A Rosser Provability Construction

Let T be a consistent primitive-recursively axiomatized extension of Peano Arithmetic (PA). We construct a genuine Σ₁ Rosser provability predicate satisfying extensionality under T-provable equivalence (E), positive introspection (D3), and provable local consistency (P). In fact, PA itself proves that 0 = 1 is not Rosser-provable with respect to the constructed predicate. At the same time, the predicate fails monotonicity (M) and conjunctive closure (C). Thus every such T admits a genuine Rosser predicate with signature E + D3 + P + ¬M + ¬C. The construction adapts the finite-frame Rosser machinery used in arithmetical completeness proofs for non-normal modal logics. Its main structural modification is to replace bounded implication paths by directed paths of literal biconditionals, allowing provable equivalence to be transported without recovering full monotonicity. The result gives an affirmative answer to the second existence question in Problem 5.2 of Kogure's “Provability interpretation of non-normal modal logics having neighborhood semantics”. No claim is made that the resulting provability logic is exactly ENP4.