A Formal Proof of Borodin-Trakhtenbrot’s Gap Theorem

In this paper, we discuss the formalization of the well known Gap Theorem of Complexity Theory, asserting the existence of arbitrarily large gaps between complexity classes. The proof is done at an abstract, machine independent level, and is particularly aimed to identify the minimal set of assumptions required to prove the result (smaller than expected, actually). The work is part of a long term reverse complexity program, whose goal is to obtain, via a reverse methodological approach, a formal treatment of Complexity Theory at a comfortable level of abstraction and logical rigor.