Interactive Proofs in Bounded Arithmetics

Abstract

Previous work [3] has shown that V02, the theory of bounded arithmetic in Buss’ Language equipped with comprehension for boundedly definable sets, is consistent with the conjecture NEXP ⊈ P/poly. That work entertains two diferent formalizations of the inclusion NEXP ⊆ P/poly inside V02, termed α and β. Both formalizations are provably equivalent in the standard model of arithmetic, by invoking the Easy Witness Lemma (EWL), a technically deep modern result in complexity theory. While the implication β → α is provable in V02, it is open whether V02 proves the converse implication α → β. Since this converse implication can be interpreted as a formalization of the EWL, whether V02 proves the equivalence of the two formalizations amounts to whether V02 proves (this formalizationof) the EWL.

In the present work, we make progress towards resolving this question in the positive. More concretely, we show that V02+α does prove a suitable formalization of IP = PSPACE, which is a central ingredient in the proof of the EWL. In the process of doing so, we lay the foundations necessary to discuss exact counting of large sets and formalization of interactive proofs in V02 and other second-order bounded arithmetics.