Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic

ABSTRACT. We formulate precisely several formalizations of theorems from computational complexity theory in bounded arithmetic that are presented in literature with various degrees of accuracy, and formalize the PCP theorem in the theory $PV_1$ (no formalization of this theorem was known). This includes a formalization of the existence and of some properties of the $(n,d,\lambda)$-graphs in $PV_1$.