Schwichtenberg’s style analysis of parameter-free fragments of Girard’s System F

Abstract Schwichtenberg developed the programme called ‘Proofs as Programs’ by measuring the ‘complexity’ of proofs as programs using the Curry-Howard correspondence. In particular, he precisely characterized the complexity of proofs in arithmetic using proof-theoretic tools. In this paper, we extend this result to parameter-free subsystems of Girard’s System F having the strength of $\varPi ^{1}_{1}$-$CA_{0}$, determining the expected complexity of terms in them (instead of proofs). This abstract setting of System F provides a new perspective on Schwichtenberg’s result. His original goal was to determine the complexity of programs, relying on the Curry-Howard correspondence. In contrast, our approach directly determines the complexity of terms in System F, which are essentially programs themselves. Another advantage of this approach should be that our approach for these fragments is more uniform than the original, owing to the abstract setting of System F.