Reverse Complexity

Reverse Complexity is a long term research program aiming at discovering the abstract, logical principles underlying Complexity Theory, by means of a formal, reverse analysis of its proofs. The final goal is to get a cleaner, machine independent presentation of the foundation of Complexity Theory and a better, synergic integration with logic; in particular, we aim to provide abstract, axiomatic characterizations of Complexity Classes with the purpose to better grasp their essence, identify their distinctive properties, suggest new, possibly non-standard computational models and finally provide new tools for separating them. In this article, we introduce the program and illustrate its methodology through an investigation of the well known Hierarchy Theorems. The analysis is conducted with the assistance of an interactive theorem prover (in our case, Matita), not only used to check the formal correctness of proofs, but as an important driver of the actual research.