Characterization of realizable space complexities
Joel Seiferas, Albert R. Meyer · Annals of Pure and Applied Logic · 1995
This is a complete exposition of a tight version of a fundamental theorem of computational complexity due to Levin: The inherent space complexity of any partial function is very accurately specifiable in a Π1 way, and every such specification that is even Σ2 does characterize the complexity of some partial function, even one that assumes only the values 0 and 1.