Adversarial Barrier in Uniform Class Separation

TL;DR

This paper uncovers a fundamental structural obstacle to achieving uniform separation in constructive arithmetic, showing that certain logical constraints prevent the existence of such separation principles.

Contribution

It introduces a novel barrier based on fixed point constructions that limits uniform separation in Heyting arithmetic, independent of semantic content.

Findings

Identifies a structural obstruction to uniform separation in constructive arithmetic.

Shows that the barrier is based on fixed point constructions and evaluator predicates.

Limits the scope of classical separation barriers within Heyting arithmetic.

Abstract

We identify a strong structural obstruction to Uniform Separation in constructive arithmetic. The mechanism is independent of semantic content; it emerges whenever two distinct evaluator predicates are sustained in parallel and inference remains uniformly representable in an extension of HA. Under these conditions, any putative Uniform Class Separation principle becomes a distinguished instance of a fixed point construction. The resulting limitation is stricter in scope than classical separation barriers (Baker; Rudich; Aaronson et al.) insofar as it constrains the logical form of uniform separation within HA, rather than limiting particular relativizing, naturalizing, or algebrizing techniques.