Transfer principles between logic-based approaches to computational complexity 

Daniel Leivant

Transfer principles are useful in organizing and unifying the many logic-based approaches to computational complexity. They also suggest new results and elucidate difficulties and anomalies.
We consider approaches to computational complexity based on provability in second and first order formalism, on definability in applicative languages, and on finite model theory. We show how conservation is a principle leading from second to first order provability, and how variants  in the Schoenfinkel.-Curry-Howard homomorphism lead from the latter to applicative programs. We exhibit a general boundedness principle that leads from predicative provability to bounded arithmetic and from predicative recurrence to bounded recurrence à la Cobham and Ritchie.
Finally, we show that simple labeling leads from the latter to characterizations in finite model theory.