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

TL;DR

This paper formalizes key theorems from computational complexity, including the PCP theorem, within bounded arithmetic, specifically PV1, providing new formalizations of graph properties relevant to complexity theory.

Contribution

It introduces the first formalization of the PCP theorem in bounded arithmetic, expanding the scope of formalized complexity results within PV1.

Findings

Formalization of the PCP theorem in PV1

Representation of (n,d,λ)-graphs in PV1

Extension of formal complexity theorems in bounded arithmetic

Abstract

We present several known formalizations of theorems from computational complexity in bounded arithmetic and formalize the PCP theorem in the theory PV1 (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 PV1.