M. Kolář

Unconditional $V^0_1$-independence of a certified hitting-set principle

We show that a certified formalization of the hitting-set-existence axiom of Atserias and Tzameret, instantiated on the parity-based Nisan-Wigderson compression class of Khaniki, is independent of the two-sorted theory $V^0_1$ of $\mathrm{AC}^0$-reasoning, unconditionally: $V^0_1$ proves neither it nor its negation. Th...